From 593faab277de53cbe2cb0c2feca5de307d9334ac Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 9 Jun 2018 00:11:39 +0200 Subject: Reorganize code --- Equal.thy | 81 ++++++++++++++++++ HoTT.thy | 248 ------------------------------------------------------ HoTT_Base.thy | 52 ++++++++++++ HoTT_Theorems.thy | 53 ++++++++++-- Prod.thy | 48 +++++++++++ Sum.thy | 78 +++++++++++++++++ 6 files changed, 303 insertions(+), 257 deletions(-) create mode 100644 Equal.thy delete mode 100644 HoTT.thy create mode 100644 HoTT_Base.thy create mode 100644 Prod.thy create mode 100644 Sum.thy diff --git a/Equal.thy b/Equal.thy new file mode 100644 index 0000000..b9f676f --- /dev/null +++ b/Equal.thy @@ -0,0 +1,81 @@ +theory Equal + imports HoTT_Base Prod + +begin + +subsection \Equality type\ + + axiomatization + Equal :: "[Term, Term, Term] \ Term" + + syntax + "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100) + "_EQUAL_ASCII" :: "[Term, Term, Term] \ Term" ("(3_ =[_]/ _)" [101, 0, 101] 100) + translations + "a =[A] b" \ "CONST Equal A a b" + "a =\<^sub>A b" \ "CONST Equal A a b" + + axiomatization + refl :: "Term \ Term" ("(refl'(_'))") and + indEqual :: "[Term, [Term, Term, Term] \ Term] \ Term" ("(indEqual[_])") + where + Equal_form: "\A a b::Term. \A : U; a : A; b : A\ \ a =\<^sub>A b : U" + (* Should I write a permuted version \\A : U; b : A; a : A\ \ \\? *) + and + Equal_intro [intro]: "\A x::Term. x : A \ refl(x) : x =\<^sub>A x" + and + Equal_elim [elim]: + "\(A::Term) (C::[Term, Term, Term] \ Term) (f::Term) (a::Term) (b::Term) (p::Term). + \ \x y::Term. \x : A; y : A\ \ C(x)(y): x =\<^sub>A y \ U; + f : \x:A. C(x)(x)(refl(x)); + a : A; + b : A; + p : a =\<^sub>A b \ + \ indEqual[A](C)`f`a`b`p : C(a)(b)(p)" + and + Equal_comp [simp]: + "\(A::Term) (C::[Term, Term, Term] \ Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \ f`a" + + lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2] + + subsubsection \Properties of equality\ + + text "Symmetry/Path inverse" + + definition inv :: "[Term, Term, Term] \ Term" ("(1inv[_,/ _,/ _])") + where "inv[A,x,y] \ indEqual[A](\x y _. y =\<^sub>A x)`(\<^bold>\x:A. refl(x))`x`y" + + lemma inv_comp: "\A a::Term. a : A \ inv[A,a,a]`refl(a) \ refl(a)" unfolding inv_def by simp + + text "Transitivity/Path composition" + + \ \"Raw" composition function\ + definition compose' :: "Term \ Term" ("(1compose''[_])") + where "compose'[A] \ indEqual[A](\x y _. \z:A. \q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\x z _. x =\<^sub>A z)`(\<^bold>\x:A. refl(x)))" + + \ \"Natural" composition function\ + abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compose[_,/ _,/ _,/ _])") + where "compose[A,x,y,z] \ \<^bold>\p:x =\<^sub>A y. \<^bold>\q:y =\<^sub>A z. compose'[A]`x`y`p`z`q" + + (**** GOOD CANDIDATE FOR AUTOMATION ****) + lemma compose_comp: + assumes "a : A" + shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" using assms Equal_intro[OF assms] unfolding compose'_def by simp + + text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \using\ clause in the proof. + This would likely involve something like: + 1. Recognizing that there is a function application that can be simplified. + 2. Noting that the obstruction to applying \Prod_comp\ is the requirement that \refl(a) : a =\<^sub>A a\. + 3. Obtaining such a condition, using the known fact \a : A\ and the introduction rule \Equal_intro\." + + lemmas Equal_simps [simp] = inv_comp compose_comp + + subsubsection \Pretty printing\ + + abbreviation inv_pretty :: "[Term, Term, Term, Term] \ Term" ("(1_\<^sup>-\<^sup>1[_, _, _])" 500) + where "p\<^sup>-\<^sup>1[A,x,y] \ inv[A,x,y]`p" + + abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \ Term" ("(1_ \[_, _, _, _]/ _)") + where "p \[A,x,y,z] q \ compose[A,x,y,z]`p`q" + +end \ No newline at end of file diff --git a/HoTT.thy b/HoTT.thy deleted file mode 100644 index cfb29df..0000000 --- a/HoTT.thy +++ /dev/null @@ -1,248 +0,0 @@ -theory HoTT - imports Pure -begin - -section \Setup\ -text "For ML files, routines and setup." - -section \Basic definitions\ -text "A single meta-level type \Term\ suffices to implement the object-level types and terms. -We do not implement universes, but simply follow the informal notation in the HoTT book." - -typedecl Term - -section \Judgments\ - -consts - is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) - is_of_type :: "[Term, Term] \ prop" ("(3_ :/ _)" [0, 0] 1000) - -section \Definitional equality\ -text "We take the meta-equality \\\, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory. - -Note that the Pure framework already provides axioms and results for various properties of \\\, which we make use of and extend where necessary." - -theorem equal_types: - assumes "A \ B" and "A : U" - shows "B : U" using assms by simp - -theorem equal_type_element: - assumes "A \ B" and "x : A" - shows "x : B" using assms by simp - -lemmas type_equality [intro, simp] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] - -section \Type families\ -text "Type families are implemented using meta-level lambda expressions \P::Term \ Term\ that further satisfy the following property." - -abbreviation is_type_family :: "[Term \ Term, Term] \ prop" ("(3_:/ _ \ U)") - where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" - -section \Types\ - -subsection \Dependent function/product\ - -axiomatization - Prod :: "[Term, Term \ Term] \ Term" and - lambda :: "[Term, Term \ Term] \ Term" -syntax - "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 30) - "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 30) - "_PROD_ASCII" :: "[idt, Term, Term] \ Term" ("(3PROD _:_./ _)" 30) - "_LAMBDA_ASCII" :: "[idt, Term, Term] \ Term" ("(3%%_:_./ _)" 30) -translations - "\x:A. B" \ "CONST Prod A (\x. B)" - "\<^bold>\x:A. b" \ "CONST lambda A (\x. b)" - "PROD x:A. B" \ "CONST Prod A (\x. B)" - "%%x:A. b" \ "CONST lambda A (\x. b)" - (* The above syntax translations bind the x in the expressions B, b. *) - -abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 40) - where "A\B \ \_:A. B" - -axiomatization - appl :: "[Term, Term] \ Term" (infixl "`" 60) -where - Prod_form: "\(A::Term) (B::Term \ Term). \A : U; B : A \ U\ \ \x:A. B(x) : U" -and - Prod_intro [intro]: - "\(A::Term) (B::Term \ Term) (b::Term \ Term). (\x::Term. x : A \ b(x) : B(x)) \ \<^bold>\x:A. b(x) : \x:A. B(x)" -and - Prod_elim [elim]: - "\(A::Term) (B::Term \ Term) (f::Term) (a::Term). \f : \x:A. B(x); a : A\ \ f`a : B(a)" -and - Prod_comp [simp]: "\(A::Term) (b::Term \ Term) (a::Term). a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" -and - Prod_uniq [simp]: "\A f::Term. \<^bold>\x:A. (f`x) \ f" - -lemmas Prod_formation [intro] = Prod_form Prod_form[rotated] - -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)." - -subsection \Dependent pair/sum\ - -axiomatization - Sum :: "[Term, Term \ Term] \ Term" -syntax - "_SUM" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) - "_SUM_ASCII" :: "[idt, Term, Term] \ Term" ("(3SUM _:_./ _)" 20) -translations - "\x:A. B" \ "CONST Sum A (\x. B)" - "SUM x:A. B" \ "CONST Sum A (\x. B)" - -abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) - where "A\B \ \_:A. B" - -axiomatization - pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and - indSum :: "(Term \ Term) \ Term" -where - Sum_form: "\(A::Term) (B::Term \ Term). \A : U; B: A \ U\ \ \x:A. B(x) : U" -and - Sum_intro [intro]: - "\(A::Term) (B::Term \ Term) (a::Term) (b::Term). \a : A; b : B(a)\ \ (a, b) : \x:A. B(x)" -and - Sum_elim [elim]: - "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term) (p::Term). - \C: \x:A. B(x) \ U; f : \x:A. \y:B(x). C((x,y)); p : \x:A. B(x)\ \ indSum(C)`f`p : C(p)" -and - Sum_comp [simp]: "\(C::Term \ Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \ f`a`b" - -lemmas Sum_formation [intro] = Sum_form Sum_form[rotated] - -text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible. -Hence only the type family \C\ is left as a meta-level argument to the inductor indSum." - -subsubsection \Projections\ - -consts - fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") - snd :: "[Term, 'a] \ Term" ("(1snd[/_,/ _])") -overloading - fst_dep \ fst - snd_dep \ snd - fst_nondep \ fst - snd_nondep \ snd -begin -definition fst_dep :: "[Term, Term \ Term] \ Term" where - "fst_dep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B(x). x)" - -definition snd_dep :: "[Term, Term \ Term] \ Term" where - "snd_dep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B(x). y)" - -definition fst_nondep :: "[Term, Term] \ Term" where - "fst_nondep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B. x)" - -definition snd_nondep :: "[Term, Term] \ Term" where - "snd_nondep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B. y)" -end - -lemma fst_dep_comp: "\a : A; b : B(a)\ \ fst[A,B]`(a,b) \ a" unfolding fst_dep_def by simp -lemma snd_dep_comp: "\a : A; b : B(a)\ \ snd[A,B]`(a,b) \ b" unfolding snd_dep_def by simp - -lemma fst_nondep_comp: "\a : A; b : B\ \ fst[A,B]`(a,b) \ a" unfolding fst_nondep_def by simp -lemma snd_nondep_comp: "\a : A; b : B\ \ snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by simp - -\ \Simplification rules for projections\ -lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp - -subsection \Equality type\ - -axiomatization - Equal :: "[Term, Term, Term] \ Term" -syntax - "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)" [101, 101] 100) - "_EQUAL_ASCII" :: "[Term, Term, Term] \ Term" ("(3_ =[_]/ _)" [101, 101] 100) -translations - "a =\<^sub>A b" \ "CONST Equal A a b" - "a =[A] b" \ "CONST Equal A a b" - -axiomatization - refl :: "Term \ Term" ("(refl'(_'))") and - indEqual :: "[Term, [Term, Term, Term] \ Term] \ Term" ("(indEqual[_])") -where - Equal_form: "\A a b::Term. \A : U; a : A; b : A\ \ a =\<^sub>A b : U" - (* Should I write a permuted version \\A : U; b : A; a : A\ \ \\? *) -and - Equal_intro [intro]: "\A x::Term. x : A \ refl(x) : x =\<^sub>A x" -and - Equal_elim [elim]: - "\(A::Term) (C::[Term, Term, Term] \ Term) (f::Term) (a::Term) (b::Term) (p::Term). - \ \x y::Term. \x : A; y : A\ \ C(x)(y): x =\<^sub>A y \ U; - f : \x:A. C(x)(x)(refl(x)); - a : A; - b : A; - p : a =\<^sub>A b \ - \ indEqual[A](C)`f`a`b`p : C(a)(b)(p)" -and - Equal_comp [simp]: - "\(A::Term) (C::[Term, Term, Term] \ Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \ f`a" - -lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2] - -subsubsection \Properties of equality\ - -text "Symmetry/Path inverse" - -definition inv :: "[Term, Term, Term] \ Term" ("(1inv[_,/ _,/ _])") - where "inv[A,x,y] \ indEqual[A](\x y _. y =\<^sub>A x)`(\<^bold>\x:A. refl(x))`x`y" - -lemma inv_comp: "\A a::Term. a : A \ inv[A,a,a]`refl(a) \ refl(a)" unfolding inv_def by simp - -text "Transitivity/Path composition" - -\ \"Raw" composition function\ -abbreviation compose' :: "Term \ Term" ("(1compose''[_])") - where "compose'[A] \ indEqual[A](\x y _. \z:A. \q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\x z _. x =\<^sub>A z)`(\<^bold>\x:A. refl(x)))" - -\ \"Natural" composition function\ -abbreviation compose :: "[Term, Term, Term, Term] \ Term" ("(1compose[_,/ _,/ _,/ _])") - where "compose[A,x,y,z] \ \<^bold>\p:x =\<^sub>A y. \<^bold>\q:y =\<^sub>A z. compose'[A]`x`y`p`z`q" - -(**** GOOD CANDIDATE FOR AUTOMATION ****) -lemma compose_comp: - assumes "a : A" - shows "compose[A,a,a,a]`refl(a)`refl(a) \ refl(a)" using assms Equal_intro[OF assms] by simp - -text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \using\ clause in the proof. -This would likely involve something like: - 1. Recognizing that there is a function application that can be simplified. - 2. Noting that the obstruction to applying \Prod_comp\ is the requirement that \refl(a) : a =\<^sub>A a\. - 3. Obtaining such a condition, using the known fact \a : A\ and the introduction rule \Equal_intro\." - -lemmas Equal_simps [simp] = inv_comp compose_comp - -subsubsection \Pretty printing\ - -abbreviation inv_pretty :: "[Term, Term, Term, Term] \ Term" ("(1_\<^sup>-\<^sup>1\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_)" 500) - where "p\<^sup>-\<^sup>1\<^sub>A\<^sub>,\<^sub>x\<^sub>,\<^sub>y \ inv[A,x,y]`p" - -abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \ Term" ("(1_ \\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_\<^sub>,\<^sub>_/ _)") - where "p \\<^sub>A\<^sub>,\<^sub>x\<^sub>,\<^sub>y\<^sub>,\<^sub>z q \ compose[A,x,y,z]`p`q" - -end - -(* -subsubsection \Empty type\ - -axiomatization - Null :: Term and - ind_Null :: "Term \ Term \ Term" ("(ind'_Null'(_,/ _'))") -where - Null_form: "Null : U" and - Null_elim: "\C x a. \x : Null \ C(x) : U; a : Null\ \ ind_Null(C(x), a) : C(a)" - -subsubsection \Natural numbers\ - -axiomatization - Nat :: Term and - zero :: Term ("0") and - succ :: "Term \ Term" and (* how to enforce \succ : Nat\Nat\? *) - ind_Nat :: "Term \ Term \ Term \ Term \ Term" -where - Nat_form: "Nat : U" and - Nat_intro1: "0 : Nat" and - Nat_intro2: "\n. n : Nat \ succ n : Nat" - (* computation rules *) - -*) \ No newline at end of file diff --git a/HoTT_Base.thy b/HoTT_Base.thy new file mode 100644 index 0000000..9650c4c --- /dev/null +++ b/HoTT_Base.thy @@ -0,0 +1,52 @@ +(* Title: HoTT/HoTT_Base.thy + Author: Josh Chen + +Basic setup and definitions of a homotopy type theory object logic. +*) + +theory HoTT_Base + imports Pure + +begin + +section \Basic definitions\ + +text "A single meta-level type \Term\ suffices to implement the object-level types and terms. +We do not implement universes, but simply follow the informal notation in the HoTT book." + +typedecl Term + +section \Judgments\ + +consts +is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) +is_of_type :: "[Term, Term] \ prop" ("(3_ :/ _)" [0, 0] 1000) + + +section \Definitional equality\ + +text "We use the Pure equality \\\ for definitional/judgmental equality of types and terms in our theory." + +theorem equal_types: + assumes "A \ B" and "A : U" + shows "B : U" using assms by simp + +theorem equal_type_element: + assumes "A \ B" and "x : A" + shows "x : B" using assms by simp + +lemmas type_equality [intro, simp] = + equal_types + equal_types[rotated] + equal_type_element + equal_type_element[rotated] + + +section \Type families\ + +text "A type family is a meta lambda term \P :: Term \ Term\ that further satisfies the following property." + +abbreviation is_type_family :: "[Term \ Term, Term] \ prop" ("(3_:/ _ \ U)") + where "P: A \ U \ (\x. x : A \ P(x) : U)" + +end \ No newline at end of file diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index f05363a..95f1d0c 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -6,13 +6,13 @@ text "A bunch of theorems and other statements for sanity-checking, as well as t Things that *should* be automated: \ Checking that \A\ is a well-formed type, when writing things like \x : A\ and \A : U\. - \ Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair? -" + \ Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?" \ \Turn on trace for unification and the simplifier, for debugging.\ declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=1]] -section \Functions\ + +section \\ type\ subsection \Typing functions\ @@ -35,6 +35,7 @@ proof then show "\<^bold>\y:B. a : B \ A" .. qed + subsection \Function application\ proposition "a : A \ (\<^bold>\x:A. x)`a \ a" by simp @@ -47,7 +48,10 @@ lemma "a : A \ (\<^bold>\x:A. \<^bold>\y:B(x). f lemma "\a : A; b : B(a); c : C(a)(b)\ \ (\<^bold>\x:A. \<^bold>\y:B(x). \<^bold>\z:C(x)(y). f x y z)`a`b`c \ f a b c" by simp -proposition wellformed_currying: + +subsection \Currying functions\ + +proposition curried_function_formation: fixes A::Term and B::"Term \ Term" and @@ -67,7 +71,7 @@ proof qed (rule assms) (**** GOOD CANDIDATE FOR AUTOMATION - EISBACH! ****) -proposition triply_curried: +proposition higher_order_currying_formation: fixes A::Term and B::"Term \ Term" and @@ -94,7 +98,8 @@ proof qed qed (rule assms) -lemma curried_type: +(**** AND PROBABLY THIS TOO? ****) +lemma curried_type_judgment: fixes a b A::Term and B::"Term \ Term" and @@ -115,6 +120,9 @@ qed text "Note that the propositions and proofs above often say nothing about the well-formedness of the types, or the well-typedness of the lambdas involved; one has to be very explicit and prove such things separately! This is the result of the choices made regarding the premises of the type rules." + +section \\ type\ + text "The following shows that the dependent sum inductor has the type we expect it to have:" lemma @@ -126,7 +134,7 @@ proof - "P \ \x:A. B(x)" have "\<^bold>\f:F. \<^bold>\p:P. indSum(C)`f`p : \f:F. \p:P. C(p)" - proof (rule curried_type) + proof (rule curried_type_judgment) fix f p::Term assume "f : F" and "p : P" with assms show "indSum(C)`f`p : C(p)" unfolding F_def P_def .. @@ -135,15 +143,42 @@ proof - then show "indSum(C) : \f:F. \p:P. C(p)" by simp qed +(**** AUTOMATION CANDIDATE ****) +text "Propositional uniqueness principle for dependent sums:" + +text "We would like to eventually automate proving that 'a given type \A\ is inhabited', i.e. search for an element \a:A\. + +A good starting point would be to automate the application of elimination rules." + +notepad begin + +fix A B assume "A : U" and "B: A \ U" + +define C where "C \ \p. p =[\x:A. B(x)] (fst[A,B]`p, snd[A,B]`p)" +have *: "C: \x:A. B(x) \ U" +proof - + fix p assume "p : \x:A. B(x)" + have "(fst[A,B]`p, snd[A,B]`p) : \x:A. B(x)" + +define f where "f \ \<^bold>\x:A. \<^bold>\y:B(x). refl((x,y))" +have "f`x`y : C((x,y))" +sorry + +have "p : \x:A. B(x) \ indSum(C)`f`p : C(p)" using * ** by (rule Sum_elim) + +end + +section \Universes and polymorphism\ + text "Polymorphic identity function." consts Ui::Term definition Id where "Id \ \<^bold>\A:Ui. \<^bold>\x:A. x" -(* Have to think about universes... *) + (* -section \Nats\ +section \Natural numbers\ text "Here's a dumb proof that 2 is a natural number." diff --git a/Prod.thy b/Prod.thy new file mode 100644 index 0000000..9ecab4d --- /dev/null +++ b/Prod.thy @@ -0,0 +1,48 @@ +(* Title: HoTT/Prod.thy + Author: Josh Chen + +Dependent product (function) type for the HoTT logic. +*) + +theory Prod + imports HoTT_Base + +begin + +axiomatization + Prod :: "[Term, Term \ Term] \ Term" and + lambda :: "[Term, Term \ Term] \ Term" and + appl :: "[Term, Term] \ Term" (infixl "`" 60) + +syntax + "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 30) + "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 30) + "_PROD_ASCII" :: "[idt, Term, Term] \ Term" ("(3PROD _:_./ _)" 30) + "_LAMBDA_ASCII" :: "[idt, Term, Term] \ Term" ("(3%%_:_./ _)" 30) + +\ \The translations below bind the variable \x\ in the expressions \B\ and \b\.\ +translations + "\x:A. B" \ "CONST Prod A (\x. B)" + "\<^bold>\x:A. b" \ "CONST lambda A (\x. b)" + "PROD x:A. B" \ "CONST Prod A (\x. B)" + "%%x:A. b" \ "CONST lambda A (\x. b)" + +\ \Type rules\ +axiomatization where + Prod_form [intro]: "\A B. \A : U; B : A \ U\ \ \x:A. B(x) : U" +and + Prod_intro [intro]: "\A B b. (\x. x : A \ b(x) : B(x)) \ \<^bold>\x:A. b(x) : \x:A. B(x)" +and + Prod_elim [elim]: "\A B f a. \f : \x:A. B(x); a : A\ \ f`a : B(a)" +and + Prod_comp [simp]: "\A b a. a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" +and + Prod_uniq [simp]: "\A f. \<^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)." + +\ \Nondependent functions are a special case.\ +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 40) + where "A \ B \ \_:A. B" + +end \ No newline at end of file diff --git a/Sum.thy b/Sum.thy new file mode 100644 index 0000000..e34749a --- /dev/null +++ b/Sum.thy @@ -0,0 +1,78 @@ +(* Title: HoTT/Sum.thy + Author: Josh Chen + +Dependent sum type. +*) + +theory Sum + imports HoTT_Base Prod + +begin + +axiomatization + Sum :: "[Term, Term \ Term] \ Term" and + pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and + indSum :: "(Term \ Term) \ Term" + +syntax + "_SUM" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) + "_SUM_ASCII" :: "[idt, Term, Term] \ Term" ("(3SUM _:_./ _)" 20) + +translations + "\x:A. B" \ "CONST Sum A (\x. B)" + "SUM x:A. B" \ "CONST Sum A (\x. B)" + +axiomatization where + Sum_form [intro]: "\A B. \A : U; B: A \ U\ \ \x:A. B(x) : U" +and + Sum_intro [intro]: "\A B a b. \a : A; b : B(a)\ \ (a, b) : \x:A. B(x)" +and + Sum_elim [elim]: "\A B C f p. + \ C: \x:A. B(x) \ U; + f : \x:A. \y:B(x). C((x,y)); + p : \x:A. B(x) \ \ indSum(C)`f`p : C(p)" +and + Sum_comp [simp]: "\(C::Term \ Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \ f`a`b" + +text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible. +Hence only the type family \C\ is left as a meta-level argument to the inductor indSum." + +\ \Nondependent pair\ +abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) + where "A\B \ \_:A. B" + +subsubsection \Projections\ + +consts + fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") + snd :: "[Term, 'a] \ Term" ("(1snd[/_,/ _])") + +overloading + fst_dep \ fst + snd_dep \ snd + fst_nondep \ fst + snd_nondep \ snd +begin + definition fst_dep :: "[Term, Term \ Term] \ Term" where + "fst_dep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B(x). x)" + + definition snd_dep :: "[Term, Term \ Term] \ Term" where + "snd_dep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B(x). y)" + + definition fst_nondep :: "[Term, Term] \ Term" where + "fst_nondep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B. x)" + + definition snd_nondep :: "[Term, Term] \ Term" where + "snd_nondep A B \ indSum(\_. A)`(\<^bold>\x:A. \<^bold>\y:B. y)" +end + +text "Simplification rules for the projections:" + +lemma fst_dep_comp: "\a : A; b : B(a)\ \ fst[A,B]`(a,b) \ a" unfolding fst_dep_def by simp +lemma snd_dep_comp: "\a : A; b : B(a)\ \ snd[A,B]`(a,b) \ b" unfolding snd_dep_def by simp + +lemma fst_nondep_comp: "\a : A; b : B\ \ fst[A,B]`(a,b) \ a" unfolding fst_nondep_def by simp +lemma snd_nondep_comp: "\a : A; b : B\ \ snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by simp + +lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp +end \ No newline at end of file -- cgit v1.2.3