Mercurial > cpdt > repo

annotate src/DataStruct.v @ 563:af97676583f3

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