From 120879c099a2fb71e67a41a1c852c5db65e9eb4f Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Mon, 28 May 2018 15:53:07 +0200 Subject: Dependent product rules done and proofs of typing properties so far work. Starting on dependent sums. --- HoTT.thy | 81 ++++++++++++++++++++++++++++++++---------------- HoTT_Theorems.thy | 93 +++++++++++++++++++++++++++++++++---------------------- 2 files changed, 110 insertions(+), 64 deletions(-) diff --git a/HoTT.thy b/HoTT.thy index a13b1d4..4713a0d 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -19,23 +19,38 @@ consts is_a_type :: "Term \ prop" ("(_ : U)" [0] 1000) is_of_type :: "[Term, Term] \ prop" ("(3_ :/ _)" [0, 0] 1000) -subsection \Basic axioms\ +subsection \Type families\ -subsubsection \Definitional equality\ +text "Type families are implemented as meta-level lambda terms of type \Term \ Term\ that further satisfy the following property." -text "We take the meta-equality \, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory. +abbreviation is_type_family :: "[(Term \ Term), Term] \ prop" ("(3_:/ _ \ U)") + where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" -Note that the Pure framework already provides axioms and results for various properties of \, which we make use of and extend where necessary." +theorem constant_type_family: "\B : U; A : U\ \ \_. B: A \ U" + proof - + assume "B : U" + then show "\_. B: A \ U" . + qed -subsubsection \Type-related properties\ +subsection \Definitional equality\ -axiomatization where - equal_types: "\(A::Term) (B::Term) (x::Term). \A \ B; x : A\ \ x : B" and - inhabited_implies_type: "\(x::Term) (A::Term). x : A \ A : U" +text "We take the meta-equality \\\, defined by the Pure framework for any of its terms, and use it additionally for definitional/judgmental equality of types and terms in our theory. + +Note that the Pure framework already provides axioms and results for various properties of \\\, which we make use of and extend where necessary." + +theorem equal_types: + assumes "A \ B" and "A : U" + shows "B : U" using assms by simp + +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] subsection \Basic types\ -subsubsection \Dependent product type\ +subsubsection \Dependent function/product\ consts Prod :: "[Term, (Term \ Term)] \ Term" @@ -43,36 +58,48 @@ syntax "_Prod" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) translations "\x:A. B" \ "CONST Prod A (\x. B)" -(* The above syntax translation binds the x in B *) +(* The above syntax translation binds the x in the expression B *) + +abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 30) + where "A\B \ \_:A. B" axiomatization lambda :: "(Term \ Term) \ Term" (binder "\<^bold>\" 10) and appl :: "[Term, Term] \ Term" ("(3_`/_)" [10, 10] 60) where - Prod_form: "\(A::Term) (B::Term \ Term). \A : U; \(x::Term). x : A \ B(x) : U\ \ \x:A. B(x) : U" and - Prod_intro: "\(A::Term) (B::Term \ Term) (b::Term \ Term). \A : U; \(x::Term). x : A \ b(x) : B(x)\ \ \<^bold>\x. b(x) : \x:A. B(x)" and - Prod_elim: "\(A::Term) (B::Term \ Term) (f::Term) (a::Term). \f : \x:A. B(x); a : A\ \ f`a : B(a)" and - Prod_comp: "\(b::Term \ Term) (a::Term). (\<^bold>\x. b(x))`a \ b(a)" and - Prod_uniq: "\(A::Term) (B::Term \ Term) (f::Term). \f : \x:A. B(x)\ \ \<^bold>\x. (f`x) \ f" - -text "Observe that the metatype \Term \ Term\ is used to represent type families, for example \Prod\ takes a type \A\ and a type family \B\ and constructs a dependent function type from them." + Prod_form: "\(A::Term) (B::Term \ Term). \A : U; B : A \ U\ \ \x:A. B(x) : U" and + Prod_intro [intro]: "\(A::Term) (B::Term \ Term) (b::Term \ Term). \A : U; B : A \ U; \x::Term. x : A \ b(x) : B(x)\ \ \<^bold>\x. b(x) : \x:A. B(x)" and + 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]: "\(b::Term \ Term) (a::Term). (\<^bold>\x. b(x))`a \ b(a)" and + Prod_uniq [simp]: "\(A::Term) (B::Term \ Term) (f::Term). f : \x:A. B(x) \ \<^bold>\x. (f`x) \ f" 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)." -abbreviation Function :: "[Term, Term] \ Term" (infixr "\" 30) -where "A\B \ \_:A. B" +lemmas Prod_formation = Prod_form Prod_form[rotated] -subsubsection \Nondependent product type\ +subsubsection \Dependent pair/sum\ + +consts + Sum :: "[Term, Term \ Term] \ Term" +syntax + "_Sum" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) +translations + "\x:A. B" \ "CONST Sum A (\x. B)" + +abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) + where "A\B \ \_:A. B" axiomatization - Product :: "Term \ Term \ Term" ("(_\/ _)") and - pair :: "Term \ Term \ Term" ("(_,/ _)") and - rec_Product :: "Term \ Term \ Term \ Term \ Term" ("(rec'_Product'(_,_,_,_'))") + pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and + indSum :: "[Term \ Term, Term \ Term, Term] \ Term" where - Product_form: "\A B. \A : U; B : U\ \ A\B : U" and - Product_intro: "\A B a b. \a : A; b : B\ \ (a,b) : A\B" and - Product_elim: "\A B C g. \A : U; B : U; C : U; g : A\B\C\ \ rec_Product(A,B,C,g) : (A\B)\C" and - Product_comp: "\A B C g a b. \C : U; g : A\B\C; a : A; b : B\ \ rec_Product(A,B,C,g)`(a,b) \ (g`a)`b" + Sum_form: "\(A::Term) (B::Term \ Term). \A : U; B: A \ U\ \ \x:A. B(x) : U" and + Sum_intro: "\(A::Term) (B::Term \ Term) (a::Term) (b::Term). \A : U; B: A \ U; a : A; b : B(a)\ \ (a, b) : \x:A. B(x)" and + Sum_elim: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term \ Term) (p::Term). \A : U; B: A \ U; 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)" + 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-lambda \f::Term \ Term\ instead of an object dependent function \f : \x:A. B(x)\. +However we should be able to later show the equivalence of the formalizations." \ \Projection onto first component\ (* diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index bea3dfe..33b0957 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -2,63 +2,82 @@ 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." +text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified. -section \Foundational stuff\ +Things that *should* be automated: + \ Checking that \A\ is a well-formed type, when writing things like \x : A\ and \A : U\. +" -theorem "\A : U; A \ B\ \ B : U" by simp +\ \Turn on trace for unification and the simplifier, for debugging.\ +declare[[unify_trace_simp, unify_trace_types, simp_trace]] section \Functions\ -lemma "A : U \ \<^bold>\x. x : A\A" - by (rule Prod_intro) +text "Declaring \Prod_intro\ with the \intro\ attribute (in HoTT.thy) enables \standard\ to prove the following." + +lemma id_function: "A : U \ \<^bold>\x. x : A\A" .. + +text "Here is the same result, stated and proved differently. +The standard method invoked after the keyword \proof\ is applied to the goal \\<^bold>\x. x: A\A\, and so we need to show the prover how to continue, as opposed to the previous lemma." + +lemma + assumes "A : U" + shows "\<^bold>\x. x : A\A" +proof + show "A : U" using assms . + show "\x. A : A \ U" using assms .. +qed text "Note that there is no provision for declaring the type of bound variables outside of the scope of a lambda expression. -Hence a statement like \x : A\ is not needed (nor possible!) in the premises of the following lemma." +More generally, we cannot write an assumption stating 'Let \x\ be a variable of type \A\'." -lemma "\A : U; A \ B\ \ \<^bold>\x. x : B\A" +proposition "\A : U; A \ B\ \ \<^bold>\x. x : B\A" proof - assume - 0: "A : U" and - 1: "A \ B" - from 0 have 2: "\<^bold>\x. x : A\A" by (rule Prod_intro) - from 1 have 3: "A\A \ B\A" by simp - from 3 and 2 show "\<^bold>\x. x : B\A" by (rule equal_types) - qed - -lemma "\A : U; B : U; x : A\ \ \<^bold>\y. x : B\A" -proof - -assume - 1: "A : U" and - 2: "B : U" and - 3: "x : A" -then show "\<^bold>\y. x : B\A" -proof - -from 3 have "\<^bold>\y. x : B\A" by (rule Prod_intro) + 1: "A : U" and + 2: "A \ B" + from id_function[OF 1] have 3: "\<^bold>\x. x : A\A" . + from 2 have "A\A \ B\A" by simp + with 3 show "\<^bold>\x. x : B\A" .. qed + +text "It is instructive to try to prove \\A : U; B : U\ \ \<^bold>\x. \<^bold>\y. x : A\B\A\. +First we prove an intermediate step." + +lemma constant_function: "\A : U; B : U; x : A\ \ \<^bold>\y. x : B\A" .. + +text "And now the actual result:" + +proposition + assumes 1: "A : U" and 2: "B : U" + shows "\<^bold>\x. \<^bold>\y. x : A\B\A" +proof + show "A : U" using assms(1) . + show "\x. x : A \ \<^bold>\y. x : B \ A" using assms by (rule constant_function) + + from assms have "B \ A : U" by (rule Prod_formation) + then show "\x. B \ A: A \ U" using assms(1) by (rule constant_type_family) qed -lemma "\A : U; B : U\ \ \<^bold>\x. \<^bold>\y. x : A\B\A" -proof - +text "Maybe a nicer way to write it:" + +proposition "\A : U; B: U\ \ \<^bold>\x. \<^bold>\y. x : A\B\A" +proof fix x - assume - "A : U" and - "B : U" and - "x : A" - then have "\<^bold>\y. x : B\A" by (rule Prod_intro) - + show "\A : U; B : U; x : A\ \ \<^bold>\y. x : B \ A" by (rule constant_function) + show "\A : U; B : U\ \ B\A : U" by (rule Prod_formation) qed section \Nats\ text "Here's a dumb proof that 2 is a natural number." -lemma "succ(succ 0) : Nat" -proof - - have "0 : Nat" by (rule Nat_intro1) - from this have "(succ 0) : Nat" by (rule Nat_intro2) - thus "succ(succ 0) : Nat" by (rule Nat_intro2) -qed +proposition "succ(succ 0) : Nat" + proof - + have "0 : Nat" by (rule Nat_intro1) + from this have "(succ 0) : Nat" by (rule Nat_intro2) + thus "succ(succ 0) : Nat" by (rule Nat_intro2) + qed text "We can of course iterate the above for as many applications of \succ\ as we like. The next thing to do is to implement induction to automate such proofs. -- cgit v1.2.3