diff options
| -rw-r--r-- | HoTT_Base.thy | 3 | ||||
| -rw-r--r-- | Prod.thy | 18 | ||||
| -rw-r--r-- | Sum.thy | 97 |
3 files changed, 95 insertions, 23 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 7794601..a0078fa 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -7,7 +7,6 @@ Basic setup and definitions of a homotopy type theory object logic without unive theory HoTT_Base imports Pure - begin section \<open>Setup\<close> @@ -34,7 +33,7 @@ consts is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ :/ _)" [0, 0] 1000) axiomatization where - inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U" + inhabited_implies_type [intro, elim]: "\<And>a A. a : A \<Longrightarrow> A : U" section \<open>Type families\<close> @@ -7,7 +7,6 @@ Dependent product (function) type for the HoTT logic. theory Prod imports HoTT_Base - begin axiomatization @@ -37,7 +36,11 @@ translations section \<open>Type rules\<close> axiomatization where - Prod_form: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U" + Prod_form: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U" +and + Prod_form_cond1: "\<And>A B. (\<Prod>x:A. B x : U) \<Longrightarrow> A : U" +and + Prod_form_cond2: "\<And>A B. (\<Prod>x:A. B x : U) \<Longrightarrow> B: A \<rightarrow> U" and Prod_intro: "\<And>A B b. \<lbrakk>A : U; \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" and @@ -47,11 +50,16 @@ and and Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f" -text "The type rules should be able to be used as introduction rules by the standard reasoner:" +text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)." + +text "In textbook presentations it is usual to present type formation as a forward implication, stating conditions sufficient for the formation of the type. +It is however implicit that the premises of the rule are also necessary, so that for example the only way for one to have that \<open>\<Prod>x:A. B x : U\<close> is for \<open>A : U\<close> and \<open>B: A \<rightarrow> U\<close> in the first place. +This is what the additional formation rules \<open>Prod_form_cond1\<close> and \<open>Prod_form_cond2\<close> express." -lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:" -text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)." +lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq +lemmas Prod_form_conds [elim] = Prod_form_cond1 Prod_form_cond2 text "Nondependent functions are a special case." @@ -7,7 +7,6 @@ Dependent sum type. theory Sum imports Prod - begin axiomatization @@ -32,6 +31,10 @@ section \<open>Type rules\<close> axiomatization where Sum_form: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U" and + Sum_form_cond1: "\<And>A B. (\<Sum>x:A. B x : U) \<Longrightarrow> A : U" +and + Sum_form_cond2: "\<And>A B. (\<Sum>x:A. B x : U) \<Longrightarrow> B: A \<rightarrow> U" +and Sum_intro: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x" and Sum_elim: "\<And>A B C f p. \<lbrakk> @@ -48,6 +51,7 @@ and \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp +lemmas Sum_form_conds [elim] = Sum_form_cond1 Sum_form_cond2 \<comment> \<open>Nondependent pair\<close> abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) @@ -76,44 +80,104 @@ overloading snd_nondep \<equiv> snd begin definition snd_dep :: "[Term, Typefam] \<Rightarrow> Term" where - "snd_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>p. B fst[A,B]`p) (\<lambda>x y. y) p" + "snd_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p" definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where "snd_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p" end -text "Simplifying projections:" +text "Results about projections:" + +lemma fst_dep_type: + assumes "p : \<Sum>x:A. B x" + shows "fst[A,B]`p : A" + +proof \<comment> \<open>The standard reasoner knows to backchain with the product elimination rule here...\<close> + \<comment> \<open>Also write about this proof: compare the effect of letting the standard reasoner do simplifications, as opposed to using the minus switch and writing everything out explicitly from first principles.\<close> + + have *: "\<Sum>x:A. B x : U" using assms .. + + show "fst[A,B]: (\<Sum>x:A. B x) \<rightarrow> A" + + proof (unfold fst_dep_def, standard) \<comment> \<open>...and with the product introduction rule here...\<close> + show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A" + + proof \<comment> \<open>...and with sum elimination here.\<close> + show "A : U" using * .. + qed + + qed (rule *) + +qed (rule assms) + lemma fst_dep_comp: (* Potential for automation *) assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \<equiv> a" -proof (unfold fst_dep_def) + +proof - \<comment> "Write about this proof: unfolding, how we set up the introduction rules (explain \<open>..\<close>), do a trace of the proof, explain the meaning of keywords, etc." have *: "A : U" using assms(2) .. (* I keep thinking this should not have to be done explicitly, but rather automated. *) - - then have "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A" .. - - moreover have "(a,b) : \<Sum>x:A. B x" using assms .. - - ultimately have "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv> - indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" .. + + have "fst[A,B]`(a,b) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" + proof (unfold fst_dep_def, standard) + show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p : A" using * .. + show "(a,b) : \<Sum>x:A. B x" using assms .. + qed also have "indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a" by (rule Sum_comp) (rule *, assumption, (rule assms)+) - finally show "(\<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p)`(a,b) \<equiv> a" . + finally show "fst[A,B]`(a,b) \<equiv> a" . qed + +lemma snd_dep_type: + assumes "p : \<Sum>x:A. B x" + shows "snd[A,B]`p : B (fst[A,B]`p)" +oops +\<comment> \<open>Do we need this for the following lemma?\<close> + + lemma snd_dep_comp: - assumes "a : A" and "b : B a" + assumes "B: A \<rightarrow> U" and "a : A" and "b : B a" shows "snd[A,B]`(a,b) \<equiv> b" proof - - have "\<lambda>p. B fst[A,B]`p: \<Sum>x:A. B x \<rightarrow> U" - - show "snd[A,B]`(a,b) \<equiv> b" unfolding fst_dep_def + \<comment> \<open>We use the following two lemmas:\<close> + + have lemma1: "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> B (fst[A,B]`p) : U" + proof - + fix p assume "p : \<Sum>x:A. B x" + then have "fst[A,B]`p : A" by (rule fst_dep_type) + then show "B (fst[A,B]`p) : U" by (rule assms(1)) + qed + + have lemma2: "\<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> y : B (fst[A,B]`(x, y))" + proof - + fix x y assume "x : A" and "y : B x" + moreover with assms(1) have "fst[A,B]`(x,y) \<equiv> x" by (rule fst_dep_comp) + ultimately show "y : B (fst[A,B]`(x,y))" by simp + qed + + \<comment> \<open>And now the proof.\<close> + + have "snd[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b)" + proof (unfold snd_dep_def, standard) + show "(a,b) : \<Sum>x:A. B x" using assms .. + + fix p assume *: "p : \<Sum>x:A. B x" + show "indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)" + by (standard, elim lemma1, elim lemma2) (assumption, rule *) + qed + + also have "indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b) \<equiv> b" + by (standard, elim lemma1, elim lemma2) (assumption, (rule assms)+) + + finally show "snd[A,B]`(a,b) \<equiv> b" . qed + lemma fst_nondep_comp: assumes "a : A" and "b : B" shows "fst[A,B]`(a,b) \<equiv> a" @@ -131,4 +195,5 @@ qed lemmas proj_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp + end
\ No newline at end of file |