Mercurial > cpdt > repo

annotate src/DataStruct.v @ 112:623478074c2f

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