Overhaul of the theory presentations. New methods in HoTT_Methods.thy for handling universes. Commit for release 0.1.0!

2 files changed, 46 insertions, 120 deletions

diff --git a/tests/Subgoal.thy b/tests/Subgoal.thy
deleted file mode 100644
index 82d7e5d..0000000
--- a/tests/Subgoal.thy
+++ /dev/null
@@ -1,63 +0,0 @@
-theory Subgoal
-  imports "../HoTT"
-begin
-
-
-text "
-  Proof of \<open>rpathcomp_type\<close> (see EqualProps.thy) in apply-style.
-  Subgoaling can be used to fix variables and apply the elimination rules.
-"
-
-lemma rpathcomp_type:
-  assumes "A: U(i)"
-  shows "rpathcomp: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-unfolding rpathcomp_def
-apply standard
-  subgoal premises 1 for x  \<comment> \<open>\<open>subgoal\<close> is the proof script version of \<open>fix-assume-show\<close>.\<close>
-  apply standard
-    subgoal premises 2 for y
-    apply standard
-      subgoal premises 3 for p
-      apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
-        \<comment> \<open>specifying \<open>?A=A\<close> is crucial here to prevent the next \<open>subgoal\<close> from binding a schematic ?A which should be instantiated to \<open>A\<close>.\<close>
-      prefer 4
-        apply standard
-          apply (rule Prod_intro)
-            subgoal premises 4 for u z q
-            apply (rule Equal_elim[where ?x=u and ?y=z])
-            apply (routine lems: assms 4)
-            done
-          apply (routine lems: assms 1 2 3)
-      done
-    apply (routine lems: assms 1 2)
-    done
-  apply fact
-  done
-apply fact
-done
-
-
-text "
-  \<open>subgoal\<close> converts schematic variables to fixed free variables, making it unsuitable for use in \<open>schematic_goal\<close> proofs.
-  This is the same thing as being unable to start a ``sub schematic-goal'' inside an ongoing proof.
-
-  This is a problem for syntheses which need to use induction (elimination rules), as these often have to be applied to fixed variables, while keeping any schematic variables intact.
-"
-
-schematic_goal rpathcomp_synthesis:
-  assumes "A: U(i)"
-  shows "?a: \<Prod>x:A. \<Prod>y:A. x =\<^sub>A y \<rightarrow> (\<Prod>z:A. y =\<^sub>A z \<rightarrow> x =\<^sub>A z)"
-
-text "
-  Try (and fail) to synthesize the constant for path composition, following the proof of \<open>rpathcomp_type\<close> below.
-"
-
-apply (rule intros)
-  apply (rule intros)
-    apply (rule intros)
-      subgoal 123 for x y p
-      apply (rule Equal_elim[where ?x=x and ?y=y and ?A=A])
-      oops
-
-
-end
diff --git a/tests/Test.thy b/tests/Test.thy
index de65dbd..6f9f996 100644
--- a/tests/Test.thy
+++ b/tests/Test.thy
@@ -1,121 +1,110 @@
-(*  Title:  HoTT/tests/Test.thy
-    Author: Josh Chen
-    Date:   Aug 2018
+(*
+Title:  tests/Test.thy
+Author: Joshua Chen
+Date:   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.
+This is an old test suite from early implementations.
+It is not always guaranteed to be up to date or to reflect most recent versions of the theory.
 *)
 
 theory Test
-  imports "../HoTT"
+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?
-"
+text \<open>
+A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
+
+Things that *should* be automated:
+\<^item> Checking that @{term A} is a well-formed type, when writing things like @{prop "x: A"} and @{prop "A: U i"}.
+\<^item> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?
+\<close>
 
 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>
+\<comment> \<open>Turn on trace for unification and the Simplifier, for debugging.\<close>
 
 
 section \<open>\<Prod>-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.
-"
+text \<open>Declaring @{thm Prod_intro} with the @{attribute intro} attribute enables @{method rule} to prove the following.\<close>
 
-proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A" by (routine lems: assms)
+proposition assumes "A : U(i)" shows "\<^bold>\<lambda>x. x: A \<rightarrow> A"
+by (routine add: 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" by (routine lems: assms)
+  moreover have "\<^bold>\<lambda>x. x : A \<rightarrow> A" by (routine add: assms)
   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 (routine lems: assms)
-
+by (routine add: assms)
 
 subsection \<open>Function application\<close>
 
-proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a" by (derive lems: assms)
-
-text "Currying:"
+proposition assumes "a : A" shows "(\<^bold>\<lambda>x. x)`a \<equiv> a"
+by (derive lems: assms)
 
 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 compute
-  show "\<And>x. x : A \<Longrightarrow> \<^bold>\<lambda>y. y : B(x) \<rightarrow> B(x)" by (routine lems: assms)
-qed fact
+by (derive lems: assms)
 
-lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b" by derive
+lemma "\<lbrakk>A: U(i); B: U(i); a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. y)`a`b \<equiv> b"
+by derive
 
-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: U(i); a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x y. f x y)`a \<equiv> \<^bold>\<lambda>y. f a y"
+proof derive
+oops  \<comment> \<open>Missing some premises.\<close>
 
 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
+proof derive
+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)"
+  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 (routine lems: assms)
-
+by (routine add: assms)
 
 proposition higher_order_currying_formation:
   assumes
-    "A: U(i)" and
-    "B: A \<longrightarrow> U(i)" and
+    "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 (routine lems: assms)
-
+by (routine add: 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"
+  assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "\<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 (routine lems: assms)
+by (routine add: assms)
 
 
-text "
-  Polymorphic identity function is now trivial due to lambda expression polymorphism.
-  (Was more involved in previous monomorphic incarnations.)
-"
+text \<open>
+Polymorphic identity function is now trivial due to lambda expression polymorphism.
+It was more involved in previous monomorphic incarnations.
+\<close>
 
-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, routine)
+lemma "x: A \<Longrightarrow> id`x \<equiv> x"
+by derive
   
 
 section \<open>Natural numbers\<close>
 
-text "Automatic proof methods recognize natural numbers."
+text \<open>Automatic proof methods recognize natural numbers.\<close>
+
+proposition "succ(succ(succ 0)): \<nat>" by routine
 
-proposition "succ(succ(succ 0)): Nat" by routine
 
 end