diff options
| -rw-r--r-- | Equal.thy | 29 | ||||
| -rw-r--r-- | HoTT_Base.thy | 76 | ||||
| -rw-r--r-- | Prod.thy | 56 | ||||
| -rw-r--r-- | Proj.thy | 30 | ||||
| -rw-r--r-- | Sum.thy | 39 |
5 files changed, 130 insertions, 100 deletions
@@ -10,13 +10,12 @@ theory Equal begin +section \<open>Constants and syntax\<close> + axiomatization Equal :: "[Term, Term, Term] \<Rightarrow> Term" and refl :: "Term \<Rightarrow> Term" ("(refl'(_'))" 1000) and - indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1indEqual[_])") - - -section \<open>Syntax\<close> + indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>=[_])") syntax "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) @@ -31,12 +30,6 @@ section \<open>Type rules\<close> axiomatization where Equal_form: "\<And>i A a b. \<lbrakk>A : U(i); a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)" and - Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> A : U(i)" -and - Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> a : A" -and - Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> b : A" -and Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a) : a =\<^sub>A a" and Equal_elim: "\<And>i A C f a b p. \<lbrakk> @@ -45,17 +38,27 @@ and a : A; b : A; p : a =\<^sub>A b - \<rbrakk> \<Longrightarrow> indEqual[A] C f a b p : C a b p" + \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a b p : C a b p" and Equal_comp: "\<And>i A C f a. \<lbrakk> \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i); \<And>x. x : A \<Longrightarrow> f x : C x x refl(x); a : A - \<rbrakk> \<Longrightarrow> indEqual[A] C f a a refl(a) \<equiv> f a" + \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a a refl(a) \<equiv> f a" + +text "Admissible inference rules for equality type formation:" + +axiomatization where + Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> A : U(i)" +and + Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> a : A" +and + Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> b : A" lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -lemmas Equal_form_conds [elim, wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 +lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 lemmas Equal_comps [comp] = Equal_comp + end
\ No newline at end of file diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 8c45d35..cf71813 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,8 +1,8 @@ (* Title: HoTT/HoTT_Base.thy Author: Josh Chen - Date: Jun 2018 + Date: Aug 2018 -Basic setup and definitions of a homotopy type theory object logic. +Basic setup and definitions of a homotopy type theory object logic with a cumulative universe hierarchy à la Russell. *) theory HoTT_Base @@ -12,71 +12,77 @@ begin section \<open>Foundational definitions\<close> -text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms." +text "Meta syntactic type for object-logic types and terms." typedecl Term -section \<open>Named theorems\<close> - -text "Named theorems to be used by proof methods later (see HoTT_Methods.thy). - -\<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while -\<open>comp\<close> declares computation rules, which are used by the simplification method as equational rewrite rules." - -named_theorems wellform -named_theorems comp - - section \<open>Judgments\<close> -text "Formalize the context and typing judgments \<open>a : A\<close>. - -For judgmental equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it." +text " + Formalize the typing judgment \<open>a : A\<close>. + For judgmental/definitional equality we use the existing Pure equality \<open>\<equiv>\<close> and hence do not need to define a separate judgment for it. +" consts - is_of_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 0] 1000) + has_type :: "[Term, Term] \<Rightarrow> prop" ("(1_ : _)" [0, 0] 1000) -section \<open>Universes\<close> +section \<open>Universe hierarchy\<close> -text "Strictly-ordered meta-level natural numbers to index the universes." +text "Finite meta-ordinals to index the universes." -typedecl Numeral +typedecl Ord axiomatization - O :: Numeral ("0") and - S :: "Numeral \<Rightarrow> Numeral" ("S_") and - lt :: "[Numeral, Numeral] \<Rightarrow> prop" (infix "<-" 999) + O :: Ord and + S :: "Ord \<Rightarrow> Ord" ("S_" [0] 1000) and + lt :: "[Ord, Ord] \<Rightarrow> prop" (infix "<-" 999) where - Numeral_lt_min: "\<And>n. 0 <- S n" + Ord_lt_min: "\<And>n. O <- S n" and - Numeral_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n" + Ord_lt_trans: "\<And>m n. m <- n \<Longrightarrow> S m <- S n" -lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans +lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_trans \<comment> \<open>Enables \<open>standard\<close> to automatically solve inequalities.\<close> -text "Universe types:" +text "Define the universe types." axiomatization - U :: "Numeral \<Rightarrow> Term" ("U _") + U :: "Ord \<Rightarrow> Term" where - Universe_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)" + U_hierarchy: "\<And>i j. i <- j \<Longrightarrow> U(i) : U(j)" and - Universe_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)" - \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> + U_cumulative: "\<And>A i j. \<lbrakk>A : U(i); i <- j\<rbrakk> \<Longrightarrow> A : U(j)" + \<comment> \<open>WARNING: \<open>rule Universe_cumulative\<close> can result in an infinite rewrite loop!\<close> section \<open>Type families\<close> -text "We define the following abbreviation constraining the output type of a meta lambda expression when given input of certain type." +text " + The following abbreviation constrains the output type of a meta lambda expression when given input of certain type. +" -abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop" ("_: _ \<longrightarrow> _") +abbreviation (input) constrained :: "[Term \<Rightarrow> Term, Term, Term] \<Rightarrow> prop" ("(1_: _ \<longrightarrow> _)") where "f: A \<longrightarrow> B \<equiv> (\<And>x. x : A \<Longrightarrow> f x : B)" -text "The above is used to define type families, which are just constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are elements of some universe type." +text " + The above is used to define type families, which are constrained meta-lambdas \<open>P: A \<longrightarrow> B\<close> where \<open>A\<close> and \<open>B\<close> are small types. +" type_synonym Typefam = "Term \<Rightarrow> Term" +section \<open>Named theorems\<close> + +text " + Named theorems to be used by proof methods later (see HoTT_Methods.thy). + + \<open>wellform\<close> declares necessary wellformedness conditions for type and inhabitation judgments, while \<open>comp\<close> declares computation rules, which are used by the simplification method as equational rewrite rules. +" + +named_theorems wellform +named_theorems comp + + end
\ No newline at end of file @@ -1,8 +1,8 @@ (* Title: HoTT/Prod.thy Author: Josh Chen - Date: Jun 2018 + Date: Aug 2018 -Dependent product (function) type for the HoTT logic. +Dependent product (function) type. *) theory Prod @@ -10,14 +10,13 @@ theory Prod begin +section \<open>Constants and syntax\<close> + axiomatization Prod :: "[Term, Typefam] \<Rightarrow> Term" and lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and - \<comment> \<open>Application binds tighter than abstraction.\<close> appl :: "[Term, Term] \<Rightarrow> Term" (infixl "`" 60) - - -section \<open>Syntax\<close> + \<comment> \<open>Application binds tighter than abstraction.\<close> syntax "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30) @@ -33,17 +32,18 @@ translations "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)" "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)" +text "Nondependent functions are a special case." + +abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40) + where "A \<rightarrow> B \<equiv> \<Prod>_:A. B" + section \<open>Type rules\<close> axiomatization where Prod_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U(i)" and - Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> A : U(i)" -and - Prod_form_cond2: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" -and - Prod_intro: "\<And>i A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" + Prod_intro: "\<And>i A B b. \<lbrakk>A : U(i); \<And>x. x : A \<Longrightarrow> b x : B x\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x" and Prod_elim: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a" and @@ -51,38 +51,42 @@ and and Prod_uniq: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f" -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 " + 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 addition to the usual type rules, it is a meta-theorem (*PROVE THIS!*) that whenever \<open>\<Prod>x:A. B x : U(i)\<close> is derivable from some set of premises \<Gamma>, then so are \<open>A : U(i)\<close> and \<open>B: A \<longrightarrow> U(i)\<close>. + + That is to say, the following inference rules are admissible, and it simplifies proofs greatly to axiomatize them directly. +" -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." +axiomatization where + Prod_form_cond1: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> A : U(i)" +and + Prod_form_cond2: "\<And>i A B. (\<Prod>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" -text "The type rules should be able to be used as introduction and elimination rules by the standard reasoner:" +text "Set up the standard reasoner to use the type rules:" lemmas Prod_rules [intro] = Prod_form Prod_intro Prod_elim Prod_comp Prod_uniq -lemmas Prod_form_conds [elim, wellform] = Prod_form_cond1 Prod_form_cond2 +lemmas Prod_form_conds [intro (*elim, wellform*)] = Prod_form_cond1 Prod_form_cond2 lemmas Prod_comps [comp] = Prod_comp Prod_uniq -text "Nondependent functions are a special case." - -abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 40) - where "A \<rightarrow> B \<equiv> \<Prod>_:A. B" - section \<open>Unit type\<close> axiomatization Unit :: Term ("\<one>") and pt :: Term ("\<star>") and - indUnit :: "[Typefam, Term, Term] \<Rightarrow> Term" + indUnit :: "[Typefam, Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<one>)") where - Unit_form: "\<one> : U(0)" + Unit_form: "\<one> : U(O)" and Unit_intro: "\<star> : \<one>" and - Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>; a : \<one>\<rbrakk> \<Longrightarrow> indUnit C c a : C a" + Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>; a : \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> C c a : C a" and - Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>\<rbrakk> \<Longrightarrow> indUnit C c \<star> \<equiv> c" + Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c : C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> C c \<star> \<equiv> c" lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp lemmas Unit_comps [comp] = Unit_comp @@ -25,10 +25,10 @@ overloading fst_nondep \<equiv> fst begin definition fst_dep :: "[Term, Typefam] \<Rightarrow> Term" where - "fst_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p" + "fst_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). ind\<^sub>\<Sum>[A,B] (\<lambda>_. A) (\<lambda>x y. x) p" definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where - "fst_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) p" + "fst_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. ind\<^sub>\<Sum>[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) p" end overloading @@ -36,10 +36,10 @@ 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>q. B (fst[A,B]`q)) (\<lambda>x y. y) p" + "snd_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). ind\<^sub>\<Sum>[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" + "snd_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. ind\<^sub>\<Sum>[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p" end @@ -48,15 +48,29 @@ section \<open>Properties\<close> text "Typing judgments and computation rules for the dependent and non-dependent projection functions." lemma fst_dep_type: assumes "\<Sum>x:A. B x : U(i)" and "p : \<Sum>x:A. B x" shows "fst[A,B]`p : A" - unfolding fst_dep_def - by (derive lems: assms) +unfolding fst_dep_def +proof + show "lambda (Sum A B) (ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x)) : (\<Sum>x:A. B x) \<rightarrow> A" + proof + show "Sum A B : U(i)" by (rule assms) + show "\<And>p. p : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) p : A" + proof + show "A : U(i)" using assms(1) .. + qed + qed +qed (rule assms) lemma fst_dep_comp: assumes "A : U(i)" and "B: A \<longrightarrow> U(i)" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \<equiv> a" - unfolding fst_dep_def - by (simplify lems: assms) +unfolding fst_dep_def +proof (subst comp) + show "\<And>x. x : Sum A B \<Longrightarrow> ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) x : A" by (standard, rule assms(1), assumption+) + show "(a,b) : Sum A B" using assms(2-4) .. + show "ind\<^sub>\<Sum>[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a, b) \<equiv> a" + proof + oops \<comment> \<open> (* Old proof *) proof - @@ -10,13 +10,12 @@ theory Sum begin +section \<open>Constants and syntax\<close> + axiomatization Sum :: "[Term, Typefam] \<Rightarrow> Term" and pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and - indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1indSum[_,/ _])") - - -section \<open>Syntax\<close> + indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<Sum>[_,/ _])") syntax "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) @@ -26,49 +25,53 @@ translations "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)" +text "Nondependent pair." + +abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) + where "A \<times> B \<equiv> \<Sum>_:A. B" + section \<open>Type rules\<close> axiomatization where Sum_form: "\<And>i A B. \<lbrakk>A : U(i); B: A \<longrightarrow> U(i)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U(i)" and - Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> A : U(i)" -and - Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" -and Sum_intro: "\<And>i A B a b. \<lbrakk>B: A \<longrightarrow> U(i); a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x" and Sum_elim: "\<And>i A B C f p. \<lbrakk> C: \<Sum>x:A. B x \<longrightarrow> U(i); \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y); p : \<Sum>x:A. B x - \<rbrakk> \<Longrightarrow> indSum[A,B] C f p : C p" + \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>[A,B] C f p : C p" and Sum_comp: "\<And>i A B C f a b. \<lbrakk> C: \<Sum>x:A. B x \<longrightarrow> U(i); \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y); a : A; b : B a - \<rbrakk> \<Longrightarrow> indSum[A,B] C f (a,b) \<equiv> f a b" + \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>[A,B] C f (a,b) \<equiv> f a b" + +text "Admissible inference rules for sum formation:" + +axiomatization where + Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> A : U(i)" +and + Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)" lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp -lemmas Sum_form_conds [elim, wellform] = Sum_form_cond1 Sum_form_cond2 +lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2 lemmas Sum_comps [comp] = Sum_comp -text "Nondependent pair." -abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) - where "A \<times> B \<equiv> \<Sum>_:A. B" - section \<open>Null type\<close> axiomatization Null :: Term ("\<zero>") and - indNull :: "[Typefam, Term] \<Rightarrow> Term" + indNull :: "[Typefam, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") where - Null_form: "\<zero> : U(0)" + Null_form: "\<zero> : U(O)" and - Null_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> indNull C z : C z" + Null_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z" lemmas Null_rules [intro] = Null_form Null_elim |