0

Basically, I want to do pose (h st) on this equation:

h : (forall st : state, (P st -> wp st) /\ sd st) ->
    forall st st' : state,
    extract d1 / st \\ st' -> P st -> Q st'

However, when I run the command, coq tells me:

The term "st" has type "state" while it is expected to have type
 "forall st : state, (P st -> wp st) /\ sd st".

What is the right step?

Improve this question
2
  • Did you mean to paste the same snippet twice?
    – Arthur Azevedo De Amorim
    Commented Dec 21, 2020 at 14:10
  • That is better. Just to clarify, what do you expect to obtain after running this tactic?
    – Arthur Azevedo De Amorim
    Commented Dec 21, 2020 at 15:08

1 Answer 1

Reset to default
1

The problem is that st is the second argument of h, while the first is expected to have that complicated type in the error. You can instead do pose (fun H => h H st).

Improve this answer

Not the answer you're looking for? Browse other questions tagged or ask your own question.