DataStruct.v 39.4 KB
Newer Older
1
(* Copyright (c) 2008-2012, 2015, Adam Chlipala
Adam Chlipala's avatar
Adam Chlipala committed
2 3 4 5 6 7 8 9 10
 * 
 * This work is licensed under a
 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
 * Unported License.
 * The license text is available at:
 *   http://creativecommons.org/licenses/by-nc-nd/3.0/
 *)

(* begin hide *)
11
Require Import Arith List.
Adam Chlipala's avatar
Adam Chlipala committed
12

13
Require Import Cpdt.CpdtTactics.
Adam Chlipala's avatar
Adam Chlipala committed
14 15

Set Implicit Arguments.
16
Set Asymmetric Patterns.
Adam Chlipala's avatar
Adam Chlipala committed
17 18 19 20 21
(* end hide *)


(** %\chapter{Dependent Data Structures}% *)

Adam Chlipala's avatar
Adam Chlipala committed
22
(** Our red-black tree example from the last chapter illustrated how dependent types enable static enforcement of data structure invariants.  To find interesting uses of dependent data structures, however, we need not look to the favorite examples of data structures and algorithms textbooks.  More basic examples like length-indexed and heterogeneous lists come up again and again as the building blocks of dependent programs.  There is a surprisingly large design space for this class of data structure, and we will spend this chapter exploring it. *)
Adam Chlipala's avatar
Adam Chlipala committed
23 24


Adam Chlipala's avatar
Adam Chlipala committed
25 26
(** * More Length-Indexed Lists *)

Adam Chlipala's avatar
Adam Chlipala committed
27
(** We begin with a deeper look at the length-indexed lists that began the last chapter.%\index{Gallina terms!ilist}% *)
Adam Chlipala's avatar
Adam Chlipala committed
28 29 30 31 32 33 34 35

Section ilist.
  Variable A : Set.

  Inductive ilist : nat -> Set :=
  | Nil : ilist O
  | Cons : forall n, A -> ilist n -> ilist (S n).

36
  (** We might like to have a certified function for selecting an element of an [ilist] by position.  We could do this using subset types and explicit manipulation of proofs, but dependent types let us do it more directly.  It is helpful to define a type family %\index{Gallina terms!fin}%[fin], where [fin n] is isomorphic to [{m : nat | m < n}].  The type family name stands for "finite." *)
Adam Chlipala's avatar
Adam Chlipala committed
37

Adam Chlipala's avatar
Adam Chlipala committed
38 39 40
  (* EX: Define a function [get] for extracting an [ilist] element by position. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
41 42 43
  Inductive fin : nat -> Set :=
  | First : forall n, fin (S n)
  | Next : forall n, fin n -> fin (S n).
Adam Chlipala's avatar
Adam Chlipala committed
44

Adam Chlipala's avatar
Adam Chlipala committed
45
  (** An instance of [fin] is essentially a more richly typed copy of a prefix of the natural numbers.  Every element is a [First] iterated through applying [Next] a number of times that indicates which number is being selected.  For instance, the three values of type [fin 3] are [First 2], [Next (First 1)], and [Next (Next (First 0))].
Adam Chlipala's avatar
Adam Chlipala committed
46 47 48

     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.
     [[
Adam Chlipala's avatar
Adam Chlipala committed
49 50
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
Adam Chlipala's avatar
Adam Chlipala committed
51 52 53 54 55 56 57
      | Nil => fun idx => ?
      | Cons _ x ls' => fun idx =>
        match idx with
          | First _ => x
          | Next _ idx' => get ls' idx'
        end
    end.
58
    ]]
59
    %\vspace{-.15in}%We apply the usual wisdom of delaying arguments in [Fixpoint]s so that they may be included in [return] clauses.  This still leaves us with a quandary in each of the [match] cases.  First, we need to figure out how to take advantage of the contradiction in the [Nil] case.  Every [fin] has a type of the form [S n], which cannot unify with the [O] value that we learn for [n] in the [Nil] case.  The solution we adopt is another case of [match]-within-[return], with the [return] clause chosen carefully so that it returns the proper type [A] in case the [fin] index is [O], which we know is true here; and so that it returns an easy-to-inhabit type [unit] in the remaining, impossible cases, which nonetheless appear explicitly in the body of the [match].
Adam Chlipala's avatar
Adam Chlipala committed
60
    [[
Adam Chlipala's avatar
Adam Chlipala committed
61 62
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
Adam Chlipala's avatar
Adam Chlipala committed
63
      | Nil => fun idx =>
Adam Chlipala's avatar
Adam Chlipala committed
64
        match idx in fin n' return (match n' with
Adam Chlipala's avatar
Adam Chlipala committed
65 66 67 68 69 70 71 72 73 74 75 76
                                        | O => A
                                        | S _ => unit
                                      end) with
          | First _ => tt
          | Next _ _ => tt
        end
      | Cons _ x ls' => fun idx =>
        match idx with
          | First _ => x
          | Next _ idx' => get ls' idx'
        end
    end.
77
    ]]
78
    %\vspace{-.15in}%Now the first [match] case type-checks, and we see that the problem with the [Cons] case is that the pattern-bound variable [idx'] does not have an apparent type compatible with [ls'].  In fact, the error message Coq gives for this exact code can be confusing, thanks to an overenthusiastic type inference heuristic.  We are told that the [Nil] case body has type [match X with | O => A | S _ => unit end] for a unification variable [X], while it is expected to have type [A].  We can see that setting [X] to [O] resolves the conflict, but Coq is not yet smart enough to do this unification automatically.  Repeating the function's type in a [return] annotation, used with an [in] annotation, leads us to a more informative error message, saying that [idx'] has type [fin n1] while it is expected to have type [fin n0], where [n0] is bound by the [Cons] pattern and [n1] by the [Next] pattern.  As the code is written above, nothing forces these two natural numbers to be equal, though we know intuitively that they must be.
79 80

    We need to use [match] annotations to make the relationship explicit.  Unfortunately, the usual trick of postponing argument binding will not help us here.  We need to match on both [ls] and [idx]; one or the other must be matched first.  To get around this, we apply the convoy pattern that we met last chapter.  This application is a little more clever than those we saw before; we use the natural number predecessor function [pred] to express the relationship between the types of these variables.
Adam Chlipala's avatar
Adam Chlipala committed
81
    [[
Adam Chlipala's avatar
Adam Chlipala committed
82 83
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
Adam Chlipala's avatar
Adam Chlipala committed
84
      | Nil => fun idx =>
Adam Chlipala's avatar
Adam Chlipala committed
85
        match idx in fin n' return (match n' with
Adam Chlipala's avatar
Adam Chlipala committed
86 87 88 89 90 91 92
                                        | O => A
                                        | S _ => unit
                                      end) with
          | First _ => tt
          | Next _ _ => tt
        end
      | Cons _ x ls' => fun idx =>
Adam Chlipala's avatar
Adam Chlipala committed
93
        match idx in fin n' return ilist (pred n') -> A with
Adam Chlipala's avatar
Adam Chlipala committed
94 95 96 97
          | First _ => fun _ => x
          | Next _ idx' => fun ls' => get ls' idx'
        end ls'
    end.
98
    ]]
99
    %\vspace{-.15in}%There is just one problem left with this implementation.  Though we know that the local [ls'] in the [Next] case is equal to the original [ls'], the type-checker is not satisfied that the recursive call to [get] does not introduce non-termination.  We solve the problem by convoy-binding the partial application of [get] to [ls'], rather than [ls'] by itself. *)
Adam Chlipala's avatar
Adam Chlipala committed
100

Adam Chlipala's avatar
Adam Chlipala committed
101 102
  Fixpoint get n (ls : ilist n) : fin n -> A :=
    match ls with
Adam Chlipala's avatar
Adam Chlipala committed
103
      | Nil => fun idx =>
Adam Chlipala's avatar
Adam Chlipala committed
104
        match idx in fin n' return (match n' with
Adam Chlipala's avatar
Adam Chlipala committed
105 106 107 108 109 110 111
                                        | O => A
                                        | S _ => unit
                                      end) with
          | First _ => tt
          | Next _ _ => tt
        end
      | Cons _ x ls' => fun idx =>
Adam Chlipala's avatar
Adam Chlipala committed
112
        match idx in fin n' return (fin (pred n') -> A) -> A with
Adam Chlipala's avatar
Adam Chlipala committed
113 114 115 116
          | First _ => fun _ => x
          | Next _ idx' => fun get_ls' => get_ls' idx'
        end (get ls')
    end.
Adam Chlipala's avatar
Adam Chlipala committed
117
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
118 119 120
End ilist.

Implicit Arguments Nil [A].
Adam Chlipala's avatar
Adam Chlipala committed
121
Implicit Arguments First [n].
Adam Chlipala's avatar
Adam Chlipala committed
122

Adam Chlipala's avatar
Adam Chlipala committed
123 124 125
(** A few examples show how to make use of these definitions. *)

Check Cons 0 (Cons 1 (Cons 2 Nil)).
Adam Chlipala's avatar
Adam Chlipala committed
126 127
(** %\vspace{-.15in}% [[
  Cons 0 (Cons 1 (Cons 2 Nil))
Adam Chlipala's avatar
Adam Chlipala committed
128
     : ilist nat 3
129 130
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
131

Adam Chlipala's avatar
Adam Chlipala committed
132
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
133
Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) First.
Adam Chlipala's avatar
Adam Chlipala committed
134
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
135 136
     = 0
     : nat
137 138
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
139

Adam Chlipala's avatar
Adam Chlipala committed
140 141
Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next First).
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
142 143
     = 1
     : nat
144 145
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
146

Adam Chlipala's avatar
Adam Chlipala committed
147 148
Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
149 150
     = 2
     : nat
151 152
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
153
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
154

155
(* begin hide *)
156
(* begin thide *)
157
Definition map' := map.
158
(* end thide *)
159 160
(* end hide *)

Adam Chlipala's avatar
Adam Chlipala committed
161
(** Our [get] function is also quite easy to reason about.  We show how with a short example about an analogue to the list [map] function. *)
Adam Chlipala's avatar
Adam Chlipala committed
162

Adam Chlipala's avatar
Adam Chlipala committed
163 164 165 166
Section ilist_map.
  Variables A B : Set.
  Variable f : A -> B.

Adam Chlipala's avatar
Adam Chlipala committed
167 168
  Fixpoint imap n (ls : ilist A n) : ilist B n :=
    match ls with
Adam Chlipala's avatar
Adam Chlipala committed
169 170 171 172
      | Nil => Nil
      | Cons _ x ls' => Cons (f x) (imap ls')
    end.

173
  (** It is easy to prove that [get] "distributes over" [imap] calls. *)
Adam Chlipala's avatar
Adam Chlipala committed
174

Adam Chlipala's avatar
Adam Chlipala committed
175 176 177
(* EX: Prove that [get] distributes over [imap]. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
178
  Theorem get_imap : forall n (idx : fin n) (ls : ilist A n),
Adam Chlipala's avatar
Adam Chlipala committed
179
    get (imap ls) idx = f (get ls idx).
Adam Chlipala's avatar
Adam Chlipala committed
180
    induction ls; dep_destruct idx; crush.
Adam Chlipala's avatar
Adam Chlipala committed
181
  Qed.
Adam Chlipala's avatar
Adam Chlipala committed
182
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
183
End ilist_map.
Adam Chlipala's avatar
Adam Chlipala committed
184

185
(** The only tricky bit is remembering to use our [dep_destruct] tactic in place of plain [destruct] when faced with a baffling tactic error message. *)
Adam Chlipala's avatar
Adam Chlipala committed
186 187 188

(** * Heterogeneous Lists *)

189
(** Programmers who move to statically typed functional languages from scripting languages often complain about the requirement that every element of a list have the same type.  With fancy type systems, we can partially lift this requirement.  We can index a list type with a "type-level" list that explains what type each element of the list should have.  This has been done in a variety of ways in Haskell using type classes, and we can do it much more cleanly and directly in Coq. *)
Adam Chlipala's avatar
Adam Chlipala committed
190 191 192 193 194

Section hlist.
  Variable A : Type.
  Variable B : A -> Type.

Adam Chlipala's avatar
Adam Chlipala committed
195 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. *)

Adam Chlipala's avatar
Adam Chlipala committed
197
  (** We parameterize our heterogeneous lists by a type [A] and an [A]-indexed type [B].%\index{Gallina terms!hlist}% *)
Adam Chlipala's avatar
Adam Chlipala committed
198

Adam Chlipala's avatar
Adam Chlipala committed
199
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
200
  Inductive hlist : list A -> Type :=
201 202
  | HNil : hlist nil
  | HCons : forall (x : A) (ls : list A), B x -> hlist ls -> hlist (x :: ls).
Adam Chlipala's avatar
Adam Chlipala committed
203

204
  (** We can implement a variant of the last section's [get] function for [hlist]s.  To get the dependent typing to work out, we will need to index our element selectors (in type family [member]) by the types of data that they point to.%\index{Gallina terms!member}% *)
Adam Chlipala's avatar
Adam Chlipala committed
205

Adam Chlipala's avatar
Adam Chlipala committed
206 207 208 209
(* end thide *)
  (* EX: Define an analogue to [get] for [hlist]s. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
210 211 212
  Variable elm : A.

  Inductive member : list A -> Type :=
213 214
  | HFirst : forall ls, member (elm :: ls)
  | HNext : forall x ls, member ls -> member (x :: ls).
Adam Chlipala's avatar
Adam Chlipala committed
215

216
  (** Because the element [elm] that we are "searching for" in a list does not change across the constructors of [member], we simplify our definitions by making [elm] a local variable.  In the definition of [member], we say that [elm] is found in any list that begins with [elm], and, if removing the first element of a list leaves [elm] present, then [elm] is present in the original list, too.  The form looks much like a predicate for list membership, but we purposely define [member] in [Type] so that we may decompose its values to guide computations.
Adam Chlipala's avatar
Adam Chlipala committed
217

218
     We can use [member] to adapt our definition of [get] to [hlist]s.  The same basic [match] tricks apply.  In the [HCons] case, we form a two-element convoy, passing both the data element [x] and the recursor for the sublist [mls'] to the result of the inner [match].  We did not need to do that in [get]'s definition because the types of list elements were not dependent there. *)
Adam Chlipala's avatar
Adam Chlipala committed
219

Adam Chlipala's avatar
Adam Chlipala committed
220 221
  Fixpoint hget ls (mls : hlist ls) : member ls -> B elm :=
    match mls with
222
      | HNil => fun mem =>
Adam Chlipala's avatar
Adam Chlipala committed
223 224 225 226
        match mem in member ls' return (match ls' with
                                          | nil => B elm
                                          | _ :: _ => unit
                                        end) with
227 228
          | HFirst _ => tt
          | HNext _ _ _ => tt
Adam Chlipala's avatar
Adam Chlipala committed
229
        end
230
      | HCons _ _ x mls' => fun mem =>
Adam Chlipala's avatar
Adam Chlipala committed
231 232 233
        match mem in member ls' return (match ls' with
                                          | nil => Empty_set
                                          | x' :: ls'' =>
234 235
                                            B x' -> (member ls'' -> B elm)
                                            -> B elm
Adam Chlipala's avatar
Adam Chlipala committed
236
                                        end) with
237 238
          | HFirst _ => fun x _ => x
          | HNext _ _ mem' => fun _ get_mls' => get_mls' mem'
Adam Chlipala's avatar
Adam Chlipala committed
239 240
        end x (hget mls')
    end.
Adam Chlipala's avatar
Adam Chlipala committed
241
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
242
End hlist.
Adam Chlipala's avatar
Adam Chlipala committed
243

Adam Chlipala's avatar
Adam Chlipala committed
244
(* begin thide *)
245 246
Implicit Arguments HNil [A B].
Implicit Arguments HCons [A B x ls].
Adam Chlipala's avatar
Adam Chlipala committed
247

248 249
Implicit Arguments HFirst [A elm ls].
Implicit Arguments HNext [A elm x ls].
Adam Chlipala's avatar
Adam Chlipala committed
250
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
251

252
(** By putting the parameters [A] and [B] in [Type], we enable fancier kinds of polymorphism than in mainstream functional languages.  For instance, one use of [hlist] is for the simple heterogeneous lists that we referred to earlier. *)
Adam Chlipala's avatar
Adam Chlipala committed
253 254 255

Definition someTypes : list Set := nat :: bool :: nil.

Adam Chlipala's avatar
Adam Chlipala committed
256 257
(* begin thide *)

Adam Chlipala's avatar
Adam Chlipala committed
258
Example someValues : hlist (fun T : Set => T) someTypes :=
259
  HCons 5 (HCons true HNil).
Adam Chlipala's avatar
Adam Chlipala committed
260

261
Eval simpl in hget someValues HFirst.
Adam Chlipala's avatar
Adam Chlipala committed
262
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
263 264
     = 5
     : (fun T : Set => T) nat
265 266
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
267

268
Eval simpl in hget someValues (HNext HFirst).
Adam Chlipala's avatar
Adam Chlipala committed
269
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
270 271
     = true
     : (fun T : Set => T) bool
272 273
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
274 275 276 277

(** We can also build indexed lists of pairs in this way. *)

Example somePairs : hlist (fun T : Set => T * T)%type someTypes :=
278
  HCons (1, 2) (HCons (true, false) HNil).
Adam Chlipala's avatar
Adam Chlipala committed
279

Adam Chlipala's avatar
Adam Chlipala committed
280
(** There are many other useful applications of heterogeneous lists, based on different choices of the first argument to [hlist]. *)
281

Adam Chlipala's avatar
Adam Chlipala committed
282 283 284
(* end thide *)


Adam Chlipala's avatar
Adam Chlipala committed
285 286
(** ** A Lambda Calculus Interpreter *)

287
(** Heterogeneous lists are very useful in implementing %\index{interpreters}%interpreters for functional programming languages.  Using the types and operations we have already defined, it is trivial to write an interpreter for simply typed lambda calculus%\index{lambda calculus}%.  Our interpreter can alternatively be thought of as a denotational semantics (but worry not if you are not familiar with such terminology from semantics).
Adam Chlipala's avatar
Adam Chlipala committed
288 289 290 291 292 293 294

   We start with an algebraic datatype for types. *)

Inductive type : Set :=
| Unit : type
| Arrow : type -> type -> type.

Adam Chlipala's avatar
Adam Chlipala committed
295
(** Now we can define a type family for expressions.  An [exp ts t] will stand for an expression that has type [t] and whose free variables have types in the list [ts].  We effectively use the de Bruijn index variable representation%~\cite{DeBruijn}%.  Variables are represented as [member] values; that is, a variable is more or less a constructive proof that a particular type is found in the type environment. *)
Adam Chlipala's avatar
Adam Chlipala committed
296 297 298

Inductive exp : list type -> type -> Set :=
| Const : forall ts, exp ts Unit
Adam Chlipala's avatar
Adam Chlipala committed
299
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
300 301 302
| Var : forall ts t, member t ts -> exp ts t
| App : forall ts dom ran, exp ts (Arrow dom ran) -> exp ts dom -> exp ts ran
| Abs : forall ts dom ran, exp (dom :: ts) ran -> exp ts (Arrow dom ran).
Adam Chlipala's avatar
Adam Chlipala committed
303
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
304 305 306 307 308 309 310 311 312 313 314

Implicit Arguments Const [ts].

(** We write a simple recursive function to translate [type]s into [Set]s. *)

Fixpoint typeDenote (t : type) : Set :=
  match t with
    | Unit => unit
    | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
  end.

315
(** Now it is straightforward to write an expression interpreter.  The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values.  An environment for a free variable list [ts] is simply an [hlist typeDenote ts].  That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type.  We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *)
Adam Chlipala's avatar
Adam Chlipala committed
316

Adam Chlipala's avatar
Adam Chlipala committed
317 318 319
(* EX: Define an interpreter for [exp]s. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
320 321
Fixpoint expDenote ts t (e : exp ts t) : hlist typeDenote ts -> typeDenote t :=
  match e with
Adam Chlipala's avatar
Adam Chlipala committed
322 323 324 325
    | Const _ => fun _ => tt

    | Var _ _ mem => fun s => hget s mem
    | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
326
    | Abs _ _ _ e' => fun s => fun x => expDenote e' (HCons x s)
Adam Chlipala's avatar
Adam Chlipala committed
327 328 329 330
  end.

(** Like for previous examples, our interpreter is easy to run with [simpl]. *)

331
Eval simpl in expDenote Const HNil.
Adam Chlipala's avatar
Adam Chlipala committed
332
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
333 334
    = tt
     : typeDenote Unit
335 336
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
337

338
Eval simpl in expDenote (Abs (dom := Unit) (Var HFirst)) HNil.
Adam Chlipala's avatar
Adam Chlipala committed
339
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
340 341
     = fun x : unit => x
     : typeDenote (Arrow Unit Unit)
342 343
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
344

Adam Chlipala's avatar
Adam Chlipala committed
345
Eval simpl in expDenote (Abs (dom := Unit)
346
  (Abs (dom := Unit) (Var (HNext HFirst)))) HNil.
Adam Chlipala's avatar
Adam Chlipala committed
347
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
348 349
     = fun x _ : unit => x
     : typeDenote (Arrow Unit (Arrow Unit Unit))
350 351
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
352

353
Eval simpl in expDenote (Abs (dom := Unit) (Abs (dom := Unit) (Var HFirst))) HNil.
Adam Chlipala's avatar
Adam Chlipala committed
354
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
355 356
     = fun _ x0 : unit => x0
     : typeDenote (Arrow Unit (Arrow Unit Unit))
357 358
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
359

360
Eval simpl in expDenote (App (Abs (Var HFirst)) Const) HNil.
Adam Chlipala's avatar
Adam Chlipala committed
361
(** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
362 363
     = tt
     : typeDenote Unit
364 365
]]
*)
Adam Chlipala's avatar
Adam Chlipala committed
366

Adam Chlipala's avatar
Adam Chlipala committed
367 368
(* end thide *)

Adam Chlipala's avatar
Adam Chlipala committed
369
(** We are starting to develop the tools behind dependent typing's amazing advantage over alternative approaches in several important areas.  Here, we have implemented complete syntax, typing rules, and evaluation semantics for simply typed lambda calculus without even needing to define a syntactic substitution operation.  We did it all without a single line of proof, and our implementation is manifestly executable.  Other, more common approaches to language formalization often state and prove explicit theorems about type safety of languages.  In the above example, we got type safety, termination, and other meta-theorems for free, by reduction to CIC, which we know has those properties. *)
Adam Chlipala's avatar
Adam Chlipala committed
370 371


372 373
(** * Recursive Type Definitions *)

374
(** %\index{recursive type definition}%There is another style of datatype definition that leads to much simpler definitions of the [get] and [hget] definitions above.  Because Coq supports "type-level computation," we can redo our inductive definitions as _recursive_ definitions.  Here we will preface type names with the letter [f] to indicate that they are based on explicit recursive _function_ definitions. *)
375

Adam Chlipala's avatar
Adam Chlipala committed
376 377
(* EX: Come up with an alternate [ilist] definition that makes it easier to write [get]. *)

378 379 380
Section filist.
  Variable A : Set.

Adam Chlipala's avatar
Adam Chlipala committed
381
(* begin thide *)
382 383 384 385 386 387 388 389
  Fixpoint filist (n : nat) : Set :=
    match n with
      | O => unit
      | S n' => A * filist n'
    end%type.

  (** 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']. *)

Adam Chlipala's avatar
Adam Chlipala committed
390
  Fixpoint ffin (n : nat) : Set :=
391 392
    match n with
      | O => Empty_set
Adam Chlipala's avatar
Adam Chlipala committed
393
      | S n' => option (ffin n')
394 395
    end.

396
  (** We express that there are no index values when [n = O], by defining such indices as type [Empty_set]; and we express that, at [n = S n'], there is a choice between picking the first element of the list (represented as [None]) or choosing a later element (represented by [Some idx], where [idx] is an index into the list tail).  For instance, the three values of type [ffin 3] are [None], [Some None], and [Some (Some None)]. *)
397

Adam Chlipala's avatar
Adam Chlipala committed
398 399
  Fixpoint fget (n : nat) : filist n -> ffin n -> A :=
    match n with
400 401 402 403 404 405 406 407
      | O => fun _ idx => match idx with end
      | S n' => fun ls idx =>
        match idx with
          | None => fst ls
          | Some idx' => fget n' (snd ls) idx'
        end
    end.

Adam Chlipala's avatar
Adam Chlipala committed
408
  (** Our new [get] implementation needs only one dependent [match], and its annotation is inferred for us.  Our choices of data structure implementations lead to just the right typing behavior for this new definition to work out. *)
Adam Chlipala's avatar
Adam Chlipala committed
409
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
410

411 412 413 414
End filist.

(** Heterogeneous lists are a little trickier to define with recursion, but we then reap similar benefits in simplicity of use. *)

Adam Chlipala's avatar
Adam Chlipala committed
415 416
(* EX: Come up with an alternate [hlist] definition that makes it easier to write [hget]. *)

417 418 419 420
Section fhlist.
  Variable A : Type.
  Variable B : A -> Type.

Adam Chlipala's avatar
Adam Chlipala committed
421
(* begin thide *)
422 423 424 425 426 427
  Fixpoint fhlist (ls : list A) : Type :=
    match ls with
      | nil => unit
      | x :: ls' => B x * fhlist ls'
    end%type.

Adam Chlipala's avatar
Adam Chlipala committed
428
  (** The definition of [fhlist] follows the definition of [filist], with the added wrinkle of dependently typed data elements. *)
429 430 431 432 433 434 435 436 437

  Variable elm : A.

  Fixpoint fmember (ls : list A) : Type :=
    match ls with
      | nil => Empty_set
      | x :: ls' => (x = elm) + fmember ls'
    end%type.

438
  (** The definition of [fmember] follows the definition of [ffin].  Empty lists have no members, and member types for nonempty lists are built by adding one new option to the type of members of the list tail.  While for [ffin] we needed no new information associated with the option that we add, here we need to know that the head of the list equals the element we are searching for.  We express that idea with a sum type whose left branch is the appropriate equality proposition.  Since we define [fmember] to live in [Type], we can insert [Prop] types as needed, because [Prop] is a subtype of [Type].
439 440 441 442

     We know all of the tricks needed to write a first attempt at a [get] function for [fhlist]s.
     [[
  Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
Adam Chlipala's avatar
Adam Chlipala committed
443
    match ls with
444 445 446 447 448 449 450
      | nil => fun _ idx => match idx with end
      | _ :: ls' => fun mls idx =>
        match idx with
          | inl _ => fst mls
          | inr idx' => fhget ls' (snd mls) idx'
        end
    end.
451
    ]]
452
    %\vspace{-.15in}%Only one problem remains.  The expression [fst mls] is not known to have the proper type.  To demonstrate that it does, we need to use the proof available in the [inl] case of the inner [match]. *)
453 454

  Fixpoint fhget (ls : list A) : fhlist ls -> fmember ls -> B elm :=
Adam Chlipala's avatar
Adam Chlipala committed
455
    match ls with
456 457 458 459
      | nil => fun _ idx => match idx with end
      | _ :: ls' => fun mls idx =>
        match idx with
          | inl pf => match pf with
460
                        | eq_refl => fst mls
461 462 463 464 465 466 467
                      end
          | inr idx' => fhget ls' (snd mls) idx'
        end
    end.

  (** 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. *)

468
  (* begin hide *)
469 470 471
  (* begin thide *)
  Definition foo := @eq_refl.
  (* end thide *)
472 473
  (* end hide *)

474
  Print eq.
Adam Chlipala's avatar
Adam Chlipala committed
475
  (** %\vspace{-.15in}% [[
476
Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
477 478
]]

479
In a proposition [x = y], we see that [x] is a parameter and [y] is a regular argument.  The type of the constructor [eq_refl] shows that [y] can only ever be instantiated to [x].  Thus, within a pattern-match with [eq_refl], occurrences of [y] can be replaced with occurrences of [x] for typing purposes. *)
Adam Chlipala's avatar
Adam Chlipala committed
480
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
481

482
End fhlist.
Adam Chlipala's avatar
Adam Chlipala committed
483

484 485
Implicit Arguments fhget [A B elm ls].

486 487
(** How does one choose between the two data structure encoding strategies we have presented so far?  Before answering that question in this chapter's final section, we introduce one further approach. *)

Adam Chlipala's avatar
Adam Chlipala committed
488 489 490

(** * Data Structures as Index Functions *)

Adam Chlipala's avatar
Adam Chlipala committed
491
(** %\index{index function}%Indexed lists can be useful in defining other inductive types with constructors that take variable numbers of arguments.  In this section, we consider parameterized trees with arbitrary branching factor. *)
Adam Chlipala's avatar
Adam Chlipala committed
492

493 494 495 496 497
(* begin hide *)
Definition red_herring := O.
(* working around a bug in Coq 8.5! *)
(* end hide *)

Adam Chlipala's avatar
Adam Chlipala committed
498 499 500 501 502 503 504 505 506 507 508 509 510 511 512
Section tree.
  Variable A : Set.

  Inductive tree : Set :=
  | Leaf : A -> tree
  | Node : forall n, ilist tree n -> tree.
End tree.

(** 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. *)

Section ifoldr.
  Variables A B : Set.
  Variable f : A -> B -> B.
  Variable i : B.

Adam Chlipala's avatar
Adam Chlipala committed
513
  Fixpoint ifoldr n (ls : ilist A n) : B :=
Adam Chlipala's avatar
Adam Chlipala committed
514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534
    match ls with
      | Nil => i
      | Cons _ x ls' => f x (ifoldr ls')
    end.
End ifoldr.

Fixpoint sum (t : tree nat) : nat :=
  match t with
    | Leaf n => n
    | Node _ ls => ifoldr (fun t' n => sum t' + n) O ls
  end.

Fixpoint inc (t : tree nat) : tree nat :=
  match t with
    | Leaf n => Leaf (S n)
    | Node _ ls => Node (imap inc ls)
  end.

(** Now we might like to prove that [inc] does not decrease a tree's [sum]. *)

Theorem sum_inc : forall t, sum (inc t) >= sum t.
Adam Chlipala's avatar
Adam Chlipala committed
535
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
536 537 538 539 540 541 542
  induction t; crush.
  (** [[
  n : nat
  i : ilist (tree nat) n
  ============================
   ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 (imap inc i) >=
   ifoldr (fun (t' : tree nat) (n0 : nat) => sum t' + n0) 0 i
Adam Chlipala's avatar
Adam Chlipala committed
543
 
Adam Chlipala's avatar
Adam Chlipala committed
544 545
   ]]

Adam Chlipala's avatar
Adam Chlipala committed
546
   We are left with a single subgoal which does not seem provable directly.  This is the same problem that we met in Chapter 3 with other %\index{nested inductive type}%nested inductive types. *)
Adam Chlipala's avatar
Adam Chlipala committed
547 548

  Check tree_ind.
Adam Chlipala's avatar
Adam Chlipala committed
549 550
  (** %\vspace{-.15in}% [[
  tree_ind
Adam Chlipala's avatar
Adam Chlipala committed
551 552 553 554 555 556
     : forall (A : Set) (P : tree A -> Prop),
       (forall a : A, P (Leaf a)) ->
       (forall (n : nat) (i : ilist (tree A) n), P (Node i)) ->
       forall t : tree A, P t
]]

Adam Chlipala's avatar
Adam Chlipala committed
557
The automatically generated induction principle is too weak.  For the [Node] case, it gives us no inductive hypothesis.  We could write our own induction principle, as we did in Chapter 3, but there is an easier way, if we are willing to alter the definition of [tree]. *)
Adam Chlipala's avatar
Adam Chlipala committed
558

Adam Chlipala's avatar
Adam Chlipala committed
559 560 561
Abort.

Reset tree.
562 563 564 565
(* begin hide *)
Reset red_herring.
(* working around a bug in Coq 8.5! *)
(* end hide *)
Adam Chlipala's avatar
Adam Chlipala committed
566 567 568 569 570 571

(** First, let us try using our recursive definition of [ilist]s instead of the inductive version. *)

Section tree.
  Variable A : Set.

Adam Chlipala's avatar
Adam Chlipala committed
572
  (** %\vspace{-.15in}% [[
Adam Chlipala's avatar
Adam Chlipala committed
573 574 575
  Inductive tree : Set :=
  | Leaf : A -> tree
  | Node : forall n, filist tree n -> tree.
Adam Chlipala's avatar
Adam Chlipala committed
576
]]
Adam Chlipala's avatar
Adam Chlipala committed
577

Adam Chlipala's avatar
Adam Chlipala committed
578
<<
Adam Chlipala's avatar
Adam Chlipala committed
579 580
Error: Non strictly positive occurrence of "tree" in
 "forall n : nat, filist tree n -> tree"
Adam Chlipala's avatar
Adam Chlipala committed
581
>>
Adam Chlipala's avatar
Adam Chlipala committed
582

Adam Chlipala's avatar
Adam Chlipala committed
583
  The special-case rule for nested datatypes only works with nested uses of other inductive types, which could be replaced with uses of new mutually inductive types.  We defined [filist] recursively, so it may not be used in nested inductive definitions.
Adam Chlipala's avatar
Adam Chlipala committed
584

585
  Our final solution uses yet another of the inductive definition techniques introduced in Chapter 3, %\index{reflexive inductive type}%reflexive types.  Instead of merely using [fin] to get elements out of [ilist], we can _define_ [ilist] in terms of [fin].  For the reasons outlined above, it turns out to be easier to work with [ffin] in place of [fin]. *)
Adam Chlipala's avatar
Adam Chlipala committed
586 587 588

  Inductive tree : Set :=
  | Leaf : A -> tree
Adam Chlipala's avatar
Adam Chlipala committed
589 590 591
  | Node : forall n, (ffin n -> tree) -> tree.

  (** 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. *)
Adam Chlipala's avatar
Adam Chlipala committed
592 593 594 595 596

End tree.

Implicit Arguments Node [A n].

597
(** We can redefine [sum] and [inc] for our new [tree] type.  Again, it is useful to define a generic fold function first.  This time, it takes in a function whose domain is some [ffin] type, and it folds another function over the results of calling the first function at every possible [ffin] value. *)
Adam Chlipala's avatar
Adam Chlipala committed
598 599 600 601 602 603

Section rifoldr.
  Variables A B : Set.
  Variable f : A -> B -> B.
  Variable i : B.

Adam Chlipala's avatar
Adam Chlipala committed
604 605
  Fixpoint rifoldr (n : nat) : (ffin n -> A) -> B :=
    match n with
Adam Chlipala's avatar
Adam Chlipala committed
606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624
      | O => fun _ => i
      | S n' => fun get => f (get None) (rifoldr n' (fun idx => get (Some idx)))
    end.
End rifoldr.

Implicit Arguments rifoldr [A B n].

Fixpoint sum (t : tree nat) : nat :=
  match t with
    | Leaf n => n
    | Node _ f => rifoldr plus O (fun idx => sum (f idx))
  end.

Fixpoint inc (t : tree nat) : tree nat :=
  match t with
    | Leaf n => Leaf (S n)
    | Node _ f => Node (fun idx => inc (f idx))
  end.

625
(** Now we are ready to prove the theorem where we got stuck before.  We will not need to define any new induction principle, but it _will_ be helpful to prove some lemmas. *)
Adam Chlipala's avatar
Adam Chlipala committed
626 627 628 629 630 631 632 633

Lemma plus_ge : forall x1 y1 x2 y2,
  x1 >= x2
  -> y1 >= y2
  -> x1 + y1 >= x2 + y2.
  crush.
Qed.

Adam Chlipala's avatar
Adam Chlipala committed
634
Lemma sum_inc' : forall n (f1 f2 : ffin n -> nat),
Adam Chlipala's avatar
Adam Chlipala committed
635
  (forall idx, f1 idx >= f2 idx)
636
  -> rifoldr plus O f1 >= rifoldr plus O f2.
Adam Chlipala's avatar
Adam Chlipala committed
637 638 639 640 641 642 643 644 645 646 647
  Hint Resolve plus_ge.

  induction n; crush.
Qed.

Theorem sum_inc : forall t, sum (inc t) >= sum t.
  Hint Resolve sum_inc'.

  induction t; crush.
Qed.

Adam Chlipala's avatar
Adam Chlipala committed
648 649
(* end thide *)

Adam Chlipala's avatar
Adam Chlipala committed
650
(** Even if Coq would generate complete induction principles automatically for nested inductive definitions like the one we started with, there would still be advantages to using this style of reflexive encoding.  We see one of those advantages in the definition of [inc], where we did not need to use any kind of auxiliary function.  In general, reflexive encodings often admit direct implementations of operations that would require recursion if performed with more traditional inductive data structures. *)
651 652 653

(** ** Another Interpreter Example *)

654
(** We develop another example of variable-arity constructors, in the form of optimization of a small expression language with a construct like Scheme's <<cond>>.  Each of our conditional expressions takes a list of pairs of boolean tests and bodies.  The value of the conditional comes from the body of the first test in the list to evaluate to [true].  To simplify the %\index{interpreters}%interpreter we will write, we force each conditional to include a final, default case. *)
655 656

Inductive type' : Type := Nat | Bool.
657 658

Inductive exp' : type' -> Type :=
659 660 661
| NConst : nat -> exp' Nat
| Plus : exp' Nat -> exp' Nat -> exp' Nat
| Eq : exp' Nat -> exp' Nat -> exp' Bool
662

663
| BConst : bool -> exp' Bool
Adam Chlipala's avatar
Adam Chlipala committed
664
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
665 666
| Cond : forall n t, (ffin n -> exp' Bool)
  -> (ffin n -> exp' t) -> exp' t -> exp' t.
Adam Chlipala's avatar
Adam Chlipala committed
667
(* end thide *)
668

669 670 671 672 673 674 675 676 677 678 679 680 681 682
(** 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. *)

Example ex1 := Cond 2
  (fun f => match f with
              | None => Eq (Plus (NConst 2) (NConst 2)) (NConst 5)
              | Some None => Eq (Plus (NConst 1) (NConst 1)) (NConst 2)
              | Some (Some v) => match v with end
            end)
  (fun f => match f with
              | None => NConst 0
              | Some None => NConst 1
              | Some (Some v) => match v with end
            end)
  (NConst 2).
683

684
(** We start implementing our interpreter with a standard type denotation function. *)
685

686 687
Definition type'Denote (t : type') : Set :=
  match t with
688 689
    | Nat => nat
    | Bool => bool
690 691
  end.

692 693
(** To implement the expression interpreter, it is useful to have the following function that implements the functionality of [Cond] without involving any syntax. *)

Adam Chlipala's avatar
Adam Chlipala committed
694
(* begin thide *)
695 696 697 698
Section cond.
  Variable A : Set.
  Variable default : A.

Adam Chlipala's avatar
Adam Chlipala committed
699 700
  Fixpoint cond (n : nat) : (ffin n -> bool) -> (ffin n -> A) -> A :=
    match n with
701 702 703 704 705 706 707 708 709 710 711
      | O => fun _ _ => default
      | S n' => fun tests bodies =>
        if tests None
          then bodies None
          else cond n'
            (fun idx => tests (Some idx))
            (fun idx => bodies (Some idx))
    end.
End cond.

Implicit Arguments cond [A n].
Adam Chlipala's avatar
Adam Chlipala committed
712
(* end thide *)
713

714 715
(** Now the expression interpreter is straightforward to write. *)

716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736
(* begin thide *)
Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
  match e with
    | NConst n => n
    | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
    | Eq e1 e2 =>
      if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false

    | BConst b => b
    | Cond _ _ tests bodies default =>
      cond
      (exp'Denote default)
      (fun idx => exp'Denote (tests idx))
      (fun idx => exp'Denote (bodies idx))
  end.
(* begin hide *)
Reset exp'Denote.
(* end hide *)
(* end thide *)

(* begin hide *)
Adam Chlipala's avatar
Adam Chlipala committed
737 738 739 740
Fixpoint exp'Denote t (e : exp' t) : type'Denote t :=
  match e with
    | NConst n => n
    | Plus e1 e2 => exp'Denote e1 + exp'Denote e2
741 742 743
    | Eq e1 e2 =>
      if eq_nat_dec (exp'Denote e1) (exp'Denote e2) then true else false

Adam Chlipala's avatar
Adam Chlipala committed
744
    | BConst b => b
745
    | Cond _ _ tests bodies default =>
Adam Chlipala's avatar
Adam Chlipala committed
746
(* begin thide *)
747 748 749 750
      cond
      (exp'Denote default)
      (fun idx => exp'Denote (tests idx))
      (fun idx => exp'Denote (bodies idx))
Adam Chlipala's avatar
Adam Chlipala committed
751
(* end thide *)
752
  end.
753
(* end hide *)
754

755 756
(** 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. *)

Adam Chlipala's avatar
Adam Chlipala committed
757
(* begin thide *)
758 759 760 761
Section cfoldCond.
  Variable t : type'.
  Variable default : exp' t.

762
  Fixpoint cfoldCond (n : nat)
Adam Chlipala's avatar
Adam Chlipala committed
763 764
    : (ffin n -> exp' Bool) -> (ffin n -> exp' t) -> exp' t :=
    match n with
765 766
      | O => fun _ _ => default
      | S n' => fun tests bodies =>
767
        match tests None return _ with
768 769 770 771 772 773 774 775
          | BConst true => bodies None
          | BConst false => cfoldCond n'
            (fun idx => tests (Some idx))
            (fun idx => bodies (Some idx))
          | _ =>
            let e := cfoldCond n'
              (fun idx => tests (Some idx))
              (fun idx => bodies (Some idx)) in
776 777
            match e in exp' t return exp' t -> exp' t with
              | Cond n _ tests' bodies' default' => fun body =>
778 779 780
                Cond
                (S n)
                (fun idx => match idx with
781
                              | None => tests None
782 783 784 785 786 787 788
                              | Some idx => tests' idx
                            end)
                (fun idx => match idx with
                              | None => body
                              | Some idx => bodies' idx
                            end)
                default'
789
              | e => fun body =>
790 791
                Cond
                1
792
                (fun _ => tests None)
793 794
                (fun _ => body)
                e
795
            end (bodies None)
796 797 798 799 800
        end
    end.
End cfoldCond.

Implicit Arguments cfoldCond [t n].
Adam Chlipala's avatar
Adam Chlipala committed
801
(* end thide *)
802

803 804
(** Like for the interpreters, most of the action was in this helper function, and [cfold] itself is easy to write. *)

805
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
806 807
Fixpoint cfold t (e : exp' t) : exp' t :=
  match e with
808 809 810 811
    | NConst n => NConst n
    | Plus e1 e2 =>
      let e1' := cfold e1 in
      let e2' := cfold e2 in
812
      match e1', e2' return exp' Nat with
813 814 815 816 817 818
        | NConst n1, NConst n2 => NConst (n1 + n2)
        | _, _ => Plus e1' e2'
      end
    | Eq e1 e2 =>
      let e1' := cfold e1 in
      let e2' := cfold e2 in
819
      match e1', e2' return exp' Bool with
820 821 822 823 824 825 826 827 828 829 830
        | NConst n1, NConst n2 => BConst (if eq_nat_dec n1 n2 then true else false)
        | _, _ => Eq e1' e2'
      end

    | BConst b => BConst b
    | Cond _ _ tests bodies default =>
      cfoldCond
      (cfold default)
      (fun idx => cfold (tests idx))
      (fun idx => cfold (bodies idx))
  end.
831
(* end thide *)
832

Adam Chlipala's avatar
Adam Chlipala committed
833
(* begin thide *)
834
(** To prove our final correctness theorem, it is useful to know that [cfoldCond] preserves expression meanings.  The following lemma formalizes that property.  The proof is a standard mostly automated one, with the only wrinkle being a guided instantiation of the quantifiers in the induction hypothesis. *)
835

836
Lemma cfoldCond_correct : forall t (default : exp' t)
Adam Chlipala's avatar
Adam Chlipala committed
837
  n (tests : ffin n -> exp' Bool) (bodies : ffin n -> exp' t),
838 839 840 841 842
  exp'Denote (cfoldCond default tests bodies)
  = exp'Denote (Cond n tests bodies default).
  induction n; crush;
    match goal with
      | [ IHn : forall tests bodies, _, tests : _ -> _, bodies : _ -> _ |- _ ] =>
843
        specialize (IHn (fun idx => tests (Some idx)) (fun idx => bodies (Some idx)))
844 845
    end;
    repeat (match goal with
846 847
              | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>
                dep_destruct E
848 849 850 851
              | [ |- context[if ?B then _ else _] ] => destruct B
            end; crush).
Qed.

852
(** It is also useful to know that the result of a call to [cond] is not changed by substituting new tests and bodies functions, so long as the new functions have the same input-output behavior as the old.  It turns out that, in Coq, it is not possible to prove in general that functions related in this way are equal.  We treat this issue with our discussion of axioms in a later chapter.  For now, it suffices to prove that the particular function [cond] is _extensional_; that is, it is unaffected by substitution of functions with input-output equivalents. *)
853

Adam Chlipala's avatar
Adam Chlipala committed
854 855
Lemma cond_ext : forall (A : Set) (default : A) n (tests tests' : ffin n -> bool)
  (bodies bodies' : ffin n -> A),
856 857 858 859 860 861 862 863 864 865
  (forall idx, tests idx = tests' idx)
  -> (forall idx, bodies idx = bodies' idx)
  -> cond default tests bodies
  = cond default tests' bodies'.
  induction n; crush;
    match goal with
      | [ |- context[if ?E then _ else _] ] => destruct E
    end; crush.
Qed.

866
(** Now the final theorem is easy to prove. *)
Adam Chlipala's avatar
Adam Chlipala committed
867
(* end thide *)
868

869 870
Theorem cfold_correct : forall t (e : exp' t),
  exp'Denote (cfold e) = exp'Denote e.
Adam Chlipala's avatar
Adam Chlipala committed
871
(* begin thide *)
872
  Hint Rewrite cfoldCond_correct.
873 874 875 876 877 878 879
  Hint Resolve cond_ext.

  induction e; crush;
    repeat (match goal with
              | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
            end; crush).
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
880
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
881

882
(** We add our two lemmas as hints and perform standard automation with pattern-matching of subterms to destruct. *)
Adam Chlipala's avatar
Adam Chlipala committed
883

Adam Chlipala's avatar
Adam Chlipala committed
884 885 886 887 888 889
(** * Choosing Between Representations *)

(** 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.

   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.

890
   Recursive types usually involve much less initial effort, but they can be less convenient to use with proof automation.  For instance, the [simpl] tactic (which is among the ingredients in [crush]) will sometimes be overzealous in simplifying uses of functions over recursive types.  Consider a call [get l f], where variable [l] has type [filist A (S n)].  The type of [l] would be simplified to an explicit pair type.  In a proof involving many recursive types, this kind of unhelpful "simplification" can lead to rapid bloat in the sizes of subgoals.  Even worse, it can prevent syntactic pattern-matching, like in cases where [filist] is expected but a pair type is found in the "simplified" version.  The same problem applies to applications of recursive functions to values in recursive types: the recursive function call may "simplify" when the top-level structure of the type index but not the recursive value is known, because such functions are generally defined by recursion on the index, not the value.
Adam Chlipala's avatar
Adam Chlipala committed
891

892
   Another disadvantage of recursive types is that they only apply to type families whose indices determine their "skeletons."  This is not true for all data structures; a good counterexample comes from the richly typed programming language syntax types we have used several times so far.  The fact that a piece of syntax has type [Nat] tells us nothing about the tree structure of that syntax.
Adam Chlipala's avatar
Adam Chlipala committed
893

894
   Finally, Coq type inference can be more helpful in constructing values in inductive types.  Application of a particular constructor of that type tells Coq what to expect from the arguments, while, for instance, forming a generic pair does not make clear an intention to interpret the value as belonging to a particular recursive type.  This downside can be mitigated to an extent by writing "constructor" functions for a recursive type, mirroring the definition of the corresponding inductive type.
Adam Chlipala's avatar
Adam Chlipala committed
895

Adam Chlipala's avatar
Adam Chlipala committed
896
   Reflexive encodings of data types are seen relatively rarely.  As our examples demonstrated, manipulating index values manually can lead to hard-to-read code.  A normal inductive type is generally easier to work with, once someone has gone through the trouble of implementing an induction principle manually with the techniques we studied in Chapter 3.  For small developments, avoiding that kind of coding can justify the use of reflexive data structures.  There are also some useful instances of %\index{co-inductive types}%co-inductive definitions with nested data structures (e.g., lists of values in the co-inductive type) that can only be deconstructed effectively with reflexive encoding of the nested structures. *)