From 4fd7d22b0efb69bc13c43dae4e4c1bd6d392f37d Mon Sep 17 00:00:00 2001 From: stuebinm Date: Wed, 29 Jun 2022 01:28:53 +0200 Subject: (broken) update hott for Isabelle 2021-1 this just replaces all instance of `this` with instances of `infer`. Unfortunately, it looks likes something else also broke, and I have no idea what it is (but the proof for equiv_if_equal fails). Sadly this means we can't get to univalence for now … (but rn I'm too tired to try anything else with it) --- hott/Equivalence.thy | 12 ++++++------ hott/Identity.thy | 23 ++++++++++++----------- hott/Nat.thy | 12 ++++++------ 3 files changed, 24 insertions(+), 23 deletions(-) (limited to 'hott') diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index 8007b89..c888714 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -160,7 +160,7 @@ Corollary (def) commute_homotopy': by (rule left_whisker, rewr eq: ap_id, refl) also have [simplified id_comp]: "H (f x) \ (id A)[H x] = f[H x] \ H x" by (rule commute_homotopy) - finally have "?" by this + finally have "?" by infer thus "H (f x) = f [H x]" by pathcomp_cancelr (fact, typechk+) qed @@ -240,7 +240,7 @@ Lemma (def) funcomp_is_qinv: have "(finv \ ginv) \ g \ f ~ finv \ (ginv \ g) \ f" by compute refl also have ".. ~ finv \ id B \ f" by (rhtpy, lhtpy) fact also have ".. ~ id A" by compute fact - finally show "?" by this + finally show "?" by infer qed show "(g \ f) \ finv \ ginv ~ id C" @@ -248,7 +248,7 @@ Lemma (def) funcomp_is_qinv: have "(g \ f) \ finv \ ginv ~ g \ (f \ finv) \ ginv" by compute refl also have ".. ~ g \ id B \ ginv" by (rhtpy, lhtpy) fact also have ".. ~ id C" by compute fact - finally show "?" by this + finally show "?" by infer qed qed done @@ -313,10 +313,10 @@ Lemma (def) is_qinv_if_is_biinv: also have ".. ~ g \ f \ h" by rhtpy (rule \H2:_\[symmetric]) also have ".. ~ (id A) \ h" by (comp funcomp_assoc[symmetric]) (lhtpy, fact) also have ".. ~ h" by compute refl - finally have "g ~ h" by this - then have "f \ g ~ f \ h" by (rhtpy, this) + finally have "g ~ h" by infer + then have "f \ g ~ f \ h" by (rhtpy, infer) also note \H2:_\ - finally show "f \ g ~ id B" by this + finally show "f \ g ~ id B" by infer qed done done diff --git a/hott/Identity.thy b/hott/Identity.thy index ce0e0ec..6c044b4 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -203,6 +203,7 @@ Lemma (def) ap: shows "f x = f y" by (eq p) intro + definition ap_i ("_[_]" [1000, 0]) where [implicit]: "ap_i f p \ ap {} {} {} {} f p" @@ -304,7 +305,7 @@ Lemma (def) pathcomp_cancel_left: by (rewr eq: pathcomp_assoc, rewr eq: inv_pathcomp, rewr eq: refl_pathcomp) refl - finally show "?" by this + finally show "?" by infer qed Lemma (def) pathcomp_cancel_right: @@ -323,7 +324,7 @@ Lemma (def) pathcomp_cancel_right: rewr eq: pathcomp_assoc[symmetric], rewr eq: pathcomp_inv, rewr eq: pathcomp_refl) refl - finally show "?" by this + finally show "?" by infer qed method pathcomp_cancell = rule pathcomp_cancel_left[rotated 7] @@ -488,7 +489,7 @@ Lemma (def) right_whisker: have "s \ refl x = s" by (rule pathcomp_refl) also have ".. = t" by fact also have ".. = t \ refl x" by (rule pathcomp_refl[symmetric]) - finally show "?" by this + finally show "?" by infer qed done @@ -502,7 +503,7 @@ Lemma (def) left_whisker: have "refl x \ s = s" by (rule refl_pathcomp) also have ".. = t" by fact also have ".. = refl x \ t" by (rule refl_pathcomp[symmetric]) - finally show "?" by this + finally show "?" by infer qed done @@ -608,17 +609,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp: have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "? = \" by this + finally have eq\: "? = \" by infer have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "? = \" by this + finally have eq\: "? = \" by infer have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) - finally show "? = \ \ \" by this + finally show "? = \ \ \" by infer qed Lemma (def) pathcomp_eq_horiz_pathcomp': @@ -630,17 +631,17 @@ Lemma (def) pathcomp_eq_horiz_pathcomp': have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "? = \" by this + finally have eq\: "? = \" by infer have "refl (refl a) \ \ \ refl (refl a) = refl (refl a) \ \" by (rule pathcomp_refl) also have ".. = \" by (rule refl_pathcomp) - finally have eq\: "? = \" by this + finally have eq\: "? = \" by infer have "refl (refl a) \ \ \ refl (refl a) \ (refl (refl a) \ \ \ refl (refl a)) = \ \ ?" by right_whisker (fact eq\) also have ".. = \ \ \" by left_whisker (fact eq\) - finally show "? = \ \ \" by this + finally show "? = \ \ \" by infer qed Lemma (def) eckmann_hilton: @@ -657,7 +658,7 @@ Lemma (def) eckmann_hilton: also have ".. = \ \ \" by (rule pathcomp_eq_horiz_pathcomp') finally show "\ \ \ = \ \ \" - by this + by infer qed end diff --git a/hott/Nat.thy b/hott/Nat.thy index 33a5d0a..0a38f99 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -115,7 +115,7 @@ Lemma (def) add_comm: proof compute have "suc (m + n) = suc (n + m)" by (eq ih) refl also have ".. = suc n + m" by (rewr eq: suc_add) refl - finally show "?" by this + finally show "?" by infer qed done @@ -152,7 +152,7 @@ Lemma (def) zero_mul: proof compute have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by compute refl - finally show "?" by this + finally show "?" by infer qed done @@ -165,7 +165,7 @@ Lemma (def) suc_mul: proof (compute, rewr eq: \ih:_\) have "suc m + (m * n + n) = suc (m + ?)" by (rule suc_add) also have ".. = suc (m + m * n + n)" by (rewr eq: add_assoc) refl - finally show "?" by this + finally show "?" by infer qed done @@ -180,7 +180,7 @@ Lemma (def) mul_dist_add: also have ".. = l + l * m + l * n" by (rule add_assoc) also have ".. = l * m + l + l * n" by (rewr eq: add_comm) refl also have ".. = l * m + (l + l * n)" by (rewr eq: add_assoc) refl - finally show "?" by this + finally show "?" by infer qed done @@ -193,7 +193,7 @@ Lemma (def) mul_assoc: proof compute have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add) also have ".. = l * m + l * m * n" by (rewr eq: \ih:_\) refl - finally show "?" by this + finally show "?" by infer qed done @@ -207,7 +207,7 @@ Lemma (def) mul_comm: have "suc n * m = n * m + m" by (rule suc_mul) also have ".. = m + m * n" by (rewr eq: \ih:_\, rewr eq: add_comm) refl - finally show "?" by this + finally show "?" by infer qed done -- cgit v1.2.3