From 607c3971e08d1ded22bd9f1cabdd309653af1248 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 29 May 2018 12:28:13 +0200 Subject: More rigorous rules for Product type. Propositions and proofs all working, but have to think about maybe relaxing the computation rule, or else automating the currying of dependent functions. --- HoTT.thy | 29 ++++++++++++++---------- HoTT_Theorems.thy | 67 +++++++++++++++++++++++++++++++++++++++++++++---------- 2 files changed, 72 insertions(+), 24 deletions(-) diff --git a/HoTT.thy b/HoTT.thy index 4713a0d..96bd3c1 100644 --- a/HoTT.thy +++ b/HoTT.thy @@ -54,24 +54,27 @@ subsubsection \Dependent function/product\ consts Prod :: "[Term, (Term \ Term)] \ Term" + lambda :: "[Term, (Term \ Term)] \ Term" syntax - "_Prod" :: "[idt, Term, Term] \ Term" ("(3\_:_./ _)" 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)" -(* The above syntax translation binds the x in the expression B *) + "\<^bold>\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 "\" 30) where "A\B \ \_:A. B" axiomatization - lambda :: "(Term \ Term) \ Term" (binder "\<^bold>\" 10) and - appl :: "[Term, Term] \ Term" ("(3_`/_)" [10, 10] 60) + appl :: "[Term, Term] \ Term" (infixl "`" 60) 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). \A : U; B : A \ U; \x::Term. x : A \ b(x) : B(x)\ \ \<^bold>\x. b(x) : \x:A. B(x)" 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:A. 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" + Prod_comp [simp]: "\(A::Term) (B::Term \ Term) (b::Term \ Term) (a::Term). \A : U; B : A \ U; \x::Term. x : A \ b(x) : B(x); a : A\ \ (\<^bold>\x:A. b(x))`a \ b(a)" and + Prod_uniq [simp]: "\(A::Term) (B::Term \ Term) (f::Term). f : \x:A. B(x) \ \<^bold>\x:A. (f`x) \ f" +(* Thinking about the premises for the computation rule... they make simplification rather cumbersome, should I remove them? Would this potentially result in logical problems with being able to state untrue statements? (But probably not prove them?) *) 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)." @@ -90,17 +93,19 @@ abbreviation Pair :: "[Term, Term] \ Term" (infixr "\" 50) where "A\B \ \_:A. B" axiomatization - pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and + pair :: "[Term, Term] \ Term" ("(1'(_,/ _'))") and indSum :: "[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: "\(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: "" + Sum_intro [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 [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)" and + Sum_comp [simp]: "\(A::Term) (B::Term \ Term) (C::Term \ Term) (f::Term \ Term) (a::Term) (b::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)); a : A; b : B(a)\ \ (indSum C f (a,b)) \ f((a,b))" -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)\. +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." + + \ \Projection onto first component\ (* definition proj1 :: "Term \ Term \ Term" ("(proj1\_,_\)") where diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index 33b0957..d83a08c 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -6,23 +6,25 @@ text "A bunch of theorems and other statements for sanity-checking, as well as t Things that *should* be automated: \ Checking that \A\ is a well-formed type, when writing things like \x : A\ and \A : U\. -" + \ 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]] +declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=2]] section \Functions\ +subsection \Typing functions\ + 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" .. +lemma id_function: "A : U \ \<^bold>\x:A. 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" + shows "\<^bold>\x:A. x : A\A" proof show "A : U" using assms . show "\x. A : A \ U" using assms .. @@ -31,29 +33,29 @@ qed text "Note that there is no provision for declaring the type of bound variables outside of the scope of a lambda expression. More generally, we cannot write an assumption stating 'Let \x\ be a variable of type \A\'." -proposition "\A : U; A \ B\ \ \<^bold>\x. x : B\A" +proposition "\A : U; A \ B\ \ \<^bold>\x:A. x : B\A" proof - assume 1: "A : U" and 2: "A \ B" - from id_function[OF 1] have 3: "\<^bold>\x. x : A\A" . + from id_function[OF 1] have 3: "\<^bold>\x:A. x : A\A" . from 2 have "A\A \ B\A" by simp - with 3 show "\<^bold>\x. x : B\A" .. + with 3 show "\<^bold>\x:A. 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" .. +lemma constant_function: "\A : U; B : U; x : A\ \ \<^bold>\y:B. 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" + shows "\<^bold>\x:A. \<^bold>\y:B. 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) + show "\x. x : A \ \<^bold>\y:B. 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) @@ -61,13 +63,54 @@ qed text "Maybe a nicer way to write it:" -proposition "\A : U; B: U\ \ \<^bold>\x. \<^bold>\y. x : A\B\A" +proposition alternating_function: "\A : U; B: U\ \ \<^bold>\x:A. \<^bold>\y:B. x : A\B\A" proof fix x - show "\A : U; B : U; x : A\ \ \<^bold>\y. x : B \ A" by (rule constant_function) + show "\A : U; B : U; x : A\ \ \<^bold>\y:B. x : B \ A" by (rule constant_function) show "\A : U; B : U\ \ B\A : U" by (rule Prod_formation) qed +subsection \Function application\ + +lemma "\A : U; a : A\ \ (\<^bold>\x:A. x)`a \ a" by simp + +lemma + assumes + "A:U" and + "B:U" and + "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" + proof (rule Prod_comp[of A "\_. B\A"]) + have "B \ A : U" using constant_type_family[OF assms(1) assms(2)] assms(2) by (rule Prod_formation) + then show "\x. B \ A: A \ U" using assms(1) by (rule constant_type_family[of "B\A"]) + + show "\x. x : A \ \<^bold>\y:B. x : B \ A" using assms(2) assms(1) .. + show "A:U" using assms(1) . + show "a:A" using assms(3) . + qed (* Why do I need to do the above for the last two goals? Can't Isabelle do it automatically? *) + + 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" + proof (rule Prod_comp[of B "\_. A"]) + show "\y. A: B \ U" using assms(1) assms(2) by (rule constant_type_family) + show "\y. y : B \ a : A" using assms(3) . + show "B:U" using assms(2) . + show "b:B" using assms(4) . + qed + + finally show "(\<^bold>\x:A. \<^bold>\y:B. x)`a`b \ a" . +qed + +text "Polymorphic identity function." + +consts Ui::Term +definition Id where "Id \ \<^bold>\A:Ui. \<^bold>\x:A. x" +(* Have to think about universes... *) + section \Nats\ text "Here's a dumb proof that 2 is a natural number." -- cgit v1.2.3