From a7303e36651ea1f8ec50958415fa0db7295ad957 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Fri, 1 Jun 2018 03:39:51 +0200 Subject: Should be final version of Prod. Theorems proving stuff about currying. Rules for Sum, going to change them to use object-level arguments more. --- HoTT.thy | 37 ++++++++++++----------------- HoTT_Theorems.thy | 69 ++++++++++++++++++++++++++++++++++++++++--------------- 2 files changed, 65 insertions(+), 41 deletions(-) diff --git a/HoTT.thy b/HoTT.thy index 6de4efb..8c9fa20 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -23,20 +23,9 @@ subsection \Type families\ text "Type families are implemented as meta-level lambda terms of type \Term \ Term\ that further satisfy the following property." -abbreviation is_type_family :: "[(Term \ Term), Term] \ prop" ("(3_:/ _ \ U)") +abbreviation is_type_family :: "[Term \ Term, Term] \ prop" ("(3_:/ _ \ U)") where "P: A \ U \ (\x::Term. x : A \ P(x) : U)" -\ \ -I originally wrote the following, but I'm not sure it's useful. -\theorem constant_type_family': "B : U \ \_. B: A \ U" - proof - - assume "B : U" - then show "\_. B: A \ U" . - qed - -lemmas constant_type_family = constant_type_family' constant_type_family'[rotated]\ -\ - subsection \Definitional equality\ 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. @@ -58,8 +47,8 @@ subsection \Basic types\ subsubsection \Dependent function/product\ consts - Prod :: "[Term, (Term \ Term)] \ Term" - lambda :: "[Term, (Term \ Term)] \ Term" + Prod :: "[Term, Term \ Term] \ Term" + lambda :: "[Term, Term \ Term] \ Term" syntax "_Prod" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 10) "__lambda" :: "[idt, Term, Term] \ Term" ("(3\<^bold>\_:_./ _)" 10) @@ -76,13 +65,13 @@ axiomatization where 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). + Prod_intro [intro]: "\(A::Term) (B::Term \ Term) (b::Term \ Term). (\x::Term. x : A \ b(x) : B(x)) \ \<^bold>\x:A. b(x) : \x:A. B(x)" and - Prod_elim [elim]: "\(f::Term) (A::Term) (B::Term \ Term) (a::Term). + 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) (A::Term) (b::Term \ Term). a : A \ (\<^bold>\x:A. b(x))`a \ b(a)" and + Prod_comp [simp]: "\(A::Term) (b::Term \ Term) (a::Term). (\<^bold>\x:A. b(x))`a \ b(a)" and Prod_uniq [simp]: "\(A::Term) (f::Term). \<^bold>\x:A. (f`x) \ f" @@ -104,21 +93,25 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) axiomatization pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and - indSum :: "[Term \ Term, Term \ Term, Term] \ Term" + indSum :: "[Term \ Term, [Term, Term] \ 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) (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, 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_comp [simp]: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term \ Term) (a::Term) (b::Term). - (indSum C f (a,b)) \ f((a,b))" + Sum_comp [simp]: "\(C::Term \ Term) (f::[Term, Term] \ Term) (a::Term) (b::Term). (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)" + +lemma "fst[A, B](a,b) \ a" unfolding fst_def by simp + 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." diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 0aefe94..5922b51 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -21,34 +21,65 @@ text "Declaring \Prod_intro\ with the \intro\ attribut 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" .. -qed + 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" .. + 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" .. -qed + proof + fix a + assume "a : A" + then show "\<^bold>\y:B. a : B \ A" .. + qed subsection \Function application\ proposition "a : A \ (\<^bold>\x:A. x)`a \ a" by simp -text "Two arguments:" +text "Currying:" + +lemma "(\<^bold>\x:A. \<^bold>\y:B. f x y)`a \ \<^bold>\y:B. 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 + +proposition wellformed_currying: + fixes + A::Term and + B::"Term \ Term" and + C::"Term \ Term \ Term" + assumes + "A : U" and + "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) + show "\x::Term. x : A \ \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)) lemma - assumes "a : A" and "b : B" - shows "(\<^bold>\x:A. \<^bold>\y:B. x)`a`b \ a" -proof - - have "(\<^bold>\x:A. \<^bold>\y:B. x)`a \ \<^bold>\y:B. a" using assms(1) by (rule Prod_comp[of a A "\x. \<^bold>\y:B. x"]) - then have "(\<^bold>\x:A. \<^bold>\y:B. x)`a`b \ (\<^bold>\y:B. a)`b" by simp - also have "(\<^bold>\y:B. a)`b \ a" using assms by simp - finally show "(\<^bold>\x:A. \<^bold>\y:B. x)`a`b \ a" . + 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" + 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 * **]) + qed qed text "Note that the propositions and proofs above often say nothing about the well-formedness of the types, or the well-typedness of the lambdas involved; one has to be very explicit and prove such things separately! -- cgit v1.2.3