Hints on proving theorems in Twelf, continued Andrew W. Appel March 2000 19. Extensionality & Equivalence Relations Load the usual sources.cfg, then visit core/set/set.elf and load that file (by control-C control-S). If you would like some exercises to practice your proving skills, reprove each of the theorems in that file by visiting proving7a.elf instead and replacing each hole. Now warm up by proving the following theorem: set_congr: pf (eq A B) -> pf (set_equiv @ A @ B) = ... The next theorem is just the converse. Prove this one, and if you get stuck, see the hint (proving7b.elf) sooner rather than later. set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) = ... Do not continue with this section until you have either proved the theorem or looked at the hint. More hints (but see proving7b first): The solution to set_extensionality starts like this, set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) = [p1: pf (set_equiv @ A @ B)] extensionality (forall_i [x] cut p1 [_] hole (eq (A @ x) (B @ x))). fill in the hole if you can; otherwise keep reading. set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) = [p1: pf (set_equiv @ A @ B)] cut p1 [_] extensionality (forall_i [x] or_e excluded_middle ([p11: pf (A @ x)] hole (eq (A @ x) (B @ x))) ([p21: pf (not (A @ x))] hole (eq (A @ x) (B @ x)))). fill in the hole if you can; otherwise keep reading. set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) = [p1: pf (set_equiv @ A @ B)] cut p1 [_] extensionality (forall_i [x] or_e excluded_middle ([p11: pf (A @ x)] cut (set_equiv_e1 p1 p11) [p12: pf (B @ x)] trans (extensional_true p11) (symm (extensional_true p12))) ([p21: pf (not (A @ x))] hole (eq (A @ x) (B @ x)))). fill in the hole if you can; otherwise keep reading. set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) = [p1: pf (set_equiv @ A @ B)] cut p1 [_] extensionality (forall_i [x] or_e excluded_middle ([p11: pf (A @ x)] cut (set_equiv_e1 p1 p11) [p12: pf (B @ x)] trans (extensional_true p11) (symm (extensional_true p12))) ([p21: pf (not (A @ x))] cut (not_ei p21 [p22: pf (B @ x)] set_equiv_e2 p1 p22) [p23: pf (not (B @ x))] trans (extensional_false p21) (symm (extensional_false p23)))). Well, that's all very nice, but our object logic doesn't have an extensionality law, so these proofs can't be used. In fact, now your Twelf server is corrupted by the loading of the extensionality axioms, so you should reset Twelf (see the Twelf menu at the top of the Emacs window) and reload the sources.cfg and core/set/set.elf. Why do we avoid extensionality? There are three reasons: 1. It's unnecessary. We can do without it, so we avoid cluttering are axiom base. 2. We wish to construct proofs that are checkable in many other mechanical proof assistants, such as Coq (which uses the Calculus of Constructions) or HOL (which uses higher-order logic). Coq has no extensionality law -- in the full calculus of constructions it is not sound -- so we will avoid it too. 3. If we build theorem libraries that rely on "eq" equality, they will be insufficiently general. Very often the appropriate equivalence relation on mathematical structures is not "eq" but something else. Avoiding the extensionality axiom disciplines us, requires us to construct more general theories. Now, back to set_extensionality. Without the extensionality axiom, set_extensionality is unprovable. Therefore, we must avoid constructing theorems that rely on the "eq" equality of two sets; instead we should rely on "set_equiv" equality. In general, each type has its own natural equality function: eqrel: tp -> tp = [T] T arrow T arrow form. eq_arith: tm (eqrel num) = lam2 [x][y] eq x y. eq_set: tm (eqrel (set T)) = set_equiv. eq_form: tm (eqrel form) = lam2 [a][b] a equiv b. Each of these has the property that it is an equivalence relation; that is, it is reflexive, symmetric, and transitive. Examine (and load) the file core/rel/equiv.elf and find the definition of an equivalence relation: valideqv: tm (rel T T arrow form) = lam [R] reflexive @ R and symmetric @ R and transitive @ R. Exercise: prove each of the following. eq_arith_eqv: pf (valideqv @ eq_arith) = ... eq_set_eqv: pf (valideqv @ eq_set) = ... eq_form_eqv: pf (valideqv @ eq_form) = ... Solutions in proving7d.elf. It would be a good thing to make a utility lemma "valideqv_i" for proving that things are equivalence relations. This lemma would include the standard verbiage of def1_i (and3_i (def1_i (forall_i ...)) (def1_i (forall2_i ...)) (def1_i (forall3_i ...))) Using the lemma, we could prove eq_form_eqv more concisely: eq_form_eqv: pf (valideqv @ eq_form) = valideqv_i ([x] def2_i equiv_refl) ([x][y][p1: pf (eq_form @ x @ y)] def2_i (equiv_symm (def2_e p1))) ([x][y][z][p2: pf (eq_form @ x @ y)] [p3: pf (eq_form @ y @ z)] def2_i (equiv_trans (def2_e p2) (def2_e p3))). Exercise: Design and prove the valideqv_i lemma, so that the proof above is valid. (Solution in proving7e.elf.) We say that a function [respects extensionality] (is that the right term?) if it maps equivalent arguments to equivalent results. But there are many notions of "equivalent", as we have seen. So we must phrase the notion more precisely: function_extens: tm (eqrel S arrow eqrel T arrow (S arrow T) arrow form) = lam3 [eqS: tm (eqrel S)] [eqT: tm (eqrel T)] [f: tm (S arrow T)] forall2 [x: tm S][y: tm S] eqS @ x @ y imp eqT @ (f @ x) @ (f @ y). An example is the predicate "isempty", isempty: tm (set U arrow form) = lam [s] not (exists [x] s @ x). Here, S is "set U", T is "form", and the theorem is that isempty respects extensionality: isempty_extens: pf (function_extens @ eq_set @ eq_form @ isempty) = ... Exercise: Prove this theorem. Solution: proving7f.elf. Suppose we have functions F and G, each of type (Ta arrow Tb), and suppose we have an equality function (equivalence relation) H1 on Ta and an equality H2 on Tb: H1 : tm (eqrel Ta) H2 : tm (eqrel Tb) F : tm (Ta arrow Tb) G : tm (Ta arrow Tb) Then we say that F and G are equivalent functions if they map equivalent arguments to equivalent results. This is expressed by the eq+ predicate (found in core/eq.elf). eq+ : tm (eqrel Ta arrow eqrel Tb arrow eqrel (Ta arrow Tb)) = lam4 [H1 : tm (eqrel Ta)] [H2 : tm (eqrel Tb)] [F : tm (Ta arrow Tb)] [G : tm (Ta arrow Tb)] forall2 [x : tm Ta][y : tm Ta] (H1 @ x @ y imp H2 @ (F @ x) @ (F @ y)) imp (H1 @ x @ y imp H2 @ (G @ x) @ (G @ y)) imp (H1 @ x @ y imp H2 @ (F @ x) @ (G @ y)). (Actually, we are a bit more liberal: if F or G does not respect the equivalences H1 & H2 -- that is, if F maps equivalent arguments to inequivalent results -- then we're also willing to say that F=G. This is mainly so that every function will be equivalent to itself.) For example, consider two different formulations of isempty: isempty: tm (set U arrow form) = lam [s] not (exists [x] s @ x). isempty2: tm (set U arrow form) = lam [s] forall [t] subset @ (set_union @ s @ t) @ t. We can say that these functions are "equal" by asserting, isempty_eq_isempty2: (eq+ @ eq_set @ eq_form) @ isempty @ isempty2. So, eq+ is used to construct equality predicates on functions from the equality predicates on the argument and result types. Exercise: prove isempty_eq_isempty2. Hints & solution: proving7g.elf. Exercise: Using eq+, construct the appropriate equality function for the type (num arrow num arrow num), and then show that the following two functions are equal: f: tm (num arrow num arrow num) = lam2 plus. g: tm (num arrow num arrow num) = lam2 [x][y] plus y x. Solution: proving7h.elf. Conclusion: Though it's tempting to use the polymorphic "eq" function in defining other predicates, beware. Users of your predicates will be able to use the congruence rule (congr) to eliminate the eq, but may have a difficult time introducing facts of the form (eq A B). To avoid this problem, use the appropriate higher-order equality function, constructed using eq+, eq_arith, eq_form, etc.