From 0daf45af7c5489c34336a31f5054b9271685dacf Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 4 Aug 2018 22:37:29 +0200 Subject: Reorganize theories --- Equal.thy | 29 +++++++++++++---------- HoTT_Base.thy | 76 ++++++++++++++++++++++++++++++++--------------------------- Prod.thy | 56 +++++++++++++++++++++++-------------------- Proj.thy | 30 ++++++++++++++++------- Sum.thy | 39 ++++++++++++++++-------------- 5 files changed, 130 insertions(+), 100 deletions(-) diff --git a/Equal.thy b/Equal.thy index 8c5cf29..2b49213 100644 --- a/Equal.thy +++ b/Equal.thy @@ -10,13 +10,12 @@ theory Equal begin +section \Constants and syntax\ + axiomatization Equal :: "[Term, Term, Term] \ Term" and refl :: "Term \ Term" ("(refl'(_'))" 1000) and - indEqual :: "[Term, [Term, Term] \ Typefam, Term \ Term, Term, Term, Term] \ Term" ("(1indEqual[_])") - - -section \Syntax\ + indEqual :: "[Term, [Term, Term] \ Typefam, Term \ Term, Term, Term, Term] \ Term" ("(1ind\<^sub>=[_])") syntax "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100) @@ -30,12 +29,6 @@ section \Type rules\ axiomatization where Equal_form: "\i A a b. \A : U(i); a : A; b : A\ \ a =\<^sub>A b : U(i)" -and - Equal_form_cond1: "\i A a b. a =\<^sub>A b : U(i) \ A : U(i)" -and - Equal_form_cond2: "\i A a b. a =\<^sub>A b : U(i) \ a : A" -and - Equal_form_cond3: "\i A a b. a =\<^sub>A b : U(i) \ b : A" and Equal_intro: "\A a. a : A \ refl(a) : a =\<^sub>A a" and @@ -45,17 +38,27 @@ and a : A; b : A; p : a =\<^sub>A b - \ \ indEqual[A] C f a b p : C a b p" + \ \ ind\<^sub>=[A] C f a b p : C a b p" and Equal_comp: "\i A C f a. \ \x y. \x : A; y : A\ \ C x y: x =\<^sub>A y \ U(i); \x. x : A \ f x : C x x refl(x); a : A - \ \ indEqual[A] C f a a refl(a) \ f a" + \ \ ind\<^sub>=[A] C f a a refl(a) \ f a" + +text "Admissible inference rules for equality type formation:" + +axiomatization where + Equal_form_cond1: "\i A a b. a =\<^sub>A b : U(i) \ A : U(i)" +and + Equal_form_cond2: "\i A a b. a =\<^sub>A b : U(i) \ a : A" +and + Equal_form_cond3: "\i A a b. a =\<^sub>A b : U(i) \ 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 \Foundational definitions\ -text "A single meta-type \Term\ suffices to implement the object-logic types and terms." +text "Meta syntactic type for object-logic types and terms." typedecl Term -section \Named theorems\ - -text "Named theorems to be used by proof methods later (see HoTT_Methods.thy). - -\wellform\ declares necessary wellformedness conditions for type and inhabitation judgments, while -\comp\ declares computation rules, which are used by the simplification method as equational rewrite rules." - -named_theorems wellform -named_theorems comp - - section \Judgments\ -text "Formalize the context and typing judgments \a : A\. - -For judgmental equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it." +text " + Formalize the typing judgment \a : A\. + For judgmental/definitional equality we use the existing Pure equality \\\ and hence do not need to define a separate judgment for it. +" consts - is_of_type :: "[Term, Term] \ prop" ("(1_ : _)" [0, 0] 1000) + has_type :: "[Term, Term] \ prop" ("(1_ : _)" [0, 0] 1000) -section \Universes\ +section \Universe hierarchy\ -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 \ Numeral" ("S_") and - lt :: "[Numeral, Numeral] \ prop" (infix "<-" 999) + O :: Ord and + S :: "Ord \ Ord" ("S_" [0] 1000) and + lt :: "[Ord, Ord] \ prop" (infix "<-" 999) where - Numeral_lt_min: "\n. 0 <- S n" + Ord_lt_min: "\n. O <- S n" and - Numeral_lt_trans: "\m n. m <- n \ S m <- S n" + Ord_lt_trans: "\m n. m <- n \ S m <- S n" -lemmas Numeral_rules [intro] = Numeral_lt_min Numeral_lt_trans +lemmas Ord_rules [intro] = Ord_lt_min Ord_lt_trans \ \Enables \standard\ to automatically solve inequalities.\ -text "Universe types:" +text "Define the universe types." axiomatization - U :: "Numeral \ Term" ("U _") + U :: "Ord \ Term" where - Universe_hierarchy: "\i j. i <- j \ U(i) : U(j)" + U_hierarchy: "\i j. i <- j \ U(i) : U(j)" and - Universe_cumulative: "\A i j. \A : U(i); i <- j\ \ A : U(j)" - \ \WARNING: \rule Universe_cumulative\ can result in an infinite rewrite loop!\ + U_cumulative: "\A i j. \A : U(i); i <- j\ \ A : U(j)" + \ \WARNING: \rule Universe_cumulative\ can result in an infinite rewrite loop!\ section \Type families\ -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 \ Term, Term, Term] \ prop" ("_: _ \ _") +abbreviation (input) constrained :: "[Term \ Term, Term, Term] \ prop" ("(1_: _ \ _)") where "f: A \ B \ (\x. x : A \ f x : B)" -text "The above is used to define type families, which are just constrained meta-lambdas \P: A \ B\ where \A\ and \B\ are elements of some universe type." +text " + The above is used to define type families, which are constrained meta-lambdas \P: A \ B\ where \A\ and \B\ are small types. +" type_synonym Typefam = "Term \ Term" +section \Named theorems\ + +text " + Named theorems to be used by proof methods later (see HoTT_Methods.thy). + + \wellform\ declares necessary wellformedness conditions for type and inhabitation judgments, while \comp\ 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 diff --git a/Prod.thy b/Prod.thy index fbea4df..8fa73f3 100644 --- a/Prod.thy +++ b/Prod.thy @@ -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 \Constants and syntax\ + axiomatization Prod :: "[Term, Typefam] \ Term" and lambda :: "[Term, Term \ Term] \ Term" and - \ \Application binds tighter than abstraction.\ appl :: "[Term, Term] \ Term" (infixl "`" 60) - - -section \Syntax\ + \ \Application binds tighter than abstraction.\ syntax "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 30) @@ -33,17 +32,18 @@ translations "PROD x:A. B" \ "CONST Prod A (\x. B)" "%%x:A. b" \ "CONST lambda A (\x. b)" +text "Nondependent functions are a special case." + +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 40) + where "A \ B \ \_:A. B" + section \Type rules\ axiomatization where Prod_form: "\i A B. \A : U(i); B: A \ U(i)\ \ \x:A. B x : U(i)" and - Prod_form_cond1: "\i A B. (\x:A. B x : U(i)) \ A : U(i)" -and - Prod_form_cond2: "\i A B. (\x:A. B x : U(i)) \ B: A \ U(i)" -and - Prod_intro: "\i A B b. (\x. x : A \ b x : B x) \ \<^bold>\x:A. b x : \x:A. B x" + Prod_intro: "\i A B b. \A : U(i); \x. x : A \ b x : B x\ \ \<^bold>\x:A. b x : \x:A. B x" and Prod_elim: "\A B f a. \f : \x:A. B x; a : A\ \ f`a : B a" and @@ -51,38 +51,42 @@ and and Prod_uniq: "\A B f. f : \x:A. B x \ \<^bold>\x:A. (f`x) \ f" -text "Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
2.5.2 of the Isabelle/Isar Implementation)." +text " + Note that the syntax \\<^bold>\\ (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \
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 \\x:A. B x : U(i)\ is derivable from some set of premises \, then so are \A : U(i)\ and \B: A \ U(i)\. + + 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 \\x:A. B x : U\ is for \A : U\ and \B: A \ U\ in the first place. -This is what the additional formation rules \Prod_form_cond1\ and \Prod_form_cond2\ express." +axiomatization where + Prod_form_cond1: "\i A B. (\x:A. B x : U(i)) \ A : U(i)" +and + Prod_form_cond2: "\i A B. (\x:A. B x : U(i)) \ B: A \ 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] \ Term" (infixr "\" 40) - where "A \ B \ \_:A. B" - section \Unit type\ axiomatization Unit :: Term ("\") and pt :: Term ("\") and - indUnit :: "[Typefam, Term, Term] \ Term" + indUnit :: "[Typefam, Term, Term] \ Term" ("(1ind\<^sub>\)") where - Unit_form: "\ : U(0)" + Unit_form: "\ : U(O)" and Unit_intro: "\ : \" and - Unit_elim: "\i C c a. \C: \ \ U(i); c : C \; a : \\ \ indUnit C c a : C a" + Unit_elim: "\i C c a. \C: \ \ U(i); c : C \; a : \\ \ ind\<^sub>\ C c a : C a" and - Unit_comp: "\i C c. \C: \ \ U(i); c : C \\ \ indUnit C c \ \ c" + Unit_comp: "\i C c. \C: \ \ U(i); c : C \\ \ ind\<^sub>\ C c \ \ c" lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp lemmas Unit_comps [comp] = Unit_comp diff --git a/Proj.thy b/Proj.thy index f878469..bcef939 100644 --- a/Proj.thy +++ b/Proj.thy @@ -25,10 +25,10 @@ overloading fst_nondep \ fst begin definition fst_dep :: "[Term, Typefam] \ Term" where - "fst_dep A B \ \<^bold>\p: (\x:A. B x). indSum[A,B] (\_. A) (\x y. x) p" + "fst_dep A B \ \<^bold>\p: (\x:A. B x). ind\<^sub>\[A,B] (\_. A) (\x y. x) p" definition fst_nondep :: "[Term, Term] \ Term" where - "fst_nondep A B \ \<^bold>\p: A \ B. indSum[A, \_. B] (\_. A) (\x y. x) p" + "fst_nondep A B \ \<^bold>\p: A \ B. ind\<^sub>\[A, \_. B] (\_. A) (\x y. x) p" end overloading @@ -36,10 +36,10 @@ overloading snd_nondep \ snd begin definition snd_dep :: "[Term, Typefam] \ Term" where - "snd_dep A B \ \<^bold>\p: (\x:A. B x). indSum[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p" + "snd_dep A B \ \<^bold>\p: (\x:A. B x). ind\<^sub>\[A,B] (\q. B (fst[A,B]`q)) (\x y. y) p" definition snd_nondep :: "[Term, Term] \ Term" where - "snd_nondep A B \ \<^bold>\p: A \ B. indSum[A, \_. B] (\_. B) (\x y. y) p" + "snd_nondep A B \ \<^bold>\p: A \ B. ind\<^sub>\[A, \_. B] (\_. B) (\x y. y) p" end @@ -48,15 +48,29 @@ section \Properties\ text "Typing judgments and computation rules for the dependent and non-dependent projection functions." lemma fst_dep_type: assumes "\x:A. B x : U(i)" and "p : \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>\[A, B] (\_. A) (\x y. x)) : (\x:A. B x) \ A" + proof + show "Sum A B : U(i)" by (rule assms) + show "\p. p : Sum A B \ ind\<^sub>\[A, B] (\_. A) (\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 \ U(i)" and "a : A" and "b : B a" shows "fst[A,B]`(a,b) \ a" - unfolding fst_dep_def - by (simplify lems: assms) +unfolding fst_dep_def +proof (subst comp) + show "\x. x : Sum A B \ ind\<^sub>\[A, B] (\_. A) (\x y. x) x : A" by (standard, rule assms(1), assumption+) + show "(a,b) : Sum A B" using assms(2-4) .. + show "ind\<^sub>\[A, B] (\_. A) (\x y. x) (a, b) \ a" + proof + oops \ \ (* Old proof *) proof - diff --git a/Sum.thy b/Sum.thy index 99b4df2..80f8a9c 100644 --- a/Sum.thy +++ b/Sum.thy @@ -10,13 +10,12 @@ theory Sum begin +section \Constants and syntax\ + axiomatization Sum :: "[Term, Typefam] \ Term" and pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and - indSum :: "[Term, Typefam, Typefam, [Term, Term] \ Term, Term] \ Term" ("(1indSum[_,/ _])") - - -section \Syntax\ + indSum :: "[Term, Typefam, Typefam, [Term, Term] \ Term, Term] \ Term" ("(1ind\<^sub>\[_,/ _])") syntax "_SUM" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) @@ -26,15 +25,16 @@ translations "\x:A. B" \ "CONST Sum A (\x. B)" "SUM x:A. B" \ "CONST Sum A (\x. B)" +text "Nondependent pair." + +abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) + where "A \ B \ \_:A. B" + section \Type rules\ axiomatization where Sum_form: "\i A B. \A : U(i); B: A \ U(i)\ \ \x:A. B x : U(i)" -and - Sum_form_cond1: "\i A B. (\x:A. B x : U(i)) \ A : U(i)" -and - Sum_form_cond2: "\i A B. (\x:A. B x : U(i)) \ B: A \ U(i)" and Sum_intro: "\i A B a b. \B: A \ U(i); a : A; b : B a\ \ (a,b) : \x:A. B x" and @@ -42,33 +42,36 @@ and C: \x:A. B x \ U(i); \x y. \x : A; y : B x\ \ f x y : C (x,y); p : \x:A. B x - \ \ indSum[A,B] C f p : C p" + \ \ ind\<^sub>\[A,B] C f p : C p" and Sum_comp: "\i A B C f a b. \ C: \x:A. B x \ U(i); \x y. \x : A; y : B x\ \ f x y : C (x,y); a : A; b : B a - \ \ indSum[A,B] C f (a,b) \ f a b" + \ \ ind\<^sub>\[A,B] C f (a,b) \ f a b" + +text "Admissible inference rules for sum formation:" + +axiomatization where + Sum_form_cond1: "\i A B. (\x:A. B x : U(i)) \ A : U(i)" +and + Sum_form_cond2: "\i A B. (\x:A. B x : U(i)) \ B: A \ 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] \ Term" (infixr "\" 50) - where "A \ B \ \_:A. B" - section \Null type\ axiomatization Null :: Term ("\") and - indNull :: "[Typefam, Term] \ Term" + indNull :: "[Typefam, Term] \ Term" ("(1ind\<^sub>\)") where - Null_form: "\ : U(0)" + Null_form: "\ : U(O)" and - Null_elim: "\i C z. \C: \ \ U(i); z : \\ \ indNull C z : C z" + Null_elim: "\i C z. \C: \ \ U(i); z : \\ \ ind\<^sub>\ C z : C z" lemmas Null_rules [intro] = Null_form Null_elim -- cgit v1.2.3