I am trying to prove something like that.

```
Definition subject_expansion := forall T t t', t --> t' -> |- t' \in T -> |- t \in T.
Theorem subject_expansion_does_not_hold: ~ subject_expansion.
Proof.
unfold subject_expansion.
intros H.
remember (H Bool (test tru tru zro) tru).
assert (H': |- tru \in Bool). { constructor. }
assert(H'': test tru tru zro --> tru). {constructor. }
apply (h H'') in H'.
inversion H'; subst.
inversion H6.
Qed.
```

Is there a more elegant way to do forwad proofs than abusing the remember tactic? I hope what I am trying to prove is not really relevant, but if it is this is exercise from PLF chapter *Types: Type Systems*.

What I am trying to avoid is all those asserts, they feel like not the right way but I could be wrong and they could be the way do things hence me asking.

You can use `pose`

and `set`

tactics for forward reasoning. In your situation I would probably do `unshelve epose (H Bool (test tru tru zro) tru _ _).`

or using ssreflect tactics I would do `move=> /(_ Bool (test tru tru zro) tru) [].`

instead of `intros H.`

and what follows.

I think pose tactic is cool since it doe not require new imports from coq and the `=>`

syntax is over used in PLF a lot so I cant use ssreflect without learning how to deal with syntax overloading.

thanks for the pose trick!

Last updated: Jul 23 2024 at 18:02 UTC