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 %%