Hints on proving theorems in Twelf, continued Andrew W. Appel February 2000 16. A case study Debugging a proof and understanding Twelf error messages takes practice. The following case study should improve your skills. Start by loading the core definitions (control-C control-C), then load each of these definitions: set: tp -> tp = [T] T arrow form. rel: tp -> tp -> tp = [T][U] T arrow U arrow form. emptyset: tm (set T) = lam [X:tm T] false. subset : tm (set T arrow set T arrow form) = lam2[S][T] forall [V] S @ V imp T @ V. emptyset_subset: pf (subset @ emptyset @ S) = def2_i (forall_i [X] imp_i [P1:pf (emptyset @ X)] false_e (def1_e P1)). transitive: tm (rel T T arrow form) = lam [R] forall3 [X][Y][Z] R @ X @ Y imp R @ Y @ Z imp R @ X @ Z. poset_to_set: tm (rel T T arrow set T) = lam [R] lam [E] R @ E @ E. upper_bound: tm (rel T T arrow set T arrow T arrow form) = lam3 [R][S][X] transitive @ R and subset @ S @ (poset_to_set @ R) and R @ X @ X and (forall [Y] S @ Y imp R @ Y @ X). set_finite: tm (set T arrow form). % body of definition omitted here. emptyset_finite: pf (set_finite @ emptyset). % body of theorem omitted. directed_subset : tm (rel T T arrow set T arrow form) = lam2 [R][S] transitive @ R and subset @ S @ (poset_to_set @ R) and (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X). Now, a theorem: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = ... A first attempt to prove this theorem looked like this: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1] [p2] [p3] and_e1 (imp_e (forall_e p3 emptyset) (and_i emptyset_subset emptyset_finite)). Load this definition. EXERCISE: Try to complete this proof before reading further. The definition above fails with a Twelf error message: stdIn:4.20-7.47 Error: Type mismatch Expected: pf (transitive @ `R) -> pf (subset @ `S @ (poset_to_set @ `R)) -> pf (forall ([So:tm (set X1)] subset @ So @ `S and set_finite @ So imp exists ([X:tm X1] `S @ X and upper_bound @ `R @ So @ X))) -> pf (X2 p) Found: {p1:pf (transitive @ `R)} {p2:pf (subset @ `S @ (poset_to_set @ `R))} {p3:pf (forall ([x:tm (set X1)] subset @ x @ `S and set_finite @ x imp exists ([X:tm X1] `S @ X and upper_bound @ `R @ x @ X)))} pf (X2 p) Constant clash Such a lengthy message is hard to interpret. First it's useful to understand that {p1: pf A} pf B is exactly the same type as pf A -> pf B The latter type-notation is just shorthand for a dependent type in which the right hand side does not actually use the argument. Also, in Twelf's error message, in "Expected" there is a bound variable "So" and in "Found" there is a variable "x". But expressions in Twelf are equivalent modulo renaming of bound variables, so this difference is not the source of the error message. If we rewrite the "Found" type with these identities, we find that the "Expected" type is identical to the "Found" type! This is a bug in Twelf error-reporting. It's not that the proof is correct but judged wrong -- there is indeed a bug in the proof, and it should not type-check. It's that Twelf has been unable to inform us of what's wrong. There is a solution, however. We can just attempt the proof one step at a time, using "cut". We can also fill in the types of the bound variables p1,p2,p3. EXERCISE: Before reading further, fill in the types of p1,p2,p3 and replace the last three lines of the proof with the appropriate "hole". Now the proof looks like this: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1: pf (transitive @ R)] [p2: pf (subset @ S @ (poset_to_set @ R))] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] hole (exists [X] S @ X). Now we con proceed forward using "cut". EXERCISE: Before reading further, cut in a formula before the hole, a forall-elimination, instantiating the "So" of fact "p3" with the empty set. directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1: pf (transitive @ R)] [p2: pf (subset @ S @ (poset_to_set @ R))] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] cut (forall_e p3 emptyset) [p4: pf (subset @ emptyset @ S and set_finite @ emptyset imp exists [X] S @ X and upper_bound @ R @ emptyset @ X)] hole (exists [X] S @ X). The next step is to imp_e p4, using provable facts about the empty set: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1: pf (transitive @ R)] [p2: pf (subset @ S @ (poset_to_set @ R))] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] cut (forall_e p3 emptyset) [p4: pf (subset @ emptyset @ S and set_finite @ emptyset imp exists [X] S @ X and upper_bound @ R @ emptyset @ X)] cut (imp_e p4 (and_i emptyset_subset emptyset_finite)) [p5: pf (exists [X] S @ X and upper_bound @ R @ emptyset @ X)] hole (exists [X] S @ X). Now we're almost at the place where the proof failed before: we do and-elimination on p5: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1: pf (transitive @ R)] [p2: pf (subset @ S @ (poset_to_set @ R))] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] cut (forall_e p3 emptyset) [p4: pf (subset @ emptyset @ S and set_finite @ emptyset imp exists [X] S @ X and upper_bound @ R @ emptyset @ X)] cut (imp_e p4 (and_i emptyset_subset emptyset_finite)) [p5: pf (exists [X] S @ X and upper_bound @ R @ emptyset @ X)] and_e1 p5. Load this definition. It fails, with the error message stdIn:14.9-14.11 Error: Type mismatch Expected: pf (forall ([x:tm form] (X1 p p1 p2 p3 p4 p5 imp X2 p p1 p2 p3 p4 p5 imp x) imp x)) Found: pf (exists ([X:tm X3] `S @ X and upper_bound @ `R @ emptyset @ X)) Constant clash This error message doesn't exactly tell us what's wrong. However, at least the "Expected" and "Found" formulas are different! Also, the location of the error has been narrowed down significantly. Instead of reading the details of the error message, we examine "and_e1 p5". EXERCISE: Figure out why (and_e1 p5) does not prove (exists [X] S @ X). Solution is in proving5a.elf To complete the proof, we would like to show (exists [X] S @ X). The fact "p5" is very useful, but we don't know which X it's talking about. Therefore, we use exists-elimination to give us the name of the unknown X: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1: pf (transitive @ R)] [p2: pf (subset @ S @ (poset_to_set @ R))] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] cut (forall_e p3 emptyset) [p4: pf (subset @ emptyset @ S and set_finite @ emptyset imp exists [X] S @ X and upper_bound @ R @ emptyset @ X)] cut (imp_e p4 (and_i emptyset_subset emptyset_finite)) [p5: pf (exists [X] S @ X and upper_bound @ R @ emptyset @ X)] exists_e p5 [X] [p6: pf (S @ X and upper_bound @ R @ emptyset @ T)] hole (exists [X] S @ X). EXERCISE: Load this definition. It fails. Find the bug and fix it. Solution: in proving5b.elf. Now that this minor bug is fixed, we can pick apart p6 using and_l: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1: pf (transitive @ R)] [p2: pf (subset @ S @ (poset_to_set @ R))] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] cut (forall_e p3 emptyset) [p4: pf (subset @ emptyset @ S and set_finite @ emptyset imp exists [X] S @ X and upper_bound @ R @ emptyset @ X)] cut (imp_e p4 (and_i emptyset_subset emptyset_finite)) [p5: pf (exists [X] S @ X and upper_bound @ R @ emptyset @ X)] exists_e p5 [X] [p6: pf (S @ X and upper_bound @ R @ emptyset @ X)] and_l p6 [p7: pf (S @ X)] [p8: pf (upper_bound @ R @ emptyset @ X)] hole (exists [X] S @ X). Armed with p7, we can now do exists_i to fill the hole: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1: pf (transitive @ R)] [p2: pf (subset @ S @ (poset_to_set @ R))] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] cut (forall_e p3 emptyset) [p4: pf (subset @ emptyset @ S and set_finite @ emptyset imp exists [X] S @ X and upper_bound @ R @ emptyset @ X)] cut (imp_e p4 (and_i emptyset_subset emptyset_finite)) [p5: pf (exists [X] S @ X and upper_bound @ R @ emptyset @ X)] exists_e p5 [X] [p6: pf (S @ X and upper_bound @ R @ emptyset @ X)] and_l p6 [p7: pf (S @ X)] [p8: pf (upper_bound @ R @ emptyset @ X)] exists_i X p7. A more concise version of this proof is as follows: directed_nonempty: pf (directed_subset @ R @ S) -> pf (exists [X] S @ X) = [p: pf (directed_subset @ R @ S)] and3_l (def2_e p) [p1] [p2] [p3: pf (forall [So] subset @ So @ S and set_finite @ So imp exists [X] S @ X and upper_bound @ R @ So @ X)] cut (imp_e (forall_e p3 emptyset) (and_i emptyset_subset emptyset_finite)) [p5: pf (exists [X] S @ X and upper_bound @ R @ emptyset @ X)] exists_ei p5 [X] [p6: pf (S @ X and upper_bound @ R @ emptyset @ X)] and_e1 p6. Look up "exists_ei" in core/basiclem.elf to see what it does.