adamc@105: (* Copyright (c) 2008, Adam Chlipala
adamc@105:  * 
adamc@105:  * This work is licensed under a
adamc@105:  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@105:  * Unported License.
adamc@105:  * The license text is available at:
adamc@105:  *   http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@105:  *)
adamc@105: 
adamc@105: (* begin hide *)
adamc@105: Require Import List.
adamc@105: 
adamc@105: Require Import Tactics.
adamc@105: 
adamc@105: Set Implicit Arguments.
adamc@105: (* end hide *)
adamc@105: 
adamc@105: 
adamc@105: (** %\chapter{Dependent Data Structures}% *)
adamc@105: 
adamc@105: (** 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. *)
adamc@105: 
adamc@105: 
adamc@105: (** * More Known-Length Lists *)
adamc@105: 
adamc@105: Section ilist.
adamc@105:   Variable A : Set.
adamc@105: 
adamc@105:   Inductive ilist : nat -> Set :=
adamc@105:   | Nil : ilist O
adamc@105:   | Cons : forall n, A -> ilist n -> ilist (S n).
adamc@105: 
adamc@105:   Inductive index : nat -> Set :=
adamc@105:   | First : forall n, index (S n)
adamc@105:   | Next : forall n, index n -> index (S n).
adamc@105: 
adamc@105:   Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@105:     match ls in ilist n return index n -> A with
adamc@105:       | Nil => fun idx =>
adamc@105:         match idx in index n' return (match n' with
adamc@105:                                         | O => A
adamc@105:                                         | S _ => unit
adamc@105:                                       end) with
adamc@105:           | First _ => tt
adamc@105:           | Next _ _ => tt
adamc@105:         end
adamc@105:       | Cons _ x ls' => fun idx =>
adamc@105:         match idx in index n' return (index (pred n') -> A) -> A with
adamc@105:           | First _ => fun _ => x
adamc@105:           | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105:         end (get ls')
adamc@105:     end.
adamc@105: End ilist.
adamc@105: 
adamc@105: Implicit Arguments Nil [A].
adamc@105: 
adamc@105: Section ilist_map.
adamc@105:   Variables A B : Set.
adamc@105:   Variable f : A -> B.
adamc@105: 
adamc@105:   Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
adamc@105:     match ls in ilist _ n return ilist B n with
adamc@105:       | Nil => Nil
adamc@105:       | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105:     end.
adamc@105: 
adamc@105:   Theorem get_imap : forall n (ls : ilist A n) (idx : index n),
adamc@105:     get (imap ls) idx = f (get ls idx).
adamc@105:     induction ls; crush;
adamc@105:       match goal with
adamc@105:         | [ |- context[match ?IDX with First _ => _ | Next _ _ => _ end] ] =>
adamc@105:           dep_destruct IDX; crush
adamc@105:       end.
adamc@105:   Qed.
adamc@105: End ilist_map.