From f602cb54b39b3c1bb4f755db09bdeeb2f31a9559 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 19 Sep 2018 11:55:45 +0200 Subject: proof of associativity of path composition --- EqualProps.thy | 89 ++++++++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 65 insertions(+), 24 deletions(-) (limited to 'EqualProps.thy') diff --git a/EqualProps.thy b/EqualProps.thy index f7a8d91..847d964 100644 --- a/EqualProps.thy +++ b/EqualProps.thy @@ -22,6 +22,10 @@ unfolding inv_def by (elim Equal_elim) routine lemma inv_comp: "\A: U i; a: A\ \ (refl a)\ \ refl a" unfolding inv_def by compute routine +declare + inv_type [intro] + inv_comp [comp] + section \Transitivity of equality/Path composition\ @@ -35,7 +39,7 @@ syntax "_pathcomp" :: "[t, t] \ t" (infixl "\" 120) translations "p \ q" \ "CONST pathcomp`p`q" lemma pathcomp_type: - assumes "A: U i" and "x: A" "y: A" "z: A" + assumes "A: U i" "x: A" "y: A" "z: A" shows "pathcomp: x =\<^sub>A y \ (y =\<^sub>A z) \ (x =\<^sub>A z)" unfolding pathcomp_def by rule (elim Equal_elim, routine add: assms) @@ -63,6 +67,11 @@ unfolding pathcomp_def proof compute by (routine add: assms) qed (routine add: assms) +declare + pathcomp_type [intro] + pathcomp_trans [intro] + pathcomp_comp [comp] + section \Higher groupoid structure of types\ @@ -71,54 +80,86 @@ schematic_goal pathcomp_right_id: shows "?a: p \ (refl y) =[x =\<^sub>A y] p" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) \ \@{method elim} does not seem to work with schematic goals.\ show "\x. x: A \ refl(refl x): (refl x) \ (refl x) =[x =\<^sub>A x] (refl x)" - by (derive lems: assms pathcomp_comp) -qed (routine add: assms pathcomp_type) + by (derive lems: assms) +qed (routine add: assms) schematic_goal pathcomp_left_id: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" shows "?a: (refl x) \ p =[x =\<^sub>A y] p" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) show "\x. x: A \ refl(refl x): (refl x) \ (refl x) =[x =\<^sub>A x] (refl x)" - by (derive lems: assms pathcomp_comp) -qed (routine add: assms pathcomp_type) + by (derive lems: assms) +qed (routine add: assms) schematic_goal pathcomp_left_inv: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" shows "?a: (p\ \ p) =[y =\<^sub>A y] refl(y)" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) show "\x. x: A \ refl(refl x): (refl x)\ \ (refl x) =[x =\<^sub>A x] (refl x)" - by (derive lems: assms inv_comp pathcomp_comp) -qed (routine add: assms inv_type pathcomp_type) + by (derive lems: assms) +qed (routine add: assms) schematic_goal pathcomp_right_inv: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" shows "?a: (p \ p\) =[x =\<^sub>A x] refl(x)" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) show "\x. x: A \ refl(refl x): (refl x) \ (refl x)\ =[x =\<^sub>A x] (refl x)" - by (derive lems: assms inv_comp pathcomp_comp) -qed (routine add: assms inv_type pathcomp_type) + by (derive lems: assms) +qed (routine add: assms) schematic_goal inv_involutive: assumes "A: U(i)" "x: A" "y: A" "p: x =\<^sub>A y" shows "?a: p\\ =[x =\<^sub>A y] p" proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) show "\x. x: A \ refl(refl x): (refl x)\\ =[x =\<^sub>A x] (refl x)" - by (derive lems: assms inv_comp) -qed (routine add: assms inv_type) - -schematic_goal pathcomp_assoc: - assumes - "A: U(i)" - "x: A" "y: A" "z: A" "w: A" - "p: x =\<^sub>A y" "q: y =\<^sub>A z" "r: z =\<^sub>A w" - shows - "?a: p \ (q \ r) =[x =\<^sub>A w] (p \ q) \ r" -proof (rule Equal_elim[where ?x=x and ?y=y and ?p=p]) - fix x assume "x: A" - show "refl (q \ r): (refl x) \ (q \ r) =[x =\<^sub>A w] ((refl x) \ q) \ r" - \ \This requires substitution of *propositional* equality. \ - oops + by (derive lems: assms) +qed (routine add: assms) +text \All of the propositions above have the same proof term, which we abbreviate here.\ +abbreviation \ :: "t \ t" where "\ p \ ind\<^sub>= (\x. refl (refl x)) p" + +text \The next proof has a triply-nested path induction.\ + +lemma pathcomp_assoc: + assumes "A: U i" "x: A" "y: A" "z: A" "w: A" + shows "\<^bold>\p. ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\_. \<^bold>\r. \ r) q) p: + \p: x =\<^sub>A y. \q: y =\<^sub>A z. \r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] (p \ q) \ r" +proof + show "\p. p: x =\<^sub>A y \ ind\<^sub>= (\_. \<^bold>\q. ind\<^sub>= (\_. \<^bold>\r. \ r) q) p: + \q: y =\<^sub>A z. \r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] p \ q \ r" + proof (elim Equal_elim) + fix x assume 1: "x: A" + show "\<^bold>\q. ind\<^sub>= (\_. \<^bold>\r. \ r) q: + \q: x =\<^sub>A z. \r: z =\<^sub>A w. refl x \ (q \ r) =[x =\<^sub>A w] refl x \ q \ r" + proof + show "\q. q: x =\<^sub>A z \ ind\<^sub>= (\_. \<^bold>\r. \ r) q: + \r: z =\<^sub>A w. refl x \ (q \ r) =[x =\<^sub>A w] refl x \ q \ r" + proof (elim Equal_elim) + fix x assume *: "x: A" + show "\<^bold>\r. \ r: \r: x =\<^sub>A w. refl x \ (refl x \ r) =[x =\<^sub>A w] refl x \ refl x \ r" + proof + show "\r. r: x =[A] w \ \ r: refl x \ (refl x \ r) =[x =[A] w] refl x \ refl x \ r" + by (elim Equal_elim, derive lems: * assms) + qed (routine add: * assms) + qed (routine add: 1 assms) + qed (routine add: 1 assms) + + text \ + In the following part @{method derive} fails to obtain the correct subgoals, so we have to prove the statement manually. + \ + fix y p assume 2: "y: A" "p: x =\<^sub>A y" + show "\q: y =\<^sub>A z. \r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] p \ q \ r: U i" + proof (routine add: assms) + fix q assume 3: "q: y =\<^sub>A z" + show "\r: z =\<^sub>A w. p \ (q \ r) =[x =\<^sub>A w] p \ q \ r: U i" + proof (routine add: assms) + show "\r. r: z =[A] w \ p \ (q \ r): x =[A] w" and "\r. r: z =[A] w \ p \ q \ r: x =[A] w" + by (routine add: 1 2 3 assms) + qed (routine add: 1 assms) + qed fact+ + qed fact+ +qed (routine add: assms) + section \Transport\ -- cgit v1.2.3