From e9df793ecee5a1e3b94615a701a5cea8640d0b87 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 23 Feb 2019 18:14:09 +0100 Subject: more proofs involving equality --- Eq.thy | 141 +++++++++++++++++++++++++++++++++++++++++++++-------------------- 1 file changed, 97 insertions(+), 44 deletions(-) diff --git a/Eq.thy b/Eq.thy index e89aeea..d8e3153 100644 --- a/Eq.thy +++ b/Eq.thy @@ -48,14 +48,14 @@ section \Path induction\ text \We set up rudimentary automation of path induction:\ -method path_ind for a b p :: t = - (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (assumption | fact)?) - -method path_ind' for C :: "[t, t, t] \ t" = +method path_ind for C :: "[t, t, t] \ t" = (rule Eq_elim[where ?C=C]; (assumption | fact)?) +method path_ind' for a b p :: t = + (rule Eq_elim[where ?a=a and ?b=b and ?p=p]; (assumption | fact)?) + syntax "_induct_over" :: "[idt, idt, idt, t] \ [t, t, t] \ t" ("(2{_, _, _}/ _)" 0) -translations "{x, y, p} C" \ "\x y p. C" +translations "{x, y, p} C" \ "\x y p. C" section \Properties of equality\ @@ -95,15 +95,19 @@ subsection \Transitivity (path composition)\ schematic_goal transitivity: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?p: \z: A. y =[A]z \ x =[A] z" -proof (path_ind x y p, quantify_all) - fix x z show "\p. p: x =[A] z \ p: x =[A] z" . -qed (routine add: assms) + shows "?p: \z: A. y =[A] z \ x =[A] z" +by + (path_ind' x y p, quantify_all, + path_ind "{x, z, _} x =[A] z", + rule Eq_intro, routine add: assms) definition pathcomp :: "[t, t, t, t, t, t] \ t" where - "pathcomp A x y z p q \ - (indEq (\x y _. \z: A. y =[A] z \ x =[A] z) (\x. \y: A. id (x =[A] y)) x y p)`z`q" + "pathcomp A x y z p q \ (indEq + (\x y _. \z: A. y =[A] z \ x =[A] z) + (\x. \(z: A). \(q: x =[A] z). indEq (\x z _. x =[A] z) (\x. refl x) x z q) + x y p)`z`q" + syntax "_pathcomp" :: "[t, t] \ t" (infixl "*" 110) @@ -124,12 +128,12 @@ end lemma pathcomp_type: assumes "A: U i" "x: A" "y: A" "z: A" "p: x =[A] y" "q: y =[A] z" shows "pathcomp A x y z p q: x =[A] z" -unfolding pathcomp_def by (routine add: transitivity assms) +unfolding pathcomp_def by (derive lems: transitivity assms) lemma pathcomp_cmp: assumes "A: U i" and "a: A" shows "pathcomp A a a a (refl a) (refl a) \ refl a" -unfolding pathcomp_def by (derive lems: assms) +unfolding pathcomp_def by (derive lems: transitivity assms) lemmas pathcomp_type [intro] lemmas pathcomp_comp [comp] = pathcomp_cmp @@ -140,7 +144,7 @@ section \Higher groupoid structure of types\ schematic_goal pathcomp_idr: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" shows "?a: pathcomp A x y y p (refl y) =[x =[A] y] p" -proof (path_ind x y p) +proof (path_ind' x y p) show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" by (derive lems: assms) qed (routine add: assms) @@ -148,7 +152,7 @@ qed (routine add: assms) schematic_goal pathcomp_idl: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" shows "?a: pathcomp A x x y (refl x) p =[x =[A] y] p" -proof (path_ind x y p) +proof (path_ind' x y p) show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (refl x) =[x =[A] x] (refl x)" by (derive lems: assms) qed (routine add: assms) @@ -156,7 +160,7 @@ qed (routine add: assms) schematic_goal pathcomp_invr: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" shows "?a: pathcomp A x y x p (inv A x y p) =[x =[A] x] (refl x)" -proof (path_ind x y p) +proof (path_ind' x y p) show "\x. x: A \ refl(refl x): pathcomp A x x x (refl x) (inv A x x (refl x)) =[x =[A] x] (refl x)" @@ -166,7 +170,7 @@ qed (routine add: assms) schematic_goal pathcomp_invl: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" shows "?a: pathcomp A y x y (inv A x y p) p =[y =[A] y] refl(y)" -proof (path_ind x y p) +proof (path_ind' x y p) show "\x. x: A \ refl(refl x): pathcomp A x x x (inv A x x (refl x)) (refl x) =[x =[A] x] (refl x)" @@ -176,7 +180,7 @@ qed (routine add: assms) schematic_goal inv_involutive: assumes "A: U i" "x: A" "y: A" "p: x =[A] y" shows "?a: inv A y x (inv A x y p) =[x =[A] y] p" -proof (path_ind x y p) +proof (path_ind' x y p) show "\x. x: A \ refl(refl x): inv A x x (inv A x x (refl x)) =[x =[A] x] (refl x)" by (derive lems: assms) qed (routine add: assms) @@ -191,6 +195,7 @@ In particular, changing the order causes unification to fail in the path inducti It seems to be good practice to order the variables in the order over which we will path-induct. \ +declare[[pretty_pathcomp=false]] schematic_goal pathcomp_assoc: assumes "A: U i" shows @@ -198,38 +203,86 @@ schematic_goal pathcomp_assoc: pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] pathcomp A x z w (pathcomp A x y z p q) r" - apply (quantify 3) - apply (path_ind' "{x, y, p} - \(z: A). \(q: y =[A] z). \(w: A). \(r: z =[A] w). - Eq.pathcomp A x y w p (Eq.pathcomp A y z w q r) =[x =[A] w] - Eq.pathcomp A x z w (Eq.pathcomp A x y z p q) r") - apply (quantify 2) - apply (path_ind' "{xa, z, q} - \(w: A). \(r: z =[A] w). - Eq.pathcomp A xa xa w (refl xa) (Eq.pathcomp A xa z w q r) =[xa =[A] w] - Eq.pathcomp A xa z w (Eq.pathcomp A xa xa z (refl xa) q) r") - apply (quantify 2) - apply (path_ind' "{xb, w, r} - Eq.pathcomp A xb xb w (refl xb) (Eq.pathcomp A xb xb w (refl xb) r) =[xb =[A] w] - Eq.pathcomp A xb xb w (Eq.pathcomp A xb xb xb (refl xb) (refl xb)) r") +apply (quantify 3) +apply (path_ind "{x, y, p} + \(z: A). \(q: y =[A] z). \(w: A). \(r: z =[A] w). + pathcomp A x y w p (pathcomp A y z w q r) =[x =[A] w] + pathcomp A x z w (pathcomp A x y z p q) r") +apply (quantify 2) +apply (path_ind "{xa, z, q} + \(w: A). \(r: z =[A] w). + pathcomp A xa xa w (refl xa) (pathcomp A xa z w q r) =[xa =[A] w] + pathcomp A xa z w (pathcomp A xa xa z (refl xa) q) r") +apply (quantify 2) +apply (path_ind "{xb, w, r} + pathcomp A xb xb w (refl xb) (pathcomp A xb xb w (refl xb) r) =[xb =[A] w] + pathcomp A xb xb w (pathcomp A xb xb xb (refl xb) (refl xb)) r") text \The rest is now routine.\ -proof - fix x assume *: "x: A" - show "pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)): x =[A] x" - and "pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x): x =[A] x" - and "pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x): x =[A] x" - and "refl(refl x): pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x] - pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)" - and "refl(refl x): pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x) =[x =[A] x] - pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)" - by (derive lems: * assms) +proof - + show + "\x. x: A \ refl(refl x): + pathcomp A x x x (refl x) (pathcomp A x x x (refl x) (refl x)) =[x =[A] x] + pathcomp A x x x (pathcomp A x x x (refl x) (refl x)) (refl x)" + by (derive lems: assms) qed (derive lems: assms) -(* Possible todo: - implement a custom version of schematic_goal/theorem that exports the derived proof term. +(* Todo, if possible: + Implement a custom version of schematic_goal/theorem that exports the derived proof term. *) +section \Functoriality of functions on types\ + +schematic_goal transfer: + assumes + "A: U i" "B: U i" "f: A \ B" + "x: A" "y: A" "p: x =[A] y" + shows "?a: f`x =[B] f`y" +by (path_ind' x y p, rule Eq_intro, routine add: assms) + +definition ap :: "[t, t, t, t, t] \ t" +where "ap B f x y p \ indEq ({x, y, _} f`x =[B] f`y) (\x. refl (f`x)) x y p" + +lemma ap_type: + assumes + "A: U i" "B: U i" "f: A \ B" + "x: A" "y: A" "p: x =[A] y" + shows "ap B f x y p: f`x =[B] f`y" +unfolding ap_def using assms by (rule transfer) + +lemma ap_cmp: + assumes "A: U i" "B: U i" "f: A \ B" "x: A" + shows "ap B f x x (refl x) \ refl (f`x)" +unfolding ap_def by (derive lems: assms) + +lemmas ap_type [intro] +lemmas ap_comp [comp] = ap_cmp + + +schematic_goal ap_func1: + assumes "A: U i" "B: U i" "f: A \ B" + shows + "?a: \x: A. \y: A. \p: x =[A] y. \z: A. \q: y =[A] z. + ap B f x z (pathcomp A x y z p q) =[f`x =[B] f`z] + pathcomp B (f`x) (f`y) (f`z) (ap B f x y p) (ap B f y z q)" + +apply (quantify 3) +apply (path_ind "{x, y, p} + \z: A. \q: y =[A] z. + ap B f x z (pathcomp A x y z p q) =[f`x =[B] f`z] + pathcomp B (f`x) (f`y) (f`z) (ap B f x y p) (ap B f y z q)") +apply (quantify 2) +apply (path_ind "{x, z, q} + ap B f x z (pathcomp A x x z (refl x) q) =[f`x =[B] f`z] + pathcomp B (f`x) (f`x) (f`z) (ap B f x x (refl x)) (ap B f x z q)") + +proof - + show + "\x. x: A \ refl(refl(f`x)): ap B f x x (pathcomp A x x x (refl x) (refl x)) =[f`x =[B] f`x] + pathcomp B (f`x) (f`x) (f`x) (ap B f x x (refl x)) (ap B f x x (refl x))" + by (derive lems: assms) +qed (derive lems: assms) + end -- cgit v1.2.3