Mercurial > cpdt > repo

annotate src/Generic.v @ 552:c8d01fb69970

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