Mercurial > cpdt > repo

annotate src/Generic.v @ 471:51a8472aca68

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Batch of changes based on proofreader feedback
author Adam Chlipala <adam@chlipala.net>
date Mon, 08 Oct 2012 16:04:49 -0400
parents 4320c1a967c2
children f38a3af9dd17
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@457 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. 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
adamc@219 33 The first step is to define a representation for constructors of our datatypes. *)
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
adamc@219 45 With this definition, it as easy to define a datatype representation in terms of lists of constructors. *)
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
adamc@219 90 (** Some example pieces of evidence should help clarify the convention. First, we define some helpful notations, providing different ways of writing constructor denotations. There is really just one notation, but we need several versions of it to cover different choices of which variables will be used in the body of a definition. %The ASCII \texttt{\textasciitilde{}>} from the notation will be rendered later as $\leadsto$.% *)
adamc@219 91
adamc@193 92 Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
adamc@193 93 Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
adamc@219 94 Notation "[ ! , r ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ _)).
adamc@219 95 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)).
adamc@193 96
adamc@198 97 (* begin thide *)
adamc@193 98 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
adamc@216 99 HNil.
adamc@193 100 Definition unit_den : datatypeDenote unit unit_dt :=
adamc@216 101 [!, ! ~> tt] ::: HNil.
adamc@193 102 Definition bool_den : datatypeDenote bool bool_dt :=
adamc@216 103 [!, ! ~> true] ::: [!, ! ~> false] ::: HNil.
adamc@193 104 Definition nat_den : datatypeDenote nat nat_dt :=
adamc@219 105 [!, ! ~> O] ::: [!, r ~> S (hd r)] ::: HNil.
adamc@193 106 Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
adamc@219 107 [!, ! ~> nil] ::: [x, r ~> x :: hd r] ::: HNil.
adamc@193 108 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
adamc@219 109 [v, ! ~> Leaf v] ::: [!, r ~> Node (hd r) (hd (tl r))] ::: HNil.
adamc@198 110 (* end thide *)
adamc@194 111
adam@358 112 (** 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 113
adamc@195 114
adamc@195 115 (** * Recursive Definitions *)
adamc@195 116
adamc@198 117 (* EX: Define a generic [size] function. *)
adamc@198 118
adam@457 119 (** 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 120
adamc@198 121 (* begin thide *)
adamc@194 122 Definition fixDenote (T : Type) (dt : datatype) :=
adamc@194 123 forall (R : Type), datatypeDenote R dt -> (T -> R).
adamc@194 124
adam@465 125 (** 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 126
adamc@219 127 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 128
adamc@219 129 Check hmake.
adamc@219 130 (** %\vspace{-.15in}% [[
adamc@219 131 hmake
adamc@219 132 : forall (A : Type) (B : A -> Type),
adam@358 133 (forall x : A, B x) -> forall ls : list A, hlist B ls
adamc@219 134 ]]
adamc@219 135
adam@358 136 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 137
adamc@194 138 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
adamc@194 139 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
adamc@194 140
adamc@219 141 (** 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 [hlist]-specific version defined in the [DepList] module.
adamc@219 142
adamc@219 143 It is instructive to build [fixDenote] values for our example types and see what specialized [size] functions result from them. *)
adamc@219 144
adamc@194 145 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
adamc@194 146 fun R _ emp => match emp with end.
adamc@194 147 Eval compute in size Empty_set_fix.
adamc@219 148 (** %\vspace{-.15in}% [[
adamc@219 149 = fun emp : Empty_set => match emp return nat with
adamc@219 150 end
adamc@219 151 : Empty_set -> nat
adamc@219 152 ]]
adamc@219 153
adamc@219 154 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 155
adamc@194 156 Definition unit_fix : fixDenote unit unit_dt :=
adamc@216 157 fun R cases _ => (hhd cases) tt INil.
adamc@194 158 Eval compute in size unit_fix.
adamc@219 159 (** %\vspace{-.15in}% [[
adamc@219 160 = fun _ : unit => 1
adamc@219 161 : unit -> nat
adamc@219 162 ]]
adamc@219 163
adamc@219 164 Again normalization gives us the natural function definition. We see this pattern repeated for our other example types. *)
adamc@194 165
adamc@194 166 Definition bool_fix : fixDenote bool bool_dt :=
adamc@194 167 fun R cases b => if b
adamc@216 168 then (hhd cases) tt INil
adamc@216 169 else (hhd (htl cases)) tt INil.
adamc@194 170 Eval compute in size bool_fix.
adamc@219 171 (** %\vspace{-.15in}% [[
adamc@219 172 = fun b : bool => if b then 1 else 1
adamc@219 173 : bool -> nat
adam@302 174 ]]
adam@302 175 *)
adamc@194 176
adamc@194 177 Definition nat_fix : fixDenote nat nat_dt :=
adamc@194 178 fun R cases => fix F (n : nat) : R :=
adamc@194 179 match n with
adamc@216 180 | O => (hhd cases) tt INil
adamc@216 181 | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
adamc@194 182 end.
adamc@219 183
adamc@219 184 (** 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 185
adamc@194 186 Eval cbv beta iota delta -[plus] in size nat_fix.
adamc@219 187 (** %\vspace{-.15in}% [[
adamc@219 188 = fix F (n : nat) : nat := match n with
adamc@219 189 | 0 => 1
adamc@219 190 | S n' => F n' + 1
adamc@219 191 end
adamc@219 192 : nat -> nat
adam@302 193 ]]
adam@302 194 *)
adamc@194 195
adamc@194 196 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
adamc@194 197 fun R cases => fix F (ls : list A) : R :=
adamc@194 198 match ls with
adamc@216 199 | nil => (hhd cases) tt INil
adamc@216 200 | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
adamc@194 201 end.
adamc@194 202 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
adamc@219 203 (** %\vspace{-.15in}% [[
adamc@219 204 = fun A : Type =>
adamc@219 205 fix F (ls : list A) : nat :=
adamc@219 206 match ls with
adamc@219 207 | nil => 1
adamc@219 208 | _ :: ls' => F ls' + 1
adamc@219 209 end
adamc@219 210 : forall A : Type, list A -> nat
adam@302 211 ]]
adam@302 212 *)
adamc@194 213
adamc@194 214 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
adamc@194 215 fun R cases => fix F (t : tree A) : R :=
adamc@194 216 match t with
adamc@216 217 | Leaf x => (hhd cases) x INil
adamc@216 218 | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
adamc@194 219 end.
adamc@194 220 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
adamc@219 221 (** %\vspace{-.15in}% [[
adamc@219 222 = fun A : Type =>
adamc@219 223 fix F (t : tree A) : nat :=
adamc@219 224 match t with
adamc@219 225 | Leaf _ => 1
adamc@219 226 | Node t1 t2 => F t1 + (F t2 + 1)
adamc@219 227 end
adamc@219 228 : forall A : Type, tree A -> n
adam@302 229 ]]
adam@302 230 *)
adamc@198 231 (* end thide *)
adamc@195 232
adam@457 233 (** As our examples show, even recursive datatypes are mapped to normal-looking size functions. *)
adam@457 234
adamc@195 235
adamc@195 236 (** ** Pretty-Printing *)
adamc@195 237
adamc@219 238 (** 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 239
adamc@195 240 Record print_constructor (c : constructor) : Type := PI {
adamc@195 241 printName : string;
adamc@195 242 printNonrec : nonrecursive c -> string
adamc@195 243 }.
adamc@195 244
adamc@219 245 (** 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 246
adamc@195 247 Notation "^" := (PI (Con _ _)).
adamc@195 248
adamc@219 249 (** 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 250
adamc@195 251 Definition print_datatype := hlist print_constructor.
adamc@195 252
adamc@219 253 (** We will be doing some string manipulation here, so we import the notations associated with strings. *)
adamc@219 254
adamc@219 255 Local Open Scope string_scope.
adamc@219 256
adamc@219 257 (** Now it is easy to implement our generic printer, using another function from [DepList.] *)
adamc@219 258
adamc@219 259 Check hmap.
adamc@219 260 (** %\vspace{-.15in}% [[
adamc@219 261 hmap
adamc@219 262 : forall (A : Type) (B1 B2 : A -> Type),
adamc@219 263 (forall x : A, B1 x -> B2 x) ->
adamc@219 264 forall ls : list A, hlist B1 ls -> hlist B2 ls
adam@302 265 ]]
adam@302 266 *)
adamc@195 267
adamc@195 268 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
adamc@195 269 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
adamc@195 270 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
adamc@195 271 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
adamc@195 272
adamc@219 273 (** Some simple tests establish that [print] gets the job done. *)
adamc@219 274
adamc@216 275 Eval compute in print HNil Empty_set_fix.
adamc@219 276 (** %\vspace{-.15in}% [[
adamc@219 277 = fun emp : Empty_set => match emp return string with
adamc@219 278 end
adamc@219 279 : Empty_set -> string
adam@302 280 ]]
adam@302 281 *)
adamc@219 282
adamc@216 283 Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
adamc@219 284 (** %\vspace{-.15in}% [[
adamc@219 285 = fun _ : unit => "tt()"
adamc@219 286 : unit -> string
adam@302 287 ]]
adam@302 288 *)
adamc@219 289
adamc@195 290 Eval compute in print (^ "true" (fun _ => "")
adamc@195 291 ::: ^ "false" (fun _ => "")
adamc@216 292 ::: HNil) bool_fix.
adamc@219 293 (** %\vspace{-.15in}% [[
adamc@219 294 = fun b : bool => if b then "true()" else "false()"
adamc@219 295 : bool -> s
adam@302 296 ]]
adam@302 297 *)
adamc@195 298
adamc@195 299 Definition print_nat := print (^ "O" (fun _ => "")
adamc@195 300 ::: ^ "S" (fun _ => "")
adamc@216 301 ::: HNil) nat_fix.
adamc@195 302 Eval cbv beta iota delta -[append] in print_nat.
adamc@219 303 (** %\vspace{-.15in}% [[
adamc@219 304 = fix F (n : nat) : string :=
adamc@219 305 match n with
adamc@219 306 | 0%nat => "O" ++ "(" ++ "" ++ ")"
adamc@219 307 | S n' => "S" ++ "(" ++ "" ++ ", " ++ F n' ++ ")"
adamc@219 308 end
adamc@219 309 : nat -> string
adam@302 310 ]]
adam@302 311 *)
adamc@219 312
adamc@195 313 Eval simpl in print_nat 0.
adamc@219 314 (** %\vspace{-.15in}% [[
adamc@219 315 = "O()"
adamc@219 316 : string
adam@302 317 ]]
adam@302 318 *)
adamc@219 319
adamc@195 320 Eval simpl in print_nat 1.
adamc@219 321 (** %\vspace{-.15in}% [[
adamc@219 322 = "S(, O())"
adamc@219 323 : string
adam@302 324 ]]
adam@302 325 *)
adamc@219 326
adamc@195 327 Eval simpl in print_nat 2.
adamc@219 328 (** %\vspace{-.15in}% [[
adamc@219 329 = "S(, S(, O()))"
adamc@219 330 : string
adam@302 331 ]]
adam@302 332 *)
adamc@195 333
adamc@195 334 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 335 print (^ "nil" (fun _ => "")
adamc@195 336 ::: ^ "cons" pr
adamc@216 337 ::: HNil) (@list_fix A).
adamc@219 338 (** %\vspace{-.15in}% [[
adamc@219 339 = fun (A : Type) (pr : A -> string) =>
adamc@219 340 fix F (ls : list A) : string :=
adamc@219 341 match ls with
adamc@219 342 | nil => "nil" ++ "(" ++ "" ++ ")"
adamc@219 343 | x :: ls' => "cons" ++ "(" ++ pr x ++ ", " ++ F ls' ++ ")"
adamc@219 344 end
adamc@219 345 : forall A : Type, (A -> string) -> list A -> string
adam@302 346 ]]
adam@302 347 *)
adamc@219 348
adamc@195 349 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 350 print (^ "Leaf" pr
adamc@195 351 ::: ^ "Node" (fun _ => "")
adamc@216 352 ::: HNil) (@tree_fix A).
adamc@219 353 (** %\vspace{-.15in}% [[
adamc@219 354 = fun (A : Type) (pr : A -> string) =>
adamc@219 355 fix F (t : tree A) : string :=
adamc@219 356 match t with
adamc@219 357 | Leaf x => "Leaf" ++ "(" ++ pr x ++ ")"
adamc@219 358 | Node t1 t2 =>
adamc@219 359 "Node" ++ "(" ++ "" ++ ", " ++ F t1 ++ ", " ++ F t2 ++ ")"
adamc@219 360 end
adamc@219 361 : forall A : Type, (A -> string) -> tree A -> string
adam@302 362 ]]
adam@302 363 *)
adamc@196 364
adam@428 365 (* begin hide *)
adam@437 366 (* begin thide *)
adam@428 367 Definition append' := append.
adam@437 368 (* end thide *)
adam@428 369 (* end hide *)
adam@428 370
adam@358 371 (** 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 372
adamc@196 373
adamc@196 374 (** ** Mapping *)
adamc@196 375
adamc@219 376 (** 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 377
adamc@219 378 Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T)
adamc@219 379 : T -> T :=
adamc@196 380 fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
adamc@196 381 (fun _ c x r => f (c x r)) dd).
adamc@196 382
adamc@196 383 Eval compute in map Empty_set_den Empty_set_fix.
adamc@219 384 (** %\vspace{-.15in}% [[
adamc@219 385 = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) =>
adamc@219 386 match emp return Empty_set with
adamc@219 387 end
adamc@219 388 : (Empty_set -> Empty_set) -> Empty_set -> Empty_set
adam@302 389 ]]
adam@302 390 *)
adamc@219 391
adamc@196 392 Eval compute in map unit_den unit_fix.
adamc@219 393 (** %\vspace{-.15in}% [[
adamc@219 394 = fun (f : unit -> unit) (_ : unit) => f tt
adamc@219 395 : (unit -> unit) -> unit -> unit
adam@302 396 ]]
adam@302 397 *)
adamc@219 398
adamc@196 399 Eval compute in map bool_den bool_fix.
adamc@219 400 (** %\vspace{-.15in}% [[
adamc@219 401 = fun (f : bool -> bool) (b : bool) => if b then f true else f false
adamc@219 402 : (bool -> bool) -> bool -> bool
adam@302 403 ]]
adam@302 404 *)
adamc@219 405
adamc@196 406 Eval compute in map nat_den nat_fix.
adamc@219 407 (** %\vspace{-.15in}% [[
adamc@219 408 = fun f : nat -> nat =>
adamc@219 409 fix F (n : nat) : nat :=
adamc@219 410 match n with
adamc@219 411 | 0%nat => f 0%nat
adamc@219 412 | S n' => f (S (F n'))
adamc@219 413 end
adamc@219 414 : (nat -> nat) -> nat -> nat
adam@302 415 ]]
adam@302 416 *)
adamc@219 417
adamc@196 418 Eval compute in fun A => map (list_den A) (@list_fix A).
adamc@219 419 (** %\vspace{-.15in}% [[
adamc@219 420 = fun (A : Type) (f : list A -> list A) =>
adamc@219 421 fix F (ls : list A) : list A :=
adamc@219 422 match ls with
adamc@219 423 | nil => f nil
adamc@219 424 | x :: ls' => f (x :: F ls')
adamc@219 425 end
adamc@219 426 : forall A : Type, (list A -> list A) -> list A -> list A
adam@302 427 ]]
adam@302 428 *)
adamc@219 429
adamc@196 430 Eval compute in fun A => map (tree_den A) (@tree_fix A).
adamc@219 431 (** %\vspace{-.15in}% [[
adamc@219 432 = fun (A : Type) (f : tree A -> tree A) =>
adamc@219 433 fix F (t : tree A) : tree A :=
adamc@219 434 match t with
adamc@219 435 | Leaf x => f (Leaf x)
adamc@219 436 | Node t1 t2 => f (Node (F t1) (F t2))
adamc@219 437 end
adamc@219 438 : forall A : Type, (tree A -> tree A) -> tree A -> tree A
adam@302 439 ]]
adam@302 440 *)
adamc@196 441
adam@358 442 (** 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 443
adamc@196 444 Definition map_nat := map nat_den nat_fix.
adamc@196 445 Eval simpl in map_nat S 0.
adamc@219 446 (** %\vspace{-.15in}% [[
adamc@219 447 = 1%nat
adamc@219 448 : nat
adam@302 449 ]]
adam@302 450 *)
adamc@219 451
adamc@196 452 Eval simpl in map_nat S 1.
adamc@219 453 (** %\vspace{-.15in}% [[
adamc@219 454 = 3%nat
adamc@219 455 : nat
adam@302 456 ]]
adam@302 457 *)
adamc@219 458
adamc@196 459 Eval simpl in map_nat S 2.
adamc@219 460 (** %\vspace{-.15in}% [[
adamc@219 461 = 5%nat
adamc@219 462 : nat
adam@302 463 ]]
adam@302 464 *)
adamc@196 465
adam@358 466 (** 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 467
adamc@196 468
adamc@196 469 (** * Proving Theorems about Recursive Definitions *)
adamc@196 470
adamc@219 471 (** 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 472
adamc@196 473 Section ok.
adamc@196 474 Variable T : Type.
adamc@196 475 Variable dt : datatype.
adamc@196 476
adamc@196 477 Variable dd : datatypeDenote T dt.
adamc@196 478 Variable fx : fixDenote T dt.
adamc@196 479
adamc@219 480 (** 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 481
adamc@196 482 Definition datatypeDenoteOk :=
adamc@196 483 forall P : T -> Prop,
adamc@196 484 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@215 485 (forall i : fin (recursive c), P (get r i))
adamc@196 486 -> P ((hget dd m) x r))
adamc@196 487 -> forall v, P v.
adamc@196 488
adam@408 489 (** 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 490
adamc@219 491 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 492
adamc@196 493 Definition fixDenoteOk :=
adamc@196 494 forall (R : Type) (cases : datatypeDenote R dt)
adamc@196 495 c (m : member c dt)
adamc@196 496 (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@216 497 fx cases ((hget dd m) x r)
adamc@216 498 = (hget cases m) x (imap (fx cases) r).
adamc@219 499
adamc@219 500 (** 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 501
adamc@196 502 End ok.
adamc@196 503
adamc@219 504 (** 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 505
adam@359 506 (* begin thide *)
adamc@196 507 Lemma foldr_plus : forall n (ils : ilist nat n),
adamc@196 508 foldr plus 1 ils > 0.
adamc@216 509 induction ils; crush.
adamc@196 510 Qed.
adamc@198 511 (* end thide *)
adamc@196 512
adamc@197 513 Theorem size_positive : forall T dt
adamc@197 514 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197 515 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@196 516 (v : T),
adamc@196 517 size fx v > 0.
adamc@198 518 (* begin thide *)
adamc@219 519 unfold size; intros.
adamc@219 520 (** [[
adamc@219 521 ============================
adamc@219 522 fx nat
adamc@219 523 (hmake
adamc@219 524 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 525 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0
adamc@219 526 ]]
adamc@219 527
adamc@219 528 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 529 [[
adamc@219 530 apply dok.
adam@358 531 ]]
adam@358 532 %\vspace{-.3in}%
adam@358 533 <<
adamc@219 534 Error: Impossible to unify "datatypeDenoteOk dd" with
adamc@219 535 "fx nat
adamc@219 536 (hmake
adamc@219 537 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 538 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0".
adam@358 539 >>
adamc@219 540
adam@360 541 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 542
adamc@219 543 pattern v.
adam@358 544 (** %\vspace{-.15in}%[[
adamc@219 545 ============================
adamc@219 546 (fun t : T =>
adamc@219 547 fx nat
adamc@219 548 (hmake
adamc@219 549 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 550 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) t > 0) v
adam@302 551 ]]
adam@302 552 *)
adamc@219 553
adamc@219 554 apply dok; crush.
adam@358 555 (** %\vspace{-.15in}%[[
adamc@219 556 H : forall i : fin (recursive c),
adamc@219 557 fx nat
adamc@219 558 (hmake
adamc@219 559 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 560 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt)
adamc@219 561 (get r i) > 0
adamc@219 562 ============================
adamc@219 563 hget
adamc@219 564 (hmake
adamc@219 565 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 566 (r0 : ilist nat (recursive x0)) => foldr plus 1%nat r0) dt) m x
adamc@219 567 (imap
adamc@219 568 (fx nat
adamc@219 569 (hmake
adamc@219 570 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 571 (r0 : ilist nat (recursive x0)) =>
adamc@219 572 foldr plus 1%nat r0) dt)) r) > 0
adamc@219 573 ]]
adamc@219 574
adamc@219 575 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 576
adamc@219 577 rewrite hget_hmake.
adam@358 578 (** %\vspace{-.15in}%[[
adamc@219 579 ============================
adamc@219 580 foldr plus 1%nat
adamc@219 581 (imap
adamc@219 582 (fx nat
adamc@219 583 (hmake
adamc@219 584 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 585 (r0 : ilist nat (recursive x0)) =>
adamc@219 586 foldr plus 1%nat r0) dt)) r) > 0
adamc@219 587 ]]
adamc@219 588
adamc@219 589 The lemma we proved earlier finishes the proof. *)
adamc@219 590
adamc@219 591 apply foldr_plus.
adamc@219 592
adamc@219 593 (** Using hints, we can redo this proof in a nice automated form. *)
adamc@219 594
adamc@219 595 Restart.
adamc@219 596
adam@375 597 Hint Rewrite hget_hmake.
adamc@196 598 Hint Resolve foldr_plus.
adamc@196 599
adamc@197 600 unfold size; intros; pattern v; apply dok; crush.
adamc@196 601 Qed.
adamc@198 602 (* end thide *)
adamc@197 603
adamc@219 604 (** 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 605
adamc@219 606 In particular, it ought to be the case that generic [map] applied to an identity function is itself an identity function. *)
adamc@219 607
adamc@197 608 Theorem map_id : forall T dt
adamc@197 609 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197 610 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@197 611 (v : T),
adamc@197 612 map dd fx (fun x => x) v = v.
adamc@198 613 (* begin thide *)
adamc@219 614 (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *)
adamc@219 615
adam@375 616 Hint Rewrite hget_hmap.
adamc@197 617
adamc@197 618 unfold map; intros; pattern v; apply dok; crush.
adam@358 619 (** %\vspace{-.15in}%[[
adamc@219 620 H : forall i : fin (recursive c),
adamc@219 621 fx T
adamc@219 622 (hmap
adamc@219 623 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 624 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 625 c x0 r) dd) (get r i) = get r i
adamc@219 626 ============================
adamc@219 627 hget dd m x
adamc@219 628 (imap
adamc@219 629 (fx T
adamc@219 630 (hmap
adamc@219 631 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 632 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 633 c0 x1 r0) dd)) r) = hget dd m x r
adamc@219 634 ]]
adamc@197 635
adamc@219 636 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 637
adamc@197 638 f_equal.
adam@358 639 (** %\vspace{-.15in}%[[
adamc@219 640 ============================
adamc@219 641 imap
adamc@219 642 (fx T
adamc@219 643 (hmap
adamc@219 644 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 645 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 646 c0 x1 r0) dd)) r = r
adamc@219 647 ]]
adamc@219 648
adamc@219 649 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 650
adamc@219 651 induction r; crush.
adamc@219 652
adam@428 653 (* begin hide *)
adam@437 654 (* begin thide *)
adam@428 655 Definition pred' := pred.
adam@437 656 (* end thide *)
adam@428 657 (* end hide *)
adam@428 658
adamc@219 659 (** 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 [IHn] is the inner IH (for induction over the recursive arguments).
adamc@219 660 [[
adamc@219 661 H : forall i : fin (S n),
adamc@219 662 fx T
adamc@219 663 (hmap
adamc@219 664 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 665 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 666 c x0 r) dd)
adamc@219 667 (match i in (fin n') return ((fin (pred n') -> T) -> T) with
adamc@219 668 | First n => fun _ : fin n -> T => a
adamc@219 669 | Next n idx' => fun get_ls' : fin n -> T => get_ls' idx'
adamc@219 670 end (get r)) =
adamc@219 671 match i in (fin n') return ((fin (pred n') -> T) -> T) with
adamc@219 672 | First n => fun _ : fin n -> T => a
adamc@219 673 | Next n idx' => fun get_ls' : fin n -> T => get_ls' idx'
adamc@219 674 end (get r)
adamc@219 675 IHr : (forall i : fin n,
adamc@219 676 fx T
adamc@219 677 (hmap
adamc@219 678 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 679 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 680 c x0 r) dd) (get r i) = get r i) ->
adamc@219 681 imap
adamc@219 682 (fx T
adamc@219 683 (hmap
adamc@219 684 (fun (x : constructor) (c : constructorDenote T x)
adamc@219 685 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
adamc@219 686 c x0 r) dd)) r = r
adamc@219 687 ============================
adamc@219 688 ICons
adamc@219 689 (fx T
adamc@219 690 (hmap
adamc@219 691 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 692 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 693 c0 x1 r0) dd) a)
adamc@219 694 (imap
adamc@219 695 (fx T
adamc@219 696 (hmap
adamc@219 697 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 698 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 699 c0 x1 r0) dd)) r) = ICons a r
adamc@219 700 ]]
adamc@219 701
adamc@219 702 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 703
adamc@219 704 f_equal.
adamc@219 705 apply (H First).
adam@358 706 (** %\vspace{-.15in}%[[
adamc@219 707 ============================
adamc@219 708 imap
adamc@219 709 (fx T
adamc@219 710 (hmap
adamc@219 711 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 712 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 713 c0 x1 r0) dd)) r = r
adamc@219 714 ]]
adamc@219 715
adamc@219 716 Now the goal matches the inner IH [IHr]. *)
adamc@219 717
adamc@219 718 apply IHr; crush.
adam@358 719 (** %\vspace{-.15in}%[[
adamc@219 720 i : fin n
adamc@219 721 ============================
adamc@219 722 fx T
adamc@219 723 (hmap
adamc@219 724 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 725 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 726 c0 x1 r0) dd) (get r i) = get r i
adamc@219 727 ]]
adamc@219 728
adamc@219 729 We can finish the proof by applying the outer IH again, specialized to a different [fin] value. *)
adamc@219 730
adamc@216 731 apply (H (Next i)).
adamc@197 732 Qed.
adamc@198 733 (* end thide *)
adam@358 734
adam@358 735 (** The proof involves complex subgoals, but, still, few steps are required, and then we may reuse our work across a variety of datatypes. *)