From d8699451025a3bd5e8955e07fa879ed248418949 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Thu, 16 Aug 2018 16:28:50 +0200 Subject: Some comments and reorganization --- HoTT_Theorems.thy | 206 ------------------------------------------------------ 1 file changed, 206 deletions(-) delete mode 100644 HoTT_Theorems.thy (limited to 'HoTT_Theorems.thy') diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy deleted file mode 100644 index 79614d3..0000000 --- a/HoTT_Theorems.thy +++ /dev/null @@ -1,206 +0,0 @@ -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. - -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, simp_trace_depth_limit=5]] - -section \\ type\ - -subsection \Typing functions\ - -text "Declaring \Prod_intro\ with the \intro\ attribute (in HoTT.thy) enables \standard\ to prove the following." - -proposition assumes "A : U" shows "\<^bold>\x:A. x : A\A" using assms .. - -proposition - assumes "A : U" and "A \ B" - shows "\<^bold>\x:A. x : B\A" -proof - - have "A\A \ B\A" using assms by simp - moreover have "\<^bold>\x:A. x : A\A" using assms(1) .. - ultimately show "\<^bold>\x:A. x : B\A" by simp -qed - -proposition - assumes "A : U" and "B : U" - shows "\<^bold>\x:A. \<^bold>\y:B. x : A\B\A" -proof - fix x - assume "x : A" - with assms(2) show "\<^bold>\y:B. x : B\A" .. -qed (rule assms) - - -subsection \Function application\ - -proposition assumes "a : A" shows "(\<^bold>\x:A. x)`a \ a" using assms by simp - -text "Currying:" - -lemma - assumes "a : A" - shows "(\<^bold>\x:A. \<^bold>\y:B(x). y)`a \ \<^bold>\y:B(a). y" -proof - show "\x. a : A \ x : A \ \<^bold>\y:B x. y : B x \ B x" - -lemma "\a : A; b : B\ \ (\<^bold>\x:A. \<^bold>\y:B(x). y)`a`b \ b" by simp - -lemma "a : A \ (\<^bold>\x:A. \<^bold>\y:B(x). f x y)`a \ \<^bold>\y:B(a). f a y" by simp - -lemma "\a : A; b : B(a); c : C(a)(b)\ \ (\<^bold>\x:A. \<^bold>\y:B(x). \<^bold>\z:C(x)(y). f x y z)`a`b`c \ f a b c" by simp - - -subsection \Currying functions\ - -proposition curried_function_formation: - 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 - fix x::Term - assume *: "x : A" - show "\y:B(x). C x y : U" - proof - show "B(x) : U" using * by (rule assms) - qed (rule assms) -qed (rule assms) - -(**** GOOD CANDIDATE FOR AUTOMATION - EISBACH! ****) -proposition higher_order_currying_formation: - fixes - A::Term and - B::"Term \ Term" and - C::"[Term, Term] \ Term" and - D::"[Term, Term, Term] \ Term" - assumes - "A : U" and - "B: A \ U" and - "\x y::Term. y : B(x) \ C(x)(y) : U" and - "\x y z::Term. z : C(x)(y) \ D(x)(y)(z) : U" - shows "\x:A. \y:B(x). \z:C(x)(y). D(x)(y)(z) : U" -proof - fix x::Term assume 1: "x : A" - show "\y:B(x). \z:C(x)(y). D(x)(y)(z) : U" - proof - show "B(x) : U" using 1 by (rule assms) - - fix y::Term assume 2: "y : B(x)" - show "\z:C(x)(y). D(x)(y)(z) : U" - proof - show "C x y : U" using 2 by (rule assms) - show "\z::Term. z : C(x)(y) \ D(x)(y)(z) : U" by (rule assms) - qed - qed -qed (rule assms) - -(**** AND PROBABLY THIS TOO? ****) -lemma curried_type_judgment: - 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" using * ** by (rule assms) - 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! -This is the result of the choices made regarding the premises of the type rules." - - -section \\ type\ - -text "The following shows that the dependent sum inductor has the type we expect it to have:" - -lemma - assumes "C: \x:A. B(x) \ U" - shows "indSum(C) : \f:(\x:A. \y:B(x). C((x,y))). \p:(\x:A. B(x)). C(p)" -proof - - define F and P where - "F \ \x:A. \y:B(x). C((x,y))" and - "P \ \x:A. B(x)" - - have "\<^bold>\f:F. \<^bold>\p:P. indSum(C)`f`p : \f:F. \p:P. C(p)" - proof (rule curried_type_judgment) - fix f p::Term - assume "f : F" and "p : P" - with assms show "indSum(C)`f`p : C(p)" unfolding F_def P_def .. - qed - - then show "indSum(C) : \f:F. \p:P. C(p)" by simp -qed - -(**** AUTOMATION CANDIDATE ****) -text "Propositional uniqueness principle for dependent sums:" - -text "We would like to eventually automate proving that 'a given type \A\ is inhabited', i.e. search for an element \a:A\. - -A good starting point would be to automate the application of elimination rules." - -notepad begin - -fix A B assume "A : U" and "B: A \ U" - -define C where "C \ \p. p =[\x:A. B(x)] (fst[A,B]`p, snd[A,B]`p)" -have *: "C: \x:A. B(x) \ U" -proof - - fix p assume "p : \x:A. B(x)" - have "(fst[A,B]`p, snd[A,B]`p) : \x:A. B(x)" - -define f where "f \ \<^bold>\x:A. \<^bold>\y:B(x). refl((x,y))" -have "f`x`y : C((x,y))" -sorry - -have "p : \x:A. B(x) \ indSum(C)`f`p : C(p)" using * ** by (rule Sum_elim) - -end - -section \Universes and polymorphism\ - -text "Polymorphic identity function." - -consts Ui::Term - -definition Id where "Id \ \<^bold>\A:Ui. \<^bold>\x:A. x" - - -(* -section \Natural numbers\ - -text "Here's a dumb proof that 2 is a natural number." - -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. - -When we get more stuff working, I'd like to aim for formalizing the encode-decode method to be able to prove the only naturals are 0 and those obtained from it by \succ\." -*) - -end -- cgit v1.2.3