Lists + more reorganizing

7 files changed, 103 insertions, 16 deletions

diff --git a/ROOT b/ROOT
index 1e8017c..b716396 100644
--- a/ROOT
+++ b/ROOT
@@ -17,7 +17,7 @@ session Spartan in spartan = Spartan_Core +
   directories
     data
   theories
-    "data/List"
+    List
 
 session HoTT in hott = Spartan +
   description "
@@ -28,8 +28,9 @@ session HoTT in hott = Spartan +
       Available online at https://homotopytypetheory.org/book.
   "
   theories
-    Base
+    HoTT (global)
     Identity
     Equivalence
+    More_Types
     Nat
 
diff --git a/hott/HoTT.thy b/hott/HoTT.thy
new file mode 100644
index 0000000..0b3040c
--- /dev/null
+++ b/hott/HoTT.thy
@@ -0,0 +1,10 @@
+theory HoTT
+imports
+  Identity
+  Equivalence
+  More_Types
+  Nat
+
+begin
+
+end
diff --git a/hott/Identity.thy b/hott/Identity.thy
index 3a982f6..3fef536 100644
--- a/hott/Identity.thy
+++ b/hott/Identity.thy
@@ -30,13 +30,13 @@ axiomatization where
     b: A;
     \<And>x y p. \<lbrakk>p: x =\<^bsub>A\<^esub> y; x: A; y: A\<rbrakk> \<Longrightarrow> C x y p: U i;
     \<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
-    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a b p: C a b p" and
+    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a b p: C a b p" and
 
   Id_comp: "\<lbrakk>
     a: A;
     \<And>x y p. \<lbrakk>x: A; y: A; p: x =\<^bsub>A\<^esub> y\<rbrakk> \<Longrightarrow> C x y p: U i;
     \<And>x. x: A \<Longrightarrow> f x: C x x (refl x)
-    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) f a a (refl a) \<equiv> f a"
+    \<rbrakk> \<Longrightarrow> IdInd A (\<lambda>x y p. C x y p) (\<lambda>x. f x) a a (refl a) \<equiv> f a"
 
 lemmas
   [intros] = IdF IdI and
diff --git a/hott/Base.thy b/hott/More_Types.thy
index 610a373..17789f8 100644
--- a/hott/Base.thy
+++ b/hott/More_Types.thy
@@ -1,17 +1,9 @@
-theory Base
+theory More_Types
 imports Equivalence
 
 begin
 
 
-section \<open>Notation\<close>
-
-syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
-translations "a $ b" \<rightharpoonup> "a (b)"
-
-abbreviation (input) K where "K x \<equiv> \<lambda>_. x"
-
-
 section \<open>Sum type\<close>
 
 axiomatization
diff --git a/hott/Nat.thy b/hott/Nat.thy
index 311f2d9..e129be0 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -1,5 +1,5 @@
 theory Nat
-imports Base
+imports Equivalence
 
 begin
 
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index b4f7772..50002a6 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -18,6 +18,11 @@ section \<open>Preamble\<close>
 
 declare [[eta_contract=false]]
 
+syntax "_dollar" :: \<open>logic \<Rightarrow> logic \<Rightarrow> logic\<close> (infixr "$" 3)
+translations "a $ b" \<rightharpoonup> "a (b)"
+
+abbreviation (input) K where "K x \<equiv> \<lambda>_. x"
+
 
 section \<open>Metatype setup\<close>
 
@@ -118,8 +123,8 @@ axiomatization where
     p: \<Sum>x: A. B x;
     A: U i;
     \<And>x. x : A \<Longrightarrow> B x: U i;
-    \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i;
-    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>
+    \<And>x y. \<lbrakk>x: A; y: B x\<rbrakk> \<Longrightarrow> f x y: C <x, y>;
+    \<And>p. p: \<Sum>x: A. B x \<Longrightarrow> C p: U i
     \<rbrakk> \<Longrightarrow> SigInd A (\<lambda>x. B x) (\<lambda>p. C p) f p: C p" and
 
   Sig_comp: "\<lbrakk>
diff --git a/spartan/data/List.thy b/spartan/data/List.thy
index 71a879b..323ef7e 100644
--- a/spartan/data/List.thy
+++ b/spartan/data/List.thy
@@ -3,4 +3,83 @@ imports Spartan
 
 begin
 
+(*TODO: Inductive type and recursive function definitions. The ad-hoc
+  axiomatization below should be subsumed once general inductive types are
+  properly implemented.*)
+
+axiomatization
+  List    :: \<open>o \<Rightarrow> o\<close> and
+  nil     :: \<open>o \<Rightarrow> o\<close> and
+  cons    :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and
+  ListInd :: \<open>o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
+where
+  ListF: "A: U i \<Longrightarrow> List A: U i" and
+
+  List_nil: "A: U i \<Longrightarrow> nil A: List A" and
+
+  List_cons: "\<lbrakk>x: A; l: List A\<rbrakk> \<Longrightarrow> cons A x l: List A" and
+
+  ListE: "\<lbrakk>
+    xs: List A;
+    c\<^sub>0: C (nil A);
+    \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+    \<And>xs. xs: List A \<Longrightarrow> C xs: U i
+    \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) xs: C xs" and
+
+  List_comp_nil: "\<lbrakk>
+    c\<^sub>0: C (nil A);
+    \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+    \<And>xs. xs: List A \<Longrightarrow> C xs: U i
+    \<rbrakk> \<Longrightarrow> ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) (nil A) \<equiv> c\<^sub>0" and
+
+  List_comp_cons: "\<lbrakk>
+    xs: List A;
+    c\<^sub>0: C (nil A);
+    \<And>x xs c. \<lbrakk>x: A; xs: List A; c: C xs\<rbrakk> \<Longrightarrow> f x xs c: C (cons A x xs);
+    \<And>xs. xs: List A \<Longrightarrow> C xs: U i
+    \<rbrakk> \<Longrightarrow>
+      ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) (cons A x xs) \<equiv>
+        f x xs (ListInd A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs c. f x xs c) xs)"
+
+lemmas
+  [intros] = ListF List_nil List_cons and
+  [elims "?xs"] = ListE and
+  [comps] = List_comp_nil List_comp_cons
+
+abbreviation "ListRec A C \<equiv> ListInd A (K C)"
+
+
+section \<open>Implicit notation\<close>
+
+definition nil_i ("[]")
+  where [implicit]: "[] \<equiv> nil ?"
+
+definition cons_i (infixr "#" 50)
+  where [implicit]: "x # l \<equiv> cons ? x l"
+
+
+section \<open>Standard functions\<close>
+
+definition "tail A \<equiv> \<lambda>xs: List A. ListRec A (List A) (nil A) (\<lambda>x xs _. xs) xs"
+
+definition "map A B \<equiv> \<lambda>f: A \<rightarrow> B. \<lambda>xs: List A.
+  ListRec A (List B) (nil B) (\<lambda>x _ c. cons B (f `x) c) xs"
+
+definition tail_i ("tail")
+  where [implicit]: "tail xs \<equiv> List.tail ? xs"
+
+definition map_i ("map")
+  where [implicit]: "map \<equiv> List.map ? ?"
+
+Lemma tail_type [typechk]:
+  assumes "A: U i" "xs: List A"
+  shows "tail xs: List A"
+  unfolding tail_def by typechk
+
+Lemma map_type [typechk]:
+  assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
+  shows "map f xs: List B"
+  unfolding map_def by typechk
+
+
 end