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