From c2dfffffb7586662c67e44a2d255a1a97ab0398b Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 2 Apr 2020 17:57:48 +0200 Subject: Brand-spanking new version using Spartan infrastructure --- Eq.thy | 390 ----------------------------------------------------------------- 1 file changed, 390 deletions(-) delete mode 100644 Eq.thy (limited to 'Eq.thy') diff --git a/Eq.thy b/Eq.thy deleted file mode 100644 index dd92fce..0000000 --- a/Eq.thy +++ /dev/null @@ -1,390 +0,0 @@ -(******** -Isabelle/HoTT: Equality -Feb 2019 - -Contains: -* Type definitions for intensional equality -* Some setup for path induction -* Basic properties of equality (inv, pathcomp) -* The higher groupoid structure of types -* Functoriality of functions (ap) - -********) - -theory Eq -imports HoTT_Methods Prod - -begin - - -section \Type definitions\ - -axiomatization - Eq :: "[t, t, t] \ t" and - refl :: "t \ t" and - indEq :: "[[t, t, t] \ t, t \ t, t, t, t] \ t" - -syntax - "_Eq" :: "[t, t, t] \ t" ("(2_ =[_]/ _)" [101, 0, 101] 100) -translations - "a =[A] b" \ "(CONST Eq) A a b" - -axiomatization where - Eq_form: "\A: U i; a: A; b: A\ \ a =[A] b: U i" and - - Eq_intro: "a: A \ (refl a): a =[A] a" and - - Eq_elim: "\ - p: a =[A] b; - a: A; - b: A; - \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f a b p: C a b p" and - - Eq_comp: "\ - a: A; - \x. x: A \ f x: C x x (refl x); - \x y. \x: A; y: A\ \ C x y: x =[A] y \ U i \ \ indEq C f a a (refl a) \ f a" - -lemmas Eq_form [form] -lemmas Eq_routine [intro] = Eq_form Eq_intro Eq_elim -lemmas Eq_comp [comp] - - -section \Path induction\ - -text \We set up rudimentary automation of path induction:\ - -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" - -text \ -Use "@{method path_ind} @{term "{x, y, p} C x y p"}" to perform path induction for the given type family over the variables @{term x}, @{term y}, and @{term p}, -and "@{method path_ind'} @{term a} @{term b} @{term p}" to let Isabelle try and infer the shape of the type family itself (this doesn't always work!). - -Note that @{term "{x, y, p} C x y p"} is just syntactic sugar for @{term "\x y p. C x y p"}. -\ - - -section \Properties of equality\ - -subsection \Symmetry (path inverse)\ - -definition inv :: "[t, t, t] \ t" -where "inv A x y \ \p: x =[A] y. indEq (\x y. &(y =[A] x)) (\x. refl x) x y p" - -syntax "_inv" :: "[t, t, t] \ t" ("(2inv[_, _, _])" [0, 0, 0] 999) -translations "inv[A, x, y]" \ "(CONST inv) A x y" - -syntax "_inv'" :: "t \ t" ("inv") - -text \Pretty-printing switch for path inverse:\ - -ML \val pretty_inv = Attrib.setup_config_bool @{binding "pretty_inv"} (K true)\ - -print_translation \ -let fun inv_tr' ctxt [A, x, y] = - if Config.get ctxt pretty_inv - then Syntax.const @{syntax_const "_inv'"} - else Syntax.const @{syntax_const "_inv"} $ A $ x $ y -in - [(@{const_syntax inv}, inv_tr')] -end -\ - -lemma inv_type: "\A: U i; x: A; y: A\ \ inv[A, x, y]: x =[A] y \ y =[A] x" -unfolding inv_def by derive - -lemma inv_comp: "\A: U i; a: A\ \ inv[A, a, a]`(refl a) \ refl a" -unfolding inv_def by derive - -declare - inv_type [intro] - inv_comp [comp] - - -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" -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" -where - "pathcomp A x y z \ \p: x =[A] y. \q: y =[A] z. (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, t, t, t] \ t" - ("(2pathcomp[_, _, _, _])" [0, 0, 0, 0] 999) -translations "pathcomp[A, x, y, z]" \ "(CONST pathcomp) A x y z" - -syntax "_pathcomp'" :: "[t, t] \ t" ("pathcomp") - -ML \val pretty_pathcomp = Attrib.setup_config_bool @{binding "pretty_pathcomp"} (K true)\ -\ \Pretty-printing switch for path composition\ - -print_translation \ -let fun pathcomp_tr' ctxt [A, x, y, z] = - if Config.get ctxt pretty_pathcomp - then Syntax.const @{syntax_const "_pathcomp'"} - else Syntax.const @{syntax_const "_pathcomp"} $ A $ x $ y $ z -in - [(@{const_syntax pathcomp}, pathcomp_tr')] -end -\ - -corollary pathcomp_type: - assumes [intro]: "A: U i" "x: A" "y: A" "z: A" - shows "pathcomp[A, x, y, z]: x =[A] y \ y =[A] z \ x =[A] z" -unfolding pathcomp_def by (derive lems: transitivity) - -corollary pathcomp_comp: - assumes [intro]: "A: U i" "a: A" - shows "pathcomp[A, a, a, a]`(refl a)`(refl a) \ refl a" -unfolding pathcomp_def by (derive lems: transitivity) - -declare - pathcomp_type [intro] - pathcomp_comp [comp] - - -section \Higher groupoid structure of types\ - -schematic_goal pathcomp_idr: - assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?prf: pathcomp[A, x, y, y]`p`(refl y) =[x =[A] 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 -qed routine - -schematic_goal pathcomp_idl: - assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?prf: pathcomp[A, x, x, y]`(refl x)`p =[x =[A] 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 -qed routine - -schematic_goal pathcomp_invr: - assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?prf: pathcomp[A, x, y, x]`p`(inv[A, x, y]`p) =[x =[A] x] (refl x)" -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)" - by derive -qed routine - -schematic_goal pathcomp_invl: - assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?prf: pathcomp[A, y, x, y]`(inv[A, x, y]`p)`p =[y =[A] y] refl(y)" -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)" - by derive -qed routine - -schematic_goal inv_involutive: - assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?prf: inv[A, y, x]`(inv[A, x, y]`p) =[x =[A] 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 -qed routine - -text \ -We use the proof of associativity of path composition to demonstrate the process of deriving proof terms. -The proof involves a triply-nested path induction, which is cumbersome to write in a structured style, especially if one does not know the correct form of the proof term in the first place. -However, using proof scripts the derivation becomes quite easy: we simply give the correct form of the statements to induct over, and prove the simple subgoals returned by the prover. - -The proof is sensitive to the order of the quantifiers in the product. -In particular, changing the order causes unification to fail in the path inductions. -It seems to be good practice to order the variables in the order over which we will path-induct. -\ - -schematic_goal pathcomp_assoc: - assumes [intro]: "A: U i" - shows - "?prf: \x: A. \y: A. \p: x =[A] y. \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 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 "{x, z, q} - \(w: A). \(r: z =[A] w). - pathcomp[A, x, x, w]`(refl x)`(pathcomp[A, x, z, w]`q`r) =[x =[A] w] - pathcomp[A, x, z, w]`(pathcomp[A, x, x, z]`(refl x)`q)`r") -apply (quantify 2) -apply (path_ind "{x, w, r} - pathcomp[A, x, x, w]`(refl x)`(pathcomp[A, x, x, w] `(refl x)`r) =[x =[A] w] - pathcomp[A, x, x, w]`(pathcomp[A, x, x, x]`(refl x)`(refl x))`r") - -text \The rest is now routine.\ - -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 -qed routine - - -section \Functoriality of functions on types under equality\ - -schematic_goal transfer: - assumes [intro]: - "A: U i" "B: U i" "f: A \ B" - "x: A" "y: A" "p: x =[A] y" - shows "?prf: f`x =[B] f`y" -by (path_ind' x y p, rule Eq_routine, routine) - -definition ap :: "[t, t, t, t, t] \ t" -where "ap f A B x y \ \p: x =[A] y. indEq ({x, y, _} f`x =[B] f`y) (\x. refl (f`x)) x y p" - -syntax "_ap" :: "[t, t, t, t, t] \ t" ("(2ap[_, _, _, _, _])") -translations "ap[f, A, B, x, y]" \ "(CONST ap) f A B x y" - -syntax "_ap'" :: "t \ t" ("ap[_]") - -ML \val pretty_ap = Attrib.setup_config_bool @{binding "pretty_ap"} (K true)\ - -print_translation \ -let fun ap_tr' ctxt [f, A, B, x, y] = - if Config.get ctxt pretty_ap - then Syntax.const @{syntax_const "_ap'"} $ f - else Syntax.const @{syntax_const "_ap"} $ f $ A $ B $ x $ y -in - [(@{const_syntax ap}, ap_tr')] -end -\ - -corollary ap_typ: - assumes [intro]: - "A: U i" "B: U i" "f: A \ B" - "x: A" "y: A" - shows "ap[f, A, B, x, y]: x =[A] y \ f`x =[B] f`y" -unfolding ap_def by routine - -corollary ap_app_typ: - assumes [intro]: - "A: U i" "B: U i" "f: A \ B" - "x: A" "y: A" "p: x =[A] y" - shows "ap[f, A, B, x, y]`p: f`x =[B] f`y" -by (routine add: ap_typ) - -lemma ap_comp: - assumes [intro]: "A: U i" "B: U i" "f: A \ B" "x: A" - shows "ap[f, A, B, x, x]`(refl x) \ refl (f`x)" -unfolding ap_def by derive - -lemmas ap_type [intro] = ap_typ ap_app_typ -lemmas ap_comp [comp] - - -schematic_goal ap_func_pathcomp: - assumes [intro]: "A: U i" "B: U i" "f: A \ B" - shows - "?prf: \x: A. \y: A. \p: x =[A] y. \z: A. \q: y =[A] z. - ap[f, A, B, x, z]`(pathcomp[A, x, y, z]`p`q) =[f`x =[B] f`z] - pathcomp[B, f`x, f`y, f`z]`(ap[f, A, B, x, y]`p)`(ap[f, A, B, y, z]`q)" -apply (quantify 3) -apply (path_ind "{x, y, p} - \z: A. \q: y =[A] z. - ap[f, A, B, x, z]`(pathcomp[A, x, y, z]`p`q) =[f`x =[B] f`z] - pathcomp[B, f`x, f`y, f`z]`(ap[f, A, B, x, y]`p)`(ap[f, A, B, y, z]`q)") -apply (quantify 2) -apply (path_ind "{x, z, q} - ap[f, A, B, x, z]`(pathcomp[A, x, x, z]`(refl x)`q) =[f`x =[B] f`z] - pathcomp[B, f`x, f`x, f`z]`(ap[f, A, B, x, x]`(refl x))`(ap[f, A, B, x, z]`q)") -proof - - show - "\x. x: A \ refl(refl(f`x)) : - ap[f, A, B, 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[f, A, B, x, x]`(refl x))`(ap[f, A, B, x, x]`(refl x))" - by derive -qed routine - - -schematic_goal ap_func_compose: - assumes [intro]: - "A: U i" "B: U i" "C: U i" - "f: A \ B" "g: B \ C" - shows - "?prf: \x: A. \y: A. \p: x =[A] y. - ap[g, B, C, f`x, f`y]`(ap[f, A, B, x, y]`p) =[g`(f`x) =[C] g`(f`y)] - ap[g o[A] f, A, C, x, y]`p" -apply (quantify 3) -apply (path_ind "{x, y, p} - ap[g, B, C, f`x, f`y]`(ap[f, A, B, x, y]`p) =[g`(f`x) =[C] g`(f`y)] - ap[g o[A] f, A, C, x, y]`p") -proof - - show "\x. x: A \ refl(refl (g`(f`x))) : - ap[g, B, C, f`x, f`x]`(ap[f, A, B, x, x]`(refl x)) =[g`(f`x) =[C] g`(f`x)] - ap[g o[A] f, A, C, x, x]`(refl x)" - unfolding compose_def by derive - - fix x y p assume [intro]: "x: A" "y: A" "p: x =[A] y" - show - "ap[g, B, C, f`x, f`y]`(ap[f, A, B, x, y]`p) =[g`(f`x) =[C] g`(f`y)] - ap[g o[A] f, A, C, x, y]`p: U i" - proof - have - "ap[g o[A] f, A, C, x, y]`p: (\x: A. g`(f`x))`x =[C] (\x: A. g`(f`x))`y" - unfolding compose_def by derive - moreover have - "(\x: A. g`(f`x))`x =[C] (\x: A. g`(f`x))`y \ g`(f`x) =[C] g`(f`y)" by derive - ultimately show - "ap[g o[A] f, A, C, x, y]`p: g`(f`x) =[C] g`(f`y)" by simp - qed derive -qed routine - -schematic_goal ap_func_inv: - assumes [intro]: - "A: U i" "B: U i" "f: A \ B" - "x: A" "y: A" "p: x =[A] y" - shows "?prf: - ap[f, A, B, y, x]`(inv[A, x, y]`p) =[f`y =[B] f`x] inv[B, f`x, f`y]`(ap[f, A, B, x, y]`p)" -proof (path_ind' x y p) - show "\x. x: A \ refl(refl(f`x)): - ap[f, A, B, x, x]`(inv[A, x, x]`(refl x)) =[f`x =[B] f`x] - inv[B, f`x, f`x]`(ap[f, A, B, x, x]`(refl x))" - by derive -qed routine - -schematic_goal ap_func_id: - assumes [intro]: "A: U i" "x: A" "y: A" "p: x =[A] y" - shows "?prf: ap[id A, A, A, x, y]`p =[x =[A] y] p" -proof (path_ind' x y p) - fix x assume [intro]: "x: A" - show "refl(refl x): ap[id A, A, A, x, x]`(refl x) =[x =[A] x] refl x" by derive - - fix y p assume [intro]: "y: A" "p: x =[A] y" - have "ap[id A, A, A, x, y]`p: (id A)`x =[A] (id A)`y" by derive - moreover have "(id A)`x =[A] (id A)`y \ x =[A] y" by derive - ultimately have [intro]: "ap[id A, A, A, x, y]`p: x =[A] y" by simp - - show "ap[id A, A, A, x, y]`p =[x =[A] y] p: U i" by derive -qed - - -end -- cgit v1.2.3