From 03c734ea067bd28210530d862137133e2215ca80 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Sat, 18 Aug 2018 16:18:23 +0200 Subject: HoTT_Test.thy should go in test/ --- HoTT_Test.thy | 121 --------------------------------------------------------- tests/Test.thy | 121 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 121 insertions(+), 121 deletions(-) delete mode 100644 HoTT_Test.thy create mode 100644 tests/Test.thy diff --git a/HoTT_Test.thy b/HoTT_Test.thy deleted file mode 100644 index da044b4..0000000 --- a/HoTT_Test.thy +++ /dev/null @@ -1,121 +0,0 @@ -(* Title: HoTT/HoTT_Test.thy - Author: Josh Chen - Date: Aug 2018 - -This is an old "test suite" from early implementations of the theory. -It is not always guaranteed to be up to date, or reflect most recent versions of the theory. -*) - -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: U(i); B: U(i); a : A; b : B\ \ (\<^bold>\x y. y)`a`b \ b" by (compute, simple) - -lemma "\A: U(i); a : A \ \ (\<^bold>\x y. f x y)`a \ \<^bold>\y. f a y" -proof compute - show "\x. \A: U(i); x: A\ \ \<^bold>\y. f x y: \y:B(x). C x y" - proof - oops - -lemma "\a : A; b : B(a); c : C(a)(b)\ \ (\<^bold>\x. \<^bold>\y. \<^bold>\z. f x y z)`a`b`c \ f a b c" - oops - - -subsection \Currying functions\ - -proposition curried_function_formation: - fixes A B C - assumes - "A : U(i)" and - "B: A \ U(i)" and - "\x. C(x): B(x) \ U(i)" - shows "\x:A. \y:B(x). C x y : U(i)" - by (simple lems: assms) - - -proposition higher_order_currying_formation: - assumes - "A: U(i)" and - "B: A \ U(i)" and - "\x y. y: B(x) \ C(x)(y): U(i)" and - "\x y z. z : C(x)(y) \ D(x)(y)(z): U(i)" - shows "\x:A. \y:B(x). \z:C(x)(y). D(x)(y)(z): U(i)" - by (simple lems: assms) - - -lemma curried_type_judgment: - assumes "A: U(i)" "B: A \ U(i)" "\x y. \x : A; y : B(x)\ \ f x y : C x y" - shows "\<^bold>\x y. f x y : \x:A. \y:B(x). C x y" - by (simple lems: assms) - - -text " - Polymorphic identity function. Trivial due to lambda expression polymorphism. - (Was more involved in previous monomorphic incarnations.) -" - -definition Id :: "Term" where "Id \ \<^bold>\x. x" - -lemma "\x: A\ \ Id`x \ x" -unfolding Id_def by (compute, simple) - - -section \Natural numbers\ - -text "Automatic proof methods recognize natural numbers." - -proposition "succ(succ(succ 0)): Nat" by simple - -end diff --git a/tests/Test.thy b/tests/Test.thy new file mode 100644 index 0000000..433039c --- /dev/null +++ b/tests/Test.thy @@ -0,0 +1,121 @@ +(* Title: HoTT/tests/Test.thy + Author: Josh Chen + Date: Aug 2018 + +This is an old "test suite" from early implementations of the theory. +It is not always guaranteed to be up to date, or reflect most recent versions of the theory. +*) + +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: U(i); B: U(i); a : A; b : B\ \ (\<^bold>\x y. y)`a`b \ b" by (compute, simple) + +lemma "\A: U(i); a : A \ \ (\<^bold>\x y. f x y)`a \ \<^bold>\y. f a y" +proof compute + show "\x. \A: U(i); x: A\ \ \<^bold>\y. f x y: \y:B(x). C x y" + proof + oops + +lemma "\a : A; b : B(a); c : C(a)(b)\ \ (\<^bold>\x. \<^bold>\y. \<^bold>\z. f x y z)`a`b`c \ f a b c" + oops + + +subsection \Currying functions\ + +proposition curried_function_formation: + fixes A B C + assumes + "A : U(i)" and + "B: A \ U(i)" and + "\x. C(x): B(x) \ U(i)" + shows "\x:A. \y:B(x). C x y : U(i)" + by (simple lems: assms) + + +proposition higher_order_currying_formation: + assumes + "A: U(i)" and + "B: A \ U(i)" and + "\x y. y: B(x) \ C(x)(y): U(i)" and + "\x y z. z : C(x)(y) \ D(x)(y)(z): U(i)" + shows "\x:A. \y:B(x). \z:C(x)(y). D(x)(y)(z): U(i)" + by (simple lems: assms) + + +lemma curried_type_judgment: + assumes "A: U(i)" "B: A \ U(i)" "\x y. \x : A; y : B(x)\ \ f x y : C x y" + shows "\<^bold>\x y. f x y : \x:A. \y:B(x). C x y" + by (simple lems: assms) + + +text " + Polymorphic identity function. Trivial due to lambda expression polymorphism. + (Was more involved in previous monomorphic incarnations.) +" + +definition Id :: "Term" where "Id \ \<^bold>\x. x" + +lemma "\x: A\ \ Id`x \ x" +unfolding Id_def by (compute, simple) + + +section \Natural numbers\ + +text "Automatic proof methods recognize natural numbers." + +proposition "succ(succ(succ 0)): Nat" by simple + +end -- cgit v1.2.3