Mercurial > cpdt > repo

annotate src/DataStruct.v @ 110:4627b9caac8b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Index functions
author Adam Chlipala <adamc@hcoop.net>
date Mon, 13 Oct 2008 15:09:58 -0400
parents fe6cfbae86b9
children 702e5c35cc89
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@105 11 Require Import 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@110 422
adamc@110 423 (** * Data Structures as Index Functions *)
adamc@110 424
adamc@110 425 (** 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 426
adamc@110 427 Section tree.
adamc@110 428 Variable A : Set.
adamc@110 429
adamc@110 430 Inductive tree : Set :=
adamc@110 431 | Leaf : A -> tree
adamc@110 432 | Node : forall n, ilist tree n -> tree.
adamc@110 433 End tree.
adamc@110 434
adamc@110 435 (** 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 436
adamc@110 437 Section ifoldr.
adamc@110 438 Variables A B : Set.
adamc@110 439 Variable f : A -> B -> B.
adamc@110 440 Variable i : B.
adamc@110 441
adamc@110 442 Fixpoint ifoldr n (ls : ilist A n) {struct ls} : B :=
adamc@110 443 match ls with
adamc@110 444 | Nil => i
adamc@110 445 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 446 end.
adamc@110 447 End ifoldr.
adamc@110 448
adamc@110 449 Fixpoint sum (t : tree nat) : nat :=
adamc@110 450 match t with
adamc@110 451 | Leaf n => n
adamc@110 452 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 453 end.
adamc@110 454
adamc@110 455 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 456 match t with
adamc@110 457 | Leaf n => Leaf (S n)
adamc@110 458 | Node _ ls => Node (imap inc ls)
adamc@110 459 end.
adamc@110 460
adamc@110 461 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 462
adamc@110 463 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 464 induction t; crush.
adamc@110 465 (** [[
adamc@110 466
adamc@110 467 n : nat
adamc@110 468 i : ilist (tree nat) n
adamc@110 469 ============================
adamc@110 470 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 471 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@110 472 ]]
adamc@110 473
adamc@110 474 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 475
adamc@110 476 Check tree_ind.
adamc@110 477 (** [[
adamc@110 478
adamc@110 479 tree_ind
adamc@110 480 : forall (A : Set) (P : tree A -> Prop),
adamc@110 481 (forall a : A, P (Leaf a)) ->
adamc@110 482 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 483 forall t : tree A, P t
adamc@110 484 ]]
adamc@110 485
adamc@110 486 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 487 Abort.
adamc@110 488
adamc@110 489 Reset tree.
adamc@110 490
adamc@110 491 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
adamc@110 492
adamc@110 493 Section tree.
adamc@110 494 Variable A : Set.
adamc@110 495
adamc@110 496 (** [[
adamc@110 497
adamc@110 498 Inductive tree : Set :=
adamc@110 499 | Leaf : A -> tree
adamc@110 500 | Node : forall n, filist tree n -> tree.
adamc@110 501
adamc@110 502 [[
adamc@110 503
adamc@110 504 Error: Non strictly positive occurrence of "tree" in
adamc@110 505 "forall n : nat, filist tree n -> tree"
adamc@110 506 ]]
adamc@110 507
adamc@110 508 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 509
adamc@110 510 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 511
adamc@110 512 Inductive tree : Set :=
adamc@110 513 | Leaf : A -> tree
adamc@110 514 | Node : forall n, (findex n -> tree) -> tree.
adamc@110 515
adamc@110 516 (** 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 517 End tree.
adamc@110 518
adamc@110 519 Implicit Arguments Node [A n].
adamc@110 520
adamc@110 521 (** 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 522
adamc@110 523 Section rifoldr.
adamc@110 524 Variables A B : Set.
adamc@110 525 Variable f : A -> B -> B.
adamc@110 526 Variable i : B.
adamc@110 527
adamc@110 528 Fixpoint rifoldr (n : nat) : (findex n -> A) -> B :=
adamc@110 529 match n return (findex n -> A) -> B with
adamc@110 530 | O => fun _ => i
adamc@110 531 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 532 end.
adamc@110 533 End rifoldr.
adamc@110 534
adamc@110 535 Implicit Arguments rifoldr [A B n].
adamc@110 536
adamc@110 537 Fixpoint sum (t : tree nat) : nat :=
adamc@110 538 match t with
adamc@110 539 | Leaf n => n
adamc@110 540 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 541 end.
adamc@110 542
adamc@110 543 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 544 match t with
adamc@110 545 | Leaf n => Leaf (S n)
adamc@110 546 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 547 end.
adamc@110 548
adamc@110 549 (** 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 550
adamc@110 551 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 552 x1 >= x2
adamc@110 553 -> y1 >= y2
adamc@110 554 -> x1 + y1 >= x2 + y2.
adamc@110 555 crush.
adamc@110 556 Qed.
adamc@110 557
adamc@110 558 Lemma sum_inc' : forall n (f1 f2 : findex n -> nat),
adamc@110 559 (forall idx, f1 idx >= f2 idx)
adamc@110 560 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 561 Hint Resolve plus_ge.
adamc@110 562
adamc@110 563 induction n; crush.
adamc@110 564 Qed.
adamc@110 565
adamc@110 566 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 567 Hint Resolve sum_inc'.
adamc@110 568
adamc@110 569 induction t; crush.
adamc@110 570 Qed.
adamc@110 571
adamc@110 572 (** 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. *)