aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
authorJosh Chen2020-07-31 14:56:24 +0200
committerJosh Chen2020-07-31 14:56:24 +0200
commitff5454812f9e2720bd90c3a5437505644f63b487 (patch)
tree2df5f45de006c56391118db75e2f185036b02cd7 /hott
parent2b0e14b16dcef0e829da95800b3c0af1975bb1ce (diff)
(FEAT) Term elaboration of assumption and goal statements.
. spartan/core/goals.ML . spartan/core/elaboration.ML . spartan/core/elaborated_statement.ML (FEAT) More context tacticals and search tacticals. . spartan/core/context_tactical.ML (FEAT) Improved subgoal focus. Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY). . spartan/core/focus.ML (FIX) Normalize facts in order to be able to resolve properly. . spartan/core/typechecking.ML (MAIN) New definitions. (MAIN) Renamed theories and theorems. (MAIN) Refactor theories to fit new features.
Diffstat (limited to '')
-rw-r--r--hott/Equivalence.thy456
-rw-r--r--hott/Identity.thy239
-rw-r--r--hott/List+.thy (renamed from hott/More_List.thy)6
-rw-r--r--hott/More_Nat.thy43
-rw-r--r--hott/Nat.thy58
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"