From b01b8ee0f3472cb728f09463d0620ac8b8066bcb Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 27 Mar 2019 14:41:16 +0100 Subject: More progress. I think we are reaching the limit of what can be conveniently proved with the current implementation. --- Equivalence.thy | 75 ++++++++++++++++++++++++++++++++++++++++----------------- Prod.thy | 32 ++++++++++++++++++++++-- 2 files changed, 83 insertions(+), 24 deletions(-) diff --git a/Equivalence.thy b/Equivalence.thy index b8df15d..07ef0df 100644 --- a/Equivalence.thy +++ b/Equivalence.thy @@ -74,9 +74,7 @@ unfolding happly_def by (derive lems: fun_eq_imp_homotopy) text \Homotopy and function composition:\ -declare[[pretty_compose=false]] - -schematic_goal composition_homotopyl: +schematic_goal composition_homl: assumes [intro]: "H: f ~[x: A. B] g" "f: A \ B" "g: A \ B" "h: B \ C" @@ -84,9 +82,21 @@ schematic_goal composition_homotopyl: shows "?prf: h o[A] f ~[x: A. C] h o[A] g" unfolding homotopy_def compose_def proof (rule Prod_routine, subst (0 1) comp) fix x assume [intro]: "x: A" - show "ap[h, B, C, f`x, g`x]`(H`x): h`(f`x) =[C] h`(g`x)" by (derive, fold homotopy_def, fact+) + show "ap[h, B, C, f`x, g`x]`(H`x): h`(f`x) =[C] h`(g`x)" by (routine, fold homotopy_def, fact+) qed routine +schematic_goal composition_homr: + assumes [intro]: + "H: f ~[x: B. C] g" + "h: A \ B" "f: B \ C" "g: B \ C" + "A: U i" "B: U i" "C: U i" + shows "?prf: f o[A] h ~[x: A. C] g o[A] h" +unfolding homotopy_def compose_def proof (rule Prod_routine, subst (0 1) comp) + fix x assume [intro]: "x: A" + show "H`(h`x): f`(h`x) =[C] g`(h`x)" by (routine, fold homotopy_def, routine) +qed routine + + section \Bi-invertibility\ definition biinv :: "[t, t, t] \ t" ("(2biinv[_, _]/ _)") @@ -109,10 +119,10 @@ declare biinv_type [intro] schematic_goal id_is_biinv: assumes [intro]: "A: U i" shows "?prf: biinv[A, A] (id A)" -unfolding biinv_def proof (rule Sum_routine, compute) +unfolding biinv_def proof (rule Sum_routine) show "x: A. refl x>: \(g: A \ A). (g o[A] id A) ~[x: A. A] (id A)" by derive show "x: A. refl x>: \(g: A \ A). (id A o[A] g) ~[x: A. A] (id A)" by derive -qed routine +qed derive definition equivalence :: "[t, t] \ t" (infix "\" 100) where "A \ B \ \f: A \ B. biinv[A, B] f" @@ -135,22 +145,43 @@ schematic_goal biinv_imp_qinv: assumes [intro]: "A: U i" "B: U i" "f: A \ B" shows "?prf: (biinv[A, B] f) \ (qinv[A,B] f)" proof (rule Prod_routine) -assume "b: biinv[A, B] f" -define g H g' H' where - "g \ fst[B \ A, \g. g o[A] f ~[x: A. A] id A] ` - (fst[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" -and - "H \ snd[B \ A, \g. g o[A] f ~[x: A. A] id A] ` - (fst[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" -and - "g' \ fst[B \ A, \g. f o[B] g ~[x: B. B] id B] ` - (snd[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" -and - "H' \ snd[B \ A, \g. f o[B] g ~[x: B. B] id B] ` - (snd[\g: B \ A. g o[A] f ~[x: A. A] id A, &(\g: B \ A. f o[B] g ~[x: A. A] id B)] ` b)" - -have "g o[B] (f o[B] g') \ g" -unfolding g_def g'_def proof compute + +assume [intro]: "b: biinv[A, B] f" + +text \Components of the witness of biinvertibility of @{term f}:\ + +let ?fst_of_b = + "fst[\g: B \ A. g o[A] f ~[x: A. A] id A, &\g: B \ A. f o[B] g ~[x: B. B] id B]" +and ?snd_of_b = + "snd[\g: B \ A. g o[A] f ~[x: A. A] id A, &\g: B \ A. f o[B] g ~[x: B. B] id B]" + +define g H g' H' where + "g \ fst[B \ A, \g. g o[A] f ~[x: A. A] id A] ` (?fst_of_b ` b)" and + "H \ snd[B \ A, \g. g o[A] f ~[x: A. A] id A] ` (?fst_of_b ` b)" and + "g' \ fst[B \ A, \g. f o[B] g ~[x: B. B] id B] ` (?snd_of_b ` b)" and + "H' \ snd[B \ A, \g. f o[B] g ~[x: B. B] id B] ` (?snd_of_b ` b)" + +have "H: g o[A] f ~[x: A. A] id A" +unfolding H_def g_def proof standard+ + have + "fst[\(g: B \ A). g o[A] f ~[x: A. A] id A, &\(g: B \ A). f o[B] g ~[x: B. B] id B] : + (biinv[A, B] f) \ (\(g: B \ A). g o[A] f ~[g: A. A] id A)" unfolding biinv_def by derive + thus + "fst[\(g: B \ A). g o[A] f ~[x: A. A] id A, &\(g: B \ A). f o[B] g ~[x: B. B] id B]`b : + \(g: B \ A). g o[A] f ~[g: A. A] id A" by derive rule +qed derive + +moreover have "(id A) o[B] g' \ g'" proof derive + show "g': B \ A" unfolding g'_def proof + have + "snd[\(g: B \ A). g o[A] f ~[x: A. A] id A, &\(g: B \ A). f o[B] g ~[x: B. B] id B] : + (biinv[A, B] f) \ (\(g: B \ A). f o[B] g ~[x: B. B] id B)" unfolding biinv_def by derive + thus + "snd[\(g: B \ A). g o[A] f ~[x: A. A] id A, &\(g: B \ A). f o[B] g ~[x: B. B] id B]`b : + \(g: B \ A). f o[B] g ~[x: B. B] id B" by derive rule + qed derive +qed + section \Transport, homotopy, and bi-invertibility\ diff --git a/Prod.thy b/Prod.thy index 75db657..a35138c 100644 --- a/Prod.thy +++ b/Prod.thy @@ -119,8 +119,36 @@ unfolding compose_def by (derive lems: assms cong) abbreviation id :: "t \ t" ("(id _)" [115] 114) where "id A \ \x: A. x" -lemma id_type [intro]: "\A. A: U i \ id A: A \ A" by derive - +lemma id_type: "\A. A: U i \ id A: A \ A" by derive + +lemma id_compl: + assumes [intro]: "A: U i" "B: U i" "f: A \ B" + shows "id B o[A] f \ f" +unfolding compose_def proof - + { + fix x assume [intro]: "x: A" + have "(id B)`(f`x) \ f`x" by derive + } + hence "\x: A. (id B)`(f`x) \ \x: A. f`x" by (derive lems: cong) derive + also have "\x: A. f`x \ f" by derive + finally show "\(x: A). (id B)`(f`x) \ f" by simp +qed + +lemma id_compr: + assumes [intro]: "A: U i" "B: U i" "f: A \ B" + shows "f o[A] id A \ f" +unfolding compose_def proof - + { + fix x assume [intro]: "x: A" + have "f`((id A)`x) \ f`x" by derive + } + hence "\x: A. f`((id A)`x) \ \x: A. f`x" by (derive lems: cong) derive + also have "\x: A. f`x \ f" by derive + finally show "\x: A. f`((id A)`x) \ f" by simp +qed + +declare id_type [intro] +lemmas id_comp [comp] = id_compl id_compr section \Universal quantification\ -- cgit v1.2.3