Mercurial > cpdt > repo

annotate src/DataStruct.v @ 113:ccab8a30c05e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Templatize DataStruct
author Adam Chlipala <adamc@hcoop.net>
date Tue, 14 Oct 2008 13:05:43 -0400
parents 623478074c2f
children f6eb1ed8048c
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@111 11 Require Import Arith 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@113 37 (* EX: Define a function [get] for extracting an [ilist] element by position. *)
adamc@113 38
adamc@113 39 (* begin thide *)
adamc@105 40 Inductive index : nat -> Set :=
adamc@105 41 | First : forall n, index (S n)
adamc@105 42 | Next : forall n, index n -> index (S n).
adamc@105 43
adamc@106 44 (** [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 45
adamc@106 46 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 47
adamc@106 48 [[
adamc@106 49 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 50 match ls in ilist n return index n -> A with
adamc@106 51 | Nil => fun idx => ?
adamc@106 52 | Cons _ x ls' => fun idx =>
adamc@106 53 match idx with
adamc@106 54 | First _ => x
adamc@106 55 | Next _ idx' => get ls' idx'
adamc@106 56 end
adamc@106 57 end.
adamc@106 58
adamc@106 59 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 60
adamc@106 61 [[
adamc@106 62 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 63 match ls in ilist n return index n -> A with
adamc@106 64 | Nil => fun idx =>
adamc@106 65 match idx in index n' return (match n' with
adamc@106 66 | O => A
adamc@106 67 | S _ => unit
adamc@106 68 end) with
adamc@106 69 | First _ => tt
adamc@106 70 | Next _ _ => tt
adamc@106 71 end
adamc@106 72 | Cons _ x ls' => fun idx =>
adamc@106 73 match idx with
adamc@106 74 | First _ => x
adamc@106 75 | Next _ idx' => get ls' idx'
adamc@106 76 end
adamc@106 77 end.
adamc@106 78
adamc@106 79 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 80
adamc@106 81 [[
adamc@106 82 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@106 83 match ls in ilist n return index n -> A with
adamc@106 84 | Nil => fun idx =>
adamc@106 85 match idx in index n' return (match n' with
adamc@106 86 | O => A
adamc@106 87 | S _ => unit
adamc@106 88 end) with
adamc@106 89 | First _ => tt
adamc@106 90 | Next _ _ => tt
adamc@106 91 end
adamc@106 92 | Cons _ x ls' => fun idx =>
adamc@106 93 match idx in index n' return ilist (pred n') -> A with
adamc@106 94 | First _ => fun _ => x
adamc@106 95 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 96 end ls'
adamc@106 97 end.
adamc@106 98
adamc@106 99 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 100
adamc@105 101 Fixpoint get n (ls : ilist n) {struct ls} : index n -> A :=
adamc@105 102 match ls in ilist n return index n -> A with
adamc@105 103 | Nil => fun idx =>
adamc@105 104 match idx in index n' return (match n' with
adamc@105 105 | O => A
adamc@105 106 | S _ => unit
adamc@105 107 end) with
adamc@105 108 | First _ => tt
adamc@105 109 | Next _ _ => tt
adamc@105 110 end
adamc@105 111 | Cons _ x ls' => fun idx =>
adamc@105 112 match idx in index n' return (index (pred n') -> A) -> A with
adamc@105 113 | First _ => fun _ => x
adamc@105 114 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 115 end (get ls')
adamc@105 116 end.
adamc@113 117 (* end thide *)
adamc@105 118 End ilist.
adamc@105 119
adamc@105 120 Implicit Arguments Nil [A].
adamc@113 121 (* begin thide *)
adamc@108 122 Implicit Arguments First [n].
adamc@113 123 (* end thide *)
adamc@105 124
adamc@108 125 (** A few examples show how to make use of these definitions. *)
adamc@108 126
adamc@108 127 Check Cons 0 (Cons 1 (Cons 2 Nil)).
adamc@108 128 (** [[
adamc@108 129
adamc@108 130 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 131 : ilist nat 3
adamc@108 132 ]] *)
adamc@113 133 (* begin thide *)
adamc@108 134 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@108 135 (** [[
adamc@108 136
adamc@108 137 = 0
adamc@108 138 : nat
adamc@108 139 ]] *)
adamc@108 140 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@108 141 (** [[
adamc@108 142
adamc@108 143 = 1
adamc@108 144 : nat
adamc@108 145 ]] *)
adamc@108 146 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@108 147 (** [[
adamc@108 148
adamc@108 149 = 2
adamc@108 150 : nat
adamc@108 151 ]] *)
adamc@113 152 (* end thide *)
adamc@108 153
adamc@108 154 (** Our [get] function is also quite easy to reason about. We show how with a short example about an analogue to the list [map] function. *)
adamc@107 155
adamc@105 156 Section ilist_map.
adamc@105 157 Variables A B : Set.
adamc@105 158 Variable f : A -> B.
adamc@105 159
adamc@105 160 Fixpoint imap n (ls : ilist A n) {struct ls} : ilist B n :=
adamc@105 161 match ls in ilist _ n return ilist B n with
adamc@105 162 | Nil => Nil
adamc@105 163 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 164 end.
adamc@105 165
adamc@107 166 (** It is easy to prove that [get] "distributes over" [imap] calls. The only tricky bit is remembering to use the [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *)
adamc@107 167
adamc@107 168 Theorem get_imap : forall n (idx : index n) (ls : ilist A n),
adamc@105 169 get (imap ls) idx = f (get ls idx).
adamc@113 170 (* begin thide *)
adamc@107 171 induction ls; dep_destruct idx; crush.
adamc@105 172 Qed.
adamc@113 173 (* end thide *)
adamc@105 174 End ilist_map.
adamc@107 175
adamc@107 176
adamc@107 177 (** * Heterogeneous Lists *)
adamc@107 178
adamc@107 179 (** Programmers who move to statically-typed functional languages from "scripting languages" often complain about the requirement that every element of a list have the same type. With fancy type systems, we can partially lift this requirement. We can index a list type with a "type-level" list that explains what type each element of the list should have. This has been done in a variety of ways in Haskell using type classes, and it we can do it much more cleanly and directly in Coq. *)
adamc@107 180
adamc@107 181 Section hlist.
adamc@107 182 Variable A : Type.
adamc@107 183 Variable B : A -> Type.
adamc@107 184
adamc@113 185 (* EX: Define a type [hlist] indexed by a [list A], where the type of each element is determined by running [B] on the corresponding element of the index list. *)
adamc@113 186
adamc@107 187 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
adamc@107 188
adamc@113 189 (* begin thide *)
adamc@107 190 Inductive hlist : list A -> Type :=
adamc@107 191 | MNil : hlist nil
adamc@107 192 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 193
adamc@107 194 (** We can implement a variant of the last section's [get] function for [hlist]s. To get the dependent typing to work out, we will need to index our element selectors by the types of data that they point to. *)
adamc@107 195
adamc@113 196 (* end thide *)
adamc@113 197 (* EX: Define an analogue to [get] for [hlist]s. *)
adamc@113 198
adamc@113 199 (* begin thide *)
adamc@107 200 Variable elm : A.
adamc@107 201
adamc@107 202 Inductive member : list A -> Type :=
adamc@107 203 | MFirst : forall ls, member (elm :: ls)
adamc@107 204 | MNext : forall x ls, member ls -> member (x :: ls).
adamc@107 205
adamc@107 206 (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable. In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too. The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations.
adamc@107 207
adamc@107 208 We can use [member] to adapt our definition of [get] to [hlists]. The same basic [match] tricks apply. In the [MCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match]. We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
adamc@107 209
adamc@107 210 Fixpoint hget ls (mls : hlist ls) {struct mls} : member ls -> B elm :=
adamc@107 211 match mls in hlist ls return member ls -> B elm with
adamc@107 212 | MNil => fun mem =>
adamc@107 213 match mem in member ls' return (match ls' with
adamc@107 214 | nil => B elm
adamc@107 215 | _ :: _ => unit
adamc@107 216 end) with
adamc@107 217 | MFirst _ => tt
adamc@107 218 | MNext _ _ _ => tt
adamc@107 219 end
adamc@107 220 | MCons _ _ x mls' => fun mem =>
adamc@107 221 match mem in member ls' return (match ls' with
adamc@107 222 | nil => Empty_set
adamc@107 223 | x' :: ls'' =>
adamc@107 224 B x' -> (member ls'' -> B elm) -> B elm
adamc@107 225 end) with
adamc@107 226 | MFirst _ => fun x _ => x
adamc@107 227 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@107 228 end x (hget mls')
adamc@107 229 end.
adamc@113 230 (* end thide *)
adamc@107 231 End hlist.
adamc@108 232
adamc@113 233 (* begin thide *)
adamc@108 234 Implicit Arguments MNil [A B].
adamc@108 235 Implicit Arguments MCons [A B x ls].
adamc@108 236
adamc@108 237 Implicit Arguments MFirst [A elm ls].
adamc@108 238 Implicit Arguments MNext [A elm x ls].
adamc@113 239 (* end thide *)
adamc@108 240
adamc@108 241 (** By putting the parameters [A] and [B] in [Type], we allow some very higher-order uses. For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
adamc@108 242
adamc@108 243 Definition someTypes : list Set := nat :: bool :: nil.
adamc@108 244
adamc@113 245 (* begin thide *)
adamc@113 246
adamc@108 247 Example someValues : hlist (fun T : Set => T) someTypes :=
adamc@108 248 MCons 5 (MCons true MNil).
adamc@108 249
adamc@108 250 Eval simpl in hget someValues MFirst.
adamc@108 251 (** [[
adamc@108 252
adamc@108 253 = 5
adamc@108 254 : (fun T : Set => T) nat
adamc@108 255 ]] *)
adamc@108 256 Eval simpl in hget someValues (MNext MFirst).
adamc@108 257 (** [[
adamc@108 258
adamc@108 259 = true
adamc@108 260 : (fun T : Set => T) bool
adamc@108 261 ]] *)
adamc@108 262
adamc@108 263 (** We can also build indexed lists of pairs in this way. *)
adamc@108 264
adamc@108 265 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
adamc@108 266 MCons (1, 2) (MCons (true, false) MNil).
adamc@108 267
adamc@113 268 (* end thide *)
adamc@113 269
adamc@113 270
adamc@108 271 (** ** A Lambda Calculus Interpreter *)
adamc@108 272
adamc@108 273 (** Heterogeneous lists are very useful in implementing interpreters for functional programming languages. Using the types and operations we have already defined, it is trivial to write an interpreter for simply-typed lambda calculus. Our interpreter can alternatively be thought of as a denotational semantics.
adamc@108 274
adamc@108 275 We start with an algebraic datatype for types. *)
adamc@108 276
adamc@108 277 Inductive type : Set :=
adamc@108 278 | Unit : type
adamc@108 279 | Arrow : type -> type -> type.
adamc@108 280
adamc@108 281 (** Now we can define a type family for expressions. An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts]. We effectively use the de Bruijn variable representation, which we will discuss in more detail in later chapters. Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *)
adamc@108 282
adamc@108 283 Inductive exp : list type -> type -> Set :=
adamc@108 284 | Const : forall ts, exp ts Unit
adamc@108 285
adamc@113 286 (* begin thide *)
adamc@108 287 | Var : forall ts t, member t ts -> exp ts t
adamc@108 288 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 289 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@113 290 (* end thide *)
adamc@108 291
adamc@108 292 Implicit Arguments Const [ts].
adamc@108 293
adamc@108 294 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 295
adamc@108 296 Fixpoint typeDenote (t : type) : Set :=
adamc@108 297 match t with
adamc@108 298 | Unit => unit
adamc@108 299 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 300 end.
adamc@108 301
adamc@108 302 (** Now it is straightforward to write an expression interpreter. The type of the function, [expDenote], tells us that we translate expressions into functions from properly-typed environments to final values. An environment for a free variable list [ts] is simply a [hlist typeDenote ts]. That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type. We use [hget] to implement the [Var] case, and we use [MCons] to extend the environment in the [Abs] case. *)
adamc@108 303
adamc@113 304 (* EX: Define an interpreter for [exp]s. *)
adamc@113 305
adamc@113 306 (* begin thide *)
adamc@108 307 Fixpoint expDenote ts t (e : exp ts t) {struct e} : hlist typeDenote ts -> typeDenote t :=
adamc@108 308 match e in exp ts t return hlist typeDenote ts -> typeDenote t with
adamc@108 309 | Const _ => fun _ => tt
adamc@108 310
adamc@108 311 | Var _ _ mem => fun s => hget s mem
adamc@108 312 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@108 313 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
adamc@108 314 end.
adamc@108 315
adamc@108 316 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 317
adamc@108 318 Eval simpl in expDenote Const MNil.
adamc@108 319 (** [[
adamc@108 320
adamc@108 321 = tt
adamc@108 322 : typeDenote Unit
adamc@108 323 ]] *)
adamc@108 324 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
adamc@108 325 (** [[
adamc@108 326
adamc@108 327 = fun x : unit => x
adamc@108 328 : typeDenote (Arrow Unit Unit)
adamc@108 329 ]] *)
adamc@108 330 Eval simpl in expDenote (Abs (dom := Unit)
adamc@108 331 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
adamc@108 332 (** [[
adamc@108 333
adamc@108 334 = fun x _ : unit => x
adamc@108 335 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 336 ]] *)
adamc@108 337 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
adamc@108 338 (** [[
adamc@108 339
adamc@108 340 = fun _ x0 : unit => x0
adamc@108 341 : typeDenote (Arrow Unit (Arrow Unit Unit))
adamc@108 342 ]] *)
adamc@108 343 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
adamc@108 344 (** [[
adamc@108 345
adamc@108 346 = tt
adamc@108 347 : typeDenote Unit
adamc@108 348 ]] *)
adamc@108 349
adamc@113 350 (* end thide *)
adamc@113 351
adamc@108 352 (** We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas. Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply-typed lambda calculus without even needing to define a syntactic substitution operation. We did it all without a single line of proof, and our implementation is manifestly executable. In a later chapter, we will meet other, more common approaches to language formalization. Such approaches often state and prove explicit theorems about type safety of languages. In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties. *)
adamc@108 353
adamc@108 354
adamc@109 355 (** * Recursive Type Definitions *)
adamc@109 356
adamc@109 357 (** There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above. Because Coq supports "type-level computation," we can redo our inductive definitions as %\textit{%#<i>#recursive#</i>#%}% definitions. *)
adamc@109 358
adamc@113 359 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
adamc@113 360
adamc@109 361 Section filist.
adamc@109 362 Variable A : Set.
adamc@109 363
adamc@113 364 (* begin thide *)
adamc@109 365 Fixpoint filist (n : nat) : Set :=
adamc@109 366 match n with
adamc@109 367 | O => unit
adamc@109 368 | S n' => A * filist n'
adamc@109 369 end%type.
adamc@109 370
adamc@109 371 (** We say that a list of length 0 has no contents, and a list of length [S n'] is a pair of a data value and a list of length [n']. *)
adamc@109 372
adamc@109 373 Fixpoint findex (n : nat) : Set :=
adamc@109 374 match n with
adamc@109 375 | O => Empty_set
adamc@109 376 | S n' => option (findex n')
adamc@109 377 end.
adamc@109 378
adamc@109 379 (** We express that there are no index values when [n = O], by defining such indices as type [Empty_set]; and we express that, at [n = S n'], there is a choice between picking the first element of the list (represented as [None]) or choosing a later element (represented by [Some idx], where [idx] is an index into the list tail). *)
adamc@109 380
adamc@109 381 Fixpoint fget (n : nat) : filist n -> findex n -> A :=
adamc@109 382 match n return filist n -> findex n -> A with
adamc@109 383 | O => fun _ idx => match idx with end
adamc@109 384 | S n' => fun ls idx =>
adamc@109 385 match idx with
adamc@109 386 | None => fst ls
adamc@109 387 | Some idx' => fget n' (snd ls) idx'
adamc@109 388 end
adamc@109 389 end.
adamc@109 390
adamc@109 391 (** Our new [get] implementation needs only one dependent [match], which just copies the stated return type of the function. Our choices of data structure implementations lead to just the right typing behavior for this new definition to work out. *)
adamc@113 392 (* end thide *)
adamc@109 393 End filist.
adamc@109 394
adamc@109 395 (** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)
adamc@109 396
adamc@113 397 (* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)
adamc@113 398
adamc@109 399 Section fhlist.
adamc@109 400 Variable A : Type.
adamc@109 401 Variable B : A -> Type.
adamc@109 402
adamc@113 403 (* begin thide *)
adamc@109 404 Fixpoint fhlist (ls : list A) : Type :=
adamc@109 405 match ls with
adamc@109 406 | nil => unit
adamc@109 407 | x :: ls' => B x * fhlist ls'
adamc@109 408 end%type.
adamc@109 409
adamc@109 410 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently-typed data elements. *)
adamc@109 411
adamc@109 412 Variable elm : A.
adamc@109 413
adamc@109 414 Fixpoint fmember (ls : list A) : Type :=
adamc@109 415 match ls with
adamc@109 416 | nil => Empty_set
adamc@109 417 | x :: ls' => (x = elm) + fmember ls'
adamc@109 418 end%type.
adamc@109 419
adamc@109 420 (** The definition of [fmember] follows the definition of [findex]. Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail. While for [index] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for. We express that with a sum type whose left branch is the appropriate equality proposition. Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
adamc@109 421
adamc@109 422 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
adamc@109 423
adamc@109 424 [[
adamc@109 425
adamc@109 426 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@109 427 match ls return fhlist ls -> fmember ls -> B elm with
adamc@109 428 | nil => fun _ idx => match idx with end
adamc@109 429 | _ :: ls' => fun mls idx =>
adamc@109 430 match idx with
adamc@109 431 | inl _ => fst mls
adamc@109 432 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 433 end
adamc@109 434 end.
adamc@109 435
adamc@109 436 Only one problem remains. The expression [fst mls] is not known to have the proper type. To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
adamc@109 437
adamc@109 438 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@109 439 match ls return fhlist ls -> fmember ls -> B elm with
adamc@109 440 | nil => fun _ idx => match idx with end
adamc@109 441 | _ :: ls' => fun mls idx =>
adamc@109 442 match idx with
adamc@109 443 | inl pf => match pf with
adamc@109 444 | refl_equal => fst mls
adamc@109 445 end
adamc@109 446 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 447 end
adamc@109 448 end.
adamc@109 449
adamc@109 450 (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker. Exactly why this works can be seen by studying the definition of equality. *)
adamc@109 451
adamc@109 452 Print eq.
adamc@109 453 (** [[
adamc@109 454
adamc@109 455 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x
adamc@109 456 ]]
adamc@109 457
adamc@109 458 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument. The type of the constructor [refl_equal] shows that [y] can only ever be instantiated to [x]. Thus, within a pattern-match with [refl_equal], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. All examples of similar dependent pattern matching that we have seen before require explicit annotations, but Coq implements a special case of annotation inference for matches on equality proofs. *)
adamc@113 459 (* end thide *)
adamc@109 460 End fhlist.
adamc@110 461
adamc@111 462 Implicit Arguments fhget [A B elm ls].
adamc@111 463
adamc@110 464
adamc@110 465 (** * Data Structures as Index Functions *)
adamc@110 466
adamc@110 467 (** Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments. In this section, we consider parameterized trees with arbitrary branching factor. *)
adamc@110 468
adamc@110 469 Section tree.
adamc@110 470 Variable A : Set.
adamc@110 471
adamc@110 472 Inductive tree : Set :=
adamc@110 473 | Leaf : A -> tree
adamc@110 474 | Node : forall n, ilist tree n -> tree.
adamc@110 475 End tree.
adamc@110 476
adamc@110 477 (** Every [Node] of a [tree] has a natural number argument, which gives the number of child trees in the second argument, typed with [ilist]. We can define two operations on trees of naturals: summing their elements and incrementing their elements. It is useful to define a generic fold function on [ilist]s first. *)
adamc@110 478
adamc@110 479 Section ifoldr.
adamc@110 480 Variables A B : Set.
adamc@110 481 Variable f : A -> B -> B.
adamc@110 482 Variable i : B.
adamc@110 483
adamc@110 484 Fixpoint ifoldr n (ls : ilist A n) {struct ls} : B :=
adamc@110 485 match ls with
adamc@110 486 | Nil => i
adamc@110 487 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 488 end.
adamc@110 489 End ifoldr.
adamc@110 490
adamc@110 491 Fixpoint sum (t : tree nat) : nat :=
adamc@110 492 match t with
adamc@110 493 | Leaf n => n
adamc@110 494 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 495 end.
adamc@110 496
adamc@110 497 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 498 match t with
adamc@110 499 | Leaf n => Leaf (S n)
adamc@110 500 | Node _ ls => Node (imap inc ls)
adamc@110 501 end.
adamc@110 502
adamc@110 503 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 504
adamc@110 505 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@113 506 (* begin thide *)
adamc@110 507 induction t; crush.
adamc@110 508 (** [[
adamc@110 509
adamc@110 510 n : nat
adamc@110 511 i : ilist (tree nat) n
adamc@110 512 ============================
adamc@110 513 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 514 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@110 515 ]]
adamc@110 516
adamc@110 517 We are left with a single subgoal which does not seem provable directly. This is the same problem that we met in Chapter 3 with other nested inductive types. *)
adamc@110 518
adamc@110 519 Check tree_ind.
adamc@110 520 (** [[
adamc@110 521
adamc@110 522 tree_ind
adamc@110 523 : forall (A : Set) (P : tree A -> Prop),
adamc@110 524 (forall a : A, P (Leaf a)) ->
adamc@110 525 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 526 forall t : tree A, P t
adamc@110 527 ]]
adamc@110 528
adamc@110 529 The automatically-generated induction principle is too weak. For the [Node] case, it gives us no inductive hypothesis. We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *)
adamc@110 530 Abort.
adamc@110 531
adamc@110 532 Reset tree.
adamc@110 533
adamc@110 534 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
adamc@110 535
adamc@110 536 Section tree.
adamc@110 537 Variable A : Set.
adamc@110 538
adamc@110 539 (** [[
adamc@110 540
adamc@110 541 Inductive tree : Set :=
adamc@110 542 | Leaf : A -> tree
adamc@110 543 | Node : forall n, filist tree n -> tree.
adamc@110 544
adamc@110 545 [[
adamc@110 546
adamc@110 547 Error: Non strictly positive occurrence of "tree" in
adamc@110 548 "forall n : nat, filist tree n -> tree"
adamc@110 549 ]]
adamc@110 550
adamc@110 551 The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually-inductive types. We defined [filist] recursively, so it may not be used for nested recursion.
adamc@110 552
adamc@110 553 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, reflexive types. Instead of merely using [index] to get elements out of [ilist], we can %\textit{%#<i>#define#</i>#%}% [ilist] in terms of [index]. For the reasons outlined above, it turns out to be easier to work with [findex] in place of [index]. *)
adamc@110 554
adamc@110 555 Inductive tree : Set :=
adamc@110 556 | Leaf : A -> tree
adamc@110 557 | Node : forall n, (findex n -> tree) -> tree.
adamc@110 558
adamc@110 559 (** A [Node] is indexed by a natural number [n], and the node's [n] children are represented as a function from [findex n] to trees, which is isomorphic to the [ilist]-based representation that we used above. *)
adamc@110 560 End tree.
adamc@110 561
adamc@110 562 Implicit Arguments Node [A n].
adamc@110 563
adamc@110 564 (** We can redefine [sum] and [inc] for our new [tree] type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose range is some [findex] type, and it folds another function over the results of calling the first function at every possible [findex] value. *)
adamc@110 565
adamc@110 566 Section rifoldr.
adamc@110 567 Variables A B : Set.
adamc@110 568 Variable f : A -> B -> B.
adamc@110 569 Variable i : B.
adamc@110 570
adamc@110 571 Fixpoint rifoldr (n : nat) : (findex n -> A) -> B :=
adamc@110 572 match n return (findex n -> A) -> B with
adamc@110 573 | O => fun _ => i
adamc@110 574 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 575 end.
adamc@110 576 End rifoldr.
adamc@110 577
adamc@110 578 Implicit Arguments rifoldr [A B n].
adamc@110 579
adamc@110 580 Fixpoint sum (t : tree nat) : nat :=
adamc@110 581 match t with
adamc@110 582 | Leaf n => n
adamc@110 583 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 584 end.
adamc@110 585
adamc@110 586 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 587 match t with
adamc@110 588 | Leaf n => Leaf (S n)
adamc@110 589 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 590 end.
adamc@110 591
adamc@110 592 (** Now we are ready to prove the theorem where we got stuck before. We will not need to define any new induction principle, but it %\textit{%#<i>#will#</i>#%}% be helpful to prove some lemmas. *)
adamc@110 593
adamc@110 594 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 595 x1 >= x2
adamc@110 596 -> y1 >= y2
adamc@110 597 -> x1 + y1 >= x2 + y2.
adamc@110 598 crush.
adamc@110 599 Qed.
adamc@110 600
adamc@110 601 Lemma sum_inc' : forall n (f1 f2 : findex n -> nat),
adamc@110 602 (forall idx, f1 idx >= f2 idx)
adamc@110 603 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 604 Hint Resolve plus_ge.
adamc@110 605
adamc@110 606 induction n; crush.
adamc@110 607 Qed.
adamc@110 608
adamc@110 609 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 610 Hint Resolve sum_inc'.
adamc@110 611
adamc@110 612 induction t; crush.
adamc@110 613 Qed.
adamc@110 614
adamc@113 615 (* end thide *)
adamc@113 616
adamc@110 617 (** Even if Coq would generate complete induction principles automatically for nested inductive definitions like the one we started with, there would still be advantages to using this style of reflexive encoding. We see one of those advantages in the definition of [inc], where we did not need to use any kind of auxiliary function. In general, reflexive encodings often admit direct implementations of operations that would require recursion if performed with more traditional inductive data structures. *)
adamc@111 618
adamc@111 619 (** ** Another Interpreter Example *)
adamc@111 620
adamc@112 621 (** We develop another example of variable-arity constructors, in the form of optimization of a small expression language with a construct like Scheme's %\texttt{%#<tt>#cond#</tt>#%}%. Each of our conditional expressions takes a list of pairs of boolean tests and bodies. The value of the conditional comes from the body of the first test in the list to evaluate to [true]. To simplify the interpreter we will write, we force each conditional to include a final, default case. *)
adamc@112 622
adamc@112 623 Inductive type' : Type := Nat | Bool.
adamc@111 624
adamc@111 625 Inductive exp' : type' -> Type :=
adamc@112 626 | NConst : nat -> exp' Nat
adamc@112 627 | Plus : exp' Nat -> exp' Nat -> exp' Nat
adamc@112 628 | Eq : exp' Nat -> exp' Nat -> exp' Bool
adamc@111 629
adamc@112 630 | BConst : bool -> exp' Bool
adamc@113 631 (* begin thide *)
adamc@112 632 | Cond : forall n t, (findex n -> exp' Bool)
adamc@111 633 -> (findex n -> exp' t) -> exp' t -> exp' t.
adamc@113 634 (* end thide *)
adamc@111 635
adamc@112 636 (** A [Cond] is parameterized by a natural [n], which tells us how many cases this conditional has. The test expressions are represented with a function of type [findex n -> exp' Bool], and the bodies are represented with a function of type [findex n -> exp' t], where [t] is the overall type. The final [exp' t] argument is the default case.
adamc@112 637
adamc@112 638 We start implementing our interpreter with a standard type denotation function. *)
adamc@112 639
adamc@111 640 Definition type'Denote (t : type') : Set :=
adamc@111 641 match t with
adamc@112 642 | Nat => nat
adamc@112 643 | Bool => bool
adamc@111 644 end.
adamc@111 645
adamc@112 646 (** To implement the expression interpreter, it is useful to have the following function that implements the functionality of [Cond] without involving any syntax. *)
adamc@112 647
adamc@113 648 (* begin thide *)
adamc@111 649 Section cond.
adamc@111 650 Variable A : Set.
adamc@111 651 Variable default : A.
adamc@111 652
adamc@111 653 Fixpoint cond (n : nat) : (findex n -> bool) -> (findex n -> A) -> A :=
adamc@111 654 match n return (findex n -> bool) -> (findex n -> A) -> A with
adamc@111 655 | O => fun _ _ => default
adamc@111 656 | S n' => fun tests bodies =>
adamc@111 657 if tests None
adamc@111 658 then bodies None
adamc@111 659 else cond n'
adamc@111 660 (fun idx => tests (Some idx))
adamc@111 661 (fun idx => bodies (Some idx))
adamc@111 662 end.
adamc@111 663 End cond.
adamc@111 664
adamc@111 665 Implicit Arguments cond [A n].
adamc@113 666 (* end thide *)
adamc@111 667
adamc@112 668 (** Now the expression interpreter is straightforward to write. *)
adamc@112 669
adamc@111 670 Fixpoint exp'Denote t (e : exp' t) {struct e} : type'Denote t :=
adamc@111 671 match e in exp' t return type'Denote t with
adamc@111 672 | NConst n =>
adamc@111 673 n
adamc@111 674 | Plus e1 e2 =>
adamc@111 675 exp'Denote e1 + exp'Denote e2
adamc@111 676 | Eq e1 e2 =>
adamc@111 677 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adamc@111 678
adamc@111 679 | BConst b =>
adamc@111 680 b
adamc@111 681 | Cond _ _ tests bodies default =>
adamc@113 682 (* begin thide *)
adamc@111 683 cond
adamc@111 684 (exp'Denote default)
adamc@111 685 (fun idx => exp'Denote (tests idx))
adamc@111 686 (fun idx => exp'Denote (bodies idx))
adamc@113 687 (* end thide *)
adamc@111 688 end.
adamc@111 689
adamc@112 690 (** We will implement a constant-folding function that optimizes conditionals, removing cases with known-[false] tests and cases that come after known-[true] tests. A function [cfoldCond] implements the heart of this logic. The convoy pattern is used again near the end of the implementation. *)
adamc@112 691
adamc@113 692 (* begin thide *)
adamc@111 693 Section cfoldCond.
adamc@111 694 Variable t : type'.
adamc@111 695 Variable default : exp' t.
adamc@111 696
adamc@112 697 Fixpoint cfoldCond (n : nat)
adamc@112 698 : (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t :=
adamc@112 699 match n return (findex n -> exp' Bool) -> (findex n -> exp' t) -> exp' t with
adamc@111 700 | O => fun _ _ => default
adamc@111 701 | S n' => fun tests bodies =>
adamc@111 702 match tests None with
adamc@111 703 | BConst true => bodies None
adamc@111 704 | BConst false => cfoldCond n'
adamc@111 705 (fun idx => tests (Some idx))
adamc@111 706 (fun idx => bodies (Some idx))
adamc@111 707 | _ =>
adamc@111 708 let e := cfoldCond n'
adamc@111 709 (fun idx => tests (Some idx))
adamc@111 710 (fun idx => bodies (Some idx)) in
adamc@112 711 match e in exp' t return exp' t -> exp' t with
adamc@112 712 | Cond n _ tests' bodies' default' => fun body =>
adamc@111 713 Cond
adamc@111 714 (S n)
adamc@111 715 (fun idx => match idx with
adamc@112 716 | None => tests None
adamc@111 717 | Some idx => tests' idx
adamc@111 718 end)
adamc@111 719 (fun idx => match idx with
adamc@111 720 | None => body
adamc@111 721 | Some idx => bodies' idx
adamc@111 722 end)
adamc@111 723 default'
adamc@112 724 | e => fun body =>
adamc@111 725 Cond
adamc@111 726 1
adamc@112 727 (fun _ => tests None)
adamc@111 728 (fun _ => body)
adamc@111 729 e
adamc@112 730 end (bodies None)
adamc@111 731 end
adamc@111 732 end.
adamc@111 733 End cfoldCond.
adamc@111 734
adamc@111 735 Implicit Arguments cfoldCond [t n].
adamc@113 736 (* end thide *)
adamc@111 737
adamc@112 738 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
adamc@112 739
adamc@111 740 Fixpoint cfold t (e : exp' t) {struct e} : exp' t :=
adamc@111 741 match e in exp' t return exp' t with
adamc@111 742 | NConst n => NConst n
adamc@111 743 | Plus e1 e2 =>
adamc@111 744 let e1' := cfold e1 in
adamc@111 745 let e2' := cfold e2 in
adamc@111 746 match e1', e2' with
adamc@111 747 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@111 748 | _, _ => Plus e1' e2'
adamc@111 749 end
adamc@111 750 | Eq e1 e2 =>
adamc@111 751 let e1' := cfold e1 in
adamc@111 752 let e2' := cfold e2 in
adamc@111 753 match e1', e2' with
adamc@111 754 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@111 755 | _, _ => Eq e1' e2'
adamc@111 756 end
adamc@111 757
adamc@111 758 | BConst b => BConst b
adamc@111 759 | Cond _ _ tests bodies default =>
adamc@113 760 (* begin thide *)
adamc@111 761 cfoldCond
adamc@111 762 (cfold default)
adamc@111 763 (fun idx => cfold (tests idx))
adamc@111 764 (fun idx => cfold (bodies idx))
adamc@113 765 (* end thide *)
adamc@111 766 end.
adamc@111 767
adamc@113 768 (* begin thide *)
adamc@112 769 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. This lemma formalizes that property. The proof is a standard mostly-automated one, with the only wrinkle being a guided instantation of the quantifiers in the induction hypothesis. *)
adamc@112 770
adamc@111 771 Lemma cfoldCond_correct : forall t (default : exp' t)
adamc@112 772 n (tests : findex n -> exp' Bool) (bodies : findex n -> exp' t),
adamc@111 773 exp'Denote (cfoldCond default tests bodies)
adamc@111 774 = exp'Denote (Cond n tests bodies default).
adamc@111 775 induction n; crush;
adamc@111 776 match goal with
adamc@111 777 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
adamc@111 778 generalize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)));
adamc@111 779 clear IHn; intro IHn
adamc@111 780 end;
adamc@111 781 repeat (match goal with
adamc@111 782 | [ |- context[match ?E with
adamc@111 783 | NConst _ => _
adamc@111 784 | Plus _ _ => _
adamc@111 785 | Eq _ _ => _
adamc@111 786 | BConst _ => _
adamc@111 787 | Cond _ _ _ _ _ => _
adamc@111 788 end] ] => dep_destruct E
adamc@111 789 | [ |- context[if ?B then _ else _] ] => destruct B
adamc@111 790 end; crush).
adamc@111 791 Qed.
adamc@111 792
adamc@112 793 (** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old. It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal. We treat this issue with our discussion of axioms in a later chapter. For now, it suffices to prove that the particular function [cond] is %\textit{%#<i>#extensional#</i>#%}%; that is, it is unaffected by substitution of functions with input-output equivalents. *)
adamc@112 794
adamc@111 795 Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : findex n -> bool)
adamc@111 796 (bodies bodies' : findex n -> A),
adamc@111 797 (forall idx, tests idx = tests' idx)
adamc@111 798 -> (forall idx, bodies idx = bodies' idx)
adamc@111 799 -> cond default tests bodies
adamc@111 800 = cond default tests' bodies'.
adamc@111 801 induction n; crush;
adamc@111 802 match goal with
adamc@111 803 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@111 804 end; crush.
adamc@111 805 Qed.
adamc@111 806
adamc@112 807 (** Now the final theorem is easy to prove. We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct. *)
adamc@113 808 (* end thide *)
adamc@112 809
adamc@111 810 Theorem cfold_correct : forall t (e : exp' t),
adamc@111 811 exp'Denote (cfold e) = exp'Denote e.
adamc@113 812 (* begin thide *)
adamc@111 813 Hint Rewrite cfoldCond_correct : cpdt.
adamc@111 814 Hint Resolve cond_ext.
adamc@111 815
adamc@111 816 induction e; crush;
adamc@111 817 repeat (match goal with
adamc@111 818 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@111 819 end; crush).
adamc@111 820 Qed.
adamc@113 821 (* end thide *)