HoTT_Test.thy should go in test/

1 files changed, 121 insertions, 0 deletions

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 \<open>A\<close> is a well-formed type, when writing things like \<open>x : A\<close> and \<open>A : U\<close>.
+    - 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]]
+  \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
+
+
+section \<open>\<Pi>-type\<close>
+
+subsection \<open>Typing functions\<close>
+
+text "
+  Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribute (in HoTT.thy) enables \<open>standard\<close> to prove the following.
+"
+
+proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" using assms ..
+
+proposition
+  assumes "A : U(i)" and "A \<equiv> B"
+  shows "\<^bold>\<lambda>x. x : B \<rightarrow> A"
+proof -
+  have "A\<rightarrow>A \<equiv> B\<rightarrow>A" using assms by simp
+  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" using assms(1) ..
+  ultimately show "\<^bold>\<lambda>x. x : B \<rightarrow> A" by simp
+qed
+
+proposition
+  assumes "A : U(i)" and "B : U(i)"
+  shows "\<^bold>\<lambda>x y. x : A \<rightarrow> B \<rightarrow> A"
+by (simple lems: assms)
+
+
+subsection \<open>Function application\<close>
+
+proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (simple lems: assms)
+
+text "Currying:"
+
+lemma
+  assumes "a : A" and "\<And>x. x: A \<Longrightarrow> B(x): U(i)"
+  shows "(\<^bold>\<lambda>x y. y)`a \<equiv> \<^bold>\<lambda>y. y"
+proof
+  show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (simple lems: assms)
+qed fact
+
+lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" by (compute, simple)
+
+lemma "\<lbrakk>A: U(i); a : A \<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
+proof compute
+  show "\<And>x. \<lbrakk>A: U(i); x: A\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>y. f x y: \<Prod>y:B(x). C x y"
+  proof
+    oops
+
+lemma "\<lbrakk>a : A; b : B(a); c : C(a)(b)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. \<^bold>\<lambda>y. \<^bold>\<lambda>z. f x y z)`a`b`c \<equiv> f a b c"
+  oops
+
+
+subsection \<open>Currying functions\<close>
+
+proposition curried_function_formation:
+  fixes A B C
+  assumes
+    "A : U(i)" and
+    "B: A \<longrightarrow> U(i)" and
+    "\<And>x. C(x): B(x) \<longrightarrow> U(i)"
+  shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U(i)"
+  by (simple lems: assms)
+
+
+proposition higher_order_currying_formation:
+  assumes
+    "A: U(i)" and
+    "B: A \<longrightarrow> U(i)" and
+    "\<And>x y. y: B(x) \<Longrightarrow> C(x)(y): U(i)" and
+    "\<And>x y z. z : C(x)(y) \<Longrightarrow> D(x)(y)(z): U(i)"
+  shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z): U(i)"
+  by (simple lems: assms)
+
+
+lemma curried_type_judgment:
+  assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "\<And>x y. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
+  shows "\<^bold>\<lambda>x y. f x y : \<Prod>x:A. \<Prod>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 \<equiv> \<^bold>\<lambda>x. x"
+
+lemma "\<lbrakk>x: A\<rbrakk> \<Longrightarrow> Id`x \<equiv> x"
+unfolding Id_def by (compute, simple)
+  
+
+section \<open>Natural numbers\<close>
+
+text "Automatic proof methods recognize natural numbers."
+
+proposition "succ(succ(succ 0)): Nat" by simple
+
+end