## Stream: Coq users

### Topic: Elegant way to construct proofs starting from assumptions

#### walker (Mar 16 2022 at 20:52):

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.

#### Kenji Maillard (Mar 16 2022 at 21:06):

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.

#### walker (Mar 16 2022 at 21:23):

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.

#### walker (Mar 16 2022 at 21:23):

thanks for the pose trick!

Last updated: Jul 23 2024 at 18:02 UTC