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_Test.thy | 217 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 217 insertions(+) create mode 100644 HoTT_Test.thy (limited to 'HoTT_Test.thy') diff --git a/HoTT_Test.thy b/HoTT_Test.thy new file mode 100644 index 0000000..4c87e78 --- /dev/null +++ b/HoTT_Test.thy @@ -0,0 +1,217 @@ +(* Title: HoTT/HoTT_Test.thy + Author: Josh Chen + Date: Aug 2018 + +This is an old "test suite" from early implementations of the theory, updated for the most recent version. +It is not always guaranteed to be up to date. +*) + +theory HoTT_Test + 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? +" + +declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]] + \ \Turn on trace for unification and the simplifier, for debugging.\ + + +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(i)" shows "\<^bold>\x. x: A \ A" using assms .. + +proposition + assumes "A : U(i)" and "A \ B" + shows "\<^bold>\x. x : B \ A" +proof - + have "A\A \ B\A" using assms by simp + moreover have "\<^bold>\x. x : A \ A" using assms(1) .. + ultimately show "\<^bold>\x. x : B \ A" by simp +qed + +proposition + assumes "A : U(i)" and "B : U(i)" + shows "\<^bold>\x y. x : A \ B \ A" +by (simple lems: assms) + + +subsection \Function application\ + +proposition assumes "a : A" shows "(\<^bold>\x. x)`a \ a" by (simple lems: assms) + +text "Currying:" + +lemma + assumes "a : A" and "\x. x: A \ B(x): U(i)" + shows "(\<^bold>\x y. y)`a \ \<^bold>\y. y" +proof + show "\x. x : A \ \<^bold>\y. y : B(x) \ B(x)" by (simple lems: assms) +qed fact + +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