Hints on proving theorems in Twelf, continued
Andrew W. Appel
February 2000
12. Equality and congruence
The "eq" predicate is defined in coreTCB/coredefs.elf, and rules for
equality are in core/basiclem.elf. The key definitions and rules are:
eq: tm T -> tm T -> form = ...
refl: pf (eq X X) = ...
symm: pf (eq X Y) -> pf (eq Y X) = ...
congr : {H: tm T -> tm form} pf (eq X Z) -> pf (H Z) -> pf (H X) = ...
The refl rule says that anything is equal to itself.
The symm rule says that equality is symmetric: if A=B then B=A.
The congr rule says that for any proof of H(Z), where X=Z, we can
construct a proof of H(X). For example:
lemma10: pf (eq A (plus B C)) -> pf (eq D (plus B C)) -> pf (eq A D) =
[p1: pf (eq A (plus B C))]
[p2: pf (eq D (plus B C))]
hole (eq A D).
To start, we let H(Z) = (eq A Z) in a use of congr:
%abbrev
lemma10: pf (eq A (plus B C)) -> pf (eq D (plus B C)) -> pf (eq A D) =
[p1: pf (eq A (plus B C))]
[p2: pf (eq D (plus B C))]
congr ([Z] eq A Z) (hole (eq D (plus B C))) (hole (eq A (plus B C))).
Now each of the holes can be filled with a premise:
lemma10: pf (eq A (plus B C)) -> pf (eq D (plus B C)) -> pf (eq A D) =
[p1: pf (eq A (plus B C))]
[p2: pf (eq D (plus B C))]
congr ([Z] eq A Z) p2 p1.
Let's try another:
addup : pf (eq (plus (plus (plus one three) five) seven) (const 16)) =
hole (eq (plus (plus (plus one three) five) seven) (const 16)).
In coreTCB/coredefs.elf there are definitions of the form,
two = const 2.
three = const 3.
four = const 4.
five = const 5.
etc.
This means that "(const 3)" is completely interchangeable with "three"
in all theorems and proofs, and we don't need rules of inference to make the
change.
First we can prove that 1+3=4, using the eval_plus rule from
coreTCB/arith.elf:
add13: pf (eq (plus one three) four) = eval_plus.
Congruence now shows that if (4+5+7=16) then ((1+3)+5+7=16),
with H(Z) = (Z+5+7=16):
addup : pf (eq (plus (plus (plus one three) five) seven) (const 16)) =
congr ([Z] eq (plus (plus Z five) seven) (const 16))
(hole (eq (plus one three) four))
(hole (eq (plus (plus four five) seven) (const 16))).
The first hole we can fill with eval_plus, the second with another
congruence proof:
addup : pf (eq (plus (plus (plus one three) five) seven) (const 16)) =
congr ([Z] eq (plus (plus Z five) seven) (const 16)) eval_plus
(congr ([Z] eq (plus Z seven) (const 16)) eval_plus
(hole (eq (plus nine seven) (const 16)))).
Finally, the last hole can be filled with another eval_plus:
addup : pf (eq (plus (plus (plus one three) five) seven) (const 16)) =
congr ([Z] eq (plus (plus Z five) seven) (const 16)) eval_plus
(congr ([Z] eq (plus Z seven) (const 16)) eval_plus
eval_plus).
13. Forward proof using "cut"
All the proofs shown so far have been derived by starting with a
hole that shows what remains to be proved, then filling that hole
with an inference rule that leaves more holes, and so on. This is
"backward reasoning", and it's perfectly sound. But sometimes it's
easier to reason forward from what you know than to reason backward
from what you need to prove. The "cut" lemma is useful for this:
cut : pf A -> (pf A -> pf B) -> pf B =
Here's an example of its use. We wish to prove
lemma6: pf (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))) =
hole (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))).
The following two rules from coreTCB/arith.elf should be useful:
assoc_add : pf (eq (plus (plus A B) C) (plus A (plus B C))).
comm_add : pf (eq (plus A B) (plus B A)).
We can start with
lemma6: pf (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))) =
cut assoc_add
[p1: pf (eq (plus (plus (plus A B) C) D)
(plus (plus A B) (plus C D)))]
hole (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))).
This is how "cut" is used: (cut (proof) [proofvar: pf (fact)] rest)
is a proof of (theorem), where (fact) is a formula, (proof) is a proof
of (fact), "proofvar" is a name that will stand for the truth of
(fact), and "rest" is also a proof of (theorem), but one that gets
to use "proofvar" whenever it needs a proof of (fact).
Thus, to fill the "hole" in lemma6 above, we are free to use p1 at
any time we need a proof of ((A+B)+C)+D=(A+B)+(C+D).
Let's prove (A+B)+(C+D)=A+(B+(C+D)) as follows:
(A+B)+(C+D)=(C+D)+(A+B)=(C+D)+(B+A)=((C+D)+B)+A=(B+(C+D))+A=A+(B+(C+D))
comm congr-comm symm-assoc congr-comm comm
lemma6: pf (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))) =
cut assoc_add
[p1: pf (eq (plus (plus (plus A B) C) D)
(plus (plus A B) (plus C D)))]
cut comm_add
[p2: pf (eq (plus (plus A B) (plus C D))
(plus (plus C D) (plus A B)))]
cut (congr ([Z] eq (plus (plus C D) (plus A B)) (plus (plus C D) Z))
comm_add refl)
[p3: pf (eq (plus (plus C D) (plus A B))
(plus (plus C D) (plus B A)))]
cut (symm assoc_add)
[p4: pf (eq (plus (plus C D) (plus B A))
(plus (plus (plus C D) B) A))]
cut (congr ([Z] eq (plus (plus (plus C D) B) A) (plus Z A))
comm_add refl)
[p5: pf (eq (plus (plus (plus C D) B) A)
(plus (plus B (plus C D)) A))]
cut comm_add
[p6: pf (eq (plus (plus B (plus C D)) A)
(plus A (plus B (plus C D))))]
hole (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))).
Now we can use the transitivity of equality to tie together the
proofs p1,p2,...,p6:
trans: pf (eq X Y) -> pf (eq Y Z) -> pf (eq X Z) = ... (in basiclem.elf)
lemma6: pf (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))) =
cut assoc_add
[p1: pf (eq (plus (plus (plus A B) C) D)
(plus (plus A B) (plus C D)))]
cut comm_add
[p2: pf (eq (plus (plus A B) (plus C D))
(plus (plus C D) (plus A B)))]
cut (congr ([Z] eq (plus (plus C D) (plus A B)) (plus (plus C D) Z))
comm_add refl)
[p3: pf (eq (plus (plus C D) (plus A B))
(plus (plus C D) (plus B A)))]
cut (symm assoc_add)
[p4: pf (eq (plus (plus C D) (plus B A))
(plus (plus (plus C D) B) A))]
cut (congr ([Z] eq (plus (plus (plus C D) B) A) (plus Z A))
comm_add refl)
[p5: pf (eq (plus (plus (plus C D) B) A)
(plus (plus B (plus C D)) A))]
cut comm_add
[p6: pf (eq (plus (plus B (plus C D)) A)
(plus A (plus B (plus C D))))]
trans p1 (trans p2 (trans p3 (trans p4 (trans p5 p6)))).
Any proof that can be proved using "cut" can be proved by directly
substituting the (proof) for the (proofname); this is like beta-substitution
in lambda calculus. Thus, a shorter proof of lemma6 can be directly
derived as follows:
lemma6: pf (eq (plus (plus (plus A B) C) D)
(plus A (plus B (plus C D)))) =
trans assoc_add
(trans comm_add
(trans (congr ([Z] eq (plus (plus C D) (plus A B)) (plus (plus C D) Z))
comm_add refl)
(trans (symm assoc_add)
(trans (congr ([Z] eq (plus (plus (plus C D) B) A) (plus Z A))
comm_add refl)
comm_add)))).
However, in many cases (and perhaps in this one too) the proof
will be more readable and maintainable using cut, because all
the intermedate "facts" are better documented. Also, in proof
development, sometimes it's easier to work forward proving things
you know are true (and hope are useful), instead of working backward
from things you know are useful (and hope are true).
14. Twelf Traps and pitfalls
lemma7: pf (exists [X] forall [Y] isInt Y).
theorem8: pf (isInt (const 5/8)) =
exists_e lemma7 [X]
[p1: pf (forall [Y] isInt Y)]
forall_e p1 (const 5/8).
Load lemma7 and theorem8. Theorem8 "proves" that 5/8 is an integer.
However, 5/8 is not an integer. What's wrong?
Examine lemma7. This has the form name : type .
It is not of the form name = value .
It is not of the form name : type = value .
Therefore it is not a "definition," it is a "constructor". That is,
it's a new inference rule or axiom of the logic. From this inference rule,
anything can be proved, even false:
theorem9: pf (false) =
cut (greatereq_plus1_i theorem8 p_zero (eval_gt 5/8>0))
[p1: pf (geq (const 5/8) (succ zero))]
cut (congr (geq (const 5/8)) (symm eval_plus) p1)
[p2: pf (geq (const 5/8) one)]
cut (congr2 geq (symm eval_plus) (symm eval_plus) (ord_add_closure p2))
[p3: pf (geq zero (const 3/8))]
cut (eval_gt 3/8>0)
[p4: pf (gt (const 3/8) zero)]
not_e p4 p3.
Thus we say that the axiom "exists [X] forall [Y] isInt Y" is unsound,
or more precisely, the logic formed by adding this rule to our
coreTCB logic is unsound.
Twelf does not prevent you from adding new axioms and inference rules.
When you are in the middle of proving some theorem, you may create
a new lemma for which you don't yet have a proof, but you're sure
it's true. In this case, you can add the lemma without proof,
just like lemma7 above. But then you should go back and prove it.
For now, use the Twelf menu to do Twelf > Server State > Reset;
this will remove the unsound axiom, and all the other axioms.
Then control-c control-c to reload the logic.
15. Object-logic definitions
To explore object-logic definitions, we will use some elementary
set theory. Let a set whose elements have type T, i.e. a "set T",
be represented as a predicate that takes T as an argument, i.e.
set: tp -> tp = [T] T arrow form.
(Load this.) Then the empty set can be defined as a predicate that
always returns false:
emptyset: tm (set T) = lam [X:tm T] false.
(Load this.) This is an object-logic predicate, i.e. it has type
"tm (T arrow form)" instead of "tm T -> tm form".
In fact, we could not possibly use a metalogic function here,
emptyset_x: tm T -> tm form = [X: tm T] false.
because this not have a type compatible with "tm (set T)".
We will define "subset" as a two-argument object-logic predicate,
i.e. "subset @ A @ B" when every member of A is also a member of B:
subset : tm (set T arrow set T arrow form) =
lam2[A][B] forall [V] A @ V imp B @ V.
By the way, lam2[A][B]... means the same as lam[A] lam[B] ...
Similarly for lam3[A][B][C], lam4, lam5, etc.
Now we can prove that for any set B, emptyset is a subset of B:
emptyset_subset: pf (subset @ emptyset @ B) =
hole (subset @ emptyset @ B).
We will proving this by first proving (forall [V] emptyset @ V imp B @ V);
this is the body of the "subset" definition, with emptyset for A and
B for B. Then the lemma def2_i converts a proof of the body of
a 2-argument definition to a proof of the defined term. In other words:
emptyset_subset: pf (subset @ emptyset @ B) =
def2_i
(hole (forall [V] emptyset @ V imp B @ V)).
Now we proceed with forall-introduction and imp_introduction, i.e.
emptyset_subset: pf (subset @ emptyset @ B) =
def2_i
(forall_i [V]
imp_i [p1: pf (emptyset @ V)]
hole (B @ V)).
Just as def2_i "introduces" a defined two-arg predicate (by using
a proof of the expanded definition), def1_e "eliminates" a
one-arg definition by providing a proof of the expanded definition.
In particular, if p1 proves (emptyset @ V) then
(def1_e p1) proves (false).
emptyset_subset: pf (subset @ emptyset @ B) =
def2_i
(forall_i [V]
imp_i [p1: pf (emptyset @ V)]
cut (def1_e p1)
[p2: pf false]
hole (B @ V)).
Now false_e proves anything from a proof of false:
emptyset_subset: pf (subset @ emptyset @ B) =
def2_i
(forall_i [V]
imp_i [p1: pf (emptyset @ V)]
cut (def1_e p1)
[p2: pf false]
false_e p2).
Usually one would not use "cut" for such a trivial subproof, so we would
have
emptyset_subset: pf (subset @ emptyset @ B) =
def2_i
(forall_i [V]
imp_i [p1: pf (emptyset @ V)]
false_e (def1_e p1)).
Let's do another one: Let's prove that subset is transitive:
subset_trans: pf (subset @ A @ B) -> pf (subset @ B @ C) ->
pf (subset @ A @ C) = ...
As usual, we bind the arguments (premises) of the proof, and
since we haven't used them yet (it's not strict), we need %abbrev
for the time being:
%abbrev
subset_trans: pf (subset @ A @ B) -> pf (subset @ B @ C) ->
pf (subset @ A @ C) =
[p1: pf (subset @ A @ B)]
[p2: pf (subset @ B @ C)]
hole (subset @ A @ C).
(Load this.)
Now, we can prove subset @ A @ C using def2_i:
%abbrev
subset_trans: pf (subset @ A @ B) -> pf (subset @ B @ C) ->
pf (subset @ A @ C) =
[p1: pf (subset @ A @ B)]
[p2: pf (subset @ B @ C)]
def2_i
(hole (forall [V] A @ V imp C @ V)).
The next two steps are straightforward:
%abbrev
subset_trans: pf (subset @ A @ B) -> pf (subset @ B @ C) ->
pf (subset @ A @ C) =
[p1: pf (subset @ A @ B)]
[p2: pf (subset @ B @ C)]
def2_i
(forall_i [V]
imp_i [p3: pf (A @ V)]
hole (C @ V)).
Now we use p1 and p2. (def2_e p1) is a proof of (forall [V] A @ V imp B @ V),
so (forall_e (def2_e p1) V) is a proof of (A @ V imp B @ V),
so (imp_e (forall_e (def2_e p1) V) p3) is a proof of (B @ V):
%abbrev
subset_trans: pf (subset @ A @ B) -> pf (subset @ B @ C) ->
pf (subset @ A @ C) =
[p1: pf (subset @ A @ B)]
[p2: pf (subset @ B @ C)]
def2_i
(forall_i [V]
imp_i [p3: pf (A @ V)]
cut (imp_e (forall_e (def2_e p1) V) p3)
[p4: pf (B @ V)]
hole (C @ V)).
The rest is similar:
subset_trans: pf (subset @ A @ B) -> pf (subset @ B @ C) ->
pf (subset @ A @ C) =
[p1: pf (subset @ A @ B)]
[p2: pf (subset @ B @ C)]
def2_i
(forall_i [V]
imp_i [p3: pf (A @ V)]
cut (imp_e (forall_e (def2_e p1) V) p3)
[p4: pf (B @ V)]
imp_e (forall_e (def2_e p2) V) p4).
Exercise: define a universal set
universalset: tm (set T) = ...
that contains every element of type T, and prove
subset_universal: pf (subset @ A @ universalset) = ...
subset_refl: pf (subset @ A @ A) = ...
Solution in proving4a.elf.