From fc19fe90e7cb13acc03deaf061b2b6cf3df2d165 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 7 Jun 2018 19:35:32 +0200 Subject: Nondependent function arrow should bind tighter than the Pi former, but looser than equality. --- HoTT.thy | 64 +++++++++++++++++++++++++++++++++++++------------------ HoTT_Theorems.thy | 10 ++++----- 2 files changed, 48 insertions(+), 26 deletions(-) diff --git a/HoTT.thy b/HoTT.thy index ee81ba4..c1c6e72 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -30,7 +30,7 @@ theorem equal_type_element: assumes "A \ B" and "x : A" shows "x : B" using assms by simp -lemmas type_equality [intro] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated] +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." @@ -46,14 +46,18 @@ 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" :: "[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)" -(* The above syntax translations bind the x in the expressions B, 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 "\" 10) +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 80) where "A\B \ \_:A. B" axiomatization @@ -71,7 +75,7 @@ and and Prod_uniq [simp]: "\A f::Term. \<^bold>\x:A. (f`x) \ f" -lemmas Prod_formation = Prod_form Prod_form[rotated] +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)." @@ -80,11 +84,13 @@ subsection \Dependent pair/sum\ axiomatization Sum :: "[Term, Term \ Term] \ Term" syntax - "_Sum" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) + "_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) +abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) where "A\B \ \_:A. B" axiomatization @@ -102,7 +108,7 @@ and and 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] +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." @@ -145,35 +151,51 @@ subsection \Equality type\ axiomatization Equal :: "[Term, Term, Term] \ Term" syntax - "_EQUAL" :: "[Term, Term, Term] \ Term" ("(3_ =\<^sub>_/ _)") + "_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" and - indEqual :: "([Term, Term, Term] \ Term) \ Term" + 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 p::Term. \x : A; y : A; p : x =\<^sub>A y\ \ C(x)(y)(p) : U; - f : \x:A. C(x)(x)(refl(x)); - a : A; - b : A; - p : a =\<^sub>A b\ \ indEqual(C)`f`a`b`p : C(a)(b)(p)" + "\(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]: - "\(C::[Term, Term, Term] \ Term) (f::Term) (a::Term). indEqual(C)`f`a`a`refl(a) \ f`a" + "\(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 "Inverse" +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" + +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)))" + +lemma compose'_comp: "a : A \ compose'[A]`a`a`refl(a)`a`refl(a) \ refl(a)" unfolding compose'_def by simp -definition inv :: "Term \ Term" ("(_\<^sup>-\<^sup>1)") - where "inv \ " (* Tra la la.. *) end diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 52e1b32..5578bf8 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -57,11 +57,11 @@ proposition wellformed_currying: "B: A \ U" and "\x::Term. C(x): B(x) \ U" shows "\x:A. \y:B(x). C x y : U" -proof (rule Prod_formation) +proof fix x::Term assume *: "x : A" show "\y:B(x). C x y : U" - proof (rule Prod_formation) + proof show "B(x) : U" using * by (rule assms) qed (rule assms) qed (rule assms) @@ -78,15 +78,15 @@ proposition triply_curried: "\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) +proof fix x::Term assume 1: "x : A" show "\y:B(x). \z:C(x)(y). D(x)(y)(z) : U" - proof (rule Prod_formation) + proof 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) + proof 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 -- cgit v1.2.3