From 80412abb0fdec553d80a56af16d1cfd8da52e7ed Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 5 Jun 2018 17:35:49 +0200 Subject: Proved that the inductor on Sum has the correct type. --- HoTT.thy | 48 ++++++++++++++++++++++------------ HoTT_Theorems.thy | 77 ++++++++++++++++++++++++++++++++++++------------------- 2 files changed, 81 insertions(+), 44 deletions(-) diff --git a/HoTT.thy b/HoTT.thy index 68de364..ef39734 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -46,14 +46,14 @@ axiomatization Prod :: "[Term, Term \ Term] \ Term" and lambda :: "[Term, Term \ Term] \ Term" syntax - "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) - "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 10) + "_PROD" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 30) + "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 30) translations "\x:A. B" \ "CONST Prod A (\x. B)" "\<^bold>\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 "\" 30) +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 10) where "A\B \ \_:A. B" axiomatization @@ -69,7 +69,7 @@ where 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::Term) (f::Term). \<^bold>\x:A. (f`x) \ f" + Prod_uniq [simp]: "\A f::Term. \<^bold>\x:A. (f`x) \ f" lemmas Prod_formation = Prod_form Prod_form[rotated] @@ -80,7 +80,7 @@ subsubsection \Dependent pair/sum\ axiomatization Sum :: "[Term, Term \ Term] \ Term" syntax - "_Sum" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) + "_Sum" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) translations "\x:A. B" \ "CONST Sum A (\x. B)" @@ -89,7 +89,7 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) axiomatization pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and - indSum :: "[Term \ Term] \ Term" + indSum :: "(Term \ Term) \ Term" where Sum_form: "\(A::Term) (B::Term \ Term). \A : U; B: A \ U\ \ \x:A. B(x) : U" and @@ -97,9 +97,9 @@ where \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 + \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" + Sum_comp [simp]: "\(C::Term \ Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \ f`a`b" lemmas Sum_formation = Sum_form Sum_form[rotated] @@ -118,16 +118,16 @@ overloading 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)" + "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)" + "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)" + "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)" + "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 @@ -136,18 +136,32 @@ lemma snd_dep_comp: "\a : A; b : B(a)\ \ snd[A,B 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 Sum\ +\ \Simplification rules for projections\ lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp subsubsection \Equality type\ axiomatization - Equal :: "Term \ Term \ Term \ Term" ("(_ =_ _)") and - refl :: "Term \ Term" ("(refl'(_'))") + Equal :: "[Term, Term, Term] \ Term" +syntax + "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)") +translations + "a =\<^sub>A b" \ "CONST Equal A a b" + +axiomatization + refl :: "Term \ Term" and + indEqual :: "([Term, Term, Term] \ Term) \ Term" where - Equal_form: "\A a b. \a : A; b : A\ \ a =A b : U" and - Equal_intro: "\A x. x : A \ refl x : x =A x" + Equal_form: "\A a b::Term. \A : U; a : A; b : A\ \ a =\<^sub>A b : U" and + + Equal_intro [intro]: "\A x::Term. x : A \ refl(x) : x =\<^sub>A x" + +(* and + + Equal_elim [elim]: "\(C::[Term, Term, Term] \ Term) (f::Term) (x::Term) (y::Term) (p::Term). + \\ \ (indEqual C)`f`x`y`p : C(x)(y)(p)" +*) (* subsubsection \Empty type\ diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index a44c8f9..1ac4484 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -21,19 +21,19 @@ text "Declaring \Prod_intro\ with the \intro\ attribut lemma "\<^bold>\x:A. x : A\A" .. proposition "A \ B \ \<^bold>\x:A. x : B\A" - proof - - assume assm: "A \ B" - have id: "\<^bold>\x:A. x : A\A" .. - from assm have "A\A \ B\A" by simp - with id show "\<^bold>\x:A. x : B\A" .. - qed +proof - + assume assm: "A \ B" + have id: "\<^bold>\x:A. x : A\A" .. + from assm have "A\A \ B\A" by simp + with id show "\<^bold>\x:A. x : B\A" .. +qed proposition "\<^bold>\x:A. \<^bold>\y:B. x : A\B\A" - proof - fix a - assume "a : A" - then show "\<^bold>\y:B. a : B \ A" .. - qed +proof + fix a + assume "a : A" + then show "\<^bold>\y:B. a : B \ A" .. +qed subsection \Function application\ @@ -61,9 +61,9 @@ proof (rule Prod_formation) fix x::Term assume *: "x : A" show "\y:B(x). C x y : U" - proof (rule Prod_formation) - show "B(x) : U" using * by (rule assms) - qed (rule assms) + proof (rule Prod_formation) + show "B(x) : U" using * by (rule assms) + qed (rule assms) qed (rule assms) proposition triply_curried: @@ -81,36 +81,59 @@ proposition triply_curried: proof (rule Prod_formation) fix x::Term assume 1: "x : A" show "\y:B(x). \z:C(x)(y). D(x)(y)(z) : U" + proof (rule Prod_formation) + show "B(x) : U" using 1 by (rule assms) + + fix y::Term assume 2: "y : B(x)" + show "\z:C(x)(y). D(x)(y)(z) : U" proof (rule Prod_formation) - show "B(x) : U" using 1 by (rule assms) - - fix y::Term assume 2: "y : B(x)" - show "\z:C(x)(y). D(x)(y)(z) : U" - proof (rule Prod_formation) - show "C x y : U" using 2 by (rule assms) - show "\z::Term. z : C(x)(y) \ D(x)(y)(z) : U" by (rule assms) - qed + show "C x y : U" using 2 by (rule assms) + show "\z::Term. z : C(x)(y) \ D(x)(y)(z) : U" by (rule assms) qed + qed qed (rule assms) -lemma +lemma curried_type: fixes a b A::Term and B::"Term \ Term" and f C::"[Term, Term] \ Term" - assumes "\x y::Term. f x y : C x y" + assumes "\x y::Term. \x : A; y : B(x)\ \ f x y : C x y" shows "\<^bold>\x:A. \<^bold>\y:B(x). f x y : \x:A. \y:B(x). C x y" proof fix x::Term + assume *: "x : A" show "\<^bold>\y:B(x). f x y : \y:B(x). C x y" - proof - show "\y. f x y : C x y" by (rule assms) - qed + proof + fix y::Term + assume **: "y : B(x)" + show "f x y : C x y" using * ** by (rule assms) + qed 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." +text "The following shows that the dependent sum inductor has the type we expect it to have:" + +lemma + assumes "C: \x:A. B(x) \ U" + shows "indSum(C) : \f:(\x:A. \y:B(x). C((x,y))). \p:(\x:A. B(x)). C(p)" +proof - + define F and P where + "F \ \x:A. \y:B(x). C((x,y))" and + "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) + fix f p::Term + assume "f : F" and "p : P" + with assms show "indSum(C)`f`p : C(p)" unfolding F_def P_def .. + qed + + then show "indSum(C) : \f:F. \p:P. C(p)" by simp +qed + text "Polymorphic identity function." consts Ui::Term -- cgit v1.2.3