Mercurial > cpdt > repo

annotate src/Generic.v @ 345:518c8994a715

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
One more axiom avoidance example
author Adam Chlipala <adam@chlipala.net>
date Wed, 19 Oct 2011 10:00:07 -0400
parents d5787b70cf48
children ad315efc3b6b
rev   line source
adam@286 1 (* Copyright (c) 2008-2010, 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
adamc@193 18
adamc@219 19 (** %\chapter{Generic Programming}% *)
adamc@193 20
adam@286 21 (** %\textit{%#<i>#Generic programming#</i>#%}% makes it possible to write functions that operate over different types of data. Parametric polymorphism in ML and Haskell is one of the simplest examples. ML-style module systems and Haskell type classes 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 [deriving] clause, 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 datatype-generic programming much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support.
adamc@193 22
adamc@219 23 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 24
adamc@195 25 (** * Reflecting Datatype Definitions *)
adamc@193 26
adamc@219 27 (** The key to generic programming with dependent types is %\textit{%#<i>#universe types#</i>#%}%. This concept should not be confused with the idea of %\textit{%#<i>#universes#</i>#%}% from the metatheory of CIC and related languages. Rather, the idea of universe types is to define inductive types that provide %\textit{%#<i>#syntactic representations#</i>#%}% of Coq types. We cannot directly write CIC programs that do case analysis on types, but we %\textit{%#<i>#can#</i>#%}% case analyze on reflected syntactic versions of those types.
adamc@219 28
adamc@219 29 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 30
adamc@219 31 The first step is to define a representation for constructors of our datatypes. *)
adamc@219 32
adamc@198 33 (* EX: Define a reflected representation of simple algebraic datatypes. *)
adamc@198 34
adamc@198 35 (* begin thide *)
adamc@193 36 Record constructor : Type := Con {
adamc@193 37 nonrecursive : Type;
adamc@193 38 recursive : nat
adamc@193 39 }.
adamc@193 40
adam@286 41 (** 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 42
adamc@219 43 With this definition, it as easy to define a datatype representation in terms of lists of constructors. *)
adamc@219 44
adamc@193 45 Definition datatype := list constructor.
adamc@193 46
adamc@219 47 (** 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 48
adamc@193 49 Definition Empty_set_dt : datatype := nil.
adamc@193 50 Definition unit_dt : datatype := Con unit 0 :: nil.
adamc@193 51 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
adamc@193 52 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
adamc@193 53 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
adamc@219 54
adamc@219 55 (** [Empty_set] has no constructors, so its representation is the empty list. [unit] has one constructor with no arguments, so its one reflected 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 56
adamc@219 57 As a further example, we can do the same encoding for a generic binary tree type. *)
adamc@219 58
adamc@198 59 (* end thide *)
adamc@193 60
adamc@193 61 Section tree.
adamc@193 62 Variable A : Type.
adamc@193 63
adamc@193 64 Inductive tree : Type :=
adamc@193 65 | Leaf : A -> tree
adamc@193 66 | Node : tree -> tree -> tree.
adamc@193 67 End tree.
adamc@193 68
adamc@198 69 (* begin thide *)
adamc@193 70 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
adamc@193 71
adamc@219 72 (** 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 %\textit{%#<i>#evidence#</i>#%}% that the datatype is compatible with the encoding. *)
adamc@219 73
adamc@193 74 Section denote.
adamc@193 75 Variable T : Type.
adamc@219 76 (** This variable stands for the concrete datatype that we are interested in. *)
adamc@193 77
adamc@193 78 Definition constructorDenote (c : constructor) :=
adamc@193 79 nonrecursive c -> ilist T (recursive c) -> T.
adamc@219 80 (** 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 [ilist] that we met in Chapter 7. *)
adamc@193 81
adamc@193 82 Definition datatypeDenote := hlist constructorDenote.
adam@286 83 (** Finally, the evidence for type [T] is a 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 84
adamc@193 85 End denote.
adamc@198 86 (* end thide *)
adamc@193 87
adamc@219 88 (** 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 89
adamc@219 90 (** printing ~> $\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
adamc@195 112
adamc@195 113 (** * Recursive Definitions *)
adamc@195 114
adamc@198 115 (* EX: Define a generic [size] function. *)
adamc@198 116
adamc@219 117 (** We built these encodings of datatypes to help us write datatype-generic recursive functions. To do so, we will want a reflected representation of a %\textit{%#<i>#recursion scheme#</i>#%}% 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
adamc@219 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 hetergeneous 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 reflected 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),
adamc@219 131 (forall x : A, B x) -> forall ls : list A, hlist B l
adamc@219 132
adamc@219 133 ]]
adamc@219 134
adamc@219 135 [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 which counts the number of constructors used to build a value in a datatype. *)
adamc@219 136
adamc@194 137 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
adamc@194 138 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
adamc@194 139
adamc@219 140 (** 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 141
adamc@219 142 It is instructive to build [fixDenote] values for our example types and see what specialized [size] functions result from them. *)
adamc@219 143
adamc@194 144 Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
adamc@194 145 fun R _ emp => match emp with end.
adamc@194 146 Eval compute in size Empty_set_fix.
adamc@219 147 (** %\vspace{-.15in}% [[
adamc@219 148 = fun emp : Empty_set => match emp return nat with
adamc@219 149 end
adamc@219 150 : Empty_set -> nat
adamc@219 151
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
adamc@219 165 Again normalization gives us the natural function definition. We see this pattern repeated for our other example types. *)
adamc@194 166
adamc@194 167 Definition bool_fix : fixDenote bool bool_dt :=
adamc@194 168 fun R cases b => if b
adamc@216 169 then (hhd cases) tt INil
adamc@216 170 else (hhd (htl cases)) tt INil.
adamc@194 171 Eval compute in size bool_fix.
adamc@219 172 (** %\vspace{-.15in}% [[
adamc@219 173 = fun b : bool => if b then 1 else 1
adamc@219 174 : bool -> nat
adam@302 175 ]]
adam@302 176 *)
adamc@194 177
adamc@194 178 Definition nat_fix : fixDenote nat nat_dt :=
adamc@194 179 fun R cases => fix F (n : nat) : R :=
adamc@194 180 match n with
adamc@216 181 | O => (hhd cases) tt INil
adamc@216 182 | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
adamc@194 183 end.
adamc@219 184
adamc@219 185 (** 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 186
adamc@194 187 Eval cbv beta iota delta -[plus] in size nat_fix.
adamc@219 188 (** %\vspace{-.15in}% [[
adamc@219 189 = fix F (n : nat) : nat := match n with
adamc@219 190 | 0 => 1
adamc@219 191 | S n' => F n' + 1
adamc@219 192 end
adamc@219 193 : nat -> nat
adam@302 194 ]]
adam@302 195 *)
adamc@194 196
adamc@194 197 Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
adamc@194 198 fun R cases => fix F (ls : list A) : R :=
adamc@194 199 match ls with
adamc@216 200 | nil => (hhd cases) tt INil
adamc@216 201 | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
adamc@194 202 end.
adamc@194 203 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
adamc@219 204 (** %\vspace{-.15in}% [[
adamc@219 205 = fun A : Type =>
adamc@219 206 fix F (ls : list A) : nat :=
adamc@219 207 match ls with
adamc@219 208 | nil => 1
adamc@219 209 | _ :: ls' => F ls' + 1
adamc@219 210 end
adamc@219 211 : forall A : Type, list A -> nat
adam@302 212 ]]
adam@302 213 *)
adamc@194 214
adamc@194 215 Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
adamc@194 216 fun R cases => fix F (t : tree A) : R :=
adamc@194 217 match t with
adamc@216 218 | Leaf x => (hhd cases) x INil
adamc@216 219 | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
adamc@194 220 end.
adamc@194 221 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
adamc@219 222 (** %\vspace{-.15in}% [[
adamc@219 223 = fun A : Type =>
adamc@219 224 fix F (t : tree A) : nat :=
adamc@219 225 match t with
adamc@219 226 | Leaf _ => 1
adamc@219 227 | Node t1 t2 => F t1 + (F t2 + 1)
adamc@219 228 end
adamc@219 229 : forall A : Type, tree A -> n
adam@302 230 ]]
adam@302 231 *)
adamc@198 232 (* end thide *)
adamc@195 233
adamc@195 234
adamc@195 235 (** ** Pretty-Printing *)
adamc@195 236
adamc@198 237 (* EX: Define a generic pretty-printing function. *)
adamc@198 238
adamc@219 239 (** 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 240
adamc@198 241 (* begin thide *)
adamc@195 242 Record print_constructor (c : constructor) : Type := PI {
adamc@195 243 printName : string;
adamc@195 244 printNonrec : nonrecursive c -> string
adamc@195 245 }.
adamc@195 246
adamc@219 247 (** 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 248
adamc@195 249 Notation "^" := (PI (Con _ _)).
adamc@195 250
adamc@219 251 (** 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 252
adamc@195 253 Definition print_datatype := hlist print_constructor.
adamc@195 254
adamc@219 255 (** We will be doing some string manipulation here, so we import the notations associated with strings. *)
adamc@219 256
adamc@219 257 Local Open Scope string_scope.
adamc@219 258
adamc@219 259 (** Now it is easy to implement our generic printer, using another function from [DepList.] *)
adamc@219 260
adamc@219 261 Check hmap.
adamc@219 262 (** %\vspace{-.15in}% [[
adamc@219 263 hmap
adamc@219 264 : forall (A : Type) (B1 B2 : A -> Type),
adamc@219 265 (forall x : A, B1 x -> B2 x) ->
adamc@219 266 forall ls : list A, hlist B1 ls -> hlist B2 ls
adam@302 267 ]]
adam@302 268 *)
adamc@195 269
adamc@195 270 Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
adamc@195 271 fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
adamc@195 272 (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
adamc@195 273 ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
adamc@198 274 (* end thide *)
adamc@195 275
adamc@219 276 (** Some simple tests establish that [print] gets the job done. *)
adamc@219 277
adamc@216 278 Eval compute in print HNil Empty_set_fix.
adamc@219 279 (** %\vspace{-.15in}% [[
adamc@219 280 = fun emp : Empty_set => match emp return string with
adamc@219 281 end
adamc@219 282 : Empty_set -> string
adam@302 283 ]]
adam@302 284 *)
adamc@219 285
adamc@216 286 Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
adamc@219 287 (** %\vspace{-.15in}% [[
adamc@219 288 = fun _ : unit => "tt()"
adamc@219 289 : unit -> string
adam@302 290 ]]
adam@302 291 *)
adamc@219 292
adamc@195 293 Eval compute in print (^ "true" (fun _ => "")
adamc@195 294 ::: ^ "false" (fun _ => "")
adamc@216 295 ::: HNil) bool_fix.
adamc@219 296 (** %\vspace{-.15in}% [[
adamc@219 297 = fun b : bool => if b then "true()" else "false()"
adamc@219 298 : bool -> s
adam@302 299 ]]
adam@302 300 *)
adamc@195 301
adamc@195 302 Definition print_nat := print (^ "O" (fun _ => "")
adamc@195 303 ::: ^ "S" (fun _ => "")
adamc@216 304 ::: HNil) nat_fix.
adamc@195 305 Eval cbv beta iota delta -[append] in print_nat.
adamc@219 306 (** %\vspace{-.15in}% [[
adamc@219 307 = fix F (n : nat) : string :=
adamc@219 308 match n with
adamc@219 309 | 0%nat => "O" ++ "(" ++ "" ++ ")"
adamc@219 310 | S n' => "S" ++ "(" ++ "" ++ ", " ++ F n' ++ ")"
adamc@219 311 end
adamc@219 312 : nat -> string
adam@302 313 ]]
adam@302 314 *)
adamc@219 315
adamc@195 316 Eval simpl in print_nat 0.
adamc@219 317 (** %\vspace{-.15in}% [[
adamc@219 318 = "O()"
adamc@219 319 : string
adam@302 320 ]]
adam@302 321 *)
adamc@219 322
adamc@195 323 Eval simpl in print_nat 1.
adamc@219 324 (** %\vspace{-.15in}% [[
adamc@219 325 = "S(, O())"
adamc@219 326 : string
adam@302 327 ]]
adam@302 328 *)
adamc@219 329
adamc@195 330 Eval simpl in print_nat 2.
adamc@219 331 (** %\vspace{-.15in}% [[
adamc@219 332 = "S(, S(, O()))"
adamc@219 333 : string
adam@302 334 ]]
adam@302 335 *)
adamc@195 336
adamc@195 337 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 338 print (^ "nil" (fun _ => "")
adamc@195 339 ::: ^ "cons" pr
adamc@216 340 ::: HNil) (@list_fix A).
adamc@219 341 (** %\vspace{-.15in}% [[
adamc@219 342 = fun (A : Type) (pr : A -> string) =>
adamc@219 343 fix F (ls : list A) : string :=
adamc@219 344 match ls with
adamc@219 345 | nil => "nil" ++ "(" ++ "" ++ ")"
adamc@219 346 | x :: ls' => "cons" ++ "(" ++ pr x ++ ", " ++ F ls' ++ ")"
adamc@219 347 end
adamc@219 348 : forall A : Type, (A -> string) -> list A -> string
adam@302 349 ]]
adam@302 350 *)
adamc@219 351
adamc@195 352 Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
adamc@195 353 print (^ "Leaf" pr
adamc@195 354 ::: ^ "Node" (fun _ => "")
adamc@216 355 ::: HNil) (@tree_fix A).
adamc@219 356 (** %\vspace{-.15in}% [[
adamc@219 357 = fun (A : Type) (pr : A -> string) =>
adamc@219 358 fix F (t : tree A) : string :=
adamc@219 359 match t with
adamc@219 360 | Leaf x => "Leaf" ++ "(" ++ pr x ++ ")"
adamc@219 361 | Node t1 t2 =>
adamc@219 362 "Node" ++ "(" ++ "" ++ ", " ++ F t1 ++ ", " ++ F t2 ++ ")"
adamc@219 363 end
adamc@219 364 : forall A : Type, (A -> string) -> tree A -> string
adam@302 365 ]]
adam@302 366 *)
adamc@196 367
adamc@196 368
adamc@196 369 (** ** Mapping *)
adamc@196 370
adamc@198 371 (* EX: Define a generic [map] function. *)
adamc@198 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@198 375 (* begin thide *)
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@198 380 (* end thide *)
adamc@196 381
adamc@196 382 Eval compute in map Empty_set_den Empty_set_fix.
adamc@219 383 (** %\vspace{-.15in}% [[
adamc@219 384 = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) =>
adamc@219 385 match emp return Empty_set with
adamc@219 386 end
adamc@219 387 : (Empty_set -> Empty_set) -> Empty_set -> Empty_set
adam@302 388 ]]
adam@302 389 *)
adamc@219 390
adamc@196 391 Eval compute in map unit_den unit_fix.
adamc@219 392 (** %\vspace{-.15in}% [[
adamc@219 393 = fun (f : unit -> unit) (_ : unit) => f tt
adamc@219 394 : (unit -> unit) -> unit -> unit
adam@302 395 ]]
adam@302 396 *)
adamc@219 397
adamc@196 398 Eval compute in map bool_den bool_fix.
adamc@219 399 (** %\vspace{-.15in}% [[
adamc@219 400 = fun (f : bool -> bool) (b : bool) => if b then f true else f false
adamc@219 401 : (bool -> bool) -> bool -> bool
adam@302 402 ]]
adam@302 403 *)
adamc@219 404
adamc@196 405 Eval compute in map nat_den nat_fix.
adamc@219 406 (** %\vspace{-.15in}% [[
adamc@219 407 = fun f : nat -> nat =>
adamc@219 408 fix F (n : nat) : nat :=
adamc@219 409 match n with
adamc@219 410 | 0%nat => f 0%nat
adamc@219 411 | S n' => f (S (F n'))
adamc@219 412 end
adamc@219 413 : (nat -> nat) -> nat -> nat
adam@302 414 ]]
adam@302 415 *)
adamc@219 416
adamc@196 417 Eval compute in fun A => map (list_den A) (@list_fix A).
adamc@219 418 (** %\vspace{-.15in}% [[
adamc@219 419 = fun (A : Type) (f : list A -> list A) =>
adamc@219 420 fix F (ls : list A) : list A :=
adamc@219 421 match ls with
adamc@219 422 | nil => f nil
adamc@219 423 | x :: ls' => f (x :: F ls')
adamc@219 424 end
adamc@219 425 : forall A : Type, (list A -> list A) -> list A -> list A
adam@302 426 ]]
adam@302 427 *)
adamc@219 428
adamc@196 429 Eval compute in fun A => map (tree_den A) (@tree_fix A).
adamc@219 430 (** %\vspace{-.15in}% [[
adamc@219 431 = fun (A : Type) (f : tree A -> tree A) =>
adamc@219 432 fix F (t : tree A) : tree A :=
adamc@219 433 match t with
adamc@219 434 | Leaf x => f (Leaf x)
adamc@219 435 | Node t1 t2 => f (Node (F t1) (F t2))
adamc@219 436 end
adamc@219 437 : forall A : Type, (tree A -> tree A) -> tree A -> tree A
adam@302 438 ]]
adam@302 439 *)
adamc@196 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
adamc@196 463
adamc@196 464 (** * Proving Theorems about Recursive Definitions *)
adamc@196 465
adamc@219 466 (** 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 467
adamc@198 468 (* begin thide *)
adamc@196 469 Section ok.
adamc@196 470 Variable T : Type.
adamc@196 471 Variable dt : datatype.
adamc@196 472
adamc@196 473 Variable dd : datatypeDenote T dt.
adamc@196 474 Variable fx : fixDenote T dt.
adamc@196 475
adamc@219 476 (** 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 477
adamc@196 478 Definition datatypeDenoteOk :=
adamc@196 479 forall P : T -> Prop,
adamc@196 480 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@215 481 (forall i : fin (recursive c), P (get r i))
adamc@196 482 -> P ((hget dd m) x r))
adamc@196 483 -> forall v, P v.
adamc@196 484
adamc@219 485 (** 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 486
adamc@219 487 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 488
adamc@196 489 Definition fixDenoteOk :=
adamc@196 490 forall (R : Type) (cases : datatypeDenote R dt)
adamc@196 491 c (m : member c dt)
adamc@196 492 (x : nonrecursive c) (r : ilist T (recursive c)),
adamc@216 493 fx cases ((hget dd m) x r)
adamc@216 494 = (hget cases m) x (imap (fx cases) r).
adamc@219 495
adamc@219 496 (** 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 497
adamc@196 498 End ok.
adamc@196 499
adamc@219 500 (** 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 501
adamc@196 502 Lemma foldr_plus : forall n (ils : ilist nat n),
adamc@196 503 foldr plus 1 ils > 0.
adamc@216 504 induction ils; crush.
adamc@196 505 Qed.
adamc@198 506 (* end thide *)
adamc@196 507
adamc@197 508 Theorem size_positive : forall T dt
adamc@197 509 (dd : datatypeDenote T dt) (fx : fixDenote T dt)
adamc@197 510 (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
adamc@196 511 (v : T),
adamc@196 512 size fx v > 0.
adamc@198 513 (* begin thide *)
adamc@219 514 unfold size; intros.
adamc@219 515 (** [[
adamc@219 516 ============================
adamc@219 517 fx nat
adamc@219 518 (hmake
adamc@219 519 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 520 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0
adamc@219 521
adamc@219 522 ]]
adamc@219 523
adamc@219 524 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 525
adamc@219 526 [[
adamc@219 527 apply dok.
adamc@219 528
adamc@219 529 Error: Impossible to unify "datatypeDenoteOk dd" with
adamc@219 530 "fx nat
adamc@219 531 (hmake
adamc@219 532 (fun (x : constructor) (_ : nonrecursive x)
adamc@219 533 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0".
adamc@219 534
adamc@219 535 ]]
adamc@219 536
adamc@219 537 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 [pattern] tactic to get our goal into a form that makes it apparent exactly what the induction hypothesis is. *)
adamc@219 538
adamc@219 539 pattern v.
adamc@219 540
adamc@219 541 (** [[
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
adamc@219 548
adam@302 549 ]]
adam@302 550 *)
adamc@219 551
adamc@219 552 apply dok; crush.
adamc@219 553 (** [[
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
adamc@219 574 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 575
adamc@219 576 rewrite hget_hmake.
adamc@219 577 (** [[
adamc@219 578 ============================
adamc@219 579 foldr plus 1%nat
adamc@219 580 (imap
adamc@219 581 (fx nat
adamc@219 582 (hmake
adamc@219 583 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 584 (r0 : ilist nat (recursive x0)) =>
adamc@219 585 foldr plus 1%nat r0) dt)) r) > 0
adamc@219 586
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
adamc@196 597 Hint Rewrite hget_hmake : cpdt.
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
adamc@197 616 Hint Rewrite hget_hmap : cpdt.
adamc@197 617
adamc@197 618 unfold map; intros; pattern v; apply dok; crush.
adamc@219 619 (** [[
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@219 635 ]]
adamc@197 636
adamc@219 637 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 638
adamc@197 639 f_equal.
adamc@219 640 (** [[
adamc@219 641 ============================
adamc@219 642 imap
adamc@219 643 (fx T
adamc@219 644 (hmap
adamc@219 645 (fun (x0 : constructor) (c0 : constructorDenote T x0)
adamc@219 646 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
adamc@219 647 c0 x1 r0) dd)) r = r
adamc@219 648
adamc@219 649 ]]
adamc@219 650
adamc@219 651 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 652
adamc@219 653 induction r; crush.
adamc@219 654
adamc@219 655 (** 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 656
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
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).
adamc@219 704 (** [[
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
adamc@219 715 Now the goal matches the inner IH [IHr]. *)
adamc@219 716
adamc@219 717 apply IHr; crush.
adamc@219 718
adamc@219 719 (** [[
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
adamc@219 730 We can finish the proof by applying the outer IH again, specialized to a different [fin] value. *)
adamc@219 731
adamc@216 732 apply (H (Next i)).
adamc@197 733 Qed.
adamc@198 734 (* end thide *)