Proving metatheorems:Proving metatheorems in non-empty contexts
Previous: Proving metatheorems |
Proving metatheorems with Twelf | Next: Summary |
By using Twelf's ability to prove totality assertions for type families in general worlds, we can mechanize metatheorems about open LF terms. We prove a simple metatheorem about the judgement size E N as an example.
Lower bound on size of substitution: Theorem statement
We prove that substitution never decreases the size of a term. The informal theorem statement is as follows:
- For all terms and , .
We can restate this theorem relationally as follows:
- For all terms and , if and then there exists an such that .
For pedagogical parsimony, we have defined greater-than in terms of addition, so that we do not need to introduce any additional judgements on numbers here. Additionally, because size defines a function, we are free to assume or conclude the derivations of size as is convenient; in this case, the proof is slightly simpler if we assume these derivations.
By adequacy, this theorem can be recast as the following statement about LF terms:
- For all Γ in (size-block)*, if Γ ⊦ E' : tm and Γ ⊦ D : {x:tm} size x (s z) -> size (E x) N and Γ ⊦ D' : size (E E') N' then there exist Ndiff and Dplus such that Γ ⊦ Dplus : plus Ndiff N N'.
Considering arbitrary contexts in the world (size-block)* is necessary to capture the informal theorem statement, which ranges over all possibly-open terms and . The size derivation for the term with a distinguished free variable is represented by an LF term of higher type {x:tm} size x (s z) -> size (E x) N.
We can prove this theorem in Twelf by giving a relation that satisfies the following totality assertion:
subst-size : {E' : tm} ({x : tm} size x (s z) -> size (E x) N) -> size (E E') N' -> plus Ndiff N N' -> type. %mode subst-size +E' +D1 +D2 -DL. %worlds (size-block) (subst-size _ _ _ _).
Proof attempt
For pedagogical purposes, we first present an incorrect proof attempt; the change required to fix this attempt is small. The proof uses some straightforward lemmas about arithmetic:
plus-s-rh : plus N1 N2 N3 -> plus N1 (s N2) (s N3) -> type. %mode plus-s-rh +D1 -D2. %worlds () (plus-s-rh _ _). plus-commute : plus N1 N2 N3 -> plus N2 N1 N3 -> type. %mode plus-commute +D1 -D2. %worlds () (plus-commute _ _). lemma : plus N1 N2 Nsum -> plus Ndiff1 N1 N1' -> plus Ndiff2 N2 N2' -> plus N1' N2' Nsum' -> plus Ndiff Nsum Nsum' -> type. %mode lemma +X1 +X2 +X3 +X4 -X5. %worlds () (lemma _ _ _ _ _).
The first two would be part of an arithmetic library; the third is a simple lemma that is proved directly using commutativity and associativity of addition.
Additionally, the proof of the theorem uses the following easy lemma:
size-at-least-one : size E N -> plus (s z) N' N -> type. %mode size-at-least-one +X1 -X2. - : size-at-least-one _ (plus-s plus-z). %worlds (size-block) (size-at-least-one _ _). %total {} (size-at-least-one _ _).See Twelf's output
This relation is total because every way to create a term of type size E N syntactically produces a term of type size E (s N') for some N'. The input coverage checker notices this fact by splitting and therefore validates this simple proof.
Next, we attempt a proof of the theorem:
subst-size : {E' : tm} ({x : tm} size x (s z) -> size (E x) N) -> size (E E') N' -> plus Ndiff N N' -> type. %mode subst-size +E' +D1 +D2 -DL. - : subst-size E' ([x] [dx] dx) D Dplus' <- size-at-least-one D Dplus <- plus-commute Dplus Dplus'. - : subst-size E' ([x] [dx] size-empty) size-empty plus-z. - : subst-size E' ([x] [dx] (size-lam ([y] [dy] D x dx y dy) %% tell reconstruction that T doesn't depend on x : size (lam T _) _)) (size-lam D') Dplus' <- ({y : tm} {dy : size y (s z)} subst-size E' ([x] [dx] D x dx y dy) (D' y dy) Dplus) <- plus-s-rh Dplus Dplus'. - : subst-size E' ([x] [dx] size-app (Dplus : plus N1 N2 Nsum) ((D2 x dx) : size (E2 x) N2) ((D1 x dx) : size (E1 x) N1) ) (size-app (Dplus' : plus N1' N2' Nsum') (D2' : size (E2 E') N2') (D1' : size (E1 E') N1')) DplusRes' <- subst-size E' D1 (D1' : size (E1 E') N1') (Dplus1 : plus Ndiff1 N1 N1') <- subst-size E' D2 (D2' : size (E2 E') N2') (Dplus2 : plus Ndiff2 N2 N2') <- lemma Dplus Dplus1 Dplus2 Dplus' DplusRes <- plus-s-rh DplusRes DplusRes'. %worlds (size-block) (subst-size _ _ _ _).
By now, you should be getting good at reading relational Twelf proofs of metatheorems as the informal proofs they represent. This proof is slightly more involved than those that we have seen before, but it involves no new machinery. We call out some of the tricky parts of the proof:
- The proof inducts over and case-analyzes the LF term of type {x:tm} size x (s z) -> size (E x) N. By inversion, such a term has the form [x] [dx] M where M : size (E x) N. Thus, the proof includes one case for each possible M. This includes each constructor of type size, along with the distinguished variable x.
- Make sure you understand why each constant world checks: The subst-size premise of the case for size-lam is in an extended context, but that this context stays in the appropriate world. Additionally, by world subsumption, (size-block)* subsumes the world containing only the empty context for the arithmetic lemmas.
However, the totality check fails:
%total D (subst-size _ D _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)Error: Coverage error --- missing cases: {#size-block:{x:tm} {dx:size x (s z)}} {X1:nat} {X2:tm} {X3:plus X1 (s z) (s z)} |- subst-size X2 ([x:tm] [x1:size x (s z)] #size-block_dx) #size-block_dx X3.
%% ABORT %%
This error message tells us that this proof does not cover the case for variables in the context itself. That is, we forgot to cover the case when the size derivation is a variable (representing the use of a hypothesis) but is not the distinguished variable x.
Corrected proof
To fix the proof, we need to cover the case for other variables in the LF context. But where can we put such a theorem case, since it needs to talk about the variable in the context? The answer is that we can use LF hypotheses: we assume a case of the theorem subst-size in the LF context along with every assumption of x:tm,dx:size x (s z). This technique works because proofs of metatheorems are just LF constants of particular types.
To correct the proof, we work over contexts of a different form. Only the size-lam case needs to change, so we elide the others:
subst-size : {E' : tm} ({x : tm} size x (s z) -> size (E x) N) -> size (E E') N' -> plus Ndiff N N' -> type. %mode subst-size +E' +D1 +D2 -DL. - : subst-size E' ([x] [dx] (size-lam ([y] [dy] D x dx y dy) %% tell reconstruction that T doesn't depend on x : size (lam T _) _)) (size-lam D') Dplus' <- ({y : tm} {dy : size y (s z)} {_ : {E' : tm} subst-size E' ([x : tm] [dx : size x (s z)] dy) dy plus-z} subst-size E' ([x] [dx] D x dx y dy) (D' y dy) Dplus) <- plus-s-rh Dplus Dplus'. %% ...
%block ssblock : block {y : tm} {dy : size y (s z)} {_ : {E' : tm} subst-size E' ([x] [dx] dy) dy plus-z}. %worlds (ssblock) (subst-size _ _ _ _). %total D (subst-size _ D _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)%block ssblock : block {y:tm} {dy:size y (s z)} {_:{E':tm} subst-size E' ([x:tm] [dx:size x (s z)] dy) dy plus-z}. %worlds (ssblock) (subst-size _ _ _ _). %total D (subst-size _ D _ _).
%% OK %%
The block ssblock extends size-block with a case of the theorem: when the size derivation is dy from the context, the term E must be [_] y, so by inversion the derivation of size (([_] y) E') N' must be dy as well, in which case plus-z derives plus z (s z) (s z). The only other change is that the premise of the case for size-lam adds this extra assumption to the context. In this world, the relation is indeed total.
Correctness of the revised theorem statement
We set out to prove
- For all Γ in (size-block)*, if Γ ⊦ E' : tm and Γ ⊦ D : {x:tm} size x (s z) -> size (E x) N and Γ ⊦ D' : size (E E') N' then there exist Ndiff and Dplus such that Γ ⊦ Dplus : plus Ndiff N N'.
But the corrected Twelf proof actually proves
- For all Γ in (ssblock)*, if Γ ⊦ E' : tm and Γ ⊦ D : {x:tm} size x (s z) -> size (E x) N and Γ ⊦ D' : size (E E') N' then there exist Ndiff and Dplus such that Γ ⊦ Dplus : plus Ndiff N N'.
Did we prove the right theorem? Not necessarily: it is possible that the contexts in (ssblock)* do not cover all open terms, or that they include inadequate derivations of plus Ndiff N N'. Thus, there is a danger here: we need to check that the second statement implies the first to see that we proved the right theorem.
In this case, the implication holds. The reason is that every context in (ssblock)* corresponds to a context in (size-block)* when restricted to those declarations subordinate to the types in the theorem statement. That is, the context extension in (ssblock)* does not change the inhabitants of the types in the theorem statement—all it does is add a case of the proof type family subst-size, which is not subordinate to any of the subjects of the proof. This is another argument that can be made formal using subordination.
When you recast an informal theorem statement as a Twelf theorem statement, you need to check that the world of the theorem actually yields the theorem you had in mind. However, in a large Twelf project, this obligation is usually not very large: Usually, a Twelf proof consists of a few top-level theorems of interest and many supporting lemmas. In this case, you only need to check that these theorems correspond to what you had in mind; the various lemmas can mean whatever they mean, as long as they are strong enough to prove the overall theorem.
An even better proof
Putting a case of a theorem in the context is a general technique that is useful in many circumstances. However, in this example, we can avoid putting the theorem case in the context by using a catch-all case, as the tutorial on that Twelf proof device explains.
Previous: Proving metatheorems |
Proving metatheorems with Twelf | Next: Summary |