Mercurial > cpdt > repo

annotate src/DataStruct.v @ 106:1d2746eae1a6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Commentary on ilist get
author Adam Chlipala <adamc@hcoop.net>
date Mon, 13 Oct 2008 11:59:20 -0400
parents ec0fb0f00f46
children 924d77a177e8
rev   line source
adamc@105 1 (* Copyright (c) 2008, Adam Chlipala
adamc@105 2 *
adamc@105 3 * This work is licensed under a
adamc@105 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@105 5 * Unported License.
adamc@105 6 * The license text is available at:
adamc@105 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@105 8 *)
adamc@105 9
adamc@105 10 (* begin hide *)
adamc@105 11 Require Import List.
adamc@105 12
adamc@105 13 Require Import Tactics.
adamc@105 14
adamc@105 15 Set Implicit Arguments.
adamc@105 16 (* end hide *)
adamc@105 17
adamc@105 18
adamc@105 19 (** %\chapter{Dependent Data Structures}% *)
adamc@105 20
adamc@106 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 length-indexed and heterogeneous lists come 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 22
adamc@105 23
adamc@106 24 (** * More Length-Indexed Lists *)
adamc@106 25
adamc@106 26 (** We begin with a deeper look at the length-indexed lists that began the last chapter. *)
adamc@105 27
adamc@105 28 Section ilist.
adamc@105 29 Variable A : Set.
adamc@105 30
adamc@105 31 Inductive ilist : nat -> Set :=
adamc@105 32 | Nil : ilist O
adamc@105 33 | Cons : forall n, A -> ilist n -> ilist (S n).
adamc@105 34
adamc@106 35 (** We might like to have a certified function for selecting an element of an [ilist] by position. We could do this using subset types and explicit manipulation of proofs, but dependent types let us do it more directly. It is helpful to define a type family [index], where [index n] is isomorphic to [{m : nat | m < n}]. Such a type family is also often called [Fin] or similar, standing for "finite." *)
adamc@106 36
adamc@105 37 Inductive index : nat -> Set :=
adamc@105 38 | First : forall n, index (S n)
adamc@105 39 | Next : forall n, index n -> index (S n).
adamc@105 40
adamc@106 41 (** [index] essentially makes a more richly-typed copy of the natural numbers. Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.
adamc@106 42
adamc@106 43 Now it is easy to pick a [Prop]-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
adamc@106 44
adamc@106 45 [[
adamc@106 46 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 47 match ls in ilist n return index n -> A with
adamc@106 48 | Nil => fun idx => ?
adamc@106 49 | Cons _ x ls' => fun idx =>
adamc@106 50 match idx with
adamc@106 51 | First _ => x
adamc@106 52 | Next _ idx' => get ls' idx'
adamc@106 53 end
adamc@106 54 end.
adamc@106 55
adamc@106 56 We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [index] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return].
adamc@106 57
adamc@106 58 [[
adamc@106 59 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 60 match ls in ilist n return index n -> A with
adamc@106 61 | Nil => fun idx =>
adamc@106 62 match idx in index n' return (match n' with
adamc@106 63 | O => A
adamc@106 64 | S _ => unit
adamc@106 65 end) with
adamc@106 66 | First _ => tt
adamc@106 67 | Next _ _ => tt
adamc@106 68 end
adamc@106 69 | Cons _ x ls' => fun idx =>
adamc@106 70 match idx with
adamc@106 71 | First _ => x
adamc@106 72 | Next _ idx' => get ls' idx'
adamc@106 73 end
adamc@106 74 end.
adamc@106 75
adamc@106 76 Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply a trick that we will call "the convoy pattern," introducing a new function and applying it immediately, to satisfy the type checker.
adamc@106 77
adamc@106 78 [[
adamc@106 79 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 80 match ls in ilist n return index n -> A with
adamc@106 81 | Nil => fun idx =>
adamc@106 82 match idx in index n' return (match n' with
adamc@106 83 | O => A
adamc@106 84 | S _ => unit
adamc@106 85 end) with
adamc@106 86 | First _ => tt
adamc@106 87 | Next _ _ => tt
adamc@106 88 end
adamc@106 89 | Cons _ x ls' => fun idx =>
adamc@106 90 match idx in index n' return ilist (pred n') -> A with
adamc@106 91 | First _ => fun _ => x
adamc@106 92 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 93 end ls'
adamc@106 94 end.
adamc@106 95
adamc@106 96 There is just one problem left with this implementation. Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination. We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
adamc@106 97
adamc@105 98 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@105 99 match ls in ilist n return index n -> A with
adamc@105 100 | Nil => fun idx =>
adamc@105 101 match idx in index n' return (match n' with
adamc@105 102 | O => A
adamc@105 103 | S _ => unit
adamc@105 104 end) with
adamc@105 105 | First _ => tt
adamc@105 106 | Next _ _ => tt
adamc@105 107 end
adamc@105 108 | Cons _ x ls' => fun idx =>
adamc@105 109 match idx in index n' return (index (pred n') -> A) -> A with
adamc@105 110 | First _ => fun _ => x
adamc@105 111 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 112 end (get ls')
adamc@105 113 end.
adamc@105 114 End ilist.
adamc@105 115
adamc@105 116 Implicit Arguments Nil [A].
adamc@105 117
adamc@105 118 Section ilist_map.
adamc@105 119 Variables A B : Set.
adamc@105 120 Variable f : A -> B.
adamc@105 121
adamc@105 122 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
adamc@105 123 match ls in ilist _ n return ilist B n with
adamc@105 124 | Nil => Nil
adamc@105 125 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 126 end.
adamc@105 127
adamc@105 128 Theorem get_imap : forall n (ls : ilist A n) (idx : index n),
adamc@105 129 get (imap ls) idx = f (get ls idx).
adamc@105 130 induction ls; crush;
adamc@105 131 match goal with
adamc@105 132 | [ |- context[match ?IDX with First _ => _ | Next _ _ => _ end] ] =>
adamc@105 133 dep_destruct IDX; crush
adamc@105 134 end.
adamc@105 135 Qed.
adamc@105 136 End ilist_map.