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

Order of quantifiers in theorems proven by induction #7

Closed radeusgd closed 4 years ago

radeusgd commented 4 years ago

This is a rather simple observation, but it's something we don't notice often when doing proofs on paper.

If we formulate have

Inductive B := B0 | B1 : A -> B -> B.

the theorem as forall (a: A) (b: B), P a -> Q b -> R a b and we do induction on the structure of b, in the B1 case we will get an inductive hypothesis of the form Q b -> Q a b where a is the constant a we got from intros.

But for some theorems this may not be enough, so instead we should change the order of quantifiers to forall (b: B) (a: A) , P a -> Q b -> R a b. Now we can intro only b first, do induction on it and intro a only later, so that in B1 case we will get an inductive hypothesis like forall a : A, P a -> Q b -> R a b which is more flexible (as we can instantiate a arbirtarly).

This was important for example when proving the Substitution lemma (https://github.com/radeusgd/QuotedPatternMatchingProof/blob/e02621d96bb6a18b52f2185448e3ddff140a20af/STLC.v#L280) - we did induction on term t2 and needed to be able to instantiate G to different values than only the one introduced at the beginning.