aboutsummaryrefslogtreecommitdiff
path: root/Eq.thy
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Eq.thy141
1 files 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 \<open>Path induction\<close>
text \<open>We set up rudimentary automation of path induction:\<close>
-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] \<Rightarrow> t" =
+method path_ind for C :: "[t, t, t] \<Rightarrow> 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] \<Rightarrow> [t, t, t] \<Rightarrow> t" ("(2{_, _, _}/ _)" 0)
-translations "{x, y, p} C" \<rightleftharpoons> "\<lambda>x y p. C"
+translations "{x, y, p} C" \<rightharpoonup> "\<lambda>x y p. C"
section \<open>Properties of equality\<close>
@@ -95,15 +95,19 @@ subsection \<open>Transitivity (path composition)\<close>
schematic_goal transitivity:
assumes "A: U i" "x: A" "y: A" "p: x =[A] y"
- shows "?p: \<Prod>z: A. y =[A]z \<rightarrow> x =[A] z"
-proof (path_ind x y p, quantify_all)
- fix x z show "\<And>p. p: x =[A] z \<Longrightarrow> p: x =[A] z" .
-qed (routine add: assms)
+ shows "?p: \<Prod>z: A. y =[A] z \<rightarrow> 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] \<Rightarrow> t"
where
- "pathcomp A x y z p q \<equiv>
- (indEq (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z) (\<lambda>x. \<lambda>y: A. id (x =[A] y)) x y p)`z`q"
+ "pathcomp A x y z p q \<equiv> (indEq
+ (\<lambda>x y _. \<Prod>z: A. y =[A] z \<rightarrow> x =[A] z)
+ (\<lambda>x. \<lambda>(z: A). \<lambda>(q: x =[A] z). indEq (\<lambda>x z _. x =[A] z) (\<lambda>x. refl x) x z q)
+ x y p)`z`q"
+
syntax "_pathcomp" :: "[t, t] \<Rightarrow> 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) \<equiv> 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 \<open>Higher groupoid structure of types\<close>
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 "\<And>x. x: A \<Longrightarrow> 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 "\<And>x. x: A \<Longrightarrow> 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
"\<And>x. x: A \<Longrightarrow> 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
"\<And>x. x: A \<Longrightarrow> 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 "\<And>x. x: A \<Longrightarrow> 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.
\<close>
+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}
- \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(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}
- \<Prod>(w: A). \<Prod>(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}
+ \<Prod>(z: A). \<Prod>(q: y =[A] z). \<Prod>(w: A). \<Prod>(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}
+ \<Prod>(w: A). \<Prod>(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 \<open>The rest is now routine.\<close>
-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
+ "\<And>x. x: A \<Longrightarrow> 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 \<open>Functoriality of functions on types\<close>
+
+schematic_goal transfer:
+ assumes
+ "A: U i" "B: U i" "f: A \<rightarrow> 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] \<Rightarrow> t"
+where "ap B f x y p \<equiv> indEq ({x, y, _} f`x =[B] f`y) (\<lambda>x. refl (f`x)) x y p"
+
+lemma ap_type:
+ assumes
+ "A: U i" "B: U i" "f: A \<rightarrow> 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 \<rightarrow> B" "x: A"
+ shows "ap B f x x (refl x) \<equiv> 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 \<rightarrow> B"
+ shows
+ "?a: \<Prod>x: A. \<Prod>y: A. \<Prod>p: x =[A] y. \<Prod>z: A. \<Prod>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}
+ \<Prod>z: A. \<Prod>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
+ "\<And>x. x: A \<Longrightarrow> 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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-20 08:12:32 +0000