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.