Mercurial > cpdt > repo

annotate src/Generic.v @ 511:67d59a15b0e3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
RSS update
author Adam Chlipala <adam@chlipala.net>
date Wed, 13 Feb 2013 10:24:28 -0500
parents 04177dd1b133
children ed829eaa91b2
rev   line source
adam@398 1 (* Copyright (c) 2008-2010, 2012, Adam Chlipala
adamc@193 2 *
adamc@193 3 * This work is licensed under a
adamc@193 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@193 5 * Unported License.
adamc@193 6 * The license text is available at:
adamc@193 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@193 8 *)
adamc@193 9
adamc@193 10 (* begin hide *)
adamc@195 11 Require Import String List.
adamc@193 12
adam@314 13 Require Import CpdtTactics DepList.
adamc@193 14
adamc@193 15 Set Implicit Arguments.
adamc@193 16 (* end hide *)
adamc@193 17
adam@408 18 (** printing ~> $\leadsto$ *)
adam@408 19
adamc@193 20
adamc@219 21 (** %\chapter{Generic Programming}% *)
adamc@193 22
adam@408 23 (** %\index{generic programming}% _Generic programming_ makes it possible to write functions that operate over different types of data. %\index{parametric polymorphism}%Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style %\index{module systems}%module systems%~\cite{modules}% and Haskell %\index{type classes}%type classes%~\cite{typeclasses}% are more flexible cases. These language features are often not as powerful as we would like. For instance, while Haskell includes a type class classifying those types whose values can be pretty-printed, per-type pretty-printing is usually either implemented manually or implemented via a %\index{deriving clauses}%[deriving] clause%~\cite{deriving}%, which triggers ad-hoc code generation. Some clever encoding tricks have been used to achieve better within Haskell and other languages, but we can do%\index{datatype-generic programming}% _datatype-generic programming_ much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support.
adamc@193 24
adamc@219 25 Generic programming can often be very useful in Coq developments, so we devote this chapter to studying it. In a proof assistant, there is the new possibility of generic proofs about generic programs, which we also devote some space to. *)
adamc@193 26
adam@457 27 (** * Reifying Datatype Definitions *)
adamc@193 28
adam@488 29 (** The key to generic programming with dependent types is%\index{universe types}% _universe types_. This concept should not be confused with the idea of _universes_ from the metatheory of CIC and related languages, which we will study in more detail in the next chapter. Rather, the idea of universe types is to define inductive types that provide _syntactic representations_ of Coq types. We cannot directly write CIC programs that do case analysis on types, but we _can_ case analyze on reified syntactic versions of those types.
adamc@219 30
adam@358 31 Thus, to begin, we must define a syntactic representation of some class of datatypes. In this chapter, our running example will have to do with basic algebraic datatypes, of the kind found in ML and Haskell, but without additional bells and whistles like type parameters and mutually recursive definitions.
adamc@219 32
adam@480 33 The first step is to define a representation for constructors of our datatypes. We use the [Record] command as a shorthand for defining an inductive type with a single constructor, plus projection functions for pulling out any of the named arguments to that constructor. *)
adamc@219 34
adam@457 35 (* EX: Define a reified representation of simple algebraic datatypes. *)
adamc@198 36
adamc@198 37 (* begin thide *)
adamc@193 38 Record constructor : Type := Con {
adamc@193 39 nonrecursive : Type;
adamc@193 40 recursive : nat
adamc@193 41 }.
adamc@193 42
adam@286 43 (** The idea is that a constructor represented as [Con T n] has [n] arguments of the type that we are defining. Additionally, all of the other, non-recursive arguments can be encoded in the type [T]. When there are no non-recursive arguments, [T] can be [unit]. When there are two non-recursive arguments, of types [A] and [B], [T] can be [A * B]. We can generalize to any number of arguments via tupling.
adamc@219 44
adam@480 45 With this definition, it is easy to define a datatype representation in terms of lists of constructors. The intended meaning is that the datatype came from an inductive definition including exactly the constructors in the list. *)
adamc@219 46
adamc@193 47 Definition datatype := list constructor.
adamc@193 48
adamc@219 49 (** Here are a few example encodings for some common types from the Coq standard library. While our syntax type does not support type parameters directly, we can implement them at the meta level, via functions from types to [datatype]s. *)
adamc@219 50
adamc@193 51 Definition Empty_set_dt : datatype := nil.
adamc@193 52 Definition unit_dt : datatype := Con unit 0 :: nil.
adamc@193 53 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
adamc@193 54 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
adamc@193 55 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
adamc@219 56
adam@457 57 (** The type [Empty_set] has no constructors, so its representation is the empty list. The type [unit] has one constructor with no arguments, so its one reified constructor indicates no non-recursive data and [0] recursive arguments. The representation for [bool] just duplicates this single argumentless constructor. We get from [bool] to [nat] by changing one of the constructors to indicate 1 recursive argument. We get from [nat] to [list] by adding a non-recursive argument of a parameter type [A].
adamc@219 58
adamc@219 59 As a further example, we can do the same encoding for a generic binary tree type. *)
adamc@219 60
adamc@198 61 (* end thide *)
adamc@193 62
adamc@193 63 Section tree.
adamc@193 64 Variable A : Type.
adamc@193 65
adamc@193 66 Inductive tree : Type :=
adamc@193 67 | Leaf : A -> tree
adamc@193 68 | Node : tree -> tree -> tree.
adamc@193 69 End tree.
adamc@193 70
adamc@198 71 (* begin thide *)
adamc@193 72 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
adamc@193 73
adam@398 74 (** Each datatype representation stands for a family of inductive types. For a specific real datatype and a reputed representation for it, it is useful to define a type of _evidence_ that the datatype is compatible with the encoding. *)
adamc@219 75
adamc@193 76 Section denote.
adamc@193 77 Variable T : Type.
adamc@219 78 (** This variable stands for the concrete datatype that we are interested in. *)
adamc@193 79
adamc@193 80 Definition constructorDenote (c : constructor) :=
adamc@193 81 nonrecursive c -> ilist T (recursive c) -> T.
adam@358 82 (** We write that a constructor is represented as a function returning a [T]. Such a function takes two arguments, which pack together the non-recursive and recursive arguments of the constructor. We represent a tuple of all recursive arguments using the length-indexed list type %\index{Gallina terms!ilist}%[ilist] that we met in Chapter 8. *)
adamc@193 83
adamc@193 84 Definition datatypeDenote := hlist constructorDenote.
adam@358 85 (** Finally, the evidence for type [T] is a %\index{Gallina terms!hlist}%heterogeneous list, including a constructor denotation for every constructor encoding in a datatype encoding. Recall that, since we are inside a section binding [T] as a variable, [constructorDenote] is automatically parameterized by [T]. *)
adamc@219 86
adamc@193 87 End denote.
adamc@198 88 (* end thide *)
adamc@193 89
adam@504 90 (** Some example pieces of evidence should help clarify the convention. First, we define a helpful notation for constructor denotations. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *)
adamc@219 91
adamc@219 92 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)).
adamc@193 93
adamc@198 94 (* begin thide *)
adamc@193 95 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
adamc@216 96 HNil.
adamc@193 97 Definition unit_den : datatypeDenote unit unit_dt :=
adam@504 98 [_, _ ~> tt] ::: HNil.
adamc@193 99 Definition bool_den : datatypeDenote bool bool_dt :=
adam@504 100 [_, _ ~> true] ::: [_, _ ~> false] ::: HNil.
adamc@193 101 Definition nat_den : datatypeDenote nat nat_dt :=
adam@504 102 [_, _ ~> O] ::: [_, r ~> S (hd r)] ::: HNil.
adamc@193 103 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
adam@504 104 [_, _ ~> nil] ::: [x, r ~> x :: hd r] ::: HNil.
adamc@193 105 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
adam@504 106 [v, _ ~> Leaf v] ::: [_, r ~> Node (hd r) (hd (tl r))] ::: HNil.
adamc@198 107 (* end thide *)
adamc@194 108
adam@358 109 (** Recall that the [hd] and [tl] calls above operate on richly typed lists, where type indices tell us the lengths of lists, guaranteeing the safety of operations like [hd]. The type annotation attached to each definition provides enough information for Coq to infer list lengths at appropriate points. *)
adam@358 110
adamc@195 111
adamc@195 112 (** * Recursive Definitions *)
adamc@195 113
adamc@198 114 (* EX: Define a generic [size] function. *)
adamc@198 115
adam@457 116 (** We built these encodings of datatypes to help us write datatype-generic recursive functions. To do so, we will want a reified representation of a%\index{recursion schemes}% _recursion scheme_ for each type, similar to the [T_rect] principle generated automatically for an inductive definition of [T]. A clever reuse of [datatypeDenote] yields a short definition. *)
adamc@219 117
adamc@198 118 (* begin thide *)
adamc@194 119 Definition fixDenote (T : Type) (dt : datatype) :=
adamc@194 120 forall (R : Type), datatypeDenote R dt -> (T -> R).
adamc@194 121
adam@465 122 (** The idea of a recursion scheme is parameterized by a type and a reputed encoding of it. The principle itself is polymorphic in a type [R], which is the return type of the recursive function that we mean to write. The next argument is a heterogeneous list of one case of the recursive function definition for each datatype constructor. The [datatypeDenote] function turns out to have just the right definition to express the type we need; a set of function cases is just like an alternate set of constructors where we replace the original type [T] with the function result type [R]. Given such a reified definition, a [fixDenote] invocation returns a function from [T] to [R], which is just what we wanted.
adamc@219 123
adamc@219 124 We are ready to write some example functions now. It will be useful to use one new function from the [DepList] library included in the book source. *)
adamc@219 125
adamc@219 126 Check hmake.
adamc@219 127 (** %\vspace{-.15in}% [[
adamc@219 128 hmake
adamc@219 129 : forall (A : Type) (B : A -> Type),
adam@358 130 (forall x : A, B x) -> forall ls : list A, hlist B ls
adamc@219 131 ]]
adamc@219 132
adam@358 133 The function [hmake] is a kind of [map] alternative that goes from a regular [list] to an [hlist]. We can use it to define a generic size function that counts the number of constructors used to build a value in a datatype. *)
adamc@219 134
adamc@194 135 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
adamc@194 136 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
adamc@194 137
adam@488 138 (** Our definition is parameterized over a recursion scheme [fx]. We instantiate [fx] by passing it the function result type and a set of function cases, where we build the latter with [hmake]. The function argument to [hmake] takes three arguments: the representation of a constructor, its non-recursive arguments, and the results of recursive calls on all of its recursive arguments. We only need the recursive call results here, so we call them [r] and bind the other two inputs with wildcards. The actual case body is simple: we add together the recursive call results and increment the result by one (to account for the current constructor). This [foldr] function is an [ilist]-specific version defined in the [DepList] module.
adamc@219 139
adamc@219 140 It is instructive to build [fixDenote] values for our example types and see what specialized [size] functions result from them. *)
adamc@219 141
adamc@194 142 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
adamc@194 143 fun R _ emp => match emp with end.
adamc@194 144 Eval compute in size Empty_set_fix.
adamc@219 145 (** %\vspace{-.15in}% [[
adamc@219 146 = fun emp : Empty_set => match emp return nat with
adamc@219 147 end
adamc@219 148 : Empty_set -> nat
adamc@219 149 ]]
adamc@219 150
adamc@219 151 Despite all the fanciness of the generic [size] function, CIC's standard computation rules suffice to normalize the generic function specialization to exactly what we would have written manually. *)
adamc@194 152
adamc@194 153 Definition unit_fix : fixDenote unit unit_dt :=
adamc@216 154 fun R cases _ => (hhd cases) tt INil.
adamc@194 155 Eval compute in size unit_fix.
adamc@219 156 (** %\vspace{-.15in}% [[
adamc@219 157 = fun _ : unit => 1
adamc@219 158 : unit -> nat
adamc@219 159 ]]
adamc@219 160
adamc@219 161 Again normalization gives us the natural function definition. We see this pattern repeated for our other example types. *)
adamc@194 162
adamc@194 163 Definition bool_fix : fixDenote bool bool_dt :=
adamc@194 164 fun R cases b => if b
adamc@216 165 then (hhd cases) tt INil
adamc@216 166 else (hhd (htl cases)) tt INil.
adamc@194 167 Eval compute in size bool_fix.
adamc@219 168 (** %\vspace{-.15in}% [[
adamc@219 169 = fun b : bool => if b then 1 else 1
adamc@219 170 : bool -> nat
adam@302 171 ]]
adam@302 172 *)
adamc@194 173
adamc@194 174 Definition nat_fix : fixDenote nat nat_dt :=
adamc@194 175 fun R cases => fix F (n : nat) : R :=
adamc@194 176 match n with
adamc@216 177 | O => (hhd cases) tt INil
adamc@216 178 | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
adamc@194 179 end.
adamc@219 180
adamc@219 181 (** To peek at the [size] function for [nat], it is useful to avoid full computation, so that the recursive definition of addition is not expanded inline. We can accomplish this with proper flags for the [cbv] reduction strategy. *)
adamc@219 182
adamc@194 183 Eval cbv beta iota delta -[plus] in size nat_fix.
adamc@219 184 (** %\vspace{-.15in}% [[
adamc@219 185 = fix F (n : nat) : nat := match n with
adamc@219 186 | 0 => 1
adamc@219 187 | S n' => F n' + 1
adamc@219 188 end
adamc@219 189 : nat -> nat
adam@302 190 ]]
adam@302 191 *)
adamc@194 192
adamc@194 193 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
adamc@194 194 fun R cases => fix F (ls : list A) : R :=
adamc@194 195 match ls with
adamc@216 196 | nil => (hhd cases) tt INil
adamc@216 197 | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
adamc@194 198 end.
adamc@194 199 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
adamc@219 200 (** %\vspace{-.15in}% [[
adamc@219 201 = fun A : Type =>
adamc@219 202 fix F (ls : list A) : nat :=
adamc@219 203 match ls with
adamc@219 204 | nil => 1
adamc@219 205 | _ :: ls' => F ls' + 1
adamc@219 206 end
adamc@219 207 : forall A : Type, list A -> nat
adam@302 208 ]]
adam@302 209 *)
adamc@194 210
adamc@194 211 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
adamc@194 212 fun R cases => fix F (t : tree A) : R :=
adamc@194 213 match t with
adamc@216 214 | Leaf x => (hhd cases) x INil
adamc@216 215 | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
adamc@194 216 end.
adamc@194 217 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
adamc@219 218 (** %\vspace{-.15in}% [[
adamc@219 219 = fun A : Type =>
adamc@219 220 fix F (t : tree A) : nat :=
adamc@219 221 match t with
adamc@219 222 | Leaf _ => 1
adamc@219 223 | Node t1 t2 => F t1 + (F t2 + 1)
adamc@219 224 end
adamc@219 225 : forall A : Type, tree A -> n
adam@302 226 ]]
adam@302 227 *)
adamc@198 228 (* end thide *)
adamc@195 229
adam@457 230 (** As our examples show, even recursive datatypes are mapped to normal-looking size functions. *)
adam@457 231
adamc@195 232
adamc@195 233 (** ** Pretty-Printing *)
adamc@195 234
adamc@219 235 (** It is also useful to do generic pretty-printing of datatype values, rendering them as human-readable strings. To do so, we will need a bit of metadata for each constructor. Specifically, we need the name to print for the constructor and the function to use to render its non-recursive arguments. Everything else can be done generically. *)
adamc@219 236
adamc@195 237 Record print_constructor (c : constructor) : Type := PI {
adamc@195 238 printName : string;
adamc@195 239 printNonrec : nonrecursive c -> string
adamc@195 240 }.
adamc@195 241
adamc@219 242 (** It is useful to define a shorthand for applying the constructor [PI]. By applying it explicitly to an unknown application of the constructor [Con], we help type inference work. *)
adamc@219 243
adamc@195 244 Notation "^" := (PI (Con _ _)).
adamc@195 245
adamc@219 246 (** As in earlier examples, we define the type of metadata for a datatype to be a heterogeneous list type collecting metadata for each constructor. *)
adamc@219 247
adamc@195 248 Definition print_datatype := hlist print_constructor.
adamc@195 249
adamc@219 250 (** We will be doing some string manipulation here, so we import the notations associated with strings. *)
adamc@219 251
adamc@219 252 Local Open Scope string_scope.
adamc@219 253
adamc@219 254 (** Now it is easy to implement our generic printer, using another function from [DepList.] *)
adamc@219 255
adamc@219 256 Check hmap.
adamc@219 257 (** %\vspace{-.15in}% [[
adamc@219 258 hmap
adamc@219 259 : forall (A : Type) (B1 B2 : A -> Type),
adamc@219 260 (forall x : A, B1 x -> B2 x) ->
adamc@219 261 forall ls : list A, hlist B1 ls -> hlist B2 ls
adam@302 262 ]]
adam@302 263 *)
adamc@195 264
adamc@195 265 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
adamc@195 266 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
adamc@195 267 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
adamc@195 268 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
adamc@195 269
adamc@219 270 (** Some simple tests establish that [print] gets the job done. *)
adamc@219 271
adamc@216 272 Eval compute in print HNil Empty_set_fix.
adamc@219 273 (** %\vspace{-.15in}% [[
adamc@219 274 = fun emp : Empty_set => match emp return string with
adamc@219 275 end
adamc@219 276 : Empty_set -> string
adam@302 277 ]]
adam@302 278 *)
adamc@219 279
adamc@216 280 Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
adamc@219 281 (** %\vspace{-.15in}% [[
adamc@219 282 = fun _ : unit => "tt()"
adamc@219 283 : unit -> string
adam@302 284 ]]
adam@302 285 *)
adamc@219 286
adamc@195 287 Eval compute in print (^ "true" (fun _ => "")
adamc@195 288 ::: ^ "false" (fun _ => "")
adamc@216 289 ::: HNil) bool_fix.
adamc@219 290 (** %\vspace{-.15in}% [[
adamc@219 291 = fun b : bool => if b then "true()" else "false()"
adam@488 292 : bool -> string
adam@302 293 ]]
adam@302 294 *)
adamc@195 295
adamc@195 296 Definition print_nat := print (^ "O" (fun _ => "")
adamc@195 297 ::: ^ "S" (fun _ => "")
adamc@216 298 ::: HNil) nat_fix.
adamc@195 299 Eval cbv beta iota delta -[append] in print_nat.
adamc@219 300 (** %\vspace{-.15in}% [[
adamc@219 301 = fix F (n : nat) : string :=
adamc@219 302 match n with
adamc@219 303 | 0%nat => "O" ++ "(" ++ "" ++ ")"
adamc@219 304 | S n' => "S" ++ "(" ++ "" ++ ", " ++ F n' ++ ")"
adamc@219 305 end
adamc@219 306 : nat -> string
adam@302 307 ]]
adam@302 308 *)
adamc@219 309
adamc@195 310 Eval simpl in print_nat 0.
adamc@219 311 (** %\vspace{-.15in}% [[
adamc@219 312 = "O()"
adamc@219 313 : string
adam@302 314 ]]
adam@302 315 *)
adamc@219 316
adamc@195 317 Eval simpl in print_nat 1.
adamc@219 318 (** %\vspace{-.15in}% [[
adamc@219 319 = "S(, O())"
adamc@219 320 : string
adam@302 321 ]]
adam@302 322 *)
adamc@219 323
adamc@195 324 Eval simpl in print_nat 2.
adamc@219 325 (** %\vspace{-.15in}% [[
adamc@219 326 = "S(, S(, O()))"
adamc@219 327 : string
adam@302 328 ]]
adam@302 329 *)
adamc@195 330
adamc@195 331 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 332 print (^ "nil" (fun _ => "")
adamc@195 333 ::: ^ "cons" pr
adamc@216 334 ::: HNil) (@list_fix A).
adamc@219 335 (** %\vspace{-.15in}% [[
adamc@219 336 = fun (A : Type) (pr : A -> string) =>
adamc@219 337 fix F (ls : list A) : string :=
adamc@219 338 match ls with
adamc@219 339 | nil => "nil" ++ "(" ++ "" ++ ")"
adamc@219 340 | x :: ls' => "cons" ++ "(" ++ pr x ++ ", " ++ F ls' ++ ")"
adamc@219 341 end
adamc@219 342 : forall A : Type, (A -> string) -> list A -> string
adam@302 343 ]]
adam@302 344 *)
adamc@219 345
adamc@195 346 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 347 print (^ "Leaf" pr
adamc@195 348 ::: ^ "Node" (fun _ => "")
adamc@216 349 ::: HNil) (@tree_fix A).
adamc@219 350 (** %\vspace{-.15in}% [[
adamc@219 351 = fun (A : Type) (pr : A -> string) =>
adamc@219 352 fix F (t : tree A) : string :=
adamc@219 353 match t with
adamc@219 354 | Leaf x => "Leaf" ++ "(" ++ pr x ++ ")"
adamc@219 355 | Node t1 t2 =>
adamc@219 356 "Node" ++ "(" ++ "" ++ ", " ++ F t1 ++ ", " ++ F t2 ++ ")"
adamc@219 357 end
adamc@219 358 : forall A : Type, (A -> string) -> tree A -> string
adam@302 359 ]]
adam@302 360 *)
adamc@196 361
adam@428 362 (* begin hide *)
adam@437 363 (* begin thide *)
adam@428 364 Definition append' := append.
adam@437 365 (* end thide *)
adam@428 366 (* end hide *)
adam@428 367
adam@358 368 (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to. Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *)
adam@358 369
adamc@196 370
adamc@196 371 (** ** Mapping *)
adamc@196 372
adamc@219 373 (** By this point, we have developed enough machinery that it is old hat to define a generic function similar to the list [map] function. *)
adamc@219 374
adamc@219 375 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T)
adamc@219 376 : T -> T :=
adamc@196 377 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
adamc@196 378 (fun _ c x r => f (c x r)) dd).
adamc@196 379
adamc@196 380 Eval compute in map Empty_set_den Empty_set_fix.
adamc@219 381 (** %\vspace{-.15in}% [[
adamc@219 382 = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) =>
adamc@219 383 match emp return Empty_set with
adamc@219 384 end
adamc@219 385 : (Empty_set -> Empty_set) -> Empty_set -> Empty_set
adam@302 386 ]]
adam@302 387 *)
adamc@219 388
adamc@196 389 Eval compute in map unit_den unit_fix.
adamc@219 390 (** %\vspace{-.15in}% [[
adamc@219 391 = fun (f : unit -> unit) (_ : unit) => f tt
adamc@219 392 : (unit -> unit) -> unit -> unit
adam@302 393 ]]
adam@302 394 *)
adamc@219 395
adamc@196 396 Eval compute in map bool_den bool_fix.
adamc@219 397 (** %\vspace{-.15in}% [[
adamc@219 398 = fun (f : bool -> bool) (b : bool) => if b then f true else f false
adamc@219 399 : (bool -> bool) -> bool -> bool
adam@302 400 ]]
adam@302 401 *)
adamc@219 402
adamc@196 403 Eval compute in map nat_den nat_fix.
adamc@219 404 (** %\vspace{-.15in}% [[
adamc@219 405 = fun f : nat -> nat =>
adamc@219 406 fix F (n : nat) : nat :=
adamc@219 407 match n with
adamc@219 408 | 0%nat => f 0%nat
adamc@219 409 | S n' => f (S (F n'))
adamc@219 410 end
adamc@219 411 : (nat -> nat) -> nat -> nat
adam@302 412 ]]
adam@302 413 *)
adamc@219 414
adamc@196 415 Eval compute in fun A => map (list_den A) (@list_fix A).
adamc@219 416 (** %\vspace{-.15in}% [[
adamc@219 417 = fun (A : Type) (f : list A -> list A) =>
adamc@219 418 fix F (ls : list A) : list A :=
adamc@219 419 match ls with
adamc@219 420 | nil => f nil
adamc@219 421 | x :: ls' => f (x :: F ls')
adamc@219 422 end
adamc@219 423 : forall A : Type, (list A -> list A) -> list A -> list A
adam@302 424 ]]
adam@302 425 *)
adamc@219 426
adamc@196 427 Eval compute in fun A => map (tree_den A) (@tree_fix A).
adamc@219 428 (** %\vspace{-.15in}% [[
adamc@219 429 = fun (A : Type) (f : tree A -> tree A) =>
adamc@219 430 fix F (t : tree A) : tree A :=
adamc@219 431 match t with
adamc@219 432 | Leaf x => f (Leaf x)
adamc@219 433 | Node t1 t2 => f (Node (F t1) (F t2))
adamc@219 434 end
adamc@219 435 : forall A : Type, (tree A -> tree A) -> tree A -> tree A
adam@302 436 ]]
adam@302 437 *)
adamc@196 438
adam@358 439 (** These [map] functions are just as easy to use as those we write by hand. Can you figure out the input-output pattern that [map_nat S] displays in these examples? *)
adam@358 440
adamc@196 441 Definition map_nat := map nat_den nat_fix.
adamc@196 442 Eval simpl in map_nat S 0.
adamc@219 443 (** %\vspace{-.15in}% [[
adamc@219 444 = 1%nat
adamc@219 445 : nat
adam@302 446 ]]
adam@302 447 *)
adamc@219 448
adamc@196 449 Eval simpl in map_nat S 1.
adamc@219 450 (** %\vspace{-.15in}% [[
adamc@219 451 = 3%nat
adamc@219 452 : nat
adam@302 453 ]]
adam@302 454 *)
adamc@219 455
adamc@196 456 Eval simpl in map_nat S 2.
adamc@219 457 (** %\vspace{-.15in}% [[
adamc@219 458 = 5%nat
adamc@219 459 : nat
adam@302 460 ]]
adam@302 461 *)
adamc@196 462
adam@358 463 (** We get [map_nat S n] = [2 * n + 1], because the mapping process adds an extra [S] at every level of the inductive tree that defines a natural, including at the last level, the [O] constructor. *)
adam@358 464
adamc@196 465
adamc@196 466 (** * Proving Theorems about Recursive Definitions *)
adamc@196 467
adamc@219 468 (** We would like to be able to prove theorems about our generic functions. To do so, we need to establish additional well-formedness properties that must hold of pieces of evidence. *)
adamc@219 469
adamc@196 470 Section ok.
adamc@196 471 Variable T : Type.
adamc@196 472 Variable dt : datatype.
adamc@196 473
adamc@196 474 Variable dd : datatypeDenote T dt.
adamc@196 475 Variable fx : fixDenote T dt.
adamc@196 476
adamc@219 477 (** First, we characterize when a piece of evidence about a datatype is acceptable. The basic idea is that the type [T] should really be an inductive type with the definition given by [dd]. Semantically, inductive types are characterized by the ability to do induction on them. Therefore, we require that the usual induction principle is true, with respect to the constructors given in the encoding [dd]. *)
adamc@219 478
adamc@196 479 Definition datatypeDenoteOk :=
adamc@196 480 forall P : T -> Prop,
adamc@196 481 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@215 482 (forall i : fin (recursive c), P (get r i))
adamc@196 483 -> P ((hget dd m) x r))
adamc@196 484 -> forall v, P v.
adamc@196 485
adam@408 486 (** This definition can take a while to digest. The quantifier over [m : member c dt] is considering each constructor in turn; like in normal induction principles, each constructor has an associated proof case. The expression [hget dd m] then names the constructor we have selected. After binding [m], we quantify over all possible arguments (encoded with [x] and [r]) to the constructor that [m] selects. Within each specific case, we quantify further over [i : fin (recursive c)] to consider all of our induction hypotheses, one for each recursive argument of the current constructor.
adamc@219 487
adamc@219 488 We have completed half the burden of defining side conditions. The other half comes in characterizing when a recursion scheme [fx] is valid. The natural condition is that [fx] behaves appropriately when applied to any constructor application. *)
adamc@219 489
adamc@196 490 Definition fixDenoteOk :=
adamc@196 491 forall (R : Type) (cases : datatypeDenote R dt)
adamc@196 492 c (m : member c dt)
adamc@196 493 (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@216 494 fx cases ((hget dd m) x r)
adamc@216 495 = (hget cases m) x (imap (fx cases) r).
adamc@219 496
adamc@219 497 (** As for [datatypeDenoteOk], we consider all constructors and all possible arguments to them by quantifying over [m], [x], and [r]. The lefthand side of the equality that follows shows a call to the recursive function on the specific constructor application that we selected. The righthand side shows an application of the function case associated with constructor [m], applied to the non-recursive arguments and to appropriate recursive calls on the recursive arguments. *)
adamc@219 498
adamc@196 499 End ok.
adamc@196 500
adamc@219 501 (** We are now ready to prove that the [size] function we defined earlier always returns positive results. First, we establish a simple lemma. *)
adamc@196 502
adam@359 503 (* begin thide *)
adamc@196 504 Lemma foldr_plus : forall n (ils : ilist nat n),
adamc@196 505 foldr plus 1 ils > 0.
adamc@216 506 induction ils; crush.
adamc@196 507 Qed.
adamc@198 508 (* end thide *)
adamc@196 509
adamc@197 510 Theorem size_positive : forall T dt
adamc@197 511 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197 512 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@196 513 (v : T),
adamc@196 514 size fx v > 0.
adamc@198 515 (* begin thide *)
adamc@219 516 unfold size; intros.
adamc@219 517 (** [[
adamc@219 518 ============================
adamc@219 519 fx nat
adamc@219 520 (hmake
adamc@219 521 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 522 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0
adamc@219 523 ]]
adamc@219 524
adamc@219 525 Our goal is an inequality over a particular call to [size], with its definition expanded. How can we proceed here? We cannot use [induction] directly, because there is no way for Coq to know that [T] is an inductive type. Instead, we need to use the induction principle encoded in our hypothesis [dok] of type [datatypeDenoteOk dd]. Let us try applying it directly.
adamc@219 526 [[
adamc@219 527 apply dok.
adam@358 528 ]]
adam@358 529 %\vspace{-.3in}%
adam@358 530 <<
adamc@219 531 Error: Impossible to unify "datatypeDenoteOk dd" with
adamc@219 532 "fx nat
adamc@219 533 (hmake
adamc@219 534 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 535 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0".
adam@358 536 >>
adamc@219 537
adam@360 538 Matching the type of [dok] with the type of our conclusion requires more than simple first-order unification, so [apply] is not up to the challenge. We can use the %\index{tactics!pattern}%[pattern] tactic to get our goal into a form that makes it apparent exactly what the induction hypothesis is. *)
adamc@219 539
adamc@219 540 pattern v.
adam@358 541 (** %\vspace{-.15in}%[[
adamc@219 542 ============================
adamc@219 543 (fun t : T =>
adamc@219 544 fx nat
adamc@219 545 (hmake
adamc@219 546 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 547 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) t > 0) v
adam@302 548 ]]
adam@302 549 *)
adamc@219 550
adamc@219 551 apply dok; crush.
adam@358 552 (** %\vspace{-.15in}%[[
adamc@219 553 H : forall i : fin (recursive c),
adamc@219 554 fx nat
adamc@219 555 (hmake
adamc@219 556 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 557 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt)
adamc@219 558 (get r i) > 0
adamc@219 559 ============================
adamc@219 560 hget
adamc@219 561 (hmake
adamc@219 562 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 563 (r0 : ilist nat (recursive x0)) => foldr plus 1%nat r0) dt) m x
adamc@219 564 (imap
adamc@219 565 (fx nat
adamc@219 566 (hmake
adamc@219 567 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 568 (r0 : ilist nat (recursive x0)) =>
adamc@219 569 foldr plus 1%nat r0) dt)) r) > 0
adamc@219 570 ]]
adamc@219 571
adamc@219 572 An induction hypothesis [H] is generated, but we turn out not to need it for this example. We can simplify the goal using a library theorem about the composition of [hget] and [hmake]. *)
adamc@219 573
adamc@219 574 rewrite hget_hmake.
adam@358 575 (** %\vspace{-.15in}%[[
adamc@219 576 ============================
adamc@219 577 foldr plus 1%nat
adamc@219 578 (imap
adamc@219 579 (fx nat
adamc@219 580 (hmake
adamc@219 581 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 582 (r0 : ilist nat (recursive x0)) =>
adamc@219 583 foldr plus 1%nat r0) dt)) r) > 0
adamc@219 584 ]]
adamc@219 585
adamc@219 586 The lemma we proved earlier finishes the proof. *)
adamc@219 587
adamc@219 588 apply foldr_plus.
adamc@219 589
adamc@219 590 (** Using hints, we can redo this proof in a nice automated form. *)
adamc@219 591
adamc@219 592 Restart.
adamc@219 593
adam@375 594 Hint Rewrite hget_hmake.
adamc@196 595 Hint Resolve foldr_plus.
adamc@196 596
adamc@197 597 unfold size; intros; pattern v; apply dok; crush.
adamc@196 598 Qed.
adamc@198 599 (* end thide *)
adamc@197 600
adamc@219 601 (** It turned out that, in this example, we only needed to use induction degenerately as case analysis. A more involved theorem may only be proved using induction hypotheses. We will give its proof only in unautomated form and leave effective automation as an exercise for the motivated reader.
adamc@219 602
adamc@219 603 In particular, it ought to be the case that generic [map] applied to an identity function is itself an identity function. *)
adamc@219 604
adamc@197 605 Theorem map_id : forall T dt
adamc@197 606 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197 607 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@197 608 (v : T),
adamc@197 609 map dd fx (fun x => x) v = v.
adamc@198 610 (* begin thide *)
adamc@219 611 (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *)
adamc@219 612
adam@375 613 Hint Rewrite hget_hmap.
adamc@197 614
adamc@197 615 unfold map; intros; pattern v; apply dok; crush.
adam@358 616 (** %\vspace{-.15in}%[[
adamc@219 617 H : forall i : fin (recursive c),
adamc@219 618 fx T
adamc@219 619 (hmap
adamc@219 620 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 621 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 622 c x0 r) dd) (get r i) = get r i
adamc@219 623 ============================
adamc@219 624 hget dd m x
adamc@219 625 (imap
adamc@219 626 (fx T
adamc@219 627 (hmap
adamc@219 628 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 629 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 630 c0 x1 r0) dd)) r) = hget dd m x r
adamc@219 631 ]]
adamc@197 632
adamc@219 633 Our goal is an equality whose two sides begin with the same function call and initial arguments. We believe that the remaining arguments are in fact equal as well, and the [f_equal] tactic applies this reasoning step for us formally. *)
adamc@219 634
adamc@197 635 f_equal.
adam@358 636 (** %\vspace{-.15in}%[[
adamc@219 637 ============================
adamc@219 638 imap
adamc@219 639 (fx T
adamc@219 640 (hmap
adamc@219 641 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 642 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 643 c0 x1 r0) dd)) r = r
adamc@219 644 ]]
adamc@219 645
adamc@219 646 At this point, it is helpful to proceed by an inner induction on the heterogeneous list [r] of recursive call results. We could arrive at a cleaner proof by breaking this step out into an explicit lemma, but here we will do the induction inline to save space.*)
adamc@219 647
adamc@219 648 induction r; crush.
adamc@219 649
adam@428 650 (* begin hide *)
adam@437 651 (* begin thide *)
adam@428 652 Definition pred' := pred.
adam@437 653 (* end thide *)
adam@428 654 (* end hide *)
adam@428 655
adam@488 656 (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHr] is the inner IH (for induction over the recursive arguments).
adamc@219 657 [[
adamc@219 658 H : forall i : fin (S n),
adamc@219 659 fx T
adamc@219 660 (hmap
adamc@219 661 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 662 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 663 c x0 r) dd)
adamc@219 664 (match i in (fin n') return ((fin (pred n') -> T) -> T) with
adamc@219 665 | First n => fun _ : fin n -> T => a
adamc@219 666 | Next n idx' => fun get_ls' : fin n -> T => get_ls' idx'
adamc@219 667 end (get r)) =
adamc@219 668 match i in (fin n') return ((fin (pred n') -> T) -> T) with
adamc@219 669 | First n => fun _ : fin n -> T => a
adamc@219 670 | Next n idx' => fun get_ls' : fin n -> T => get_ls' idx'
adamc@219 671 end (get r)
adamc@219 672 IHr : (forall i : fin n,
adamc@219 673 fx T
adamc@219 674 (hmap
adamc@219 675 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 676 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 677 c x0 r) dd) (get r i) = get r i) ->
adamc@219 678 imap
adamc@219 679 (fx T
adamc@219 680 (hmap
adamc@219 681 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 682 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 683 c x0 r) dd)) r = r
adamc@219 684 ============================
adamc@219 685 ICons
adamc@219 686 (fx T
adamc@219 687 (hmap
adamc@219 688 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 689 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 690 c0 x1 r0) dd) a)
adamc@219 691 (imap
adamc@219 692 (fx T
adamc@219 693 (hmap
adamc@219 694 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 695 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 696 c0 x1 r0) dd)) r) = ICons a r
adamc@219 697 ]]
adamc@219 698
adamc@219 699 We see another opportunity to apply [f_equal], this time to split our goal into two different equalities over corresponding arguments. After that, the form of the first goal matches our outer induction hypothesis [H], when we give type inference some help by specifying the right quantifier instantiation. *)
adamc@219 700
adamc@219 701 f_equal.
adamc@219 702 apply (H First).
adam@358 703 (** %\vspace{-.15in}%[[
adamc@219 704 ============================
adamc@219 705 imap
adamc@219 706 (fx T
adamc@219 707 (hmap
adamc@219 708 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 709 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 710 c0 x1 r0) dd)) r = r
adamc@219 711 ]]
adamc@219 712
adamc@219 713 Now the goal matches the inner IH [IHr]. *)
adamc@219 714
adamc@219 715 apply IHr; crush.
adam@358 716 (** %\vspace{-.15in}%[[
adamc@219 717 i : fin n
adamc@219 718 ============================
adamc@219 719 fx T
adamc@219 720 (hmap
adamc@219 721 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 722 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 723 c0 x1 r0) dd) (get r i) = get r i
adamc@219 724 ]]
adamc@219 725
adamc@219 726 We can finish the proof by applying the outer IH again, specialized to a different [fin] value. *)
adamc@219 727
adamc@216 728 apply (H (Next i)).
adamc@197 729 Qed.
adamc@198 730 (* end thide *)
adam@358 731
adam@358 732 (** The proof involves complex subgoals, but, still, few steps are required, and then we may reuse our work across a variety of datatypes. *)