# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223909241 14400
# Node ID ec0fb0f00f46d57cc420967b1556fe10ec4af684
# Parent  32a5ad6e2bb0d6e57b3293b53da5b26b4c7ba0c7
Start of DataStruct

diff -r 32a5ad6e2bb0 -r ec0fb0f00f46 Makefile
--- a/Makefile	Sun Oct 12 08:44:23 2008 -0400
+++ b/Makefile	Mon Oct 13 10:47:21 2008 -0400
@@ -1,6 +1,7 @@
 MODULES_NODOC := Tactics MoreSpecif
 MODULES_PROSE := Intro
-MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset MoreDep
+MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset \
+	MoreDep DataStruct
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)
diff -r 32a5ad6e2bb0 -r ec0fb0f00f46 src/DataStruct.v
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/DataStruct.v	Mon Oct 13 10:47:21 2008 -0400
@@ -0,0 +1,75 @@
+(* Copyright (c) 2008, Adam Chlipala
+ * 
+ * This work is licensed under a
+ * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
+ * Unported License.
+ * The license text is available at:
+ *   http://creativecommons.org/licenses/by-nc-nd/3.0/
+ *)
+
+(* begin hide *)
+Require Import List.
+
+Require Import Tactics.
+
+Set Implicit Arguments.
+(* end hide *)
+
+
+(** %\chapter{Dependent Data Structures}% *)
+
+(** Our red-black tree example from the last chapter illustrated how dependent types enable static enforcement of data structure invariants.  To find interesting uses of dependent data structures, however, we need not look to the favorite examples of data structures and algorithms textbooks.  More basic examples like known-length and heterogeneous lists prop up again and again as the building blocks of dependent programs.  There is a surprisingly large design space for this class of data structure, and we will spend this chapter exploring it. *)
+
+
+(** * More Known-Length Lists *)
+
+Section ilist.
+  Variable A : Set.
+
+  Inductive ilist : nat -> Set :=
+  | Nil : ilist O
+  | Cons : forall n, A -> ilist n -> ilist (S n).
+
+  Inductive index : nat -> Set :=
+  | First : forall n, index (S n)
+  | Next : forall n, index n -> index (S n).
+
+  Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
+    match ls in ilist n return index n -> A with
+      | Nil => fun idx =>
+        match idx in index n' return (match n' with
+                                        | O => A
+                                        | S _ => unit
+                                      end) with
+          | First _ => tt
+          | Next _ _ => tt
+        end
+      | Cons _ x ls' => fun idx =>
+        match idx in index n' return (index (pred n') -> A) -> A with
+          | First _ => fun _ => x
+          | Next _ idx' => fun get_ls' => get_ls' idx'
+        end (get ls')
+    end.
+End ilist.
+
+Implicit Arguments Nil [A].
+
+Section ilist_map.
+  Variables A B : Set.
+  Variable f : A -> B.
+
+  Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
+    match ls in ilist _ n return ilist B n with
+      | Nil => Nil
+      | Cons _ x ls' => Cons (f x) (imap ls')
+    end.
+
+  Theorem get_imap : forall n (ls : ilist A n) (idx : index n),
+    get (imap ls) idx = f (get ls idx).
+    induction ls; crush;
+      match goal with
+        | [ |- context[match ?IDX with First _ => _ | Next _ _ => _ end] ] =>
+          dep_destruct IDX; crush
+      end.
+  Qed.
+End ilist_map.
diff -r 32a5ad6e2bb0 -r ec0fb0f00f46 src/Intro.v
--- a/src/Intro.v	Sun Oct 12 08:44:23 2008 -0400
+++ b/src/Intro.v	Mon Oct 13 10:47:21 2008 -0400
@@ -195,6 +195,8 @@
 \hline
 More Dependent Types & \texttt{MoreDep.v} \\
 \hline
+Dependent Data Structures & \texttt{DataStruct.v} \\
+\hline
 \end{tabular} \end{center}
 
 % *)
diff -r 32a5ad6e2bb0 -r ec0fb0f00f46 src/toc.html
--- a/src/toc.html	Sun Oct 12 08:44:23 2008 -0400
+++ b/src/toc.html	Mon Oct 13 10:47:21 2008 -0400
@@ -11,5 +11,6 @@
 <li><a href="Coinductive.html">Infinite Data and Proofs</a>
 <li><a href="Subset.html">Subset Types and Variations</a>
 <li><a href="MoreDep.html">More Dependent Types</a>
+<li><a href="DataStruct.html">Dependent Data Structures</a>
 
 </body></html>