diff options
| -rw-r--r-- | hott/Equivalence.thy | 21 | ||||
| -rw-r--r-- | hott/Identity.thy | 40 | ||||
| -rw-r--r-- | spartan/core/Spartan.thy | 3 | ||||
| -rw-r--r-- | spartan/core/context_tactical.ML | 2 |
4 files changed, 63 insertions, 3 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index a4eea93..d85e6de 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -144,6 +144,8 @@ Lemma (def) commute_homotopy: apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp) by refl +\<comment> \<open>TODO: *Really* need normalization during type-checking and better equality + type rewriting to do the proof below properly\<close> Corollary (def) commute_homotopy': assumes "A: U i" @@ -151,7 +153,24 @@ Corollary (def) commute_homotopy': "f: A \<rightarrow> A" "H: f ~ (id A)" shows "H (f x) = f [H x]" -oops + proof - + from \<open>H: f ~ id A\<close> have "H: \<Prod>x: A. f x = x" + by (reduce add: homotopy_def) + + have "(id A)[H x]: f x = x" + by (rewrite at "\<hole> = _" id_comp[symmetric], + rewrite at "_ = \<hole>" id_comp[symmetric]) + + have "H (f x) \<bullet> H x = H (f x) \<bullet> (id A)[H x]" + by (rule left_whisker) (fact, rule + ap_id[where ?A=A and ?x="f x" and ?y=x, simplified id_comp, symmetric]) + also have [simplified id_comp]: "H (f x) \<bullet> (id A)[H x] = f[H x] \<bullet> H x" + by (rule commute_homotopy) + finally have *: "{}" by this + + show "H (f x) = f [H x]" + by pathcomp_cancelr (fact, typechk+) + qed section \<open>Quasi-inverse and bi-invertibility\<close> diff --git a/hott/Identity.thy b/hott/Identity.thy index b06604f..4829b6f 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -292,6 +292,46 @@ Lemma apply_transport: method transport uses eq = (rule apply_transport[OF _ _ _ _ eq]) +Lemma (def) pathcomp_cancel_left: + assumes + "A: U i" "x: A" "y: A" "z: A" + "p: x = y" "q: y = z" "r: y = z" + "\<alpha>: p \<bullet> q = p \<bullet> r" + shows "q = r" + proof - + have "q = (p\<inverse> \<bullet> p) \<bullet> q" + by (transport eq: inv_pathcomp, transport eq: refl_pathcomp) refl + also have ".. = p\<inverse> \<bullet> (p \<bullet> r)" + by (transport eq: pathcomp_assoc[symmetric], transport eq: \<open>\<alpha>:_\<close>) refl + also have ".. = r" thm inv_pathcomp + by (transport eq: pathcomp_assoc, + transport eq: inv_pathcomp, + transport eq: refl_pathcomp) refl + finally show "{}" by this + qed + +Lemma (def) pathcomp_cancel_right: + assumes + "A: U i" "x: A" "y: A" "z: A" + "p: x = y" "q: x = y" "r: y = z" + "\<alpha>: p \<bullet> r = q \<bullet> r" + shows "p = q" + proof - + have "p = p \<bullet> r \<bullet> r\<inverse>" + by (transport eq: pathcomp_assoc[symmetric], + transport eq: pathcomp_inv, + transport eq: pathcomp_refl) refl + also have ".. = q" + by (transport eq: \<open>\<alpha>:_\<close>, + transport eq: pathcomp_assoc[symmetric], + transport eq: pathcomp_inv, + transport eq: pathcomp_refl) refl + finally show "{}" by this + qed + +method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7] +method pathcomp_cancelr = rule pathcomp_cancel_right[rotated 7] + Lemma (def) transport_left_inv: assumes "A: U i" diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy index ea72208..7f13036 100644 --- a/spartan/core/Spartan.thy +++ b/spartan/core/Spartan.thy @@ -248,7 +248,8 @@ method_setup intros = K (CONTEXT_METHOD (fn facts => case n_opt of SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)) - | NONE => CREPEAT (CCHANGED (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))))))\<close> + | NONE => CCHANGED (CREPEAT (CCHANGED ( + CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)))))))\<close> method_setup elim = \<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD ( diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML index 0aa6f20..d0fed61 100644 --- a/spartan/core/context_tactical.ML +++ b/spartan/core/context_tactical.ML @@ -92,7 +92,7 @@ fun CREPEAT ctac = fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac -fun CREPEAT_N 0 _ = all_ctac +fun CREPEAT_N 0 _ = no_ctac | CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac fun CFILTER pred ctac cst = |