walker (Mar 16 2022 at 20:52): 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: Oct 03 2023 at 21:01 UTC