Mercurial > cpdt > repo

annotate src/DataStruct.v @ 314:d5787b70cf48

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rename Tactics; change 'principal typing' to 'principal types'
author Adam Chlipala <adam@chlipala.net>
date Wed, 07 Sep 2011 13:47:24 -0400
parents 7b38729be069
children 25d60fed2e96
rev   line source
adam@284 1 (* Copyright (c) 2008-2010, Adam Chlipala
adamc@105 2 *
adamc@105 3 * This work is licensed under a
adamc@105 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@105 5 * Unported License.
adamc@105 6 * The license text is available at:
adamc@105 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@105 8 *)
adamc@105 9
adamc@105 10 (* begin hide *)
adamc@111 11 Require Import Arith List.
adamc@105 12
adam@314 13 Require Import CpdtTactics.
adamc@105 14
adamc@105 15 Set Implicit Arguments.
adamc@105 16 (* end hide *)
adamc@105 17
adamc@105 18
adamc@105 19 (** %\chapter{Dependent Data Structures}% *)
adamc@105 20
adamc@106 21 (** Our red-black tree example from the last chapter illustrated how dependent types enable static enforcement of data structure invariants. To find interesting uses of dependent data structures, however, we need not look to the favorite examples of data structures and algorithms textbooks. More basic examples like length-indexed and heterogeneous lists come up again and again as the building blocks of dependent programs. There is a surprisingly large design space for this class of data structure, and we will spend this chapter exploring it. *)
adamc@105 22
adamc@105 23
adamc@106 24 (** * More Length-Indexed Lists *)
adamc@106 25
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
adam@284 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 [fin], where [fin n] is isomorphic to [{m : nat | m < n}]. The type family name stands for %``%#"#finite.#"#%''% *)
adamc@106 36
adamc@113 37 (* EX: Define a function [get] for extracting an [ilist] element by position. *)
adamc@113 38
adamc@113 39 (* begin thide *)
adamc@215 40 Inductive fin : nat -> Set :=
adamc@215 41 | First : forall n, fin (S n)
adamc@215 42 | Next : forall n, fin n -> fin (S n).
adamc@105 43
adam@284 44 (** [fin] 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. For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
adamc@106 45
adamc@106 46 Now it is easy to pick a [Prop]-free type for a selection function. As usual, our first implementation attempt will not convince the type checker, and we will attack the deficiencies one at a time.
adamc@106 47
adamc@106 48 [[
adamc@215 49 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 50 match ls with
adamc@106 51 | Nil => fun idx => ?
adamc@106 52 | Cons _ x ls' => fun idx =>
adamc@106 53 match idx with
adamc@106 54 | First _ => x
adamc@106 55 | Next _ idx' => get ls' idx'
adamc@106 56 end
adamc@106 57 end.
adamc@106 58
adamc@205 59 ]]
adamc@205 60
adamc@215 61 We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses. This still leaves us with a quandary in each of the [match] cases. First, we need to figure out how to take advantage of the contradiction in the [Nil] case. Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case. The solution we adopt is another case of [match]-within-[return].
adamc@106 62
adamc@106 63 [[
adamc@215 64 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 65 match ls with
adamc@106 66 | Nil => fun idx =>
adamc@215 67 match idx in fin n' return (match n' with
adamc@106 68 | O => A
adamc@106 69 | S _ => unit
adamc@106 70 end) with
adamc@106 71 | First _ => tt
adamc@106 72 | Next _ _ => tt
adamc@106 73 end
adamc@106 74 | Cons _ x ls' => fun idx =>
adamc@106 75 match idx with
adamc@106 76 | First _ => x
adamc@106 77 | Next _ idx' => get ls' idx'
adamc@106 78 end
adamc@106 79 end.
adamc@106 80
adamc@205 81 ]]
adamc@205 82
adam@284 83 Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls']. In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic. We are told that the [Nil] case body has type [match X with | 0 => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A]. We can see that setting [X] to [0] resolves the conflict, but Coq is not yet smart enough to do this unification automatically. Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern. As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
adam@284 84
adam@284 85 We need to use [match] annotations to make the relationship explicit. Unfortunately, the usual trick of postponing argument binding will not help us here. We need to match on both [ls] and [idx]; one or the other must be matched first. To get around this, we apply the convoy pattern that we met last chapter. This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables.
adamc@106 86
adamc@106 87 [[
adamc@215 88 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 89 match ls with
adamc@106 90 | Nil => fun idx =>
adamc@215 91 match idx in fin n' return (match n' with
adamc@106 92 | O => A
adamc@106 93 | S _ => unit
adamc@106 94 end) with
adamc@106 95 | First _ => tt
adamc@106 96 | Next _ _ => tt
adamc@106 97 end
adamc@106 98 | Cons _ x ls' => fun idx =>
adamc@215 99 match idx in fin n' return ilist (pred n') -> A with
adamc@106 100 | First _ => fun _ => x
adamc@106 101 | Next _ idx' => fun ls' => get ls' idx'
adamc@106 102 end ls'
adamc@106 103 end.
adamc@106 104
adamc@205 105 ]]
adamc@205 106
adamc@106 107 There is just one problem left with this implementation. Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination. We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
adamc@106 108
adamc@215 109 Fixpoint get n (ls : ilist n) : fin n -> A :=
adamc@215 110 match ls with
adamc@105 111 | Nil => fun idx =>
adamc@215 112 match idx in fin n' return (match n' with
adamc@105 113 | O => A
adamc@105 114 | S _ => unit
adamc@105 115 end) with
adamc@105 116 | First _ => tt
adamc@105 117 | Next _ _ => tt
adamc@105 118 end
adamc@105 119 | Cons _ x ls' => fun idx =>
adamc@215 120 match idx in fin n' return (fin (pred n') -> A) -> A with
adamc@105 121 | First _ => fun _ => x
adamc@105 122 | Next _ idx' => fun get_ls' => get_ls' idx'
adamc@105 123 end (get ls')
adamc@105 124 end.
adamc@113 125 (* end thide *)
adamc@105 126 End ilist.
adamc@105 127
adamc@105 128 Implicit Arguments Nil [A].
adamc@113 129 (* begin thide *)
adamc@108 130 Implicit Arguments First [n].
adamc@113 131 (* end thide *)
adamc@105 132
adamc@108 133 (** A few examples show how to make use of these definitions. *)
adamc@108 134
adamc@108 135 Check Cons 0 (Cons 1 (Cons 2 Nil)).
adamc@215 136 (** %\vspace{-.15in}% [[
adamc@215 137 Cons 0 (Cons 1 (Cons 2 Nil))
adamc@108 138 : ilist nat 3
adam@302 139 ]]
adam@302 140 *)
adamc@215 141
adamc@113 142 (* begin thide *)
adamc@108 143 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
adamc@215 144 (** %\vspace{-.15in}% [[
adamc@108 145 = 0
adamc@108 146 : nat
adam@302 147 ]]
adam@302 148 *)
adamc@215 149
adamc@108 150 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
adamc@215 151 (** %\vspace{-.15in}% [[
adamc@108 152 = 1
adamc@108 153 : nat
adam@302 154 ]]
adam@302 155 *)
adamc@215 156
adamc@108 157 Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
adamc@215 158 (** %\vspace{-.15in}% [[
adamc@108 159 = 2
adamc@108 160 : nat
adam@302 161 ]]
adam@302 162 *)
adamc@113 163 (* end thide *)
adamc@108 164
adamc@108 165 (** 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 166
adamc@105 167 Section ilist_map.
adamc@105 168 Variables A B : Set.
adamc@105 169 Variable f : A -> B.
adamc@105 170
adamc@215 171 Fixpoint imap n (ls : ilist A n) : ilist B n :=
adamc@215 172 match ls with
adamc@105 173 | Nil => Nil
adamc@105 174 | Cons _ x ls' => Cons (f x) (imap ls')
adamc@105 175 end.
adamc@105 176
adam@284 177 (** It is easy to prove that [get] %``%#"#distributes over#"#%''% [imap] calls. 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 178
adamc@215 179 Theorem get_imap : forall n (idx : fin n) (ls : ilist A n),
adamc@105 180 get (imap ls) idx = f (get ls idx).
adamc@113 181 (* begin thide *)
adamc@107 182 induction ls; dep_destruct idx; crush.
adamc@105 183 Qed.
adamc@113 184 (* end thide *)
adamc@105 185 End ilist_map.
adamc@107 186
adamc@107 187
adamc@107 188 (** * Heterogeneous Lists *)
adamc@107 189
adam@284 190 (** 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 191
adamc@107 192 Section hlist.
adamc@107 193 Variable A : Type.
adamc@107 194 Variable B : A -> Type.
adamc@107 195
adamc@113 196 (* 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 197
adamc@107 198 (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B]. *)
adamc@107 199
adamc@113 200 (* begin thide *)
adamc@107 201 Inductive hlist : list A -> Type :=
adamc@107 202 | MNil : hlist nil
adamc@107 203 | MCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
adamc@107 204
adamc@107 205 (** 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 206
adamc@113 207 (* end thide *)
adamc@113 208 (* EX: Define an analogue to [get] for [hlist]s. *)
adamc@113 209
adamc@113 210 (* begin thide *)
adamc@107 211 Variable elm : A.
adamc@107 212
adamc@107 213 Inductive member : list A -> Type :=
adamc@107 214 | MFirst : forall ls, member (elm :: ls)
adamc@107 215 | MNext : forall x ls, member ls -> member (x :: ls).
adamc@107 216
adam@284 217 (** 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 218
adamc@107 219 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 220
adamc@215 221 Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
adamc@215 222 match mls with
adamc@107 223 | MNil => fun mem =>
adamc@107 224 match mem in member ls' return (match ls' with
adamc@107 225 | nil => B elm
adamc@107 226 | _ :: _ => unit
adamc@107 227 end) with
adamc@107 228 | MFirst _ => tt
adamc@107 229 | MNext _ _ _ => tt
adamc@107 230 end
adamc@107 231 | MCons _ _ x mls' => fun mem =>
adamc@107 232 match mem in member ls' return (match ls' with
adamc@107 233 | nil => Empty_set
adamc@107 234 | x' :: ls'' =>
adamc@107 235 B x' -> (member ls'' -> B elm) -> B elm
adamc@107 236 end) with
adamc@107 237 | MFirst _ => fun x _ => x
adamc@107 238 | MNext _ _ 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 *)
adamc@108 245 Implicit Arguments MNil [A B].
adamc@108 246 Implicit Arguments MCons [A B x ls].
adamc@108 247
adamc@108 248 Implicit Arguments MFirst [A elm ls].
adamc@108 249 Implicit Arguments MNext [A elm x ls].
adamc@113 250 (* end thide *)
adamc@108 251
adamc@108 252 (** 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 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 :=
adamc@108 259 MCons 5 (MCons true MNil).
adamc@108 260
adamc@108 261 Eval simpl in hget someValues MFirst.
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
adamc@108 268 Eval simpl in hget someValues (MNext MFirst).
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 :=
adamc@108 278 MCons (1, 2) (MCons (true, false) MNil).
adamc@108 279
adamc@113 280 (* end thide *)
adamc@113 281
adamc@113 282
adamc@108 283 (** ** A Lambda Calculus Interpreter *)
adamc@108 284
adamc@108 285 (** 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 286
adamc@108 287 We start with an algebraic datatype for types. *)
adamc@108 288
adamc@108 289 Inductive type : Set :=
adamc@108 290 | Unit : type
adamc@108 291 | Arrow : type -> type -> type.
adamc@108 292
adam@284 293 (** 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, including a case study in Chapter 16. 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 294
adamc@108 295 Inductive exp : list type -> type -> Set :=
adamc@108 296 | Const : forall ts, exp ts Unit
adamc@113 297 (* begin thide *)
adamc@108 298 | Var : forall ts t, member t ts -> exp ts t
adamc@108 299 | App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
adamc@108 300 | Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
adamc@113 301 (* end thide *)
adamc@108 302
adamc@108 303 Implicit Arguments Const [ts].
adamc@108 304
adamc@108 305 (** We write a simple recursive function to translate [type]s into [Set]s. *)
adamc@108 306
adamc@108 307 Fixpoint typeDenote (t : type) : Set :=
adamc@108 308 match t with
adamc@108 309 | Unit => unit
adamc@108 310 | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
adamc@108 311 end.
adamc@108 312
adamc@108 313 (** 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 314
adamc@113 315 (* EX: Define an interpreter for [exp]s. *)
adamc@113 316
adamc@113 317 (* begin thide *)
adamc@215 318 Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
adamc@215 319 match e with
adamc@108 320 | Const _ => fun _ => tt
adamc@108 321
adamc@108 322 | Var _ _ mem => fun s => hget s mem
adamc@108 323 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@108 324 | Abs _ _ _ e' => fun s => fun x => expDenote e' (MCons x s)
adamc@108 325 end.
adamc@108 326
adamc@108 327 (** Like for previous examples, our interpreter is easy to run with [simpl]. *)
adamc@108 328
adamc@108 329 Eval simpl in expDenote Const MNil.
adamc@215 330 (** %\vspace{-.15in}% [[
adamc@108 331 = tt
adamc@108 332 : typeDenote Unit
adam@302 333 ]]
adam@302 334 *)
adamc@215 335
adamc@108 336 Eval simpl in expDenote (Abs (dom := Unit) (Var MFirst)) MNil.
adamc@215 337 (** %\vspace{-.15in}% [[
adamc@108 338 = fun x : unit => x
adamc@108 339 : typeDenote (Arrow Unit Unit)
adam@302 340 ]]
adam@302 341 *)
adamc@215 342
adamc@108 343 Eval simpl in expDenote (Abs (dom := Unit)
adamc@108 344 (Abs (dom := Unit) (Var (MNext MFirst)))) MNil.
adamc@215 345 (** %\vspace{-.15in}% [[
adamc@108 346 = fun x _ : unit => x
adamc@108 347 : typeDenote (Arrow Unit (Arrow Unit Unit))
adam@302 348 ]]
adam@302 349 *)
adamc@215 350
adamc@108 351 Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var MFirst))) MNil.
adamc@215 352 (** %\vspace{-.15in}% [[
adamc@108 353 = fun _ x0 : unit => x0
adamc@108 354 : typeDenote (Arrow Unit (Arrow Unit Unit))
adam@302 355 ]]
adam@302 356 *)
adamc@215 357
adamc@108 358 Eval simpl in expDenote (App (Abs (Var MFirst)) Const) MNil.
adamc@215 359 (** %\vspace{-.15in}% [[
adamc@108 360 = tt
adamc@108 361 : typeDenote Unit
adam@302 362 ]]
adam@302 363 *)
adamc@108 364
adamc@113 365 (* end thide *)
adamc@113 366
adamc@108 367 (** 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 368
adamc@108 369
adamc@109 370 (** * Recursive Type Definitions *)
adamc@109 371
adam@284 372 (** 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 373
adamc@113 374 (* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)
adamc@113 375
adamc@109 376 Section filist.
adamc@109 377 Variable A : Set.
adamc@109 378
adamc@113 379 (* begin thide *)
adamc@109 380 Fixpoint filist (n : nat) : Set :=
adamc@109 381 match n with
adamc@109 382 | O => unit
adamc@109 383 | S n' => A * filist n'
adamc@109 384 end%type.
adamc@109 385
adamc@109 386 (** 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 387
adamc@215 388 Fixpoint ffin (n : nat) : Set :=
adamc@109 389 match n with
adamc@109 390 | O => Empty_set
adamc@215 391 | S n' => option (ffin n')
adamc@109 392 end.
adamc@109 393
adam@284 394 (** 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 395
adamc@215 396 Fixpoint fget (n : nat) : filist n -> ffin n -> A :=
adamc@215 397 match n with
adamc@109 398 | O => fun _ idx => match idx with end
adamc@109 399 | S n' => fun ls idx =>
adamc@109 400 match idx with
adamc@109 401 | None => fst ls
adamc@109 402 | Some idx' => fget n' (snd ls) idx'
adamc@109 403 end
adamc@109 404 end.
adamc@109 405
adamc@215 406 (** 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 407 (* end thide *)
adamc@215 408
adamc@109 409 End filist.
adamc@109 410
adamc@109 411 (** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)
adamc@109 412
adamc@113 413 (* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)
adamc@113 414
adamc@109 415 Section fhlist.
adamc@109 416 Variable A : Type.
adamc@109 417 Variable B : A -> Type.
adamc@109 418
adamc@113 419 (* begin thide *)
adamc@109 420 Fixpoint fhlist (ls : list A) : Type :=
adamc@109 421 match ls with
adamc@109 422 | nil => unit
adamc@109 423 | x :: ls' => B x * fhlist ls'
adamc@109 424 end%type.
adamc@109 425
adamc@109 426 (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently-typed data elements. *)
adamc@109 427
adamc@109 428 Variable elm : A.
adamc@109 429
adamc@109 430 Fixpoint fmember (ls : list A) : Type :=
adamc@109 431 match ls with
adamc@109 432 | nil => Empty_set
adamc@109 433 | x :: ls' => (x = elm) + fmember ls'
adamc@109 434 end%type.
adamc@109 435
adamc@215 436 (** 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 [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 437
adamc@109 438 We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
adamc@109 439
adamc@109 440 [[
adamc@109 441 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 442 match ls with
adamc@109 443 | nil => fun _ idx => match idx with end
adamc@109 444 | _ :: ls' => fun mls idx =>
adamc@109 445 match idx with
adamc@109 446 | inl _ => fst mls
adamc@109 447 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 448 end
adamc@109 449 end.
adamc@109 450
adamc@205 451 ]]
adamc@205 452
adamc@109 453 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 454
adamc@109 455 Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
adamc@215 456 match ls with
adamc@109 457 | nil => fun _ idx => match idx with end
adamc@109 458 | _ :: ls' => fun mls idx =>
adamc@109 459 match idx with
adamc@109 460 | inl pf => match pf with
adamc@109 461 | refl_equal => fst mls
adamc@109 462 end
adamc@109 463 | inr idx' => fhget ls' (snd mls) idx'
adamc@109 464 end
adamc@109 465 end.
adamc@109 466
adamc@109 467 (** 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 468
adamc@109 469 Print eq.
adamc@215 470 (** %\vspace{-.15in}% [[
adamc@109 471 Inductive eq (A : Type) (x : A) : A -> Prop := refl_equal : x = x
adamc@215 472
adamc@109 473 ]]
adamc@109 474
adamc@215 475 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. *)
adamc@113 476 (* end thide *)
adamc@215 477
adamc@109 478 End fhlist.
adamc@110 479
adamc@111 480 Implicit Arguments fhget [A B elm ls].
adamc@111 481
adamc@110 482
adamc@110 483 (** * Data Structures as Index Functions *)
adamc@110 484
adamc@110 485 (** 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 486
adamc@110 487 Section tree.
adamc@110 488 Variable A : Set.
adamc@110 489
adamc@110 490 Inductive tree : Set :=
adamc@110 491 | Leaf : A -> tree
adamc@110 492 | Node : forall n, ilist tree n -> tree.
adamc@110 493 End tree.
adamc@110 494
adamc@110 495 (** 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 496
adamc@110 497 Section ifoldr.
adamc@110 498 Variables A B : Set.
adamc@110 499 Variable f : A -> B -> B.
adamc@110 500 Variable i : B.
adamc@110 501
adamc@215 502 Fixpoint ifoldr n (ls : ilist A n) : B :=
adamc@110 503 match ls with
adamc@110 504 | Nil => i
adamc@110 505 | Cons _ x ls' => f x (ifoldr ls')
adamc@110 506 end.
adamc@110 507 End ifoldr.
adamc@110 508
adamc@110 509 Fixpoint sum (t : tree nat) : nat :=
adamc@110 510 match t with
adamc@110 511 | Leaf n => n
adamc@110 512 | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
adamc@110 513 end.
adamc@110 514
adamc@110 515 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 516 match t with
adamc@110 517 | Leaf n => Leaf (S n)
adamc@110 518 | Node _ ls => Node (imap inc ls)
adamc@110 519 end.
adamc@110 520
adamc@110 521 (** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)
adamc@110 522
adamc@110 523 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@113 524 (* begin thide *)
adamc@110 525 induction t; crush.
adamc@110 526 (** [[
adamc@110 527 n : nat
adamc@110 528 i : ilist (tree nat) n
adamc@110 529 ============================
adamc@110 530 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
adamc@110 531 ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
adamc@215 532
adamc@110 533 ]]
adamc@110 534
adamc@110 535 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 536
adamc@110 537 Check tree_ind.
adamc@215 538 (** %\vspace{-.15in}% [[
adamc@215 539 tree_ind
adamc@110 540 : forall (A : Set) (P : tree A -> Prop),
adamc@110 541 (forall a : A, P (Leaf a)) ->
adamc@110 542 (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
adamc@110 543 forall t : tree A, P t
adamc@215 544
adamc@110 545 ]]
adamc@110 546
adamc@110 547 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 548
adamc@110 549 Abort.
adamc@110 550
adamc@110 551 Reset tree.
adamc@110 552
adamc@110 553 (** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)
adamc@110 554
adamc@110 555 Section tree.
adamc@110 556 Variable A : Set.
adamc@110 557
adamc@215 558 (** %\vspace{-.15in}% [[
adamc@110 559 Inductive tree : Set :=
adamc@110 560 | Leaf : A -> tree
adamc@110 561 | Node : forall n, filist tree n -> tree.
adamc@110 562
adamc@110 563 Error: Non strictly positive occurrence of "tree" in
adamc@110 564 "forall n : nat, filist tree n -> tree"
adamc@215 565
adamc@110 566 ]]
adamc@110 567
adamc@110 568 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 569
adamc@215 570 Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, reflexive types. Instead of merely using [fin] to get elements out of [ilist], we can %\textit{%#<i>#define#</i>#%}% [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 571
adamc@110 572 Inductive tree : Set :=
adamc@110 573 | Leaf : A -> tree
adamc@215 574 | Node : forall n, (ffin n -> tree) -> tree.
adamc@110 575
adamc@215 576 (** 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 577
adamc@110 578 End tree.
adamc@110 579
adamc@110 580 Implicit Arguments Node [A n].
adamc@110 581
adamc@215 582 (** We can redefine [sum] and [inc] for our new [tree] type. Again, it is useful to define a generic fold function first. This time, it takes in a function whose range is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
adamc@110 583
adamc@110 584 Section rifoldr.
adamc@110 585 Variables A B : Set.
adamc@110 586 Variable f : A -> B -> B.
adamc@110 587 Variable i : B.
adamc@110 588
adamc@215 589 Fixpoint rifoldr (n : nat) : (ffin n -> A) -> B :=
adamc@215 590 match n with
adamc@110 591 | O => fun _ => i
adamc@110 592 | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
adamc@110 593 end.
adamc@110 594 End rifoldr.
adamc@110 595
adamc@110 596 Implicit Arguments rifoldr [A B n].
adamc@110 597
adamc@110 598 Fixpoint sum (t : tree nat) : nat :=
adamc@110 599 match t with
adamc@110 600 | Leaf n => n
adamc@110 601 | Node _ f => rifoldr plus O (fun idx => sum (f idx))
adamc@110 602 end.
adamc@110 603
adamc@110 604 Fixpoint inc (t : tree nat) : tree nat :=
adamc@110 605 match t with
adamc@110 606 | Leaf n => Leaf (S n)
adamc@110 607 | Node _ f => Node (fun idx => inc (f idx))
adamc@110 608 end.
adamc@110 609
adamc@110 610 (** 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 611
adamc@110 612 Lemma plus_ge : forall x1 y1 x2 y2,
adamc@110 613 x1 >= x2
adamc@110 614 -> y1 >= y2
adamc@110 615 -> x1 + y1 >= x2 + y2.
adamc@110 616 crush.
adamc@110 617 Qed.
adamc@110 618
adamc@215 619 Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat),
adamc@110 620 (forall idx, f1 idx >= f2 idx)
adamc@110 621 -> rifoldr plus 0 f1 >= rifoldr plus 0 f2.
adamc@110 622 Hint Resolve plus_ge.
adamc@110 623
adamc@110 624 induction n; crush.
adamc@110 625 Qed.
adamc@110 626
adamc@110 627 Theorem sum_inc : forall t, sum (inc t) >= sum t.
adamc@110 628 Hint Resolve sum_inc'.
adamc@110 629
adamc@110 630 induction t; crush.
adamc@110 631 Qed.
adamc@110 632
adamc@113 633 (* end thide *)
adamc@113 634
adamc@110 635 (** 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 636
adamc@111 637 (** ** Another Interpreter Example *)
adamc@111 638
adamc@112 639 (** 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 640
adamc@112 641 Inductive type' : Type := Nat | Bool.
adamc@111 642
adamc@111 643 Inductive exp' : type' -> Type :=
adamc@112 644 | NConst : nat -> exp' Nat
adamc@112 645 | Plus : exp' Nat -> exp' Nat -> exp' Nat
adamc@112 646 | Eq : exp' Nat -> exp' Nat -> exp' Bool
adamc@111 647
adamc@112 648 | BConst : bool -> exp' Bool
adamc@113 649 (* begin thide *)
adamc@215 650 | Cond : forall n t, (ffin n -> exp' Bool)
adamc@215 651 -> (ffin n -> exp' t) -> exp' t -> exp' t.
adamc@113 652 (* end thide *)
adamc@111 653
adam@284 654 (** 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 655
adam@284 656 Example ex1 := Cond 2
adam@284 657 (fun f => match f with
adam@284 658 | None => Eq (Plus (NConst 2) (NConst 2)) (NConst 5)
adam@284 659 | Some None => Eq (Plus (NConst 1) (NConst 1)) (NConst 2)
adam@284 660 | Some (Some v) => match v with end
adam@284 661 end)
adam@284 662 (fun f => match f with
adam@284 663 | None => NConst 0
adam@284 664 | Some None => NConst 1
adam@284 665 | Some (Some v) => match v with end
adam@284 666 end)
adam@284 667 (NConst 2).
adam@284 668
adam@284 669 (** We start implementing our interpreter with a standard type denotation function. *)
adamc@112 670
adamc@111 671 Definition type'Denote (t : type') : Set :=
adamc@111 672 match t with
adamc@112 673 | Nat => nat
adamc@112 674 | Bool => bool
adamc@111 675 end.
adamc@111 676
adamc@112 677 (** 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 678
adamc@113 679 (* begin thide *)
adamc@111 680 Section cond.
adamc@111 681 Variable A : Set.
adamc@111 682 Variable default : A.
adamc@111 683
adamc@215 684 Fixpoint cond (n : nat) : (ffin n -> bool) -> (ffin n -> A) -> A :=
adamc@215 685 match n with
adamc@111 686 | O => fun _ _ => default
adamc@111 687 | S n' => fun tests bodies =>
adamc@111 688 if tests None
adamc@111 689 then bodies None
adamc@111 690 else cond n'
adamc@111 691 (fun idx => tests (Some idx))
adamc@111 692 (fun idx => bodies (Some idx))
adamc@111 693 end.
adamc@111 694 End cond.
adamc@111 695
adamc@111 696 Implicit Arguments cond [A n].
adamc@113 697 (* end thide *)
adamc@111 698
adamc@112 699 (** Now the expression interpreter is straightforward to write. *)
adamc@112 700
adamc@215 701 Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
adamc@215 702 match e with
adamc@215 703 | NConst n => n
adamc@215 704 | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
adamc@111 705 | Eq e1 e2 =>
adamc@111 706 if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false
adamc@111 707
adamc@215 708 | BConst b => b
adamc@111 709 | Cond _ _ tests bodies default =>
adamc@113 710 (* begin thide *)
adamc@111 711 cond
adamc@111 712 (exp'Denote default)
adamc@111 713 (fun idx => exp'Denote (tests idx))
adamc@111 714 (fun idx => exp'Denote (bodies idx))
adamc@113 715 (* end thide *)
adamc@111 716 end.
adamc@111 717
adamc@112 718 (** 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 719
adamc@113 720 (* begin thide *)
adamc@111 721 Section cfoldCond.
adamc@111 722 Variable t : type'.
adamc@111 723 Variable default : exp' t.
adamc@111 724
adamc@112 725 Fixpoint cfoldCond (n : nat)
adamc@215 726 : (ffin n -> exp' Bool) -> (ffin n -> exp' t) -> exp' t :=
adamc@215 727 match n with
adamc@111 728 | O => fun _ _ => default
adamc@111 729 | S n' => fun tests bodies =>
adamc@204 730 match tests None return _ with
adamc@111 731 | BConst true => bodies None
adamc@111 732 | BConst false => cfoldCond n'
adamc@111 733 (fun idx => tests (Some idx))
adamc@111 734 (fun idx => bodies (Some idx))
adamc@111 735 | _ =>
adamc@111 736 let e := cfoldCond n'
adamc@111 737 (fun idx => tests (Some idx))
adamc@111 738 (fun idx => bodies (Some idx)) in
adamc@112 739 match e in exp' t return exp' t -> exp' t with
adamc@112 740 | Cond n _ tests' bodies' default' => fun body =>
adamc@111 741 Cond
adamc@111 742 (S n)
adamc@111 743 (fun idx => match idx with
adamc@112 744 | None => tests None
adamc@111 745 | Some idx => tests' idx
adamc@111 746 end)
adamc@111 747 (fun idx => match idx with
adamc@111 748 | None => body
adamc@111 749 | Some idx => bodies' idx
adamc@111 750 end)
adamc@111 751 default'
adamc@112 752 | e => fun body =>
adamc@111 753 Cond
adamc@111 754 1
adamc@112 755 (fun _ => tests None)
adamc@111 756 (fun _ => body)
adamc@111 757 e
adamc@112 758 end (bodies None)
adamc@111 759 end
adamc@111 760 end.
adamc@111 761 End cfoldCond.
adamc@111 762
adamc@111 763 Implicit Arguments cfoldCond [t n].
adamc@113 764 (* end thide *)
adamc@111 765
adamc@112 766 (** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)
adamc@112 767
adamc@215 768 Fixpoint cfold t (e : exp' t) : exp' t :=
adamc@215 769 match e with
adamc@111 770 | NConst n => NConst n
adamc@111 771 | Plus e1 e2 =>
adamc@111 772 let e1' := cfold e1 in
adamc@111 773 let e2' := cfold e2 in
adamc@204 774 match e1', e2' return _ with
adamc@111 775 | NConst n1, NConst n2 => NConst (n1 + n2)
adamc@111 776 | _, _ => Plus e1' e2'
adamc@111 777 end
adamc@111 778 | Eq e1 e2 =>
adamc@111 779 let e1' := cfold e1 in
adamc@111 780 let e2' := cfold e2 in
adamc@204 781 match e1', e2' return _ with
adamc@111 782 | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
adamc@111 783 | _, _ => Eq e1' e2'
adamc@111 784 end
adamc@111 785
adamc@111 786 | BConst b => BConst b
adamc@111 787 | Cond _ _ tests bodies default =>
adamc@113 788 (* begin thide *)
adamc@111 789 cfoldCond
adamc@111 790 (cfold default)
adamc@111 791 (fun idx => cfold (tests idx))
adamc@111 792 (fun idx => cfold (bodies idx))
adamc@113 793 (* end thide *)
adamc@111 794 end.
adamc@111 795
adamc@113 796 (* begin thide *)
adam@296 797 (** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings. This lemma formalizes that property. The proof is a standard mostly-automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis. *)
adamc@112 798
adamc@111 799 Lemma cfoldCond_correct : forall t (default : exp' t)
adamc@215 800 n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
adamc@111 801 exp'Denote (cfoldCond default tests bodies)
adamc@111 802 = exp'Denote (Cond n tests bodies default).
adamc@111 803 induction n; crush;
adamc@111 804 match goal with
adamc@111 805 | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
adam@294 806 specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)))
adamc@111 807 end;
adamc@111 808 repeat (match goal with
adamc@111 809 | [ |- context[match ?E with
adamc@111 810 | NConst _ => _
adamc@111 811 | Plus _ _ => _
adamc@111 812 | Eq _ _ => _
adamc@111 813 | BConst _ => _
adamc@111 814 | Cond _ _ _ _ _ => _
adamc@111 815 end] ] => dep_destruct E
adamc@111 816 | [ |- context[if ?B then _ else _] ] => destruct B
adamc@111 817 end; crush).
adamc@111 818 Qed.
adamc@111 819
adamc@112 820 (** 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 821
adamc@215 822 Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : ffin n -> bool)
adamc@215 823 (bodies bodies' : ffin n -> A),
adamc@111 824 (forall idx, tests idx = tests' idx)
adamc@111 825 -> (forall idx, bodies idx = bodies' idx)
adamc@111 826 -> cond default tests bodies
adamc@111 827 = cond default tests' bodies'.
adamc@111 828 induction n; crush;
adamc@111 829 match goal with
adamc@111 830 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@111 831 end; crush.
adamc@111 832 Qed.
adamc@111 833
adamc@112 834 (** 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@113 835 (* end thide *)
adamc@112 836
adamc@111 837 Theorem cfold_correct : forall t (e : exp' t),
adamc@111 838 exp'Denote (cfold e) = exp'Denote e.
adamc@113 839 (* begin thide *)
adamc@111 840 Hint Rewrite cfoldCond_correct : cpdt.
adamc@111 841 Hint Resolve cond_ext.
adamc@111 842
adamc@111 843 induction e; crush;
adamc@111 844 repeat (match goal with
adamc@111 845 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@111 846 end; crush).
adamc@111 847 Qed.
adamc@113 848 (* end thide *)
adamc@115 849
adamc@115 850
adamc@215 851 (** * Choosing Between Representations *)
adamc@215 852
adamc@215 853 (** 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 854
adamc@215 855 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 856
adam@294 857 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.
adamc@215 858
adam@284 859 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 860
adamc@227 861 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 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. *)
adamc@215 862
adamc@215 863
adamc@115 864 (** * Exercises *)
adamc@115 865
adamc@116 866 (** remove printing * *)
adamc@116 867
adamc@216 868 (** Some of the type family definitions and associated functions from this chapter are duplicated in the [DepList] module of the book source. Some of their names have been changed to be more sensible in a general context.
adamc@115 869
adamc@115 870 %\begin{enumerate}%#<ol>#
adamc@115 871
adam@284 872 %\item%#<li># Define a tree analogue of [hlist]. That is, define a parameterized type of binary trees with data at their leaves, and define a type family [htree] indexed by trees. The structure of an [htree] mirrors its index tree, with the type of each data element (which only occur at leaves) determined by applying a type function to the corresponding element of the index tree. Define a type standing for all possible paths from the root of a tree to leaves and use it to implement a function [tget] for extracting an element of an [htree] by path. Define a function [htmap2] for %``%#"#mapping over two trees in parallel.#"#%''% That is, [htmap2] takes in two [htree]s with the same index tree, and it forms a new [htree] with the same index by applying a binary function pointwise.
adamc@115 873
adamc@129 874 Repeat this process so that you implement each definition for each of the three definition styles covered in this chapter: inductive, recursive, and index function.#</li>#
adamc@116 875
adamc@130 876 %\item%#<li># Write a dependently-typed interpreter for a simple programming language with ML-style pattern-matching, using one of the encodings of heterogeneous lists to represent the different branches of a [case] expression. (There are other ways to represent the same thing, but the point of this exercise is to practice using those heterogeneous list types.) The object language is defined informally by this grammar:
adamc@116 877
adamc@116 878 [[
adamc@116 879 t ::= bool | t + t
adamc@116 880 p ::= x | b | inl p | inr p
adamc@116 881 e ::= x | b | inl e | inr e | case e of [p => e]* | _ => e
adamc@215 882
adamc@116 883 ]]
adamc@116 884
adamc@116 885 [x] stands for a variable, and [b] stands for a boolean constant. The production for [case] expressions means that a pattern-match includes zero or more pairs of patterns and expressions, along with a default case.
adamc@116 886
adamc@117 887 Your interpreter should be implemented in the style demonstrated in this chapter. That is, your definition of expressions should use dependent types and de Bruijn indices to combine syntax and typing rules, such that the type of an expression tells the types of variables that are in scope. You should implement a simple recursive function translating types [t] to [Set], and your interpreter should produce values in the image of this translation.#</li>#
adamc@116 888
adamc@115 889 #</ol>#%\end{enumerate}% *)