Mercurial > cpdt > repo

annotate src/DataStruct.v @ 432:17d01e51256c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass through Reflection, to incorporate new coqdoc features
author Adam Chlipala <adam@chlipala.net>
date Thu, 26 Jul 2012 14:57:38 -0400
parents 5f25705a10ea
children 8077352044b2
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@106 48 [[
adamc@215 49 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 50 match ls 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@205 59 ]]
adamc@205 60
adamc@215 61 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 62
adamc@106 63 [[
adamc@215 64 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 65 match ls with
adamc@106 66 | Nil => fun idx =>
adamc@215 67 match idx in fin n' return (match n' with
adamc@106 68 | O => A
adamc@106 69 | S _ => unit
adamc@106 70 end) with
adamc@106 71 | First _ => tt
adamc@106 72 | Next _ _ => tt
adamc@106 73 end
adamc@106 74 | Cons _ x ls' => fun idx =>
adamc@106 75 match idx with
adamc@106 76 | First _ => x
adamc@106 77 | Next _ idx' => get ls' idx'
adamc@106 78 end
adamc@106 79 end.
adamc@106 80
adamc@205 81 ]]
adamc@205 82
adam@284 83 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 84
adam@284 85 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 86
adamc@106 87 [[
adamc@215 88 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 89 match ls with
adamc@106 90 | Nil => fun idx =>
adamc@215 91 match idx in fin n' return (match n' with
adamc@106 92 | O => A
adamc@106 93 | S _ => unit
adamc@106 94 end) with
adamc@106 95 | First _ => tt
adamc@106 96 | Next _ _ => tt
adamc@106 97 end
adamc@106 98 | Cons _ x ls' => fun idx =>
adamc@215 99 match idx in fin n' return ilist (pred n') -> A with
adamc@106 100 | First _ => fun _ => x
adamc@106 101 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 102 end ls'
adamc@106 103 end.
adamc@106 104
adamc@205 105 ]]
adamc@205 106
adamc@106 107 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 108
adamc@215 109 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 110 match ls with
adamc@105 111 | Nil => fun idx =>
adamc@215 112 match idx in fin n' return (match n' with
adamc@105 113 | O => A
adamc@105 114 | S _ => unit
adamc@105 115 end) with
adamc@105 116 | First _ => tt
adamc@105 117 | Next _ _ => tt
adamc@105 118 end
adamc@105 119 | Cons _ x ls' => fun idx =>
adamc@215 120 match idx in fin n' return (fin (pred n') -> A) -> A with
adamc@105 121 | First _ => fun _ => x
adamc@105 122 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 123 end (get ls')
adamc@105 124 end.
adamc@113 125 (* end thide *)
adamc@105 126 End ilist.
adamc@105 127
adamc@105 128 Implicit Arguments Nil [A].
adamc@108 129 Implicit Arguments First [n].
adamc@105 130
adamc@108 131 (** A few examples show how to make use of these definitions. *)
adamc@108 132
adamc@108 133 Check Cons 0 (Cons 1 (Cons 2 Nil)).
adamc@215 134 (** %\vspace{-.15in}% [[
adamc@215 135 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 136 : ilist nat 3
adam@302 137 ]]
adam@302 138 *)
adamc@215 139
adamc@113 140 (* begin thide *)
adamc@108 141 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@215 142 (** %\vspace{-.15in}% [[
adamc@108 143 = 0
adamc@108 144 : nat
adam@302 145 ]]
adam@302 146 *)
adamc@215 147
adamc@108 148 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@215 149 (** %\vspace{-.15in}% [[
adamc@108 150 = 1
adamc@108 151 : nat
adam@302 152 ]]
adam@302 153 *)
adamc@215 154
adamc@108 155 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@215 156 (** %\vspace{-.15in}% [[
adamc@108 157 = 2
adamc@108 158 : nat
adam@302 159 ]]
adam@302 160 *)
adamc@113 161 (* end thide *)
adamc@108 162
adam@426 163 (* begin hide *)
adam@426 164 Definition map' := map.
adam@426 165 (* end hide *)
adam@426 166
adamc@108 167 (** 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 168
adamc@105 169 Section ilist_map.
adamc@105 170 Variables A B : Set.
adamc@105 171 Variable f : A -> B.
adamc@105 172
adamc@215 173 Fixpoint imap n (ls : ilist A n) : ilist B n :=
adamc@215 174 match ls with
adamc@105 175 | Nil => Nil
adamc@105 176 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 177 end.
adamc@105 178
adam@426 179 (** It is easy to prove that [get] "distributes over" [imap] calls. *)
adamc@107 180
adam@342 181 (* EX: Prove that [get] distributes over [imap]. *)
adam@342 182
adam@342 183 (* begin thide *)
adamc@215 184 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n),
adamc@105 185 get (imap ls) idx = f (get ls idx).
adamc@107 186 induction ls; dep_destruct idx; crush.
adamc@105 187 Qed.
adamc@113 188 (* end thide *)
adamc@105 189 End ilist_map.
adamc@107 190
adam@406 191 (** 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 192
adamc@107 193 (** * Heterogeneous Lists *)
adamc@107 194
adam@426 195 (** 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 196
adamc@107 197 Section hlist.
adamc@107 198 Variable A : Type.
adamc@107 199 Variable B : A -> Type.
adamc@107 200
adamc@113 201 (* 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 202
adam@342 203 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B].%\index{Gallina terms!hlist}% *)
adamc@107 204
adamc@113 205 (* begin thide *)
adamc@107 206 Inductive hlist : list A -> Type :=
adamc@107 207 | MNil : hlist nil
adamc@107 208 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 209
adam@342 210 (** 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 211
adamc@113 212 (* end thide *)
adamc@113 213 (* EX: Define an analogue to [get] for [hlist]s. *)
adamc@113 214
adamc@113 215 (* begin thide *)
adamc@107 216 Variable elm : A.
adamc@107 217
adamc@107 218 Inductive member : list A -> Type :=
adamc@107 219 | MFirst : forall ls, member (elm :: ls)
adamc@107 220 | MNext : forall x ls, member ls -> member (x :: ls).
adamc@107 221
adam@426 222 (** 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 223
adam@342 224 We can use [member] to adapt our definition of [get] to [hlist]s. 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 225
adamc@215 226 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
adamc@215 227 match mls with
adamc@107 228 | MNil => fun mem =>
adamc@107 229 match mem in member ls' return (match ls' with
adamc@107 230 | nil => B elm
adamc@107 231 | _ :: _ => unit
adamc@107 232 end) with
adamc@107 233 | MFirst _ => tt
adamc@107 234 | MNext _ _ _ => tt
adamc@107 235 end
adamc@107 236 | MCons _ _ x mls' => fun mem =>
adamc@107 237 match mem in member ls' return (match ls' with
adamc@107 238 | nil => Empty_set
adamc@107 239 | x' :: ls'' =>
adamc@107 240 B x' -> (member ls'' -> B elm) -> B elm
adamc@107 241 end) with
adamc@107 242 | MFirst _ => fun x _ => x
adamc@107 243 | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
adamc@107 244 end x (hget mls')
adamc@107 245 end.
adamc@113 246 (* end thide *)
adamc@107 247 End hlist.
adamc@108 248
adamc@113 249 (* begin thide *)
adamc@108 250 Implicit Arguments MNil [A B].
adamc@108 251 Implicit Arguments MCons [A B x ls].
adamc@108 252
adamc@108 253 Implicit Arguments MFirst [A elm ls].
adamc@108 254 Implicit Arguments MNext [A elm x ls].
adamc@113 255 (* end thide *)
adamc@108 256
adamc@108 257 (** 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 258
adamc@108 259 Definition someTypes : list Set := nat :: bool :: nil.
adamc@108 260
adamc@113 261 (* begin thide *)
adamc@113 262
adamc@108 263 Example someValues : hlist (fun T : Set => T) someTypes :=
adamc@108 264 MCons 5 (MCons true MNil).
adamc@108 265
adamc@108 266 Eval simpl in hget someValues MFirst.
adamc@215 267 (** %\vspace{-.15in}% [[
adamc@108 268 = 5
adamc@108 269 : (fun T : Set => T) nat
adam@302 270 ]]
adam@302 271 *)
adamc@215 272
adamc@108 273 Eval simpl in hget someValues (MNext MFirst).
adamc@215 274 (** %\vspace{-.15in}% [[
adamc@108 275 = true
adamc@108 276 : (fun T : Set => T) bool
adam@302 277 ]]
adam@302 278 *)
adamc@108 279
adamc@108 280 (** We can also build indexed lists of pairs in this way. *)
adamc@108 281
adamc@108 282 Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
adamc@108 283 MCons (1, 2) (MCons (true, false) MNil).
adamc@108 284
adamc@113 285 (* end thide *)
adamc@113 286
adamc@113 287
adamc@108 288 (** ** A Lambda Calculus Interpreter *)
adamc@108 289
adam@342 290 (** 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.
adamc@108 291
adamc@108 292 We start with an algebraic datatype for types. *)
adamc@108 293
adamc@108 294 Inductive type : Set :=
adamc@108 295 | Unit : type
adamc@108 296 | Arrow : type -> type -> type.
adamc@108 297
adam@342 298 (** 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 299
adamc@108 300 Inductive exp : list type -> type -> Set :=
adamc@108 301 | Const : forall ts, exp ts Unit
adamc@113 302 (* begin thide *)
adamc@108 303 | Var : forall ts t, member t ts -> exp ts t
adamc@108 304 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 305 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@113 306 (* end thide *)
adamc@108 307
adamc@108 308 Implicit Arguments Const [ts].
adamc@108 309
adamc@108 310 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 311
adamc@108 312 Fixpoint typeDenote (t : type) : Set :=
adamc@108 313 match t with
adamc@108 314 | Unit => unit
adamc@108 315 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 316 end.
adamc@108 317
adam@342 318 (** 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 319
adamc@113 320 (* EX: Define an interpreter for [exp]s. *)
adamc@113 321
adamc@113 322 (* begin thide *)
adamc@215 323 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
adamc@215 324 match e with
adamc@108 325 | Const _ => fun _ => tt
adamc@108 326
adamc@108 327 | Var _ _ mem => fun s => hget s mem
adamc@108 328 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@108 329 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
adamc@108 330 end.
adamc@108 331
adamc@108 332 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 333
adamc@108 334 Eval simpl in expDenote Const MNil.
adamc@215 335 (** %\vspace{-.15in}% [[
adamc@108 336 = tt
adamc@108 337 : typeDenote Unit
adam@302 338 ]]
adam@302 339 *)
adamc@215 340
adamc@108 341 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
adamc@215 342 (** %\vspace{-.15in}% [[
adamc@108 343 = fun x : unit => x
adamc@108 344 : typeDenote (Arrow Unit Unit)
adam@302 345 ]]
adam@302 346 *)
adamc@215 347
adamc@108 348 Eval simpl in expDenote (Abs (dom := Unit)
adamc@108 349 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
adamc@215 350 (** %\vspace{-.15in}% [[
adamc@108 351 = fun x _ : unit => x
adamc@108 352 : typeDenote (Arrow Unit (Arrow Unit Unit))
adam@302 353 ]]
adam@302 354 *)
adamc@215 355
adamc@108 356 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
adamc@215 357 (** %\vspace{-.15in}% [[
adamc@108 358 = fun _ x0 : unit => x0
adamc@108 359 : typeDenote (Arrow Unit (Arrow Unit Unit))
adam@302 360 ]]
adam@302 361 *)
adamc@215 362
adamc@108 363 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
adamc@215 364 (** %\vspace{-.15in}% [[
adamc@108 365 = tt
adamc@108 366 : typeDenote Unit
adam@302 367 ]]
adam@302 368 *)
adamc@108 369
adamc@113 370 (* end thide *)
adamc@113 371
adam@342 372 (** 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 373
adamc@108 374
adamc@109 375 (** * Recursive Type Definitions *)
adamc@109 376
adam@426 377 (** %\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 378
adamc@113 379 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
adamc@113 380
adamc@109 381 Section filist.
adamc@109 382 Variable A : Set.
adamc@109 383
adamc@113 384 (* begin thide *)
adamc@109 385 Fixpoint filist (n : nat) : Set :=
adamc@109 386 match n with
adamc@109 387 | O => unit
adamc@109 388 | S n' => A * filist n'
adamc@109 389 end%type.
adamc@109 390
adamc@109 391 (** 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 392
adamc@215 393 Fixpoint ffin (n : nat) : Set :=
adamc@109 394 match n with
adamc@109 395 | O => Empty_set
adamc@215 396 | S n' => option (ffin n')
adamc@109 397 end.
adamc@109 398
adam@406 399 (** 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 400
adamc@215 401 Fixpoint fget (n : nat) : filist n -> ffin n -> A :=
adamc@215 402 match n with
adamc@109 403 | O => fun _ idx => match idx with end
adamc@109 404 | S n' => fun ls idx =>
adamc@109 405 match idx with
adamc@109 406 | None => fst ls
adamc@109 407 | Some idx' => fget n' (snd ls) idx'
adamc@109 408 end
adamc@109 409 end.
adamc@109 410
adamc@215 411 (** 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 412 (* end thide *)
adamc@215 413
adamc@109 414 End filist.
adamc@109 415
adamc@109 416 (** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)
adamc@109 417
adamc@113 418 (* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)
adamc@113 419
adamc@109 420 Section fhlist.
adamc@109 421 Variable A : Type.
adamc@109 422 Variable B : A -> Type.
adamc@109 423
adamc@113 424 (* begin thide *)
adamc@109 425 Fixpoint fhlist (ls : list A) : Type :=
adamc@109 426 match ls with
adamc@109 427 | nil => unit
adamc@109 428 | x :: ls' => B x * fhlist ls'
adamc@109 429 end%type.
adamc@109 430
adam@342 431 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently typed data elements. *)
adamc@109 432
adamc@109 433 Variable elm : A.
adamc@109 434
adamc@109 435 Fixpoint fmember (ls : list A) : Type :=
adamc@109 436 match ls with
adamc@109 437 | nil => Empty_set
adamc@109 438 | x :: ls' => (x = elm) + fmember ls'
adamc@109 439 end%type.
adamc@109 440
adam@426 441 (** 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 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 442
adamc@109 443 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
adamc@109 444
adamc@109 445 [[
adamc@109 446 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 447 match ls with
adamc@109 448 | nil => fun _ idx => match idx with end
adamc@109 449 | _ :: ls' => fun mls idx =>
adamc@109 450 match idx with
adamc@109 451 | inl _ => fst mls
adamc@109 452 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 453 end
adamc@109 454 end.
adamc@109 455
adamc@205 456 ]]
adamc@205 457
adamc@109 458 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 459
adamc@109 460 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 461 match ls with
adamc@109 462 | nil => fun _ idx => match idx with end
adamc@109 463 | _ :: ls' => fun mls idx =>
adamc@109 464 match idx with
adamc@109 465 | inl pf => match pf with
adam@426 466 | eq_refl => fst mls
adamc@109 467 end
adamc@109 468 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 469 end
adamc@109 470 end.
adamc@109 471
adamc@109 472 (** 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 473
adam@426 474 (* begin hide *)
adam@426 475 Definition foo := (@eq, @eq_refl).
adam@426 476 (* end hide *)
adam@426 477
adamc@109 478 Print eq.
adamc@215 479 (** %\vspace{-.15in}% [[
adam@426 480 Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
adamc@215 481
adamc@109 482 ]]
adamc@109 483
adam@426 484 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 485 (* end thide *)
adamc@215 486
adamc@109 487 End fhlist.
adamc@110 488
adamc@111 489 Implicit Arguments fhget [A B elm ls].
adamc@111 490
adamc@110 491
adamc@110 492 (** * Data Structures as Index Functions *)
adamc@110 493
adam@342 494 (** %\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 495
adamc@110 496 Section tree.
adamc@110 497 Variable A : Set.
adamc@110 498
adamc@110 499 Inductive tree : Set :=
adamc@110 500 | Leaf : A -> tree
adamc@110 501 | Node : forall n, ilist tree n -> tree.
adamc@110 502 End tree.
adamc@110 503
adamc@110 504 (** 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 505
adamc@110 506 Section ifoldr.
adamc@110 507 Variables A B : Set.
adamc@110 508 Variable f : A -> B -> B.
adamc@110 509 Variable i : B.
adamc@110 510
adamc@215 511 Fixpoint ifoldr n (ls : ilist A n) : B :=
adamc@110 512 match ls with
adamc@110 513 | Nil => i
adamc@110 514 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 515 end.
adamc@110 516 End ifoldr.
adamc@110 517
adamc@110 518 Fixpoint sum (t : tree nat) : nat :=
adamc@110 519 match t with
adamc@110 520 | Leaf n => n
adamc@110 521 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 522 end.
adamc@110 523
adamc@110 524 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 525 match t with
adamc@110 526 | Leaf n => Leaf (S n)
adamc@110 527 | Node _ ls => Node (imap inc ls)
adamc@110 528 end.
adamc@110 529
adamc@110 530 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 531
adamc@110 532 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@113 533 (* begin thide *)
adamc@110 534 induction t; crush.
adamc@110 535 (** [[
adamc@110 536 n : nat
adamc@110 537 i : ilist (tree nat) n
adamc@110 538 ============================
adamc@110 539 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 540 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@215 541
adamc@110 542 ]]
adamc@110 543
adam@342 544 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 545
adamc@110 546 Check tree_ind.
adamc@215 547 (** %\vspace{-.15in}% [[
adamc@215 548 tree_ind
adamc@110 549 : forall (A : Set) (P : tree A -> Prop),
adamc@110 550 (forall a : A, P (Leaf a)) ->
adamc@110 551 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 552 forall t : tree A, P t
adamc@215 553
adamc@110 554 ]]
adamc@110 555
adam@342 556 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 557
adamc@110 558 Abort.
adamc@110 559
adamc@110 560 Reset tree.
adamc@110 561
adamc@110 562 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
adamc@110 563
adamc@110 564 Section tree.
adamc@110 565 Variable A : Set.
adamc@110 566
adamc@215 567 (** %\vspace{-.15in}% [[
adamc@110 568 Inductive tree : Set :=
adamc@110 569 | Leaf : A -> tree
adamc@110 570 | Node : forall n, filist tree n -> tree.
adam@342 571 ]]
adamc@110 572
adam@342 573 <<
adamc@110 574 Error: Non strictly positive occurrence of "tree" in
adamc@110 575 "forall n : nat, filist tree n -> tree"
adam@342 576 >>
adamc@110 577
adam@342 578 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 579
adam@398 580 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 581
adamc@110 582 Inductive tree : Set :=
adamc@110 583 | Leaf : A -> tree
adamc@215 584 | Node : forall n, (ffin n -> tree) -> tree.
adamc@110 585
adamc@215 586 (** 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 587
adamc@110 588 End tree.
adamc@110 589
adamc@110 590 Implicit Arguments Node [A n].
adamc@110 591
adamc@215 592 (** 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 593
adamc@110 594 Section rifoldr.
adamc@110 595 Variables A B : Set.
adamc@110 596 Variable f : A -> B -> B.
adamc@110 597 Variable i : B.
adamc@110 598
adamc@215 599 Fixpoint rifoldr (n : nat) : (ffin n -> A) -> B :=
adamc@215 600 match n with
adamc@110 601 | O => fun _ => i
adamc@110 602 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 603 end.
adamc@110 604 End rifoldr.
adamc@110 605
adamc@110 606 Implicit Arguments rifoldr [A B n].
adamc@110 607
adamc@110 608 Fixpoint sum (t : tree nat) : nat :=
adamc@110 609 match t with
adamc@110 610 | Leaf n => n
adamc@110 611 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 612 end.
adamc@110 613
adamc@110 614 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 615 match t with
adamc@110 616 | Leaf n => Leaf (S n)
adamc@110 617 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 618 end.
adamc@110 619
adam@398 620 (** 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 621
adamc@110 622 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 623 x1 >= x2
adamc@110 624 -> y1 >= y2
adamc@110 625 -> x1 + y1 >= x2 + y2.
adamc@110 626 crush.
adamc@110 627 Qed.
adamc@110 628
adamc@215 629 Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat),
adamc@110 630 (forall idx, f1 idx >= f2 idx)
adamc@110 631 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 632 Hint Resolve plus_ge.
adamc@110 633
adamc@110 634 induction n; crush.
adamc@110 635 Qed.
adamc@110 636
adamc@110 637 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 638 Hint Resolve sum_inc'.
adamc@110 639
adamc@110 640 induction t; crush.
adamc@110 641 Qed.
adamc@110 642
adamc@113 643 (* end thide *)
adamc@113 644
adamc@110 645 (** 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 646
adamc@111 647 (** ** Another Interpreter Example *)
adamc@111 648
adam@426 649 (** 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 650
adamc@112 651 Inductive type' : Type := Nat | Bool.
adamc@111 652
adamc@111 653 Inductive exp' : type' -> Type :=
adamc@112 654 | NConst : nat -> exp' Nat
adamc@112 655 | Plus : exp' Nat -> exp' Nat -> exp' Nat
adamc@112 656 | Eq : exp' Nat -> exp' Nat -> exp' Bool
adamc@111 657
adamc@112 658 | BConst : bool -> exp' Bool
adamc@113 659 (* begin thide *)
adamc@215 660 | Cond : forall n t, (ffin n -> exp' Bool)
adamc@215 661 -> (ffin n -> exp' t) -> exp' t -> exp' t.
adamc@113 662 (* end thide *)
adamc@111 663
adam@284 664 (** 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 665
adam@284 666 Example ex1 := Cond 2
adam@284 667 (fun f => match f with
adam@284 668 | None => Eq (Plus (NConst 2) (NConst 2)) (NConst 5)
adam@284 669 | Some None => Eq (Plus (NConst 1) (NConst 1)) (NConst 2)
adam@284 670 | Some (Some v) => match v with end
adam@284 671 end)
adam@284 672 (fun f => match f with
adam@284 673 | None => NConst 0
adam@284 674 | Some None => NConst 1
adam@284 675 | Some (Some v) => match v with end
adam@284 676 end)
adam@284 677 (NConst 2).
adam@284 678
adam@284 679 (** We start implementing our interpreter with a standard type denotation function. *)
adamc@112 680
adamc@111 681 Definition type'Denote (t : type') : Set :=
adamc@111 682 match t with
adamc@112 683 | Nat => nat
adamc@112 684 | Bool => bool
adamc@111 685 end.
adamc@111 686
adamc@112 687 (** 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 688
adamc@113 689 (* begin thide *)
adamc@111 690 Section cond.
adamc@111 691 Variable A : Set.
adamc@111 692 Variable default : A.
adamc@111 693
adamc@215 694 Fixpoint cond (n : nat) : (ffin n -> bool) -> (ffin n -> A) -> A :=
adamc@215 695 match n with
adamc@111 696 | O => fun _ _ => default
adamc@111 697 | S n' => fun tests bodies =>
adamc@111 698 if tests None
adamc@111 699 then bodies None
adamc@111 700 else cond n'
adamc@111 701 (fun idx => tests (Some idx))
adamc@111 702 (fun idx => bodies (Some idx))
adamc@111 703 end.
adamc@111 704 End cond.
adamc@111 705
adamc@111 706 Implicit Arguments cond [A n].
adamc@113 707 (* end thide *)
adamc@111 708
adamc@112 709 (** Now the expression interpreter is straightforward to write. *)
adamc@112 710
adamc@215 711 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
adamc@215 712 match e with
adamc@215 713 | NConst n => n
adamc@215 714 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
adamc@111 715 | Eq e1 e2 =>
adamc@111 716 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adamc@111 717
adamc@215 718 | BConst b => b
adamc@111 719 | Cond _ _ tests bodies default =>
adamc@113 720 (* begin thide *)
adamc@111 721 cond
adamc@111 722 (exp'Denote default)
adamc@111 723 (fun idx => exp'Denote (tests idx))
adamc@111 724 (fun idx => exp'Denote (bodies idx))
adamc@113 725 (* end thide *)
adamc@111 726 end.
adamc@111 727
adamc@112 728 (** 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 729
adamc@113 730 (* begin thide *)
adamc@111 731 Section cfoldCond.
adamc@111 732 Variable t : type'.
adamc@111 733 Variable default : exp' t.
adamc@111 734
adamc@112 735 Fixpoint cfoldCond (n : nat)
adamc@215 736 : (ffin n -> exp' Bool) -> (ffin n -> exp' t) -> exp' t :=
adamc@215 737 match n with
adamc@111 738 | O => fun _ _ => default
adamc@111 739 | S n' => fun tests bodies =>
adamc@204 740 match tests None return _ with
adamc@111 741 | BConst true => bodies None
adamc@111 742 | BConst false => cfoldCond n'
adamc@111 743 (fun idx => tests (Some idx))
adamc@111 744 (fun idx => bodies (Some idx))
adamc@111 745 | _ =>
adamc@111 746 let e := cfoldCond n'
adamc@111 747 (fun idx => tests (Some idx))
adamc@111 748 (fun idx => bodies (Some idx)) in
adamc@112 749 match e in exp' t return exp' t -> exp' t with
adamc@112 750 | Cond n _ tests' bodies' default' => fun body =>
adamc@111 751 Cond
adamc@111 752 (S n)
adamc@111 753 (fun idx => match idx with
adamc@112 754 | None => tests None
adamc@111 755 | Some idx => tests' idx
adamc@111 756 end)
adamc@111 757 (fun idx => match idx with
adamc@111 758 | None => body
adamc@111 759 | Some idx => bodies' idx
adamc@111 760 end)
adamc@111 761 default'
adamc@112 762 | e => fun body =>
adamc@111 763 Cond
adamc@111 764 1
adamc@112 765 (fun _ => tests None)
adamc@111 766 (fun _ => body)
adamc@111 767 e
adamc@112 768 end (bodies None)
adamc@111 769 end
adamc@111 770 end.
adamc@111 771 End cfoldCond.
adamc@111 772
adamc@111 773 Implicit Arguments cfoldCond [t n].
adamc@113 774 (* end thide *)
adamc@111 775
adamc@112 776 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
adamc@112 777
adamc@215 778 Fixpoint cfold t (e : exp' t) : exp' t :=
adamc@215 779 match e with
adamc@111 780 | NConst n => NConst n
adamc@111 781 | Plus e1 e2 =>
adamc@111 782 let e1' := cfold e1 in
adamc@111 783 let e2' := cfold e2 in
adam@417 784 match e1', e2' return exp' Nat with
adamc@111 785 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@111 786 | _, _ => Plus e1' e2'
adamc@111 787 end
adamc@111 788 | Eq e1 e2 =>
adamc@111 789 let e1' := cfold e1 in
adamc@111 790 let e2' := cfold e2 in
adam@417 791 match e1', e2' return exp' Bool with
adamc@111 792 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@111 793 | _, _ => Eq e1' e2'
adamc@111 794 end
adamc@111 795
adamc@111 796 | BConst b => BConst b
adamc@111 797 | Cond _ _ tests bodies default =>
adamc@113 798 (* begin thide *)
adamc@111 799 cfoldCond
adamc@111 800 (cfold default)
adamc@111 801 (fun idx => cfold (tests idx))
adamc@111 802 (fun idx => cfold (bodies idx))
adamc@113 803 (* end thide *)
adamc@111 804 end.
adamc@111 805
adamc@113 806 (* begin thide *)
adam@342 807 (** 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 instantiation of the quantifiers in the induction hypothesis. *)
adamc@112 808
adamc@111 809 Lemma cfoldCond_correct : forall t (default : exp' t)
adamc@215 810 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
adamc@111 811 exp'Denote (cfoldCond default tests bodies)
adamc@111 812 = exp'Denote (Cond n tests bodies default).
adamc@111 813 induction n; crush;
adamc@111 814 match goal with
adamc@111 815 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
adam@294 816 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)))
adamc@111 817 end;
adamc@111 818 repeat (match goal with
adam@406 819 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => dep_destruct E
adamc@111 820 | [ |- context[if ?B then _ else _] ] => destruct B
adamc@111 821 end; crush).
adamc@111 822 Qed.
adamc@111 823
adam@398 824 (** 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 825
adamc@215 826 Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : ffin n -> bool)
adamc@215 827 (bodies bodies' : ffin n -> A),
adamc@111 828 (forall idx, tests idx = tests' idx)
adamc@111 829 -> (forall idx, bodies idx = bodies' idx)
adamc@111 830 -> cond default tests bodies
adamc@111 831 = cond default tests' bodies'.
adamc@111 832 induction n; crush;
adamc@111 833 match goal with
adamc@111 834 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@111 835 end; crush.
adamc@111 836 Qed.
adamc@111 837
adam@426 838 (** Now the final theorem is easy to prove. *)
adamc@113 839 (* end thide *)
adamc@112 840
adamc@111 841 Theorem cfold_correct : forall t (e : exp' t),
adamc@111 842 exp'Denote (cfold e) = exp'Denote e.
adamc@113 843 (* begin thide *)
adam@375 844 Hint Rewrite cfoldCond_correct.
adamc@111 845 Hint Resolve cond_ext.
adamc@111 846
adamc@111 847 induction e; crush;
adamc@111 848 repeat (match goal with
adamc@111 849 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@111 850 end; crush).
adamc@111 851 Qed.
adamc@113 852 (* end thide *)
adamc@115 853
adam@426 854 (** We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct. *)
adamc@115 855
adamc@215 856 (** * Choosing Between Representations *)
adamc@215 857
adamc@215 858 (** 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 859
adamc@215 860 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 861
adam@426 862 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 863
adam@426 864 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 865
adam@426 866 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 867
adam@342 868 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. *)