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 +++++++++++++++++++++++++++++++++++++++++++++++++++ HoTT_Theorems.thy | 206 ------------------------------------------------ ex/HoTT Book/Ch1.thy | 37 --------- ex/HoTT book/Ch1.thy | 44 +++++++++++ 4 files changed, 261 insertions(+), 243 deletions(-) create mode 100644 HoTT_Test.thy delete mode 100644 HoTT_Theorems.thy delete mode 100644 ex/HoTT Book/Ch1.thy create mode 100644 ex/HoTT book/Ch1.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 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 diff --git a/ex/HoTT Book/Ch1.thy b/ex/HoTT Book/Ch1.thy deleted file mode 100644 index 84a5cf4..0000000 --- a/ex/HoTT Book/Ch1.thy +++ /dev/null @@ -1,37 +0,0 @@ -theory Ch1 - imports "../../HoTT" -begin - -chapter \HoTT Book, Chapter 1\ - -section \1.6 Dependent pair types (\-types)\ - -text "Prove that the only inhabitants of the \-type are those given by the pair constructor." - -schematic_goal - assumes "(\x:A. B(x)): U(i)" and "p: \x:A. B(x)" - shows "?a: p =[\x:A. B(x)] " - -text "Proof by induction on \p: \x:A. B(x)\:" - -proof (rule Sum_elim[where ?p=p]) - text "We just need to prove the base case; the rest will be taken care of automatically." - - fix x y assume asm: "x: A" "y: B(x)" show - "refl(): =[\x:A. B(x)] , snd >" - proof (subst (0 1) comp) - text " - The computation rules for \fst\ and \snd\ require that \x\ and \y\ have appropriate types. - The automatic proof methods have trouble picking the appropriate types, so we state them explicitly, - " - show "x: A" and "y: B(x)" by (fact asm)+ - - text "...twice, once each for the substitutions of \fst\ and \snd\." - show "x: A" and "y: B(x)" by (fact asm)+ - - qed (derive lems: assms asm) - -qed (derive lems: assms) - - -end \ No newline at end of file diff --git a/ex/HoTT book/Ch1.thy b/ex/HoTT book/Ch1.thy new file mode 100644 index 0000000..65de875 --- /dev/null +++ b/ex/HoTT book/Ch1.thy @@ -0,0 +1,44 @@ +(* Title: HoTT/ex/HoTT book/Ch1.thy + Author: Josh Chen + Date: Aug 2018 + +A formalization of some content of Chapter 1 of the Homotopy Type Theory book. +*) + +theory Ch1 + imports "../../HoTT" +begin + +chapter \HoTT Book, Chapter 1\ + +section \1.6 Dependent pair types (\-types)\ + +text "Prove that the only inhabitants of the \-type are those given by the pair constructor." + +schematic_goal + assumes "(\x:A. B(x)): U(i)" and "p: \x:A. B(x)" + shows "?a: p =[\x:A. B(x)] " + +text "Proof by induction on \p: \x:A. B(x)\:" + +proof (rule Sum_elim[where ?p=p]) + text "We just need to prove the base case; the rest will be taken care of automatically." + + fix x y assume asm: "x: A" "y: B(x)" show + "refl(): =[\x:A. B(x)] , snd >" + proof (subst (0 1) comp) + text " + The computation rules for \fst\ and \snd\ require that \x\ and \y\ have appropriate types. + The automatic proof methods have trouble picking the appropriate types, so we state them explicitly, + " + show "x: A" and "y: B(x)" by (fact asm)+ + + text "...twice, once each for the substitutions of \fst\ and \snd\." + show "x: A" and "y: B(x)" by (fact asm)+ + + qed (derive lems: assms asm) + +qed (derive lems: assms) + + +end \ No newline at end of file -- cgit v1.2.3