Mercurial > cpdt > repo

annotate src/DataStruct.v @ 473:39c204d2262c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove hyperlinks to standard library, which were broken anyway
author Adam Chlipala <adam@chlipala.net>
date Mon, 22 Oct 2012 13:28:54 -0400
parents 218361342cd2
children 1fd4109f7b31
rev   line source
adam@398 1 (* Copyright (c) 2008-2012, 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
adam@314 13 Require Import CpdtTactics.
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
adam@342 26 (** We begin with a deeper look at the length-indexed lists that began the last chapter.%\index{Gallina terms!ilist}% *)
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
adam@426 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{Gallina terms!fin}%[fin], where [fin n] is isomorphic to [{m : nat | m < n}]. The type family name stands 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@215 40 Inductive fin : nat -> Set :=
adamc@215 41 | First : forall n, fin (S n)
adamc@215 42 | Next : forall n, fin n -> fin (S n).
adamc@105 43
adam@406 44 (** An instance of [fin] is essentially 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. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
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@215 48 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 49 match ls with
adamc@106 50 | Nil => fun idx => ?
adamc@106 51 | Cons _ x ls' => fun idx =>
adamc@106 52 match idx with
adamc@106 53 | First _ => x
adamc@106 54 | Next _ idx' => get ls' idx'
adamc@106 55 end
adamc@106 56 end.
adamc@205 57 ]]
adam@443 58 %\vspace{-.15in}%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 [fin] 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 59 [[
adamc@215 60 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 61 match ls with
adamc@106 62 | Nil => fun idx =>
adamc@215 63 match idx in fin n' return (match n' with
adamc@106 64 | O => A
adamc@106 65 | S _ => unit
adamc@106 66 end) with
adamc@106 67 | First _ => tt
adamc@106 68 | Next _ _ => tt
adamc@106 69 end
adamc@106 70 | Cons _ x ls' => fun idx =>
adamc@106 71 match idx with
adamc@106 72 | First _ => x
adamc@106 73 | Next _ idx' => get ls' idx'
adamc@106 74 end
adamc@106 75 end.
adamc@205 76 ]]
adam@443 77 %\vspace{-.15in}%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']. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A]. We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
adam@284 78
adam@284 79 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 the convoy pattern that we met last chapter. This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables.
adamc@106 80 [[
adamc@215 81 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 82 match ls with
adamc@106 83 | Nil => fun idx =>
adamc@215 84 match idx in fin n' return (match n' with
adamc@106 85 | O => A
adamc@106 86 | S _ => unit
adamc@106 87 end) with
adamc@106 88 | First _ => tt
adamc@106 89 | Next _ _ => tt
adamc@106 90 end
adamc@106 91 | Cons _ x ls' => fun idx =>
adamc@215 92 match idx in fin n' return ilist (pred n') -> A with
adamc@106 93 | First _ => fun _ => x
adamc@106 94 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 95 end ls'
adamc@106 96 end.
adamc@205 97 ]]
adam@443 98 %\vspace{-.15in}%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 99
adamc@215 100 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 101 match ls with
adamc@105 102 | Nil => fun idx =>
adamc@215 103 match idx in fin n' return (match n' with
adamc@105 104 | O => A
adamc@105 105 | S _ => unit
adamc@105 106 end) with
adamc@105 107 | First _ => tt
adamc@105 108 | Next _ _ => tt
adamc@105 109 end
adamc@105 110 | Cons _ x ls' => fun idx =>
adamc@215 111 match idx in fin n' return (fin (pred n') -> A) -> A with
adamc@105 112 | First _ => fun _ => x
adamc@105 113 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 114 end (get ls')
adamc@105 115 end.
adamc@113 116 (* end thide *)
adamc@105 117 End ilist.
adamc@105 118
adamc@105 119 Implicit Arguments Nil [A].
adamc@108 120 Implicit Arguments First [n].
adamc@105 121
adamc@108 122 (** A few examples show how to make use of these definitions. *)
adamc@108 123
adamc@108 124 Check Cons 0 (Cons 1 (Cons 2 Nil)).
adamc@215 125 (** %\vspace{-.15in}% [[
adamc@215 126 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 127 : ilist nat 3
adam@302 128 ]]
adam@302 129 *)
adamc@215 130
adamc@113 131 (* begin thide *)
adamc@108 132 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@215 133 (** %\vspace{-.15in}% [[
adamc@108 134 = 0
adamc@108 135 : nat
adam@302 136 ]]
adam@302 137 *)
adamc@215 138
adamc@108 139 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@215 140 (** %\vspace{-.15in}% [[
adamc@108 141 = 1
adamc@108 142 : nat
adam@302 143 ]]
adam@302 144 *)
adamc@215 145
adamc@108 146 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@215 147 (** %\vspace{-.15in}% [[
adamc@108 148 = 2
adamc@108 149 : nat
adam@302 150 ]]
adam@302 151 *)
adamc@113 152 (* end thide *)
adamc@108 153
adam@426 154 (* begin hide *)
adam@437 155 (* begin thide *)
adam@426 156 Definition map' := map.
adam@437 157 (* end thide *)
adam@426 158 (* end hide *)
adam@426 159
adamc@108 160 (** 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 161
adamc@105 162 Section ilist_map.
adamc@105 163 Variables A B : Set.
adamc@105 164 Variable f : A -> B.
adamc@105 165
adamc@215 166 Fixpoint imap n (ls : ilist A n) : ilist B n :=
adamc@215 167 match ls with
adamc@105 168 | Nil => Nil
adamc@105 169 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 170 end.
adamc@105 171
adam@426 172 (** It is easy to prove that [get] "distributes over" [imap] calls. *)
adamc@107 173
adam@342 174 (* EX: Prove that [get] distributes over [imap]. *)
adam@342 175
adam@342 176 (* begin thide *)
adamc@215 177 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n),
adamc@105 178 get (imap ls) idx = f (get ls idx).
adamc@107 179 induction ls; dep_destruct idx; crush.
adamc@105 180 Qed.
adamc@113 181 (* end thide *)
adamc@105 182 End ilist_map.
adamc@107 183
adam@406 184 (** The only tricky bit is remembering to use our [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *)
adamc@107 185
adamc@107 186 (** * Heterogeneous Lists *)
adamc@107 187
adam@426 188 (** 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 we can do it much more cleanly and directly in Coq. *)
adamc@107 189
adamc@107 190 Section hlist.
adamc@107 191 Variable A : Type.
adamc@107 192 Variable B : A -> Type.
adamc@107 193
adamc@113 194 (* 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 195
adam@342 196 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B].%\index{Gallina terms!hlist}% *)
adamc@107 197
adamc@113 198 (* begin thide *)
adamc@107 199 Inductive hlist : list A -> Type :=
adam@457 200 | HNil : hlist nil
adam@457 201 | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 202
adam@342 203 (** 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.%\index{Gallina terms!member}% *)
adamc@107 204
adamc@113 205 (* end thide *)
adamc@113 206 (* EX: Define an analogue to [get] for [hlist]s. *)
adamc@113 207
adamc@113 208 (* begin thide *)
adamc@107 209 Variable elm : A.
adamc@107 210
adamc@107 211 Inductive member : list A -> Type :=
adam@463 212 | HFirst : forall ls, member (elm :: ls)
adam@463 213 | HNext : forall x ls, member ls -> member (x :: ls).
adamc@107 214
adam@426 215 (** 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 216
adam@457 217 We can use [member] to adapt our definition of [get] to [hlist]s. The same basic [match] tricks apply. In the [HCons] 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 218
adamc@215 219 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
adamc@215 220 match mls with
adam@457 221 | HNil => fun mem =>
adamc@107 222 match mem in member ls' return (match ls' with
adamc@107 223 | nil => B elm
adamc@107 224 | _ :: _ => unit
adamc@107 225 end) with
adam@463 226 | HFirst _ => tt
adam@463 227 | HNext _ _ _ => tt
adamc@107 228 end
adam@457 229 | HCons _ _ x mls' => fun mem =>
adamc@107 230 match mem in member ls' return (match ls' with
adamc@107 231 | nil => Empty_set
adamc@107 232 | x' :: ls'' =>
adam@437 233 B x' -> (member ls'' -> B elm)
adam@437 234 -> B elm
adamc@107 235 end) with
adam@463 236 | HFirst _ => fun x _ => x
adam@463 237 | HNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@107 238 end x (hget mls')
adamc@107 239 end.
adamc@113 240 (* end thide *)
adamc@107 241 End hlist.
adamc@108 242
adamc@113 243 (* begin thide *)
adam@457 244 Implicit Arguments HNil [A B].
adam@457 245 Implicit Arguments HCons [A B x ls].
adamc@108 246
adam@463 247 Implicit Arguments HFirst [A elm ls].
adam@463 248 Implicit Arguments HNext [A elm x ls].
adamc@113 249 (* end thide *)
adamc@108 250
adamc@108 251 (** 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 252
adamc@108 253 Definition someTypes : list Set := nat :: bool :: nil.
adamc@108 254
adamc@113 255 (* begin thide *)
adamc@113 256
adamc@108 257 Example someValues : hlist (fun T : Set => T) someTypes :=
adam@457 258 HCons 5 (HCons true HNil).
adamc@108 259
adam@463 260 Eval simpl in hget someValues HFirst.
adamc@215 261 (** %\vspace{-.15in}% [[
adamc@108 262 = 5
adamc@108 263 : (fun T : Set => T) nat
adam@302 264 ]]
adam@302 265 *)
adamc@215 266
adam@463 267 Eval simpl in hget someValues (HNext HFirst).
adamc@215 268 (** %\vspace{-.15in}% [[
adamc@108 269 = true
adamc@108 270 : (fun T : Set => T) bool
adam@302 271 ]]
adam@302 272 *)
adamc@108 273
adamc@108 274 (** We can also build indexed lists of pairs in this way. *)
adamc@108 275
adamc@108 276 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
adam@457 277 HCons (1, 2) (HCons (true, false) HNil).
adamc@108 278
adam@443 279 (** There are many more useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)
adam@443 280
adamc@113 281 (* end thide *)
adamc@113 282
adamc@113 283
adamc@108 284 (** ** A Lambda Calculus Interpreter *)
adamc@108 285
adam@455 286 (** Heterogeneous lists are very useful in implementing %\index{interpreters}%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%\index{lambda calculus}%. Our interpreter can alternatively be thought of as a denotational semantics (but worry not if you are not familiar with such terminology from semantics).
adamc@108 287
adamc@108 288 We start with an algebraic datatype for types. *)
adamc@108 289
adamc@108 290 Inductive type : Set :=
adamc@108 291 | Unit : type
adamc@108 292 | Arrow : type -> type -> type.
adamc@108 293
adam@342 294 (** 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 index variable representation%~\cite{DeBruijn}%. 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 295
adamc@108 296 Inductive exp : list type -> type -> Set :=
adamc@108 297 | Const : forall ts, exp ts Unit
adamc@113 298 (* begin thide *)
adamc@108 299 | Var : forall ts t, member t ts -> exp ts t
adamc@108 300 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 301 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@113 302 (* end thide *)
adamc@108 303
adamc@108 304 Implicit Arguments Const [ts].
adamc@108 305
adamc@108 306 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 307
adamc@108 308 Fixpoint typeDenote (t : type) : Set :=
adamc@108 309 match t with
adamc@108 310 | Unit => unit
adamc@108 311 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 312 end.
adamc@108 313
adam@457 314 (** 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 [HCons] to extend the environment in the [Abs] case. *)
adamc@108 315
adamc@113 316 (* EX: Define an interpreter for [exp]s. *)
adamc@113 317
adamc@113 318 (* begin thide *)
adamc@215 319 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
adamc@215 320 match e with
adamc@108 321 | Const _ => fun _ => tt
adamc@108 322
adamc@108 323 | Var _ _ mem => fun s => hget s mem
adamc@108 324 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adam@457 325 | Abs _ _ _ e' => fun s => fun x => expDenote e' (HCons x s)
adamc@108 326 end.
adamc@108 327
adamc@108 328 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 329
adam@457 330 Eval simpl in expDenote Const HNil.
adamc@215 331 (** %\vspace{-.15in}% [[
adamc@108 332 = tt
adamc@108 333 : typeDenote Unit
adam@302 334 ]]
adam@302 335 *)
adamc@215 336
adam@463 337 Eval simpl in expDenote (Abs (dom := Unit) (Var HFirst)) HNil.
adamc@215 338 (** %\vspace{-.15in}% [[
adamc@108 339 = fun x : unit => x
adamc@108 340 : typeDenote (Arrow Unit Unit)
adam@302 341 ]]
adam@302 342 *)
adamc@215 343
adamc@108 344 Eval simpl in expDenote (Abs (dom := Unit)
adam@463 345 (Abs (dom := Unit) (Var (HNext HFirst)))) HNil.
adamc@215 346 (** %\vspace{-.15in}% [[
adamc@108 347 = fun x _ : unit => x
adamc@108 348 : typeDenote (Arrow Unit (Arrow Unit Unit))
adam@302 349 ]]
adam@302 350 *)
adamc@215 351
adam@463 352 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var HFirst))) HNil.
adamc@215 353 (** %\vspace{-.15in}% [[
adamc@108 354 = fun _ x0 : unit => x0
adamc@108 355 : typeDenote (Arrow Unit (Arrow Unit Unit))
adam@302 356 ]]
adam@302 357 *)
adamc@215 358
adam@463 359 Eval simpl in expDenote (App (Abs (Var HFirst)) Const) HNil.
adamc@215 360 (** %\vspace{-.15in}% [[
adamc@108 361 = tt
adamc@108 362 : typeDenote Unit
adam@302 363 ]]
adam@302 364 *)
adamc@108 365
adamc@113 366 (* end thide *)
adamc@113 367
adam@342 368 (** 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. Other, more common approaches to language formalization 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 369
adamc@108 370
adamc@109 371 (** * Recursive Type Definitions *)
adamc@109 372
adam@426 373 (** %\index{recursive type definition}%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 _recursive_ definitions. *)
adamc@109 374
adamc@113 375 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
adamc@113 376
adamc@109 377 Section filist.
adamc@109 378 Variable A : Set.
adamc@109 379
adamc@113 380 (* begin thide *)
adamc@109 381 Fixpoint filist (n : nat) : Set :=
adamc@109 382 match n with
adamc@109 383 | O => unit
adamc@109 384 | S n' => A * filist n'
adamc@109 385 end%type.
adamc@109 386
adamc@109 387 (** 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 388
adamc@215 389 Fixpoint ffin (n : nat) : Set :=
adamc@109 390 match n with
adamc@109 391 | O => Empty_set
adamc@215 392 | S n' => option (ffin n')
adamc@109 393 end.
adamc@109 394
adam@406 395 (** 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). For instance, the three values of type [ffin 3] are [None], [Some None], and [Some (Some None)]. *)
adamc@109 396
adamc@215 397 Fixpoint fget (n : nat) : filist n -> ffin n -> A :=
adamc@215 398 match n with
adamc@109 399 | O => fun _ idx => match idx with end
adamc@109 400 | S n' => fun ls idx =>
adamc@109 401 match idx with
adamc@109 402 | None => fst ls
adamc@109 403 | Some idx' => fget n' (snd ls) idx'
adamc@109 404 end
adamc@109 405 end.
adamc@109 406
adamc@215 407 (** Our new [get] implementation needs only one dependent [match], and its annotation is inferred for us. Our choices of data structure implementations lead to just the right typing behavior for this new definition to work out. *)
adamc@113 408 (* end thide *)
adamc@215 409
adamc@109 410 End filist.
adamc@109 411
adamc@109 412 (** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)
adamc@109 413
adamc@113 414 (* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)
adamc@113 415
adamc@109 416 Section fhlist.
adamc@109 417 Variable A : Type.
adamc@109 418 Variable B : A -> Type.
adamc@109 419
adamc@113 420 (* begin thide *)
adamc@109 421 Fixpoint fhlist (ls : list A) : Type :=
adamc@109 422 match ls with
adamc@109 423 | nil => unit
adamc@109 424 | x :: ls' => B x * fhlist ls'
adamc@109 425 end%type.
adamc@109 426
adam@342 427 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently typed data elements. *)
adamc@109 428
adamc@109 429 Variable elm : A.
adamc@109 430
adamc@109 431 Fixpoint fmember (ls : list A) : Type :=
adamc@109 432 match ls with
adamc@109 433 | nil => Empty_set
adamc@109 434 | x :: ls' => (x = elm) + fmember ls'
adamc@109 435 end%type.
adamc@109 436
adam@455 437 (** The definition of [fmember] follows the definition of [ffin]. 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 [ffin] 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 idea 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 438
adamc@109 439 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
adamc@109 440 [[
adamc@109 441 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 442 match ls with
adamc@109 443 | nil => fun _ idx => match idx with end
adamc@109 444 | _ :: ls' => fun mls idx =>
adamc@109 445 match idx with
adamc@109 446 | inl _ => fst mls
adamc@109 447 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 448 end
adamc@109 449 end.
adamc@205 450 ]]
adam@443 451 %\vspace{-.15in}%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 452
adamc@109 453 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 454 match ls with
adamc@109 455 | nil => fun _ idx => match idx with end
adamc@109 456 | _ :: ls' => fun mls idx =>
adamc@109 457 match idx with
adamc@109 458 | inl pf => match pf with
adam@426 459 | eq_refl => fst mls
adamc@109 460 end
adamc@109 461 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 462 end
adamc@109 463 end.
adamc@109 464
adamc@109 465 (** 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 466
adam@426 467 (* begin hide *)
adam@437 468 (* begin thide *)
adam@437 469 Definition foo := @eq_refl.
adam@437 470 (* end thide *)
adam@426 471 (* end hide *)
adam@426 472
adamc@109 473 Print eq.
adamc@215 474 (** %\vspace{-.15in}% [[
adam@426 475 Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
adamc@109 476 ]]
adamc@109 477
adam@426 478 In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument. The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x]. Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
adamc@113 479 (* end thide *)
adamc@215 480
adamc@109 481 End fhlist.
adamc@110 482
adamc@111 483 Implicit Arguments fhget [A B elm ls].
adamc@111 484
adam@455 485 (** How does one choose between the two data structure encoding strategies we have presented so far? Before answering that question in this chapter's final section, we introduce one further approach. *)
adam@455 486
adamc@110 487
adamc@110 488 (** * Data Structures as Index Functions *)
adamc@110 489
adam@342 490 (** %\index{index function}%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 491
adamc@110 492 Section tree.
adamc@110 493 Variable A : Set.
adamc@110 494
adamc@110 495 Inductive tree : Set :=
adamc@110 496 | Leaf : A -> tree
adamc@110 497 | Node : forall n, ilist tree n -> tree.
adamc@110 498 End tree.
adamc@110 499
adamc@110 500 (** 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 501
adamc@110 502 Section ifoldr.
adamc@110 503 Variables A B : Set.
adamc@110 504 Variable f : A -> B -> B.
adamc@110 505 Variable i : B.
adamc@110 506
adamc@215 507 Fixpoint ifoldr n (ls : ilist A n) : B :=
adamc@110 508 match ls with
adamc@110 509 | Nil => i
adamc@110 510 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 511 end.
adamc@110 512 End ifoldr.
adamc@110 513
adamc@110 514 Fixpoint sum (t : tree nat) : nat :=
adamc@110 515 match t with
adamc@110 516 | Leaf n => n
adamc@110 517 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 518 end.
adamc@110 519
adamc@110 520 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 521 match t with
adamc@110 522 | Leaf n => Leaf (S n)
adamc@110 523 | Node _ ls => Node (imap inc ls)
adamc@110 524 end.
adamc@110 525
adamc@110 526 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 527
adamc@110 528 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@113 529 (* begin thide *)
adamc@110 530 induction t; crush.
adamc@110 531 (** [[
adamc@110 532 n : nat
adamc@110 533 i : ilist (tree nat) n
adamc@110 534 ============================
adamc@110 535 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 536 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@215 537
adamc@110 538 ]]
adamc@110 539
adam@342 540 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 %\index{nested inductive type}%nested inductive types. *)
adamc@110 541
adamc@110 542 Check tree_ind.
adamc@215 543 (** %\vspace{-.15in}% [[
adamc@215 544 tree_ind
adamc@110 545 : forall (A : Set) (P : tree A -> Prop),
adamc@110 546 (forall a : A, P (Leaf a)) ->
adamc@110 547 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 548 forall t : tree A, P t
adamc@110 549 ]]
adamc@110 550
adam@342 551 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@215 552
adamc@110 553 Abort.
adamc@110 554
adamc@110 555 Reset tree.
adamc@110 556
adamc@110 557 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
adamc@110 558
adamc@110 559 Section tree.
adamc@110 560 Variable A : Set.
adamc@110 561
adamc@215 562 (** %\vspace{-.15in}% [[
adamc@110 563 Inductive tree : Set :=
adamc@110 564 | Leaf : A -> tree
adamc@110 565 | Node : forall n, filist tree n -> tree.
adam@342 566 ]]
adamc@110 567
adam@342 568 <<
adamc@110 569 Error: Non strictly positive occurrence of "tree" in
adamc@110 570 "forall n : nat, filist tree n -> tree"
adam@342 571 >>
adamc@110 572
adam@342 573 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 574
adam@398 575 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, %\index{reflexive inductive type}%reflexive types. Instead of merely using [fin] to get elements out of [ilist], we can _define_ [ilist] in terms of [fin]. For the reasons outlined above, it turns out to be easier to work with [ffin] in place of [fin]. *)
adamc@110 576
adamc@110 577 Inductive tree : Set :=
adamc@110 578 | Leaf : A -> tree
adamc@215 579 | Node : forall n, (ffin n -> tree) -> tree.
adamc@110 580
adamc@215 581 (** A [Node] is indexed by a natural number [n], and the node's [n] children are represented as a function from [ffin n] to trees, which is isomorphic to the [ilist]-based representation that we used above. *)
adamc@215 582
adamc@110 583 End tree.
adamc@110 584
adamc@110 585 Implicit Arguments Node [A n].
adamc@110 586
adamc@215 587 (** 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 [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
adamc@110 588
adamc@110 589 Section rifoldr.
adamc@110 590 Variables A B : Set.
adamc@110 591 Variable f : A -> B -> B.
adamc@110 592 Variable i : B.
adamc@110 593
adamc@215 594 Fixpoint rifoldr (n : nat) : (ffin n -> A) -> B :=
adamc@215 595 match n with
adamc@110 596 | O => fun _ => i
adamc@110 597 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 598 end.
adamc@110 599 End rifoldr.
adamc@110 600
adamc@110 601 Implicit Arguments rifoldr [A B n].
adamc@110 602
adamc@110 603 Fixpoint sum (t : tree nat) : nat :=
adamc@110 604 match t with
adamc@110 605 | Leaf n => n
adamc@110 606 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 607 end.
adamc@110 608
adamc@110 609 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 610 match t with
adamc@110 611 | Leaf n => Leaf (S n)
adamc@110 612 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 613 end.
adamc@110 614
adam@398 615 (** 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 _will_ be helpful to prove some lemmas. *)
adamc@110 616
adamc@110 617 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 618 x1 >= x2
adamc@110 619 -> y1 >= y2
adamc@110 620 -> x1 + y1 >= x2 + y2.
adamc@110 621 crush.
adamc@110 622 Qed.
adamc@110 623
adamc@215 624 Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat),
adamc@110 625 (forall idx, f1 idx >= f2 idx)
adamc@110 626 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 627 Hint Resolve plus_ge.
adamc@110 628
adamc@110 629 induction n; crush.
adamc@110 630 Qed.
adamc@110 631
adamc@110 632 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 633 Hint Resolve sum_inc'.
adamc@110 634
adamc@110 635 induction t; crush.
adamc@110 636 Qed.
adamc@110 637
adamc@113 638 (* end thide *)
adamc@113 639
adamc@110 640 (** 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 641
adamc@111 642 (** ** Another Interpreter Example *)
adamc@111 643
adam@426 644 (** We develop another example of variable-arity constructors, in the form of optimization of a small expression language with a construct like Scheme's <<cond>>. 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 %\index{interpreters}%interpreter we will write, we force each conditional to include a final, default case. *)
adamc@112 645
adamc@112 646 Inductive type' : Type := Nat | Bool.
adamc@111 647
adamc@111 648 Inductive exp' : type' -> Type :=
adamc@112 649 | NConst : nat -> exp' Nat
adamc@112 650 | Plus : exp' Nat -> exp' Nat -> exp' Nat
adamc@112 651 | Eq : exp' Nat -> exp' Nat -> exp' Bool
adamc@111 652
adamc@112 653 | BConst : bool -> exp' Bool
adamc@113 654 (* begin thide *)
adamc@215 655 | Cond : forall n t, (ffin n -> exp' Bool)
adamc@215 656 -> (ffin n -> exp' t) -> exp' t -> exp' t.
adamc@113 657 (* end thide *)
adamc@111 658
adam@284 659 (** 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 [ffin n -> exp' Bool], and the bodies are represented with a function of type [ffin n -> exp' t], where [t] is the overall type. The final [exp' t] argument is the default case. For example, here is an expression that successively checks whether [2 + 2 = 5] (returning 0 if so) or if [1 + 1 = 2] (returning 1 if so), returning 2 otherwise. *)
adamc@112 660
adam@284 661 Example ex1 := Cond 2
adam@284 662 (fun f => match f with
adam@284 663 | None => Eq (Plus (NConst 2) (NConst 2)) (NConst 5)
adam@284 664 | Some None => Eq (Plus (NConst 1) (NConst 1)) (NConst 2)
adam@284 665 | Some (Some v) => match v with end
adam@284 666 end)
adam@284 667 (fun f => match f with
adam@284 668 | None => NConst 0
adam@284 669 | Some None => NConst 1
adam@284 670 | Some (Some v) => match v with end
adam@284 671 end)
adam@284 672 (NConst 2).
adam@284 673
adam@284 674 (** We start implementing our interpreter with a standard type denotation function. *)
adamc@112 675
adamc@111 676 Definition type'Denote (t : type') : Set :=
adamc@111 677 match t with
adamc@112 678 | Nat => nat
adamc@112 679 | Bool => bool
adamc@111 680 end.
adamc@111 681
adamc@112 682 (** 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 683
adamc@113 684 (* begin thide *)
adamc@111 685 Section cond.
adamc@111 686 Variable A : Set.
adamc@111 687 Variable default : A.
adamc@111 688
adamc@215 689 Fixpoint cond (n : nat) : (ffin n -> bool) -> (ffin n -> A) -> A :=
adamc@215 690 match n with
adamc@111 691 | O => fun _ _ => default
adamc@111 692 | S n' => fun tests bodies =>
adamc@111 693 if tests None
adamc@111 694 then bodies None
adamc@111 695 else cond n'
adamc@111 696 (fun idx => tests (Some idx))
adamc@111 697 (fun idx => bodies (Some idx))
adamc@111 698 end.
adamc@111 699 End cond.
adamc@111 700
adamc@111 701 Implicit Arguments cond [A n].
adamc@113 702 (* end thide *)
adamc@111 703
adamc@112 704 (** Now the expression interpreter is straightforward to write. *)
adamc@112 705
adam@443 706 (* begin thide *)
adam@443 707 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
adam@443 708 match e with
adam@443 709 | NConst n => n
adam@443 710 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
adam@443 711 | Eq e1 e2 =>
adam@443 712 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adam@443 713
adam@443 714 | BConst b => b
adam@443 715 | Cond _ _ tests bodies default =>
adam@443 716 cond
adam@443 717 (exp'Denote default)
adam@443 718 (fun idx => exp'Denote (tests idx))
adam@443 719 (fun idx => exp'Denote (bodies idx))
adam@443 720 end.
adam@443 721 (* begin hide *)
adam@443 722 Reset exp'Denote.
adam@443 723 (* end hide *)
adam@443 724 (* end thide *)
adam@443 725
adam@443 726 (* begin hide *)
adamc@215 727 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
adamc@215 728 match e with
adamc@215 729 | NConst n => n
adamc@215 730 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
adamc@111 731 | Eq e1 e2 =>
adamc@111 732 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adamc@111 733
adamc@215 734 | BConst b => b
adamc@111 735 | Cond _ _ tests bodies default =>
adamc@113 736 (* begin thide *)
adamc@111 737 cond
adamc@111 738 (exp'Denote default)
adamc@111 739 (fun idx => exp'Denote (tests idx))
adamc@111 740 (fun idx => exp'Denote (bodies idx))
adamc@113 741 (* end thide *)
adamc@111 742 end.
adam@443 743 (* end hide *)
adamc@111 744
adamc@112 745 (** 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 746
adamc@113 747 (* begin thide *)
adamc@111 748 Section cfoldCond.
adamc@111 749 Variable t : type'.
adamc@111 750 Variable default : exp' t.
adamc@111 751
adamc@112 752 Fixpoint cfoldCond (n : nat)
adamc@215 753 : (ffin n -> exp' Bool) -> (ffin n -> exp' t) -> exp' t :=
adamc@215 754 match n with
adamc@111 755 | O => fun _ _ => default
adamc@111 756 | S n' => fun tests bodies =>
adamc@204 757 match tests None return _ with
adamc@111 758 | BConst true => bodies None
adamc@111 759 | BConst false => cfoldCond n'
adamc@111 760 (fun idx => tests (Some idx))
adamc@111 761 (fun idx => bodies (Some idx))
adamc@111 762 | _ =>
adamc@111 763 let e := cfoldCond n'
adamc@111 764 (fun idx => tests (Some idx))
adamc@111 765 (fun idx => bodies (Some idx)) in
adamc@112 766 match e in exp' t return exp' t -> exp' t with
adamc@112 767 | Cond n _ tests' bodies' default' => fun body =>
adamc@111 768 Cond
adamc@111 769 (S n)
adamc@111 770 (fun idx => match idx with
adamc@112 771 | None => tests None
adamc@111 772 | Some idx => tests' idx
adamc@111 773 end)
adamc@111 774 (fun idx => match idx with
adamc@111 775 | None => body
adamc@111 776 | Some idx => bodies' idx
adamc@111 777 end)
adamc@111 778 default'
adamc@112 779 | e => fun body =>
adamc@111 780 Cond
adamc@111 781 1
adamc@112 782 (fun _ => tests None)
adamc@111 783 (fun _ => body)
adamc@111 784 e
adamc@112 785 end (bodies None)
adamc@111 786 end
adamc@111 787 end.
adamc@111 788 End cfoldCond.
adamc@111 789
adamc@111 790 Implicit Arguments cfoldCond [t n].
adamc@113 791 (* end thide *)
adamc@111 792
adamc@112 793 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
adamc@112 794
adam@455 795 (* begin thide *)
adamc@215 796 Fixpoint cfold t (e : exp' t) : exp' t :=
adamc@215 797 match e with
adamc@111 798 | NConst n => NConst n
adamc@111 799 | Plus e1 e2 =>
adamc@111 800 let e1' := cfold e1 in
adamc@111 801 let e2' := cfold e2 in
adam@417 802 match e1', e2' return exp' Nat with
adamc@111 803 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@111 804 | _, _ => Plus e1' e2'
adamc@111 805 end
adamc@111 806 | Eq e1 e2 =>
adamc@111 807 let e1' := cfold e1 in
adamc@111 808 let e2' := cfold e2 in
adam@417 809 match e1', e2' return exp' Bool with
adamc@111 810 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@111 811 | _, _ => Eq e1' e2'
adamc@111 812 end
adamc@111 813
adamc@111 814 | BConst b => BConst b
adamc@111 815 | Cond _ _ tests bodies default =>
adamc@111 816 cfoldCond
adamc@111 817 (cfold default)
adamc@111 818 (fun idx => cfold (tests idx))
adamc@111 819 (fun idx => cfold (bodies idx))
adam@455 820 end.
adamc@113 821 (* end thide *)
adamc@111 822
adamc@113 823 (* begin thide *)
adam@455 824 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. The following lemma formalizes that property. The proof is a standard mostly automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis. *)
adamc@112 825
adamc@111 826 Lemma cfoldCond_correct : forall t (default : exp' t)
adamc@215 827 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
adamc@111 828 exp'Denote (cfoldCond default tests bodies)
adamc@111 829 = exp'Denote (Cond n tests bodies default).
adamc@111 830 induction n; crush;
adamc@111 831 match goal with
adamc@111 832 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
adam@294 833 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)))
adamc@111 834 end;
adamc@111 835 repeat (match goal with
adam@443 836 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
adam@443 837 dep_destruct E
adamc@111 838 | [ |- context[if ?B then _ else _] ] => destruct B
adamc@111 839 end; crush).
adamc@111 840 Qed.
adamc@111 841
adam@398 842 (** 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 _extensional_; that is, it is unaffected by substitution of functions with input-output equivalents. *)
adamc@112 843
adamc@215 844 Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : ffin n -> bool)
adamc@215 845 (bodies bodies' : ffin n -> A),
adamc@111 846 (forall idx, tests idx = tests' idx)
adamc@111 847 -> (forall idx, bodies idx = bodies' idx)
adamc@111 848 -> cond default tests bodies
adamc@111 849 = cond default tests' bodies'.
adamc@111 850 induction n; crush;
adamc@111 851 match goal with
adamc@111 852 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@111 853 end; crush.
adamc@111 854 Qed.
adamc@111 855
adam@426 856 (** Now the final theorem is easy to prove. *)
adamc@113 857 (* end thide *)
adamc@112 858
adamc@111 859 Theorem cfold_correct : forall t (e : exp' t),
adamc@111 860 exp'Denote (cfold e) = exp'Denote e.
adamc@113 861 (* begin thide *)
adam@375 862 Hint Rewrite cfoldCond_correct.
adamc@111 863 Hint Resolve cond_ext.
adamc@111 864
adamc@111 865 induction e; crush;
adamc@111 866 repeat (match goal with
adamc@111 867 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@111 868 end; crush).
adamc@111 869 Qed.
adamc@113 870 (* end thide *)
adamc@115 871
adam@426 872 (** We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct. *)
adamc@115 873
adamc@215 874 (** * Choosing Between Representations *)
adamc@215 875
adamc@215 876 (** It is not always clear which of these representation techniques to apply in a particular situation, but I will try to summarize the pros and cons of each.
adamc@215 877
adamc@215 878 Inductive types are often the most pleasant to work with, after someone has spent the time implementing some basic library functions for them, using fancy [match] annotations. Many aspects of Coq's logic and tactic support are specialized to deal with inductive types, and you may miss out if you use alternate encodings.
adamc@215 879
adam@426 880 Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation. For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types. Consider a call [get l f], where variable [l] has type [filist A (S n)]. The type of [l] would be simplified to an explicit pair type. In a proof involving many recursive types, this kind of unhelpful "simplification" can lead to rapid bloat in the sizes of subgoals. Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the "simplified" version. The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may "simplify" when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value.
adamc@215 881
adam@426 882 Another disadvantage of recursive types is that they only apply to type families whose indices determine their "skeletons." This is not true for all data structures; a good counterexample comes from the richly typed programming language syntax types we have used several times so far. The fact that a piece of syntax has type [Nat] tells us nothing about the tree structure of that syntax.
adamc@215 883
adam@426 884 Finally, Coq type inference can be more helpful in constructing values in inductive types. Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type. This downside can be mitigated to an extent by writing "constructor" functions for a recursive type, mirroring the definition of the corresponding inductive type.
adam@342 885
adam@342 886 Reflexive encodings of data types are seen relatively rarely. As our examples demonstrated, manipulating index values manually can lead to hard-to-read code. A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3. For small developments, avoiding that kind of coding can justify the use of reflexive data structures. There are also some useful instances of %\index{co-inductive types}%co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *)