Mercurial > cpdt > repo

comparison src/DataStruct.v @ 105:ec0fb0f00f46

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of DataStruct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 13 Oct 2008 10:47:21 -0400
parents
children 1d2746eae1a6
comparison
equal deleted inserted replaced
104:32a5ad6e2bb0 105:ec0fb0f00f46
1 (* Copyright (c) 2008, Adam Chlipala
2 *
3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License.
6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *)
9
10 (* begin hide *)
11 Require Import List.
12
13 Require Import Tactics.
14
15 Set Implicit Arguments.
16 (* end hide *)
17
18
19 (** %\chapter{Dependent Data Structures}% *)
20
21 (** 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. *)
22
23
24 (** * More Known-Length Lists *)
25
26 Section ilist.
27 Variable A : Set.
28
29 Inductive ilist : nat -> Set :=
30 | Nil : ilist O
31 | Cons : forall n, A -> ilist n -> ilist (S n).
32
33 Inductive index : nat -> Set :=
34 | First : forall n, index (S n)
35 | Next : forall n, index n -> index (S n).
36
37 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
38 match ls in ilist n return index n -> A with
39 | Nil => fun idx =>
40 match idx in index n' return (match n' with
41 | O => A
42 | S _ => unit
43 end) with
44 | First _ => tt
45 | Next _ _ => tt
46 end
47 | Cons _ x ls' => fun idx =>
48 match idx in index n' return (index (pred n') -> A) -> A with
49 | First _ => fun _ => x
50 | Next _ idx' => fun get_ls' => get_ls' idx'
51 end (get ls')
52 end.
53 End ilist.
54
55 Implicit Arguments Nil [A].
56
57 Section ilist_map.
58 Variables A B : Set.
59 Variable f : A -> B.
60
61 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
62 match ls in ilist _ n return ilist B n with
63 | Nil => Nil
64 | Cons _ x ls' => Cons (f x) (imap ls')
65 end.
66
67 Theorem get_imap : forall n (ls : ilist A n) (idx : index n),
68 get (imap ls) idx = f (get ls idx).
69 induction ls; crush;
70 match goal with
71 | [ |- context[match ?IDX with First _ => _ | Next _ _ => _ end] ] =>
72 dep_destruct IDX; crush
73 end.
74 Qed.
75 End ilist_map.