From 29015c5877876df28890209d2ad341c6cabd1cc8 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Wed, 30 May 2018 10:46:48 +0200 Subject: Fixed dependent product rules, hopefully final now. --- HoTT_Theorems.thy | 99 +++++++++++++++---------------------------------------- 1 file changed, 27 insertions(+), 72 deletions(-) (limited to 'HoTT_Theorems.thy') diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy index d83a08c..10a0d2c 100644 --- a/HoTT_Theorems.thy +++ b/HoTT_Theorems.thy @@ -6,10 +6,11 @@ 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?" + \ 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=2]] +declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=1]] section \Functions\ @@ -17,97 +18,51 @@ 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:A. x : A\A" .. +lemma "\<^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:A. 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. -More generally, we cannot write an assumption stating 'Let \x\ be a variable of type \A\'." - -proposition "\A : U; A \ B\ \ \<^bold>\x:A. x : B\A" +proposition "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:A. x : A\A" . - from 2 have "A\A \ B\A" by simp - 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:B. x : B\A" .. - -text "And now the actual result:" - -proposition - assumes 1: "A : U" and 2: "B : U" - shows "\<^bold>\x:A. \<^bold>\y:B. x : A\B\A" -proof - show "A : U" using assms(1) . - 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) + 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 -text "Maybe a nicer way to write it:" - -proposition alternating_function: "\A : U; B: U\ \ \<^bold>\x:A. \<^bold>\y:B. x : A\B\A" +proposition "\<^bold>\x:A. \<^bold>\y:B. x : A\B\A" proof - fix x - 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) + fix a + assume "a : A" + then show "\<^bold>\y:B. a : B \ A" .. qed subsection \Function application\ -lemma "\A : U; a : A\ \ (\<^bold>\x:A. x)`a \ a" by simp +proposition "\A : U; a : A\ \ (\<^bold>\x:A. x)`a \ a" by simp + +text "Two arguments:" lemma - assumes - "A:U" and - "B:U" and - "a:A" and - "b:B" + 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" - 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? *) - + proof (rule Prod_comp[of A _ "\_. B\A"]) + fix x + assume "x:A" + then show "\<^bold>\y:B. x : B \ A" .. + qed (rule assms) 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 - + also have "(\<^bold>\y:B. a)`b \ a" using assms by (simp add: Prod_comp[of B _ "\_. A"]) finally show "(\<^bold>\x:A. \<^bold>\y:B. x)`a`b \ a" . 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! +This is the result of the choices made regarding the premises of the type rules." + text "Polymorphic identity function." consts Ui::Term + definition Id where "Id \ \<^bold>\A:Ui. \<^bold>\x:A. x" (* Have to think about universes... *) -- cgit v1.2.3