From 5b217a7eb36906eabdcb6ec626a2d02e0f94c308 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 10 May 2018 19:13:05 +0200
Subject: Decided to go with no explicit type declarations in object-lambda
 expressions. Everything in the proof stuff is working at the moment.

---
 HoTT.thy | 39 +++++++++++++++++++++++++--------------
 test.thy | 29 ++++++++++++++++++-----------
 2 files changed, 43 insertions(+), 25 deletions(-)

diff --git a/HoTT.thy b/HoTT.thy
index 9d63388..3e5ba71 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -3,32 +3,42 @@ imports Pure
 begin
 
 section \<open>Setup\<close>
-
-(* ML files, routines and setup should probably go here *)
+text \<open>
+For ML files, routines and setup.
+\<close>
 
 section \<open>Basic definitions\<close>
-
 text \<open>
 A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
-
 For now we do not implement universes, but simply follow the informal notation in the HoTT book.
-\<close>
-(* Actually unsure if a single meta-type suffices... *)
+\<close> (* Actually unsure if a single meta-type suffices... *)
 
 typedecl Term
 
 subsection \<open>Judgements\<close>
-
 consts
   is_a_type :: "Term \<Rightarrow> prop"           ("(_ : U)")  (* Add precedences when I figure them out! *)
   is_of_type :: "Term \<Rightarrow> Term \<Rightarrow> prop"  ("(_ : _)")
 
 subsection \<open>Basic axioms\<close>
+subsubsection \<open>Definitional equality\<close>
+text\<open>
+We take the meta-equality \<equiv>, defined by the Pure framework for any of its terms,
+and use it additionally for definitional/judgmental equality of types and terms in our theory.
 
-axiomatization
-where
-  inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U" and
-  equal_types: "\<And>A B x. A \<equiv> B \<Longrightarrow> x : A \<Longrightarrow> x : B"
+Note that the Pure framework already provides axioms and results for the various properties of \<equiv>,
+which we make use of and extend where necessary.
+\<close>
+
+
+theorem DefEq_symmetry: "\<And>A B. A \<equiv> B \<Longrightarrow> B \<equiv> A"
+  by (rule Pure.symmetric)
+
+subsubsection \<open>Type-related properties\<close>
+
+axiomatization where
+  equal_types: "\<And>A B x. \<lbrakk>A \<equiv> B; x : A\<rbrakk> \<Longrightarrow> x : B" and
+  inhabited_implies_type: "\<And>x A. x : A \<Longrightarrow> A : U"
 
 subsection \<open>Basic types\<close>
 
@@ -41,7 +51,8 @@ Same for the nondependent product below.
 
 axiomatization
   Function :: "Term \<Rightarrow> Term \<Rightarrow> Term"  (infixr "\<rightarrow>" 10) and
-  lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"    (binder "\<^bold>\<lambda>" 10) and  (* precedence! *)
+  lambda :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"  (binder "\<^bold>\<lambda>" 10) and
+    (* Is bold lambda already used by something else? Proof transformers in Pure maybe?... *)
   appl :: "Term \<Rightarrow> Term \<Rightarrow> Term"      ("(_`_)")
 where
   Function_form: "\<And>A B. \<lbrakk>A : U; B : U\<rbrakk> \<Longrightarrow> A\<rightarrow>B : U" and
@@ -62,8 +73,8 @@ where
   Product_comp: "\<And>A B C g a b. \<lbrakk>C : U; g : A\<rightarrow>B\<rightarrow>C; a : A; b : B\<rbrakk> \<Longrightarrow> rec_Product(A,B,C,g)`(a,b) \<equiv> (g`a)`b"
 
 \<comment> \<open>Projection onto first component\<close>
-definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1'(_,_'))") where
-  "proj1(A,B) \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)"
+definition proj1 :: "Term \<Rightarrow> Term \<Rightarrow> Term" ("(proj1\<langle>_,_\<rangle>)") where
+  "proj1\<langle>A,B\<rangle> \<equiv> rec_Product(A, B, A, \<^bold>\<lambda>x. \<^bold>\<lambda>y. x)"
 
 subsubsection \<open>Empty type\<close>
 
diff --git a/test.thy b/test.thy
index 94ba900..d22e710 100644
--- a/test.thy
+++ b/test.thy
@@ -2,12 +2,19 @@ theory test
 imports HoTT
 begin
 
+text \<open>Check trivial stuff:\<close>
 lemma "Null : U"
   by (rule Null_form)
 
+text \<open>
+Do functions behave like we expect them to?
+(Or, is my implementation at least somewhat correct?...
+\<close>
+
 lemma "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A"
 proof -
-  have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types)
+  have "A \<equiv> B \<Longrightarrow> B \<equiv> A" by (rule DefEq_symmetry)
+  then have "\<And>x. A \<equiv> B \<Longrightarrow> x : B \<Longrightarrow> x : A" by (rule equal_types)
   thus "A \<equiv> B \<Longrightarrow> (\<^bold>\<lambda>x. x) : B\<rightarrow>A" by (rule Function_intro)
 qed
 
@@ -17,19 +24,19 @@ proof -
   thus "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : A\<rightarrow>B\<rightarrow>A" by (rule Function_intro)
 qed
 
-(* The previous proofs are nice, BUT I want to be able to do something like the following:
-lemma "x : A \<Longrightarrow> \<^bold>\<lambda>x. x : B\<rightarrow>B" <Fail>
-i.e. I want to be able to associate a type to variables, and have the type remembered by any
-binding I define later.
-
-Do I need to give up using the \<open>binder\<close> syntax in order to do this?
-*)
-
+text \<open>Here's a dumb proof that 2 is a natural number:\<close>
 lemma "succ(succ 0) : Nat"
 proof -
-  have "(succ 0) : Nat" by (rule Nat_intro2)
-  from this have "succ(succ 0) : Nat" by (rule Nat_intro2)
+  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 \<open>
+We can of course iterate the above for as many applications of \<open>succ\<close> as we like.
+The next thing to do is to implement some kind of induction tactic to automate such proofs.
+
+When we get more stuff working, I'd like to aim for formalizing the encode-decode method.
+\<close>
 
 end
\ No newline at end of file
-- 
cgit v1.2.3