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 +++++++++++++++++++++++++++++++---------------------- HoTT_Theorems.thy | 52 ++++++++++++++++++++++++++++++++++++++-------------- 2 files changed, 69 insertions(+), 36 deletions(-) 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\ diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 5922b51..aeddf9f 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -16,7 +16,7 @@ section \Functions\ subsection \Typing functions\ -text "Declaring \Prod_intro\ with the \intro\ attribute (in HoTT.thy) enables \standard\ to prove the following." +text "Declaring \Prod_intro\ with the \intro\ attribute (in HoTT.thy) enables \standard\ to prove the following." lemma "\<^bold>\x:A. x : A\A" .. @@ -41,9 +41,9 @@ proposition "a : A \ (\<^bold>\x:A. x)`a \ a" by text "Currying:" -lemma "(\<^bold>\x:A. \<^bold>\y:B. f x y)`a \ \<^bold>\y:B. f a y" by simp +lemma "a : A \ (\<^bold>\x:A. \<^bold>\y:B(x). f x y)`a \ \<^bold>\y:B(a). f a y" by simp -lemma "(\<^bold>\x:A. \<^bold>\y:B. \<^bold>\z:C. f x y z)`a`b`c \ f a b c" by simp +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: fixes @@ -56,29 +56,53 @@ proposition wellformed_currying: "\x::Term. C(x): B(x) \ U" shows "\x:A. \y:B(x). C x y : U" proof (rule Prod_formation) - show "\x::Term. x : A \ \y:B(x). C x y : U" + fix x::Term + assume *: "x : A" + show "\y:B(x). C x y : U" proof (rule Prod_formation) - fix x y::Term - assume "x : A" - show "y : B x \ C x y : U" by (rule assms(3)) - qed (rule assms(2)) -qed (rule assms(1)) + show "B(x) : U" using * by (rule assms) + qed (rule assms) +qed (rule assms) + +proposition triply_curried: + fixes + A::Term and + B::"Term \ Term" and + C::"[Term, Term] \ Term" and + D::"[Term, Term, Term] \ Term" + assumes + "A : U" and + "B: A \ U" and + "\x y::Term. y : B(x) \ C(x)(y) : U" and + "\x y z::Term. z : C(x)(y) \ D(x)(y)(z) : U" + shows "\x:A. \y:B(x). \z:C(x)(y). D(x)(y)(z) : U" +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 "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 fixes a b A::Term and B::"Term \ Term" and f C::"[Term, Term] \ Term" - assumes "\x y::Term. \x : A; y : B(x)\ \ f x y : C x y" + assumes "\x y::Term. 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 - fix y::Term - assume **: "y : B(x)" - show "f x y : C x y" by (rule assms[OF * **]) + show "\y. f x y : C x y" by (rule assms) qed qed -- cgit v1.2.3