diff options
Diffstat (limited to 'hott')
| -rw-r--r-- | hott/Equivalence.thy | 456 | ||||
| -rw-r--r-- | hott/Identity.thy | 239 | ||||
| -rw-r--r-- | hott/List+.thy (renamed from hott/More_List.thy) | 6 | ||||
| -rw-r--r-- | hott/More_Nat.thy | 43 | ||||
| -rw-r--r-- | hott/Nat.thy | 58 |
5 files changed, 400 insertions, 402 deletions
diff --git a/hott/Equivalence.thy b/hott/Equivalence.thy index d844b59..66c64f6 100644 --- a/hott/Equivalence.thy +++ b/hott/Equivalence.thy @@ -16,53 +16,68 @@ Lemma homotopy_type [typechk]: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" - "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" + "f: \<Prod>x: A. B x" + "g: \<Prod>x: A. B x" shows "f ~ g: U i" - unfolding homotopy_def by typechk + unfolding homotopy_def + by typechk -Lemma (derive) homotopy_refl [refl]: +Lemma apply_homotopy: + assumes + "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" + "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" + "H: f ~ g" + "x: A" + shows "H x: f x = g x" + using \<open>H:_\<close> unfolding homotopy_def + by typechk + +method htpy for H::o = rule apply_homotopy[where ?H=H] + +Lemma (def) homotopy_refl [refl]: assumes "A: U i" "f: \<Prod>x: A. B x" shows "f ~ f" - unfolding homotopy_def by intros + unfolding homotopy_def + by intros -Lemma (derive) hsym: +Lemma (def) hsym: assumes - "f: \<Prod>x: A. B x" - "g: \<Prod>x: A. B x" "A: U i" "\<And>x. x: A \<Longrightarrow> B x: U i" + "f: \<Prod>x: A. B x" + "g: \<Prod>x: A. B x" "H: f ~ g" shows "g ~ f" -unfolding homotopy_def -proof intro - fix x assume "x: A" then have "H x: f x = g x" - using \<open>H:_\<close>[unfolded homotopy_def] - \<comment> \<open>this should become unnecessary when definitional unfolding is implemented\<close> - by typechk - thus "g x = f x" by (rule pathinv) fact -qed typechk - -Lemma (derive) htrans: + unfolding homotopy_def + proof intro + fix x assume "x: A" then have "f x = g x" + by (htpy H) + thus "g x = f x" + by (rule pathinv) fact + qed + +Lemma (def) htrans: assumes + "A: U i" + "\<And>x. x: A \<Longrightarrow> B x: U i" "f: \<Prod>x: A. B x" "g: \<Prod>x: A. B x" "h: \<Prod>x: A. B x" - "A: U i" - "\<And>x. x: A \<Longrightarrow> B x: U i" - shows "\<lbrakk>H1: f ~ g; H2: g ~ h\<rbrakk> \<Longrightarrow> f ~ h" + "H1: f ~ g" + "H2: g ~ h" + shows "f ~ h" unfolding homotopy_def - apply intro - \<guillemotright> vars x - apply (rule pathcomp[where ?y="g x"]) - \<^item> by (elim H1) - \<^item> by (elim H2) - done - \<guillemotright> by typechk - done + proof intro + fix x assume "x: A" + have *: "f x = g x" "g x = h x" + by (htpy H1, htpy H2) + show "f x = h x" + by (rule pathcomp; (rule *)?) typechk + qed -text \<open>For calculations:\<close> +section \<open>Rewriting homotopies\<close> congruence "f ~ g" rhs g @@ -70,229 +85,258 @@ lemmas homotopy_sym [sym] = hsym[rotated 4] and homotopy_trans [trans] = htrans[rotated 5] -Lemma (derive) commute_homotopy: - assumes - "A: U i" "B: U i" - "x: A" "y: A" - "p: x = y" - "f: A \<rightarrow> B" "g: A \<rightarrow> B" - "H: f ~ g" - shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)" - \<comment> \<open>Need this assumption unfolded for typechecking\<close> - supply assms(8)[unfolded homotopy_def] - apply (eq p) - focus vars x - apply reduce - \<comment> \<open>Here it would really be nice to have automation for transport and - propositional equality.\<close> - apply (rule use_transport[where ?y="H x \<bullet> refl (g x)"]) - \<guillemotright> by (rule pathcomp_refl) - \<guillemotright> by (rule pathinv) (rule refl_pathcomp) - \<guillemotright> by typechk - done - done - -Corollary (derive) commute_homotopy': - assumes - "A: U i" - "x: A" - "f: A \<rightarrow> A" - "H: f ~ (id A)" - shows "H (f x) = f [H x]" -oops - -Lemma homotopy_id_left [typechk]: +Lemma id_funcomp_htpy: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" shows "homotopy_refl A f: (id B) \<circ> f ~ f" - unfolding homotopy_refl_def homotopy_def by reduce + by reduce -Lemma homotopy_id_right [typechk]: +Lemma funcomp_id_htpy: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" shows "homotopy_refl A f: f \<circ> (id A) ~ f" - unfolding homotopy_refl_def homotopy_def - by reduce + by reduce -Lemma homotopy_funcomp_left: +Lemma funcomp_left_htpy: assumes - "H: homotopy B C g g'" + "A: U i" "B: U i" + "\<And>x. x: B \<Longrightarrow> C x: U i" "f: A \<rightarrow> B" "g: \<Prod>x: B. C x" "g': \<Prod>x: B. C x" - "A: U i" "B: U i" - "\<And>x. x: B \<Longrightarrow> C x: U i" - shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g' \<circ>\<^bsub>A\<^esub> f)" + "H: g ~ g'" + shows "(g \<circ> f) ~ (g' \<circ> f)" unfolding homotopy_def - apply (intro; reduce) - apply (insert \<open>H: _\<close>[unfolded homotopy_def]) - apply (elim H) + apply (intro, reduce) + apply (htpy H) done -Lemma homotopy_funcomp_right: +Lemma funcomp_right_htpy: assumes - "H: homotopy A (fn _. B) f f'" + "A: U i" "B: U i" "C: U i" "f: A \<rightarrow> B" "f': A \<rightarrow> B" "g: B \<rightarrow> C" - "A: U i" "B: U i" "C: U i" - shows "homotopy A {} (g \<circ>\<^bsub>A\<^esub> f) (g \<circ>\<^bsub>A\<^esub> f')" + "H: f ~ f'" + shows "(g \<circ> f) ~ (g \<circ> f')" unfolding homotopy_def - apply (intro; reduce) - apply (insert \<open>H: _\<close>[unfolded homotopy_def]) - apply (dest PiE, assumption) - apply (rule ap, assumption) - done + proof (intro, reduce) + fix x assume "x: A" + have *: "f x = f' x" + by (htpy H) + show "g (f x) = g (f' x)" + by (transport eq: *) refl + qed -method id_htpy = (rule homotopy_id_left) -method htpy_id = (rule homotopy_id_right) -method htpy_o = (rule homotopy_funcomp_left) -method o_htpy = (rule homotopy_funcomp_right) +method lhtpy = rule funcomp_left_htpy[rotated 6] +method rhtpy = rule funcomp_right_htpy[rotated 6] + + +Lemma (def) commute_homotopy: + assumes + "A: U i" "B: U i" + "x: A" "y: A" + "p: x = y" + "f: A \<rightarrow> B" "g: A \<rightarrow> B" + "H: f ~ g" + shows "(H x) \<bullet> g[p] = f[p] \<bullet> (H y)" + using \<open>H:_\<close> + unfolding homotopy_def + apply (eq p, reduce) + apply (transport eq: pathcomp_refl, transport eq: refl_pathcomp) + by refl + +Corollary (def) commute_homotopy': + assumes + "A: U i" + "x: A" + "f: A \<rightarrow> A" + "H: f ~ (id A)" + shows "H (f x) = f [H x]" +oops section \<open>Quasi-inverse and bi-invertibility\<close> subsection \<open>Quasi-inverses\<close> -definition "qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A. +definition "is_qinv A B f \<equiv> \<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A) \<times> homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B)" -lemma qinv_type [typechk]: +lemma is_qinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" - shows "qinv A B f: U i" - unfolding qinv_def by typechk + shows "is_qinv A B f: U i" + unfolding is_qinv_def + by typechk -definition qinv_i ("qinv") - where [implicit]: "qinv f \<equiv> Equivalence.qinv ? ? f" +definition is_qinv_i ("is'_qinv") + where [implicit]: "is_qinv f \<equiv> Equivalence.is_qinv ? ? f" -translations "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f" +no_translations "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f" -Lemma (derive) id_qinv: +Lemma (def) id_is_qinv: assumes "A: U i" - shows "qinv (id A)" - unfolding qinv_def + shows "is_qinv (id A)" + unfolding is_qinv_def proof intro show "id A: A \<rightarrow> A" by typechk qed (reduce, intro; refl) -Lemma (derive) quasiinv_qinv: - assumes "A: U i" "B: U i" "f: A \<rightarrow> B" - shows "prf: qinv f \<Longrightarrow> qinv (fst prf)" - unfolding qinv_def - apply intro - \<guillemotright> by (rule \<open>f:_\<close>) - \<guillemotright> apply (elim "prf") - focus vars g HH - apply intro - \<^item> by reduce (snd HH) - \<^item> by reduce (fst HH) - done - done +Lemma is_qinvI: + assumes + "A: U i" "B: U i" "f: A \<rightarrow> B" + "g: B \<rightarrow> A" + "H1: g \<circ> f ~ id A" + "H2: f \<circ> g ~ id B" + shows "is_qinv f" + unfolding is_qinv_def + proof intro + show "g: B \<rightarrow> A" by fact + show "g \<circ> f ~ id A \<and> f \<circ> g ~ id B" by (intro; fact) + qed + +Lemma is_qinv_components [typechk]: + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f" + shows + fst_of_is_qinv: "fst pf: B \<rightarrow> A" and + p\<^sub>2\<^sub>1_of_is_qinv: "p\<^sub>2\<^sub>1 pf: fst pf \<circ> f ~ id A" and + p\<^sub>2\<^sub>2_of_is_qinv: "p\<^sub>2\<^sub>2 pf: f \<circ> fst pf ~ id B" + using assms unfolding is_qinv_def + by typechk+ + +Lemma (def) qinv_is_qinv: + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_qinv f" + shows "is_qinv (fst pf)" +using [[debug_typechk]] + using [[solve_side_conds=2]] + apply (rule is_qinvI) + back \<comment> \<open>Typechecking/inference goes too far here. Problem would likely be + solved with definitional unfolding\<close> + \<^item> by (fact \<open>f:_\<close>) + \<^item> by (rule p\<^sub>2\<^sub>2_of_is_qinv) + \<^item> by (rule p\<^sub>2\<^sub>1_of_is_qinv) done -Lemma (derive) funcomp_qinv: +Lemma (def) funcomp_is_qinv: assumes "A: U i" "B: U i" "C: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" - shows "qinv f \<rightarrow> qinv g \<rightarrow> qinv (g \<circ> f)" - apply (intros, unfold qinv_def, elims) - focus prems vars _ _ finv _ ginv - apply (intro, rule funcompI[where ?f=ginv and ?g=finv]) - proof (reduce, intro) - have "finv \<circ> ginv \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl - also have ".. ~ finv \<circ> id B \<circ> f" by (o_htpy, htpy_o) fact - also have ".. ~ id A" by reduce fact - finally show "finv \<circ> ginv \<circ> g \<circ> f ~ id A" by this - - have "g \<circ> f \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl - also have ".. ~ g \<circ> id B \<circ> ginv" by (o_htpy, htpy_o) fact - also have ".. ~ id C" by reduce fact - finally show "g \<circ> f \<circ> finv \<circ> ginv ~ id C" by this - qed + shows "is_qinv f \<rightarrow> is_qinv g \<rightarrow> is_qinv (g \<circ> f)" + apply intros + unfolding is_qinv_def apply elims + focus vars _ _ finv _ ginv + apply intro + \<^item> by (rule funcompI[where ?f=ginv and ?g=finv]) + \<^item> proof intro + show "(finv \<circ> ginv) \<circ> g \<circ> f ~ id A" + proof - + have "(finv \<circ> ginv) \<circ> g \<circ> f ~ finv \<circ> (ginv \<circ> g) \<circ> f" by reduce refl + also have ".. ~ finv \<circ> id B \<circ> f" by (rhtpy, lhtpy) fact + also have ".. ~ id A" by reduce fact + finally show "{}" by this + qed + + show "(g \<circ> f) \<circ> finv \<circ> ginv ~ id C" + proof - + have "(g \<circ> f) \<circ> finv \<circ> ginv ~ g \<circ> (f \<circ> finv) \<circ> ginv" by reduce refl + also have ".. ~ g \<circ> id B \<circ> ginv" by (rhtpy, lhtpy) fact + also have ".. ~ id C" by reduce fact + finally show "{}" by this + qed + qed + done done subsection \<open>Bi-invertible maps\<close> -definition "biinv A B f \<equiv> +definition "is_biinv A B f \<equiv> (\<Sum>g: B \<rightarrow> A. homotopy A (fn _. A) (g \<circ>\<^bsub>A\<^esub> f) (id A)) \<times> (\<Sum>g: B \<rightarrow> A. homotopy B (fn _. B) (f \<circ>\<^bsub>B\<^esub> g) (id B))" -lemma biinv_type [typechk]: +lemma is_biinv_type [typechk]: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" - shows "biinv A B f: U i" - unfolding biinv_def by typechk + shows "is_biinv A B f: U i" + unfolding is_biinv_def by typechk -definition biinv_i ("biinv") - where [implicit]: "biinv f \<equiv> Equivalence.biinv ? ? f" +definition is_biinv_i ("is'_biinv") + where [implicit]: "is_biinv f \<equiv> Equivalence.is_biinv ? ? f" -translations "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f" +translations "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f" -Lemma (derive) qinv_imp_biinv: +Lemma is_biinvI: assumes - "A: U i" "B: U i" - "f: A \<rightarrow> B" - shows "?prf: qinv f \<rightarrow> biinv f" - apply intros - unfolding qinv_def biinv_def - by (rule Sig_dist_exp) - -text \<open> - Show that bi-invertible maps are quasi-inverses, as a demonstration of how to - work in this system. -\<close> + "A: U i" "B: U i" "f: A \<rightarrow> B" + "g: B \<rightarrow> A" "h: B \<rightarrow> A" + "H1: g \<circ> f ~ id A" "H2: f \<circ> h ~ id B" + shows "is_biinv f" + unfolding is_biinv_def + proof intro + show "<g, H1>: {}" by typechk + show "<h, H2>: {}" by typechk + qed -Lemma (derive) biinv_imp_qinv: +Lemma is_biinv_components [typechk]: + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "pf: is_biinv f" + shows + p\<^sub>1\<^sub>1_of_is_biinv: "p\<^sub>1\<^sub>1 pf: B \<rightarrow> A" and + p\<^sub>2\<^sub>1_of_is_biinv: "p\<^sub>2\<^sub>1 pf: B \<rightarrow> A" and + p\<^sub>1\<^sub>2_of_is_biinv: "p\<^sub>1\<^sub>2 pf: p\<^sub>1\<^sub>1 pf \<circ> f ~ id A" and + p\<^sub>2\<^sub>2_of_is_biinv: "p\<^sub>2\<^sub>2 pf: f \<circ> p\<^sub>2\<^sub>1 pf ~ id B" + using assms unfolding is_biinv_def + by typechk+ + +Lemma (def) is_qinv_imp_is_biinv: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" - shows "biinv f \<rightarrow> qinv f" + shows "is_qinv f \<rightarrow> is_biinv f" + apply intros + unfolding is_qinv_def is_biinv_def + by (rule distribute_Sig) - text \<open>Split the hypothesis \<^term>\<open>biinv f\<close> into its components:\<close> - apply intro - unfolding biinv_def - apply elims - - text \<open>Name the components:\<close> - focus prems vars _ _ _ g H1 h H2 - thm \<open>g:_\<close> \<open>h:_\<close> \<open>H1:_\<close> \<open>H2:_\<close> - - text \<open> - \<^term>\<open>g\<close> is a quasi-inverse to \<^term>\<open>f\<close>, so the proof will be a triple - \<^term>\<open><g, <?H1, ?H2>>\<close>. - \<close> - unfolding qinv_def +Lemma (def) is_biinv_imp_is_qinv: + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" + shows "is_biinv f \<rightarrow> is_qinv f" apply intro - \<guillemotright> by (fact \<open>g: _\<close>) - \<guillemotright> apply intro - text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close> - apply (fact \<open>H1: _\<close>) + text \<open>Split the hypothesis \<^term>\<open>is_biinv f\<close> into its components and name them.\<close> + unfolding is_biinv_def apply elims + focus vars _ _ _ g H1 h H2 + text \<open>Need to give the required function and homotopies.\<close> + apply (rule is_qinvI) + text \<open>We claim that \<^term>\<open>g\<close> is a quasi-inverse to \<^term>\<open>f\<close>.\<close> + \<^item> by (fact \<open>g: _\<close>) + + text \<open>The first part \<^prop>\<open>?H1: g \<circ> f ~ id A\<close> is given by \<^term>\<open>H1\<close>.\<close> + \<^item> by (fact \<open>H1: _\<close>) + text \<open> It remains to prove \<^prop>\<open>?H2: f \<circ> g ~ id B\<close>. First show that \<open>g ~ h\<close>, then the result follows from @{thm \<open>H2: f \<circ> h ~ id B\<close>}. Here a proof - block is used to calculate "forward". + block is used for calculational reasoning. \<close> - proof - - have "g ~ g \<circ> (id B)" by reduce refl - also have ".. ~ g \<circ> f \<circ> h" by o_htpy (rule \<open>H2:_\<close>[symmetric]) - also have ".. ~ (id A) \<circ> h" by (subst funcomp_assoc[symmetric]) (htpy_o, fact) - also have ".. ~ h" by reduce refl - finally have "g ~ h" by this - then have "f \<circ> g ~ f \<circ> h" by (o_htpy, this) - also note \<open>H2:_\<close> - finally show "f \<circ> g ~ id B" by this - qed + \<^item> proof - + have "g ~ g \<circ> (id B)" by reduce refl + also have ".. ~ g \<circ> f \<circ> h" by rhtpy (rule \<open>H2:_\<close>[symmetric]) + also have ".. ~ (id A) \<circ> h" by (rewrite funcomp_assoc[symmetric]) (lhtpy, fact) + also have ".. ~ h" by reduce refl + finally have "g ~ h" by this + then have "f \<circ> g ~ f \<circ> h" by (rhtpy, this) + also note \<open>H2:_\<close> + finally show "f \<circ> g ~ id B" by this + qed done done -Lemma (derive) id_biinv: - "A: U i \<Longrightarrow> biinv (id A)" - by (rule qinv_imp_biinv) (rule id_qinv) +Lemma (def) id_is_biinv: + "A: U i \<Longrightarrow> is_biinv (id A)" + by (rule is_qinv_imp_is_biinv) (rule id_is_qinv) -Lemma (derive) funcomp_biinv: +Lemma (def) funcomp_is_biinv: assumes "A: U i" "B: U i" "C: U i" "f: A \<rightarrow> B" "g: B \<rightarrow> C" - shows "biinv f \<rightarrow> biinv g \<rightarrow> biinv (g \<circ> f)" + shows "is_biinv f \<rightarrow> is_biinv g \<rightarrow> is_biinv (g \<circ> f)" apply intros - focus vars biinv\<^sub>f biinv\<^sub>g - by (rule qinv_imp_biinv) (rule funcomp_qinv; rule biinv_imp_qinv) + focus vars pf pg + by (rule is_qinv_imp_is_biinv) + (rule funcomp_is_qinv; rule is_biinv_imp_is_qinv, fact) done @@ -304,19 +348,19 @@ text \<open> \<close> definition equivalence (infix "\<simeq>" 110) - where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.biinv A B f" + where "A \<simeq> B \<equiv> \<Sum>f: A \<rightarrow> B. Equivalence.is_biinv A B f" lemma equivalence_type [typechk]: assumes "A: U i" "B: U i" shows "A \<simeq> B: U i" unfolding equivalence_def by typechk -Lemma (derive) equivalence_refl: +Lemma (def) equivalence_refl: assumes "A: U i" shows "A \<simeq> A" unfolding equivalence_def proof intro - show "biinv (id A)" by (rule qinv_imp_biinv) (rule id_qinv) + show "is_biinv (id A)" by (rule is_qinv_imp_is_biinv) (rule id_is_qinv) qed typechk text \<open> @@ -324,32 +368,30 @@ text \<open> univalence?)... \<close> -Lemma (derive) equivalence_symmetric: +Lemma (def) equivalence_symmetric: assumes "A: U i" "B: U i" shows "A \<simeq> B \<rightarrow> B \<simeq> A" apply intros unfolding equivalence_def apply elim - \<guillemotright> vars _ f "prf" - apply (dest (4) biinv_imp_qinv) - apply intro - \<^item> unfolding qinv_def by (rule fst[of "(biinv_imp_qinv A B f) prf"]) - \<^item> by (rule qinv_imp_biinv) (rule quasiinv_qinv) - done + apply (dest (4) is_biinv_imp_is_qinv) + apply intro + \<^item> by (rule fst_of_is_qinv) facts + \<^item> by (rule is_qinv_imp_is_biinv) (rule qinv_is_qinv) done -Lemma (derive) equivalence_transitive: +Lemma (def) equivalence_transitive: assumes "A: U i" "B: U i" "C: U i" shows "A \<simeq> B \<rightarrow> B \<simeq> C \<rightarrow> A \<simeq> C" proof intros fix AB BC assume *: "AB: A \<simeq> B" "BC: B \<simeq> C" then have - "fst AB: A \<rightarrow> B" and 1: "snd AB: biinv (fst AB)" - "fst BC: B \<rightarrow> C" and 2: "snd BC: biinv (fst BC)" + "fst AB: A \<rightarrow> B" and 1: "snd AB: is_biinv (fst AB)" + "fst BC: B \<rightarrow> C" and 2: "snd BC: is_biinv (fst BC)" unfolding equivalence_def by typechk+ then have "fst BC \<circ> fst AB: A \<rightarrow> C" by typechk - moreover have "biinv (fst BC \<circ> fst AB)" - using * unfolding equivalence_def by (rules funcomp_biinv 1 2) + moreover have "is_biinv (fst BC \<circ> fst AB)" + using * unfolding equivalence_def by (rule funcomp_is_biinv 1 2) facts ultimately show "A \<simeq> C" unfolding equivalence_def by intro facts qed @@ -370,14 +412,14 @@ text \<open> (2) we don't yet have universe automation. \<close> -Lemma (derive) id_imp_equiv: +Lemma (def) id_imp_equiv: assumes "A: U i" "B: U i" "p: A =\<^bsub>U i\<^esub> B" shows "<trans (id (U i)) p, ?isequiv>: A \<simeq> B" unfolding equivalence_def apply intros defer - \<guillemotright> apply (eq p) - \<^item> prems vars A B + \<^item> apply (eq p) + \<^enum> vars A B apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric]) using [[solve_side_conds=1]] apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric]) @@ -385,16 +427,16 @@ Lemma (derive) id_imp_equiv: apply (rule lift_universe_codomain, rule Ui_in_USi) apply (typechk, rule Ui_in_USi) done - \<^item> prems vars A + \<^enum> vars A using [[solve_side_conds=1]] apply (subst transport_comp) - \<^enum> by (rule Ui_in_USi) - \<^enum> by reduce (rule in_USi_if_in_Ui) - \<^enum> by reduce (rule id_biinv) + \<circ> by (rule Ui_in_USi) + \<circ> by reduce (rule in_USi_if_in_Ui) + \<circ> by reduce (rule id_is_biinv) done done - \<guillemotright> \<comment> \<open>Similar proof as in the first subgoal above\<close> + \<^item> \<comment> \<open>Similar proof as in the first subgoal above\<close> apply (rewrite at A in "A \<rightarrow> B" id_comp[symmetric]) using [[solve_side_conds=1]] apply (rewrite at B in "_ \<rightarrow> B" id_comp[symmetric]) @@ -419,8 +461,8 @@ no_translations "lift P p u" \<leftharpoondown> "CONST pathlift A P x y p u" "apd f p" \<leftharpoondown> "CONST Identity.apd A P f x y p" "f ~ g" \<leftharpoondown> "CONST homotopy A B f g" - "qinv f" \<leftharpoondown> "CONST Equivalence.qinv A B f" - "biinv f" \<leftharpoondown> "CONST Equivalence.biinv A B f" + "is_qinv f" \<leftharpoondown> "CONST Equivalence.is_qinv A B f" + "is_biinv f" \<leftharpoondown> "CONST Equivalence.is_biinv A B f" *) diff --git a/hott/Identity.thy b/hott/Identity.thy index 728537c..d6efbf8 100644 --- a/hott/Identity.thy +++ b/hott/Identity.thy @@ -42,7 +42,7 @@ axiomatization where lemmas [form] = IdF and [intro, intros] = IdI and - [elim "?p" "?a" "?b"] = IdE and + [elim ?p ?a ?b] = IdE and [comp] = Id_comp and [refl] = IdI @@ -77,34 +77,34 @@ method_setup eq = section \<open>Symmetry and transitivity\<close> -Lemma (derive) pathinv: +Lemma (def) pathinv: assumes "A: U i" "x: A" "y: A" "p: x =\<^bsub>A\<^esub> y" shows "y =\<^bsub>A\<^esub> x" by (eq p) intro lemma pathinv_comp [comp]: - assumes "x: A" "A: U i" + assumes "A: U i" "x: A" shows "pathinv A x x (refl x) \<equiv> refl x" unfolding pathinv_def by reduce -Lemma (derive) pathcomp: +Lemma (def) pathcomp: assumes "A: U i" "x: A" "y: A" "z: A" "p: x =\<^bsub>A\<^esub> y" "q: y =\<^bsub>A\<^esub> z" shows "x =\<^bsub>A\<^esub> z" - apply (eq p) - focus prems vars x p - apply (eq p) - apply intro - done - done + proof (eq p) + fix x q assume "x: A" and "q: x =\<^bsub>A\<^esub> z" + show "x =\<^bsub>A\<^esub> z" by (eq q) refl + qed lemma pathcomp_comp [comp]: - assumes "a: A" "A: U i" + assumes "A: U i" "a: A" shows "pathcomp A a a a (refl a) (refl a) \<equiv> refl a" unfolding pathcomp_def by reduce +method pathcomp for p q :: o = rule pathcomp[where ?p=p and ?q=q] + section \<open>Notation\<close> @@ -134,26 +134,22 @@ lemmas section \<open>Basic propositional equalities\<close> -Lemma (derive) refl_pathcomp: +Lemma (def) refl_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(refl x) \<bullet> p = p" - apply (eq p) - apply (reduce; intro) - done + by (eq p) (reduce, refl) -Lemma (derive) pathcomp_refl: +Lemma (def) pathcomp_refl: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \<bullet> (refl y) = p" - apply (eq p) - apply (reduce; intro) - done + by (eq p) (reduce, refl) -definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p" definition [implicit]: "lu p \<equiv> refl_pathcomp ? ? ? p" +definition [implicit]: "ru p \<equiv> pathcomp_refl ? ? ? p" translations - "CONST ru p" \<leftharpoondown> "CONST pathcomp_refl A x y p" "CONST lu p" \<leftharpoondown> "CONST refl_pathcomp A x y p" + "CONST ru p" \<leftharpoondown> "CONST pathcomp_refl A x y p" Lemma lu_refl [comp]: assumes "A: U i" "x: A" @@ -165,40 +161,40 @@ Lemma ru_refl [comp]: shows "ru (refl x) \<equiv> refl (refl x)" unfolding pathcomp_refl_def by reduce -Lemma (derive) inv_pathcomp: +Lemma (def) inv_pathcomp: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\<inverse> \<bullet> p = refl y" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) pathcomp_inv: +Lemma (def) pathcomp_inv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p \<bullet> p\<inverse> = refl x" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) pathinv_pathinv: +Lemma (def) pathinv_pathinv: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "p\<inverse>\<inverse> = p" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) pathcomp_assoc: +Lemma (def) pathcomp_assoc: assumes "A: U i" "x: A" "y: A" "z: A" "w: A" "p: x = y" "q: y = z" "r: z = w" shows "p \<bullet> (q \<bullet> r) = p \<bullet> q \<bullet> r" - apply (eq p) - focus prems vars x p - apply (eq p) - focus prems vars x p - apply (eq p) - apply (reduce; intro) - done - done - done + proof (eq p) + fix x q assuming "x: A" "q: x = z" + show "refl x \<bullet> (q \<bullet> r) = refl x \<bullet> q \<bullet> r" + proof (eq q) + fix x r assuming "x: A" "r: x = w" + show "refl x \<bullet> (refl x \<bullet> r) = refl x \<bullet> refl x \<bullet> r" + by (eq r) (reduce, refl) + qed + qed section \<open>Functoriality of functions\<close> -Lemma (derive) ap: +Lemma (def) ap: assumes "A: U i" "B: U i" "x: A" "y: A" @@ -213,11 +209,11 @@ definition ap_i ("_[_]" [1000, 0]) translations "f[p]" \<leftharpoondown> "CONST ap A B x y f p" Lemma ap_refl [comp]: - assumes "f: A \<rightarrow> B" "x: A" "A: U i" "B: U i" + assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A" shows "f[refl x] \<equiv> refl (f x)" unfolding ap_def by reduce -Lemma (derive) ap_pathcomp: +Lemma (def) ap_pathcomp: assumes "A: U i" "B: U i" "x: A" "y: A" "z: A" @@ -225,48 +221,45 @@ Lemma (derive) ap_pathcomp: "p: x = y" "q: y = z" shows "f[p \<bullet> q] = f[p] \<bullet> f[q]" - apply (eq p) - focus prems vars x p - apply (eq p) - apply (reduce; intro) - done - done + proof (eq p) + fix x q assuming "x: A" "q: x = z" + show "f[refl x \<bullet> q] = f[refl x] \<bullet> f[q]" + by (eq q) (reduce, refl) + qed -Lemma (derive) ap_pathinv: +Lemma (def) ap_pathinv: assumes "A: U i" "B: U i" "x: A" "y: A" "f: A \<rightarrow> B" "p: x = y" shows "f[p\<inverse>] = f[p]\<inverse>" - by (eq p) (reduce; intro) - -text \<open>The next two proofs currently use some low-level rewriting.\<close> + by (eq p) (reduce, refl) -Lemma (derive) ap_funcomp: +Lemma (def) ap_funcomp: assumes "A: U i" "B: U i" "C: U i" "x: A" "y: A" "f: A \<rightarrow> B" "g: B \<rightarrow> C" "p: x = y" - shows "(g \<circ> f)[p] = g[f[p]]" + shows "(g \<circ> f)[p] = g[f[p]]" thm ap apply (eq p) - \<guillemotright> by reduce - \<guillemotright> by reduce intro + \<^item> by reduce + \<^item> by reduce refl done -Lemma (derive) ap_id: +Lemma (def) ap_id: assumes "A: U i" "x: A" "y: A" "p: x = y" shows "(id A)[p] = p" apply (eq p) - \<guillemotright> by reduce - \<guillemotright> by reduce intro + \<^item> by reduce + \<^item> by reduce refl done section \<open>Transport\<close> -Lemma (derive) transport: +Lemma (def) transport: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" @@ -288,22 +281,18 @@ Lemma transport_comp [comp]: shows "trans P (refl a) \<equiv> id (P a)" unfolding transport_def by reduce -\<comment> \<open>TODO: Build transport automation!\<close> - -Lemma use_transport: +Lemma apply_transport: assumes + "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" + "x: A" "y: A" "p: y =\<^bsub>A\<^esub> x" "u: P x" - "x: A" "y: A" - "A: U i" - "\<And>x. x: A \<Longrightarrow> P x: U i" shows "trans P p\<inverse> u: P y" - unfolding transport_def pathinv_def by typechk -method transport uses eq = (rule use_transport[OF eq]) +method transport uses eq = (rule apply_transport[OF _ _ _ _ eq]) -Lemma (derive) transport_left_inv: +Lemma (def) transport_left_inv: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" @@ -312,16 +301,16 @@ Lemma (derive) transport_left_inv: shows "(trans P p\<inverse>) \<circ> (trans P p) = id (P x)" by (eq p) (reduce; refl) -Lemma (derive) transport_right_inv: +Lemma (def) transport_right_inv: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" "x: A" "y: A" "p: x = y" shows "(trans P p) \<circ> (trans P p\<inverse>) = id (P y)" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) transport_pathcomp: +Lemma (def) transport_pathcomp: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" @@ -329,14 +318,14 @@ Lemma (derive) transport_pathcomp: "u: P x" "p: x = y" "q: y = z" shows "trans P q (trans P p u) = trans P (p \<bullet> q) u" - apply (eq p) - focus prems vars x p - apply (eq p) - apply (reduce; intro) - done - done - -Lemma (derive) transport_compose_typefam: +proof (eq p) + fix x q u + assuming "x: A" "q: x = z" "u: P x" + show "trans P q (trans P (refl x) u) = trans P ((refl x) \<bullet> q) u" + by (eq q) (reduce, refl) +qed + +Lemma (def) transport_compose_typefam: assumes "A: U i" "B: U i" "\<And>x. x: B \<Longrightarrow> P x: U i" @@ -345,9 +334,9 @@ Lemma (derive) transport_compose_typefam: "p: x = y" "u: P (f x)" shows "trans (fn x. P (f x)) p u = trans P f[p] u" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) transport_function_family: +Lemma (def) transport_function_family: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" @@ -357,15 +346,15 @@ Lemma (derive) transport_function_family: "u: P x" "p: x = y" shows "trans Q p ((f x) u) = (f y) (trans P p u)" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) -Lemma (derive) transport_const: +Lemma (def) transport_const: assumes "A: U i" "B: U i" "x: A" "y: A" "p: x = y" shows "\<Prod>b: B. trans (fn _. B) p b = b" - by (intro, eq p) (reduce; intro) + by intro (eq p, reduce, refl) definition transport_const_i ("trans'_const") where [implicit]: "trans_const B p \<equiv> transport_const ? B ? ? p" @@ -376,10 +365,10 @@ Lemma transport_const_comp [comp]: assumes "x: A" "b: B" "A: U i" "B: U i" - shows "trans_const B (refl x) b\<equiv> refl b" + shows "trans_const B (refl x) b \<equiv> refl b" unfolding transport_const_def by reduce -Lemma (derive) pathlift: +Lemma (def) pathlift: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" @@ -387,7 +376,7 @@ Lemma (derive) pathlift: "p: x = y" "u: P x" shows "<x, u> = <y, trans P p u>" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) definition pathlift_i ("lift") where [implicit]: "lift P p u \<equiv> pathlift ? P ? ? p u" @@ -403,7 +392,7 @@ Lemma pathlift_comp [comp]: shows "lift P (refl x) u \<equiv> refl <x, u>" unfolding pathlift_def by reduce -Lemma (derive) pathlift_fst: +Lemma (def) pathlift_fst: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" @@ -412,14 +401,14 @@ Lemma (derive) pathlift_fst: "p: x = y" shows "fst[lift P p u] = p" apply (eq p) - \<guillemotright> by reduce - \<guillemotright> by reduce intro + \<^item> by reduce + \<^item> by reduce refl done section \<open>Dependent paths\<close> -Lemma (derive) apd: +Lemma (def) apd: assumes "A: U i" "\<And>x. x: A \<Longrightarrow> P x: U i" @@ -427,7 +416,7 @@ Lemma (derive) apd: "x: A" "y: A" "p: x = y" shows "trans P p (f x) = f y" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) definition apd_i ("apd") where [implicit]: "apd f p \<equiv> Identity.apd ? ? f ? ? p" @@ -443,26 +432,25 @@ Lemma dependent_map_comp [comp]: shows "apd f (refl x) \<equiv> refl (f x)" unfolding apd_def by reduce -Lemma (derive) apd_ap: +Lemma (def) apd_ap: assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "x: A" "y: A" "p: x = y" shows "apd f p = trans_const B p (f x) \<bullet> f[p]" - by (eq p) (reduce; intro) + by (eq p) (reduce, refl) section \<open>Whiskering\<close> -Lemma (derive) right_whisker: +Lemma (def) right_whisker: assumes "A: U i" "a: A" "b: A" "c: A" and "p: a = b" "q: a = b" "r: b = c" and "\<alpha>: p = q" shows "p \<bullet> r = q \<bullet> r" apply (eq r) - focus prems vars x s t - proof - + focus vars x s t proof - have "t \<bullet> refl x = t" by (rule pathcomp_refl) also have ".. = s" by fact also have ".. = s \<bullet> refl x" by (rule pathcomp_refl[symmetric]) @@ -470,14 +458,13 @@ Lemma (derive) right_whisker: qed done -Lemma (derive) left_whisker: +Lemma (def) left_whisker: assumes "A: U i" "a: A" "b: A" "c: A" and "p: b = c" "q: b = c" "r: a = b" and "\<alpha>: p = q" shows "r \<bullet> p = r \<bullet> q" apply (eq r) - focus prems prms vars x s t - proof - + focus vars x s t proof - have "refl x \<bullet> t = t" by (rule refl_pathcomp) also have ".. = s" by fact also have ".. = refl x \<bullet> s" by (rule refl_pathcomp[symmetric]) @@ -485,24 +472,24 @@ Lemma (derive) left_whisker: qed done -definition right_whisker_i (infix "\<bullet>\<^sub>r\<^bsub>_\<^esub>" 121) - where [implicit]: "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r \<equiv> right_whisker ? a ? ? ? ? r \<alpha>" +definition right_whisker_i (infix "\<bullet>\<^sub>r" 121) + where [implicit]: "\<alpha> \<bullet>\<^sub>r r \<equiv> right_whisker ? ? ? ? ? ? r \<alpha>" -definition left_whisker_i (infix "\<bullet>\<^sub>l\<^bsub>_\<^esub>" 121) - where [implicit]: "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha> \<equiv> left_whisker ? ? ? c ? ? r \<alpha>" +definition left_whisker_i (infix "\<bullet>\<^sub>l" 121) + where [implicit]: "r \<bullet>\<^sub>l \<alpha> \<equiv> left_whisker ? ? ? ? ? ? r \<alpha>" translations - "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> r" \<leftharpoondown> "CONST right_whisker A a b c p q r \<alpha>" - "r \<bullet>\<^sub>l\<^bsub>c\<^esub> \<alpha>" \<leftharpoondown> "CONST left_whisker A a b c p q r \<alpha>" + "\<alpha> \<bullet>\<^sub>r r" \<leftharpoondown> "CONST right_whisker A a b c p q r \<alpha>" + "r \<bullet>\<^sub>l \<alpha>" \<leftharpoondown> "CONST left_whisker A a b c p q r \<alpha>" Lemma whisker_refl [comp]: assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q" - shows "\<alpha> \<bullet>\<^sub>r\<^bsub>a\<^esub> (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>" + shows "\<alpha> \<bullet>\<^sub>r (refl b) \<equiv> ru p \<bullet> \<alpha> \<bullet> (ru q)\<inverse>" unfolding right_whisker_def by reduce Lemma refl_whisker [comp]: assumes "A: U i" "a: A" "b: A" "p: a = b" "q: a = b" "\<alpha>: p = q" - shows "(refl a) \<bullet>\<^sub>l\<^bsub>b\<^esub> \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>" + shows "(refl a) \<bullet>\<^sub>l \<alpha> \<equiv> (lu p) \<bullet> \<alpha> \<bullet> (lu q)\<inverse>" unfolding left_whisker_def by reduce method left_whisker = (rule left_whisker) @@ -521,7 +508,7 @@ assumes assums: "r: b =\<^bsub>A\<^esub> c" "s: b =\<^bsub>A\<^esub> c" begin -Lemma (derive) horiz_pathcomp: +Lemma (def) horiz_pathcomp: notes assums assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s" @@ -532,7 +519,7 @@ qed typechk text \<open>A second horizontal composition:\<close> -Lemma (derive) horiz_pathcomp': +Lemma (def) horiz_pathcomp': notes assums assumes "\<alpha>: p = q" "\<beta>: r = s" shows "p \<bullet> r = q \<bullet> s" @@ -544,14 +531,14 @@ qed typechk notation horiz_pathcomp (infix "\<star>" 121) notation horiz_pathcomp' (infix "\<star>''" 121) -Lemma (derive) horiz_pathcomp_eq_horiz_pathcomp': +Lemma (def) horiz_pathcomp_eq_horiz_pathcomp': notes assums assumes "\<alpha>: p = q" "\<beta>: r = s" shows "\<alpha> \<star> \<beta> = \<alpha> \<star>' \<beta>" unfolding horiz_pathcomp_def horiz_pathcomp'_def apply (eq \<alpha>, eq \<beta>) focus vars p apply (eq p) - focus vars _ q by (eq q) (reduce; refl) + focus vars a q by (eq q) (reduce, refl) done done @@ -580,12 +567,20 @@ interpretation \<Omega>2: notation \<Omega>2.horiz_pathcomp (infix "\<star>" 121) notation \<Omega>2.horiz_pathcomp' (infix "\<star>''" 121) -Lemma (derive) pathcomp_eq_horiz_pathcomp: +Lemma [typechk]: + assumes "\<alpha>: \<Omega>2 A a" and "\<beta>: \<Omega>2 A a" + shows horiz_pathcomp_type: "\<alpha> \<star> \<beta>: \<Omega>2 A a" + and horiz_pathcomp'_type: "\<alpha> \<star>' \<beta>: \<Omega>2 A a" + using assms + unfolding \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def \<Omega>2_alt_def + by reduce+ + +Lemma (def) pathcomp_eq_horiz_pathcomp: assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a" shows "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>" unfolding \<Omega>2.horiz_pathcomp_def using assms[unfolded \<Omega>2_alt_def] - proof (reduce, rule pathinv) + proof (reduce, rule pathinv) \<comment> \<open>Propositional equality rewriting needs to be improved\<close> have "{} = refl (refl a) \<bullet> \<alpha>" by (rule pathcomp_refl) also have ".. = \<alpha>" by (rule refl_pathcomp) @@ -596,12 +591,12 @@ Lemma (derive) pathcomp_eq_horiz_pathcomp: finally have eq\<beta>: "{} = \<beta>" by this have "refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a)) - = \<alpha> \<bullet> {}" by right_whisker (rule eq\<alpha>) - also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (rule eq\<beta>) + = \<alpha> \<bullet> {}" by right_whisker (fact eq\<alpha>) + also have ".. = \<alpha> \<bullet> \<beta>" by left_whisker (fact eq\<beta>) finally show "{} = \<alpha> \<bullet> \<beta>" by this qed -Lemma (derive) pathcomp_eq_horiz_pathcomp': +Lemma (def) pathcomp_eq_horiz_pathcomp': assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a" shows "\<alpha> \<star>' \<beta> = \<beta> \<bullet> \<alpha>" unfolding \<Omega>2.horiz_pathcomp'_def @@ -616,12 +611,12 @@ Lemma (derive) pathcomp_eq_horiz_pathcomp': finally have eq\<alpha>: "{} = \<alpha>" by this have "refl (refl a) \<bullet> \<beta> \<bullet> refl (refl a) \<bullet> (refl (refl a) \<bullet> \<alpha> \<bullet> refl (refl a)) - = \<beta> \<bullet> {}" by right_whisker (rule eq\<beta>) - also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (rule eq\<alpha>) + = \<beta> \<bullet> {}" by right_whisker (fact eq\<beta>) + also have ".. = \<beta> \<bullet> \<alpha>" by left_whisker (fact eq\<alpha>) finally show "{} = \<beta> \<bullet> \<alpha>" by this qed -Lemma (derive) eckmann_hilton: +Lemma (def) eckmann_hilton: assumes "\<alpha>: \<Omega>2 A a" "\<beta>: \<Omega>2 A a" shows "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>" using assms[unfolded \<Omega>2_alt_def] @@ -629,11 +624,15 @@ Lemma (derive) eckmann_hilton: have "\<alpha> \<bullet> \<beta> = \<alpha> \<star> \<beta>" by (rule pathcomp_eq_horiz_pathcomp) also have [simplified comp]: ".. = \<alpha> \<star>' \<beta>" + \<comment> \<open>Danger, Will Robinson! (Inferred implicit has an equivalent form but + needs to be manually simplified.)\<close> by (transport eq: \<Omega>2.horiz_pathcomp_eq_horiz_pathcomp') refl also have ".. = \<beta> \<bullet> \<alpha>" by (rule pathcomp_eq_horiz_pathcomp') finally show "\<alpha> \<bullet> \<beta> = \<beta> \<bullet> \<alpha>" - by this (reduce add: \<Omega>2.horiz_pathcomp_def \<Omega>2.horiz_pathcomp'_def)+ + by (this; reduce add: \<Omega>2_alt_def[symmetric]) + \<comment> \<open>TODO: The finishing call to `reduce` should be unnecessary with some + kind of definitional unfolding.\<close> qed end diff --git a/hott/More_List.thy b/hott/List+.thy index 1b8034f..b73cc24 100644 --- a/hott/More_List.thy +++ b/hott/List+.thy @@ -1,4 +1,4 @@ -theory More_List +theory "List+" imports Spartan.List Nat @@ -10,8 +10,8 @@ section \<open>Length\<close> definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)" experiment begin - Lemma "len [] \<equiv> ?n" by (subst comp)+ - Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp)+ + Lemma "len [] \<equiv> ?n" by (subst comp) + Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp) end diff --git a/hott/More_Nat.thy b/hott/More_Nat.thy deleted file mode 100644 index 59c8d54..0000000 --- a/hott/More_Nat.thy +++ /dev/null @@ -1,43 +0,0 @@ -theory More_Nat -imports Nat Spartan.More_Types - -begin - -section \<open>Equality on Nat\<close> - -text \<open>Via the encode-decode method.\<close> - -context begin - -Lemma (derive) eq: shows "Nat \<rightarrow> Nat \<rightarrow> U O" - apply intro focus vars m apply elim - \<comment> \<open>m \<equiv> 0\<close> - apply intro focus vars n apply elim - \<guillemotright> by (rule TopF) \<comment> \<open>n \<equiv> 0\<close> - \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> suc _\<close> - \<guillemotright> by (rule Ui_in_USi) - done - \<comment> \<open>m \<equiv> suc k\<close> - apply intro focus vars k k_eq n apply (elim n) - \<guillemotright> by (rule BotF) \<comment> \<open>n \<equiv> 0\<close> - \<guillemotright> prems vars l proof - show "k_eq l: U O" by typechk qed - \<guillemotright> by (rule Ui_in_USi) - done - by (rule Ui_in_USi) - done - -text \<open> -\<^term>\<open>eq\<close> is defined by - eq 0 0 \<equiv> \<top> - eq 0 (suc k) \<equiv> \<bottom> - eq (suc k) 0 \<equiv> \<bottom> - eq (suc k) (suc l) \<equiv> eq k l -\<close> - - - - -end - - -end diff --git a/hott/Nat.thy b/hott/Nat.thy index 177ec47..fd567f3 100644 --- a/hott/Nat.thy +++ b/hott/Nat.thy @@ -77,43 +77,43 @@ lemma add_suc [comp]: shows "m + suc n \<equiv> suc (m + n)" unfolding add_def by reduce -Lemma (derive) zero_add: +Lemma (def) zero_add: assumes "n: Nat" shows "0 + n = n" apply (elim n) - \<guillemotright> by (reduce; intro) - \<guillemotright> vars _ ih by reduce (eq ih; intro) + \<^item> by (reduce; intro) + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) suc_add: +Lemma (def) suc_add: assumes "m: Nat" "n: Nat" shows "suc m + n = suc (m + n)" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> vars _ ih by reduce (eq ih; intro) + \<^item> by reduce refl + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) suc_eq: +Lemma (def) suc_eq: assumes "m: Nat" "n: Nat" shows "p: m = n \<Longrightarrow> suc m = suc n" by (eq p) intro -Lemma (derive) add_assoc: +Lemma (def) add_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l + (m + n) = l + m+ n" apply (elim n) - \<guillemotright> by reduce intro - \<guillemotright> vars _ ih by reduce (eq ih; intro) + \<^item> by reduce intro + \<^item> vars _ ih by reduce (eq ih; refl) done -Lemma (derive) add_comm: +Lemma (def) add_comm: assumes "m: Nat" "n: Nat" shows "m + n = n + m" apply (elim n) - \<guillemotright> by (reduce; rule zero_add[symmetric]) - \<guillemotright> prems vars n ih + \<^item> by (reduce; rule zero_add[symmetric]) + \<^item> vars n ih proof reduce - have "suc (m + n) = suc (n + m)" by (eq ih) intro + have "suc (m + n) = suc (n + m)" by (eq ih) refl also have ".. = suc n + m" by (transport eq: suc_add) refl finally show "{}" by this qed @@ -143,12 +143,12 @@ lemma mul_suc [comp]: shows "m * suc n \<equiv> m + m * n" unfolding mul_def by reduce -Lemma (derive) zero_mul: +Lemma (def) zero_mul: assumes "n: Nat" shows "0 * n = 0" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce have "0 + 0 * n = 0 + 0 " by (eq ih) refl also have ".. = 0" by reduce refl @@ -156,12 +156,12 @@ Lemma (derive) zero_mul: qed done -Lemma (derive) suc_mul: +Lemma (def) suc_mul: assumes "m: Nat" "n: Nat" shows "suc m * n = m * n + n" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof (reduce, transport eq: \<open>ih:_\<close>) have "suc m + (m * n + n) = suc (m + {})" by (rule suc_add) also have ".. = suc (m + m * n + n)" by (transport eq: add_assoc) refl @@ -169,12 +169,12 @@ Lemma (derive) suc_mul: qed done -Lemma (derive) mul_dist_add: +Lemma (def) mul_dist_add: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m + n) = l * m + l * n" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems prms vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce have "l + l * (m + n) = l + (l * m + l * n)" by (eq ih) refl also have ".. = l + l * m + l * n" by (rule add_assoc) @@ -184,12 +184,12 @@ Lemma (derive) mul_dist_add: qed done -Lemma (derive) mul_assoc: +Lemma (def) mul_assoc: assumes "l: Nat" "m: Nat" "n: Nat" shows "l * (m * n) = l * m * n" apply (elim n) - \<guillemotright> by reduce refl - \<guillemotright> prems vars n ih + \<^item> by reduce refl + \<^item> vars n ih proof reduce have "l * (m + m * n) = l * m + l * (m * n)" by (rule mul_dist_add) also have ".. = l * m + l * m * n" by (transport eq: \<open>ih:_\<close>) refl @@ -197,12 +197,12 @@ Lemma (derive) mul_assoc: qed done -Lemma (derive) mul_comm: +Lemma (def) mul_comm: assumes "m: Nat" "n: Nat" shows "m * n = n * m" apply (elim n) - \<guillemotright> by reduce (transport eq: zero_mul, refl) - \<guillemotright> prems vars n ih + \<^item> by reduce (transport eq: zero_mul, refl) + \<^item> vars n ih proof (reduce, rule pathinv) have "suc n * m = n * m + m" by (rule suc_mul) also have ".. = m + m * n" |