search

radeusgd / QuotedPatternMatchingProof

A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
3 stars 0 forks source link

Quickly applying a hypothesis with a quantifier. #8

Closed radeusgd closed 4 years ago

radeusgd commented 4 years ago

It often happens (for example when doing induction), that I have a complex hypothesis with a forall quantifier, like

  IHt1 : forall T : type,
         ∅ ⊢ t1 : T ->
         isValue t1 \/ (exists t' : term, t1 --> t')

I have some T that I know will fit. Its conclusion is not directly applicable to my current goal, so I cannot do apply IHt1 with SomeT nor eapply IHt2.

What I do is

    assert (isValue t1 \/ (exists t' : term, t1 --> t')).
    apply IHt1 with SomeT. trivial.

I'm however wondering if it's possible to do that in a more concise way (like writing the assert without mentioning the full conclusion as it can be inferred from the IH.

I' mostly thinking Don't Repeat Yourself principle - I have the conclusion already in IH so copy-pasting it into assert sounds risk (as if I change it slightly the assert will no longer work).

radeusgd commented 4 years ago

Something like this can be achieved by calling eapply IHt1 in H where H is one of the assumptions needed for IHt1.

For example:

Lemma sandbox : forall t T,
    (forall t1 T, ∅ ⊢(L0) t1 ∈ T -> isvalue t1) ->
      ∅ ⊢(L0) t ∈ T ->
    isvalue t \/ False.
  intros.
  remember H0 as H0' eqn:removeme; clear removeme.
  eapply H in H0.
...

One can also use remember to keep the original hypothesis.

One can also use rewrite with hypotheses that are not directly an equality but in the full form forall ..., H1 -> ... -> Hn -> equality.