Hints on proving theorems in Twelf, continued Andrew W. Appel March 2000 17. Coping with nonstrictness The "cut" lemma is a useful thing, as we have already seen. From a proof of A, and a function that converts any proof of A to a proof of B, we can obtain a proof of B: cut : pf A -> (pf A -> pf B) -> pf B = Let us attempt a proof: cut : pf A -> (pf A -> pf B) -> pf B = [p1: pf A] [p2: pf A -> pf B] p2 p1. Load this definition. The Twelf error message is, stdIn:2.4-4.9 Error: No strict occurrence of variable A, use %abbrev A strict occurrence of a variable is a use as the argument of a function, or as use in the type attribution of a variable with a strict occurrence. Twelf can't completely type-check a definition with a free variable (such as A, B) with no strict occurrences. For most users (including me!) this is the most mysterious part of Twelf. It's often not clear why type-checking fails. However, there is a bag of tricks that can be used, sometimes successfully. In this case the solution is to use A as the argument of a preexisting constructor or definition. We will use imp_i. Load the following definition: imp_i' : (pf A -> pf B) -> pf (A imp B). (I've put a prime there to avoid shadowing the imp_i from the core logic.) Examine the output in the *twelf-server* window, where you find, imp_i' : {A:tm form} {B:tm form} (pf A -> pf B) -> pf (A imp B). This means that imp_i actually takes three arguments; the first argument is A. Thus, if we write the expression (imp_i p2) it really means (imp_i A B p2), where the A and B arguments are added automatically in type inference. Therefore, using (imp_i p2) somewhere in the proof will solve the "no strict occurrence of A" problem. But how can we shoehorn (imp_i p2) into this proof? By applying imp_e to the result, as follows: cut : pf A -> (pf A -> pf B) -> pf B = [p1: pf A] [p2: pf A -> pf B] imp_e (imp_i p2) p1. Load this definition and notice that it is accepted! The proof of cut is less elegant than it should be, with the extra imp_i and imp_e, but at least it's proved now. And the users of cut don't have to know about it. Now, consider the following lemma: lemma57: pf A -> pf B -> pf (A imp B) = ... Before proving this, note that the first premise (pf A) is going to be useless; the lemma is provable from the second premise (pf B) alone. EXERCISE: prove this lemma. SOLUTION: read on. We start in the usual way: lemma57: pf A -> pf B -> pf (A imp B) = [p1: pf A] [p2: pf B] hole (A imp B). Load this definition. We get the usual message, stdIn:2.2-4.15 Error: No strict occurrence of variable p1, use %abbrev So we proceed as follows: %abbrev lemma57: pf A -> pf B -> pf (A imp B) = [p1: pf A] [p2: pf B] imp_i [p3: pf A] hole B. and finally, %abbrev lemma57: pf A -> pf B -> pf (A imp B) = [p1: pf A] [p2: pf B] imp_i [p3: pf A] p2. At this point we have removed all the holes, so naturally it's time to remove the %abbrev: lemma57: pf A -> pf B -> pf (A imp B) = [p1: pf A] [p2: pf B] imp_i [p3: pf A] p2. Load this definition. The error message is, stdIn:2.2-5.4 Error: No strict occurrence of variable p1, use %abbrev Upon examining the proof, we see that there is no occurrence of variable p1 at all! So, how can we use p1 in this proof, even though there's no need? One way is to "cut in" a useless fact: lemma57: pf A -> pf B -> pf (A imp B) = [p1: pf A] [p2: pf B] cut p1 [p5: pf A] imp_i [p3: pf A] p2. Load this definition. It works! There's no occurrence of variable p5, but that's OK because p5 is not an argument to the lemma as a whole, as p1 is. Now it would be a good thing to add a comment to this proof, lest some unsuspecting maintainer delete the "useless" cut: lemma57: pf A -> pf B -> pf (A imp B) = [p1: pf A] [p2: pf B] cut p1 [p5: pf A] % This cut provides a strict occurrence of p1 imp_i [p3: pf A] p2. Here's another example: prove this lemma lemma58: tm T -> pf B -> pf (A imp B) = ... We start in the usual way lemma58: tm T -> pf B -> pf (A imp B) = [X: tm T] [p2: pf B] imp_i [p3: pf A] p2. And we get the usual error message: stdIn:2.3-5.5 Error: No strict occurrence of variable T, use %abbrev In fact, there is no strict occurrence of X or T, but Twelf gives us only one error message. Now, we can't use just "cut" to use up X, because cut takes a proof as an argument, and X is not a proof. However, we can use lemma58: tm T -> pf B -> pf (A imp B) = [X: tm T] [p2: pf B] cut (exists_i X true_i) [p5: pf (exists [X] true)] % strictify X imp_i [p3: pf A] p2. This gives a hint about the recipe for creating strict occurrences: search the inference rules of the logic for a proof constructor that uses an argument of the right kind, and cut in some trivial proof using that constructor. 18. A case study in strictness and type inference by Kedar Swadi Consider proving the lemma exists_congr : pf (exists [C] (F C A)) -> pf (eq B A) -> pf (exists [C] (F C B)). **** TRYING TO COMPILE THIS (C-c C-d) CURRENTLY GENERATES AN **** UNRECOGNISED EXCEPTION Let us try to use a lemma to simplify our proof. We use a lemma: func_congr : pf (eq B A) -> pf (F A) -> pf (F B). Twelf responds with >> func_congr : pf (eq B A) -> pf (F A) -> pf (F B).%. >> stdIn:1.1-1.51 Error: >> Typing ambiguous -- unresolved constraints >> tm form = X1 `B; >> tm form = X1 `A. >> %% ABORT %% So we annotate it better with types and write : func_congr : pf (eq (A : tm T1) B) -> pf ((F : tm T1 -> tm form) B) -> pf (F A). Twelf allows this >> func_congr : pf (eq (A : tm T1) B) -> pf ((F : tm T1 -> tm form) B) -> pf (F A).%. >> func_congr : >> {T1:tp} {A:tm T1} {B:tm T1} {F:tm T1 -> tm form} >> pf (eq A B) -> pf (F B) -> pf (F A). The proof for this lemma is simple enough : func_congr : pf (eq (A : tm T1) B) -> pf ((F : tm T1 -> tm form) B) -> pf (F A) = [p1 : pf (eq (A : tm T1) B)] [p2 : pf (F B)] (congr ([za] F za) p1 p2). And Twelf outputs : >> func_congr : >> {T1:tp} {A:tm T1} {B:tm T1} {F:tm T1 -> tm form} >> pf (eq A B) -> pf (F B) -> pf (F A) >> = [T1:tp] [A:tm T1] [B:tm T1] [F:tm T1 -> tm form] [p1:pf (eq A B)] >> [p2:pf (F B)] congr ([za:tm T1] F za) p1 p2. Now we use this lemma and try to prove exists_congr, whose statement too is type annotated. We have : exists_congr : pf (exists [C : tm T2] ((F : tm T2 -> tm T1 -> tm form) C A)) -> pf (eq B A) -> pf (exists [C : tm T2] (F C B)) = [p1 : pf (exists [C : tm T2] (F C A))] [p2 : pf (eq B A)] (exists_e p1 [c] [z1 : pf (F c A)] (exists_i c (func_congr p2 z1))). But, twelf gives an error : >> No strict occurrence of variable F, use %abbrev We make another attempt, using strictify2 lemma from basiclem.elf and write : exists_congr : pf (exists [C : tm T2] ((F : tm T2 -> tm T1 -> tm form) C A)) -> pf (eq B A) -> pf (exists [C : tm T2] (F C B)) = [p1 : pf (exists [C : tm T2] (F C A))] [p2 : pf (eq B A)] strictify2 F (exists_e p1 [c] [z1 : pf (F c A)] (exists_i c (func_congr p2 z1))). Now, we get another, less helpful error : >> No strict occurrence of implicit variable, use %abbrev Let us, for a moment, put the %abbrev and see what happens. Twelf gives >> exists_congr : >> {T2:tp} {T1:tp} {F:tm T2 -> tm T1 -> tm form} {A:tm T1} {B:tm T1} >> {X1:pf (exists ([C:tm T2] F C A)) -> pf (eq B A) >> -> ({c:tm T2} pf (F c A) -> tm T1 -> tm form)} >> pf (exists ([C:tm T2] F C A)) -> pf (eq B A) >> -> pf (exists ([C:tm T2] F C B)) >> = [T2:tp] [T1:tp] [F:tm T2 -> tm T1 -> tm form] [A:tm T1] [B:tm T1] >> [X1:pf (exists ([C:tm T2] F C A)) -> pf (eq B A) >> -> ({c:tm T2} pf (F c A) -> tm T1 -> tm form)] >> [p1:pf (exists ([C:tm T2] F C A))] [p2:pf (eq B A)] >> strictify2 F >> (exists_e p1 >> ([c:tm T2] [z1:pf (F c A)] exists_i c (func_congr p2 z1))). >> %% OK %% We see an odd thing in the output. There is a parameter, X1, which is never used at all! This generally suggests that something is not quite right with the proof or some lemma that the proof is using. One way to get over this problem is to make more of the arguments to lemmas explicit. Let us go back to func_congr and make a modified lemma new_func_congr, with F explicit. We have: new_func_congr : {F} pf (eq (A : tm T1) B) -> pf ((F : tm T1 -> tm form) B) -> pf (F A) = [F] [p1 : pf (eq (A : tm T1) B)] [p2 : pf (F B)] (congr ([za] F za) p1 p2). Now, try using new_func_congr in exists_congr. We get, exists_congr : pf (exists [C : tm T2] ((F : tm T2 -> tm T1 -> tm form) C A)) -> pf (eq B A) -> pf (exists [C : tm T2] (F C B)) = [p1 : pf (exists [C : tm T2] (F C A))] [p2 : pf (eq B A)] (exists_e p1 [c] [z1 : pf (F c A)] (exists_i c (new_func_congr (F c) p2 z1))). Twelf seems to like this lemma, it goes through without any problem. As an added bonus, we can even take off the strictify2 ! Look at the twelf output. The strange X1 parameter is not there any more. >> exists_congr : >> {T2:tp} {T1:tp} {F:tm T2 -> tm T1 -> tm form} {A:tm T1} {B:tm T1} >> pf (exists ([C:tm T2] F C A)) -> pf (eq B A) >> -> pf (exists ([C:tm T2] F C B)) >> = [T2:tp] [T1:tp] [F:tm T2 -> tm T1 -> tm form] [A:tm T1] [B:tm T1] >> [p1:pf (exists ([C:tm T2] F C A))] [p2:pf (eq B A)] >> exists_e p1 >> ([c:tm T2] [z1:pf (F c A)] exists_i c (new_func_congr (F c) p2 z1)). >> %% OK %%