From c087ad35ac9365cad99b022e138348fb68bc9215 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 4 Jun 2018 19:38:01 +0200 Subject: Prod_comp should have a type constraint. This also fixes a false proof for the dependent sum projection functions. --- HoTT.thy | 53 +++++++++++++++++++++++++++++++---------------------- 1 file changed, 31 insertions(+), 22 deletions(-) (limited to 'HoTT.thy') diff --git a/HoTT.thy b/HoTT.thy index 8c9fa20..cf8b157 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -21,7 +21,7 @@ consts subsection \Type families\ -text "Type families are implemented as meta-level lambda terms of type \Term \ Term\ that further satisfy the following property." +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)" @@ -46,12 +46,12 @@ subsection \Basic types\ subsubsection \Dependent function/product\ -consts - Prod :: "[Term, Term \ Term] \ Term" +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\_:_./ _)" 10) + "_LAMBDA" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 10) translations "\x:A. B" \ "CONST Prod A (\x. B)" "\<^bold>\x:A. b" \ "CONST lambda A (\x. b)" @@ -71,17 +71,20 @@ where 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). (\<^bold>\x:A. b(x))`a \ b(a)" and + Prod_comp: "\(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: "\(A::Term) (f::Term). \<^bold>\x:A. (f`x) \ f" lemmas Prod_formation = Prod_form Prod_form[rotated] +\ \Simplification rules for Prod\ +lemmas Prod_simp [simp] = Prod_comp Prod_uniq + 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)." subsubsection \Dependent pair/sum\ -consts +axiomatization Sum :: "[Term, Term \ Term] \ Term" syntax "_Sum" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) @@ -93,33 +96,39 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) axiomatization pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and - indSum :: "[Term \ Term, [Term, Term] \ 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 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, Term] \ Term) (p::Term). - \C: \x:A. B(x) \ U; \x y::Term. \x : A; y : B(x)\ \ f x y : C((x,y)); p : \x:A. B(x)\ \ (indSum C f p) : C(p)" 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, Term] \ Term) (a::Term) (b::Term). (indSum C f (a,b)) \ f a b" + Sum_comp: "\(C::Term \ Term) (f::Term) (a::Term) (b::Term). (* ADD CONSTRAINTS HERE *) + (indSum C)`f`(a,b) \ f`a`b" lemmas Sum_formation = Sum_form Sum_form[rotated] -definition fst :: "[Term, [Term, Term] \ Term] \ (Term \ Term)" ("(1fst[/_,/ _])") - where "fst[A, B] \ indSum (\_. A) (\a. \b. a)" +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." + +\ \Projection functions\ + +definition fst :: "[Term, Term \ Term] \ Term" ("(1fst[/_,/ _])") + where "fst[A, B] \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B(x). x)" + +definition snd :: "[Term, Term \ Term] \ Term" ("(1snd[/_,/ _])") + where "snd[A, B] \ (indSum (\_. A))`(\<^bold>\x:A. \<^bold>\y:B(x). y)" -lemma "fst[A, B](a,b) \ a" unfolding fst_def by simp +lemma fst_comp: "\a : A; b : B(a)\ \ fst[A,B]`(a,b) \ a" unfolding fst_def by (simp add: Sum_comp) +lemma snd_comp: "\a : A; b : B(a)\ \ snd[A,B]`(a,b) \ b" unfolding snd_def by (simp add: Sum_comp) -text "A choice had to be made for the elimination rule: we formalize the function \f\ taking \a : A\ and \b : B(x)\ and returning \C((a,b))\ as a meta level \f::Term \ Term\ instead of an object logic dependent function \f : \x:A. B(x)\. -However we should be able to later show the equivalence of the formalizations." +\ \Simplification rules for Sum\ +lemmas Sum_simp [simp] = Sum_comp fst_comp snd_comp -\ \Projection onto first component\ -(* -definition proj1 :: "Term \ Term \ Term" ("(proj1\_,_\)") where - "\A B x y. proj1\A,B\ \ rec_Product(A, B, A, \<^bold>\x:A. \<^bold>\y:B. (\x. x))" -*) +lemma "\a : A; b : B(a)\ \ fst[A,B]`(a,b) : A" by simp subsubsection \Empty type\ -- cgit v1.2.3