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_Theorems.thy | 67 +++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 55 insertions(+), 12 deletions(-) (limited to 'HoTT_Theorems.thy') 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