From 91efce41a2319a9fb861ff26d7dc8c49ec726d4c Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 12 Jun 2018 12:30:54 +0200 Subject: Type rules now have \"all\" premises explicitly stated, matching the formulation in the HoTT book. --- Equal.thy | 154 ++++++++++++++++++++++++++++-------------------------- HoTT.thy | 15 ++++++ HoTT_Base.thy | 44 ++++++++++------ HoTT_Theorems.thy | 25 ++++++--- Prod.thy | 19 ++++--- Sum.thy | 93 ++++++++++++++++++++++----------- 6 files changed, 215 insertions(+), 135 deletions(-) create mode 100644 HoTT.thy diff --git a/Equal.thy b/Equal.thy index b9f676f..12ed272 100644 --- a/Equal.thy +++ b/Equal.thy @@ -1,81 +1,85 @@ +(* Title: HoTT/Equal.thy + Author: Josh Chen + Date: Jun 2018 + +Equality type. +*) + theory Equal - imports HoTT_Base Prod + imports HoTT_Base 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" +axiomatization + Equal :: "[Term, Term, Term] \ Term" and + refl :: "Term \ Term" ("(refl'(_'))" 1000) and + indEqual :: "[Term, [Term, Term, Term] \ Term] \ Term" ("(indEqual[_])") + +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 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 new file mode 100644 index 0000000..405364e --- /dev/null +++ b/HoTT.thy @@ -0,0 +1,15 @@ +(* Title: HoTT/HoTT.thy + Author: Josh Chen + +Load all the component modules for the HoTT logic. +*) + +theory HoTT imports + HoTT_Base + Prod Sum + +begin + +\ \Maybe tactic setup can go in here?\ + +end \ No newline at end of file diff --git a/HoTT_Base.thy b/HoTT_Base.thy index 9650c4c..9b422c4 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -1,5 +1,6 @@ (* Title: HoTT/HoTT_Base.thy Author: Josh Chen + Date: Jun 2018 Basic setup and definitions of a homotopy type theory object logic. *) @@ -9,23 +10,43 @@ theory HoTT_Base begin -section \Basic definitions\ +section \Setup\ -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." +text "Set up type checking routines, proof methods etc." + + +section \Metalogical definitions\ + +text "A single meta-type \Term\ suffices to implement the object-logic types and terms. +Our implementation does not have universes, and we simply use \a : U\ as a convenient shorthand meaning ``\a\ is a type''." typedecl Term + section \Judgments\ consts -is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) -is_of_type :: "[Term, Term] \ prop" ("(3_ :/ _)" [0, 0] 1000) +is_a_type :: "Term \ prop" ("(1_ :/ U)" [0] 1000) +is_of_type :: "[Term, Term] \ prop" ("(1_ :/ _)" [0, 0] 1000) + + +section \Type families\ + +text "A (one-variable) type family is a meta lambda term \P :: Term \ Term\ that further satisfies the following property." + +type_synonym Typefam = "Term \ Term" + +abbreviation is_type_family :: "[Typefam, Term] \ prop" ("(3_:/ _ \ U)") + where "P: A \ U \ (\x. x : A \ P x : U)" + +text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML and is for the moment not really crucial." section \Definitional equality\ -text "We use the Pure equality \\\ for definitional/judgmental equality of types and terms in our theory." +text "The Pure equality \\\ is used for definitional aka judgmental equality of types and terms." + +\ \Do these ever need to be used? theorem equal_types: assumes "A \ B" and "A : U" @@ -35,18 +56,11 @@ theorem equal_type_element: assumes "A \ B" and "x : A" shows "x : B" using assms by simp -lemmas type_equality [intro, simp] = +lemmas type_equality = 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 95f1d0c..2c2a31d 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -1,5 +1,6 @@ theory HoTT_Theorems imports HoTT + begin text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified. @@ -9,8 +10,7 @@ Things that *should* be automated: \ 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]] - +declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]] section \\ type\ @@ -22,17 +22,18 @@ 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" .. + assume "A \ B" + then have *: "A\A \ B\A" by simp + + have "\<^bold>\x:A. x : A\A" .. + with * show "\<^bold>\x:A. x : B\A" by simp 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" .. + then show "\<^bold>\y:B. a : B \ A" .. qed @@ -42,7 +43,15 @@ proposition "a : A \ (\<^bold>\x:A. x)`a \ a" by text "Currying:" -lemma "\a : A; b : B\ \ (\<^bold>\x:A. \<^bold>\y:B. y)`a`b \ b" by simp +term "lambda A (\x. \<^bold>\y:B(x). y)" + +thm Prod_comp[where ?B = "\x. \y:B(x). B(x)"] + +lemma "a : A \ (\<^bold>\x:A. \<^bold>\y:B(x). y)`a \ \<^bold>\y:B(a). y" +proof (rule Prod_comp[where ?B = "\x. \y:B(x). B(x)"]) + show "\x. a : A \ x : A \ \<^bold>\y:B x. y : B x \ B x" + +lemma "\a : A; b : B\ \ (\<^bold>\x:A. \<^bold>\y:B(x). y)`a`b \ b" 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 diff --git a/Prod.thy b/Prod.thy index 9ecab4d..113998e 100644 --- a/Prod.thy +++ b/Prod.thy @@ -1,5 +1,6 @@ (* Title: HoTT/Prod.thy Author: Josh Chen + Date: Jun 2018 Dependent product (function) type for the HoTT logic. *) @@ -10,8 +11,9 @@ theory Prod begin axiomatization - Prod :: "[Term, Term \ Term] \ Term" and + Prod :: "[Term, Typefam] \ Term" and lambda :: "[Term, Term \ Term] \ Term" and + \ \Application binds tighter than abstraction.\ appl :: "[Term, Term] \ Term" (infixl "`" 60) syntax @@ -29,15 +31,20 @@ translations \ \Type rules\ axiomatization where - Prod_form [intro]: "\A B. \A : U; B : A \ U\ \ \x:A. B(x) : U" + 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)" + 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)" + 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)" + Prod_comp [simp]: "\A B b a. \\x. x : A \ b x : B x; a : A\ \ (\<^bold>\x:A. b x)`a \ b a" and - Prod_uniq [simp]: "\A f. \<^bold>\x:A. (f`x) \ f" + Prod_uniq [simp]: "\A B f. f : \x:A. B x \ \<^bold>\x:A. (f`x) \ f" + +\ \The funny thing about the first premises of the computation and uniqueness rules is that they introduce a variable B that doesn't actually explicitly appear in the statement of the conclusion. +In a sense, they say something like "if this condition holds for some type family B... (then we can apply the rule)". +This forces the theorem prover to search for a suitable B. Is this additional overhead necessary? +It *is* a safety check for well-formedness...\ 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)." diff --git a/Sum.thy b/Sum.thy index e34749a..8dab3e8 100644 --- a/Sum.thy +++ b/Sum.thy @@ -1,5 +1,6 @@ (* Title: HoTT/Sum.thy Author: Josh Chen + Date: Jun 2018 Dependent sum type. *) @@ -10,9 +11,9 @@ theory Sum begin axiomatization - Sum :: "[Term, Term \ Term] \ Term" and + Sum :: "[Term, Typefam] \ Term" and pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and - indSum :: "(Term \ Term) \ Term" + indSum :: "[Term, Typefam, Typefam, [Term, Term] \ Term] \ Term" ("(1indSum[_,/ _])") syntax "_SUM" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 20) @@ -23,25 +24,29 @@ translations "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" + 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)" + Sum_intro [intro]: "\A B a b. \B: A \ U; 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)" + Sum_elim [elim]: "\A B C f p. \ + C: \x:A. B x \ U; + \x y. \x : A; y : B x\ \ f x y : C (x,y); + p : \x:A. B x + \ \ (indSum[A,B] 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." + Sum_comp [simp]: "\A B C f a b. \ + C: \x:A. B x \ U; + \x y. \x : A; y : B x\ \ f x y : C (x,y); + a : A; + b : B a + \ \ (indSum[A,B] C f)`(a,b) \ f a b" \ \Nondependent pair\ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) - where "A\B \ \_:A. B" + where "A \ B \ \_:A. B" + -subsubsection \Projections\ +section \Projections\ consts fst :: "[Term, 'a] \ Term" ("(1fst[/_,/ _])") @@ -49,30 +54,56 @@ consts 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_dep :: "[Term, Typefam] \ Term" where + "fst_dep A B \ indSum[A,B] (\_. A) (\x y. x)" 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, \_. B] (\_. A) (\x y. x)" +end + +overloading + snd_dep \ snd + snd_nondep \ snd +begin + definition snd_dep :: "[Term, Typefam] \ Term" where + "snd_dep A B \ indSum[A,B] (\p. B(fst[A,B]`p)) (\x y. y)" 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, \_. B] (\p. B((fst A B)`p)) (\x y. 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 +text "Simplification rules:" + +lemma fst_dep_comp: + assumes "a : A" and "b : B(a)" + shows "fst[A,B]`(a,b) \ a" +proof - + show "fst[A,B]`(a,b) \ a" unfolding fst_dep_def using assms by simp +qed + +lemma snd_dep_comp: "\a : A; b : B(a)\ \ snd[A,B]`(a,b) \ b" +proof - + assume "a : A" and "b : B(a)" + then have "(a, b) : \x:A. B(x)" .. + then show "snd[A,B]`(a,b) \ b" unfolding snd_dep_def by simp +qed + +lemma fst_nondep_comp: "\a : A; b : B\ \ fst[A,B]`(a,b) \ a" +proof - + assume "a : A" and "b : B" + then have "(a, b) : A \ B" .. + then show "fst[A,B]`(a,b) \ a" unfolding fst_nondep_def by simp +qed + +lemma snd_nondep_comp: "\a : A; b : B\ \ snd[A,B]`(a,b) \ b" +proof - + assume "a : A" and "b : B" + then have "(a, b) : A \ B" .. + then show "snd[A,B]`(a,b) \ b" unfolding snd_nondep_def by simp +qed + +lemmas proj_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp -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