Stream: Coq users

Topic: Elegant way to construct proofs starting from assumptions


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip walker (Mar 16 2022 at 21:23):

thanks for the pose trick!


Last updated: Jan 27 2023 at 02:04 UTC