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

(* begin hide *)
Adam Chlipala's avatar
Adam Chlipala committed
11
Require Import String List.
Adam Chlipala's avatar
Adam Chlipala committed
12 13 14 15 16 17 18

Require Import Tactics DepList.

Set Implicit Arguments.
(* end hide *)


Adam Chlipala's avatar
Adam Chlipala committed
19
(** %\chapter{Generic Programming}% *)
Adam Chlipala's avatar
Adam Chlipala committed
20

Adam Chlipala's avatar
Adam Chlipala committed
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 so 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.
Adam Chlipala's avatar
Adam Chlipala committed
22

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

Adam Chlipala's avatar
Adam Chlipala committed
25
(** * Reflecting Datatype Definitions *)
Adam Chlipala's avatar
Adam Chlipala committed
26

Adam Chlipala's avatar
Adam Chlipala committed
27 28 29 30 31 32
(** 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.

   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.

   The first step is to define a representation for constructors of our datatypes. *)

Adam Chlipala's avatar
Adam Chlipala committed
33 34 35
(* EX: Define a reflected representation of simple algebraic datatypes. *)

(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
36 37 38 39 40
Record constructor : Type := Con {
  nonrecursive : Type;
  recursive : nat
}.

Adam Chlipala's avatar
Adam Chlipala committed
41 42 43 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 generalizer to any number of arguments via tupling.

   With this definition, it as easy to define a datatype representation in terms of lists of constructors. *)

Adam Chlipala's avatar
Adam Chlipala committed
45 46
Definition datatype := list constructor.

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

Adam Chlipala's avatar
Adam Chlipala committed
49 50 51 52 53
Definition Empty_set_dt : datatype := nil.
Definition unit_dt : datatype := Con unit 0 :: nil.
Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
Adam Chlipala's avatar
Adam Chlipala committed
54 55 56 57 58

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

   As a further example, we can do the same encoding for a generic binary tree type. *)

Adam Chlipala's avatar
Adam Chlipala committed
59
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
60 61 62 63 64 65 66 67 68

Section tree.
  Variable A : Type.

  Inductive tree : Type :=
  | Leaf : A -> tree
  | Node : tree -> tree -> tree.
End tree.

Adam Chlipala's avatar
Adam Chlipala committed
69
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
70 71
Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.

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

Adam Chlipala's avatar
Adam Chlipala committed
74 75
Section denote.
  Variable T : Type.
Adam Chlipala's avatar
Adam Chlipala committed
76
  (** This variable stands for the concrete datatype that we are interested in. *)
Adam Chlipala's avatar
Adam Chlipala committed
77 78 79

  Definition constructorDenote (c : constructor) :=
    nonrecursive c -> ilist T (recursive c) -> T.
Adam Chlipala's avatar
Adam Chlipala committed
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. *)
Adam Chlipala's avatar
Adam Chlipala committed
81 82

  Definition datatypeDenote := hlist constructorDenote.
Adam Chlipala's avatar
Adam Chlipala committed
83 84
  (** Finally, the evidence for type [T] is a hetergeneous 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]. *)

Adam Chlipala's avatar
Adam Chlipala committed
85
End denote.
Adam Chlipala's avatar
Adam Chlipala committed
86
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
87

Adam Chlipala's avatar
Adam Chlipala committed
88 89 90 91
(** 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$.% *)

(** printing ~> $\leadsto$ *)

Adam Chlipala's avatar
Adam Chlipala committed
92 93
Notation "[ ! , ! ~> x ]" := ((fun _ _ => x) : constructorDenote _ (Con _ _)).
Notation "[ v , ! ~> x ]" := ((fun v _ => x) : constructorDenote _ (Con _ _)).
Adam Chlipala's avatar
Adam Chlipala committed
94 95
Notation "[ ! , r ~> x ]" := ((fun _ r => x) : constructorDenote _ (Con _ _)).
Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)).
Adam Chlipala's avatar
Adam Chlipala committed
96

Adam Chlipala's avatar
Adam Chlipala committed
97
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
98
Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
99
  HNil.
Adam Chlipala's avatar
Adam Chlipala committed
100
Definition unit_den : datatypeDenote unit unit_dt :=
101
  [!, ! ~> tt] ::: HNil.
Adam Chlipala's avatar
Adam Chlipala committed
102
Definition bool_den : datatypeDenote bool bool_dt :=
103
  [!, ! ~> true] ::: [!, ! ~> false] ::: HNil.
Adam Chlipala's avatar
Adam Chlipala committed
104
Definition nat_den : datatypeDenote nat nat_dt :=
Adam Chlipala's avatar
Adam Chlipala committed
105
  [!, ! ~> O] ::: [!, r ~> S (hd r)] ::: HNil.
Adam Chlipala's avatar
Adam Chlipala committed
106
Definition list_den (A : Type) : datatypeDenote (list A) (list_dt A) :=
Adam Chlipala's avatar
Adam Chlipala committed
107
  [!, ! ~> nil] ::: [x, r ~> x :: hd r] ::: HNil.
Adam Chlipala's avatar
Adam Chlipala committed
108
Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
Adam Chlipala's avatar
Adam Chlipala committed
109
  [v, ! ~> Leaf v] ::: [!, r ~> Node (hd r) (hd (tl r))] ::: HNil.
Adam Chlipala's avatar
Adam Chlipala committed
110
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
111

Adam Chlipala's avatar
Adam Chlipala committed
112 113 114

(** * Recursive Definitions *)

Adam Chlipala's avatar
Adam Chlipala committed
115 116
(* EX: Define a generic [size] function. *)

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

Adam Chlipala's avatar
Adam Chlipala committed
119
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
120 121 122
Definition fixDenote (T : Type) (dt : datatype) :=
  forall (R : Type), datatypeDenote R dt -> (T -> R).

Adam Chlipala's avatar
Adam Chlipala committed
123 124 125 126 127 128 129 130 131 132 133 134 135 136
(** 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.

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

Check hmake.
(** %\vspace{-.15in}% [[
  hmake
     : forall (A : Type) (B : A -> Type),
       (forall x : A, B x) -> forall ls : list A, hlist B l
 
       ]]

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

Adam Chlipala's avatar
Adam Chlipala committed
137 138 139
Definition size T dt (fx : fixDenote T dt) : T -> nat :=
  fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).

Adam Chlipala's avatar
Adam Chlipala committed
140 141 142 143
(** 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.

   It is instructive to build [fixDenote] values for our example types and see what specialized [size] functions result from them. *)

Adam Chlipala's avatar
Adam Chlipala committed
144 145 146
Definition Empty_set_fix : fixDenote Empty_set Empty_set_dt :=
  fun R _ emp => match emp with end.
Eval compute in size Empty_set_fix.
Adam Chlipala's avatar
Adam Chlipala committed
147 148 149 150 151 152 153 154
(** %\vspace{-.15in}% [[
     = fun emp : Empty_set => match emp return nat with
                              end
     : Empty_set -> nat
 
]]

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

Definition unit_fix : fixDenote unit unit_dt :=
157
  fun R cases _ => (hhd cases) tt INil.
Adam Chlipala's avatar
Adam Chlipala committed
158
Eval compute in size unit_fix.
Adam Chlipala's avatar
Adam Chlipala committed
159 160 161 162 163 164 165
(** %\vspace{-.15in}% [[
     = fun _ : unit => 1
     : unit -> nat
 
]]

Again normalization gives us the natural function definition.  We see this pattern repeated for our other example types. *)
Adam Chlipala's avatar
Adam Chlipala committed
166 167 168

Definition bool_fix : fixDenote bool bool_dt :=
  fun R cases b => if b
169 170
    then (hhd cases) tt INil
    else (hhd (htl cases)) tt INil.
Adam Chlipala's avatar
Adam Chlipala committed
171
Eval compute in size bool_fix.
Adam Chlipala's avatar
Adam Chlipala committed
172 173 174 175
(** %\vspace{-.15in}% [[
     = fun b : bool => if b then 1 else 1
     : bool -> nat
]] *)
Adam Chlipala's avatar
Adam Chlipala committed
176 177 178 179

Definition nat_fix : fixDenote nat nat_dt :=
  fun R cases => fix F (n : nat) : R :=
    match n with
180 181
      | O => (hhd cases) tt INil
      | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
Adam Chlipala's avatar
Adam Chlipala committed
182
    end.
Adam Chlipala's avatar
Adam Chlipala committed
183 184 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. *)

Adam Chlipala's avatar
Adam Chlipala committed
186
Eval cbv beta iota delta -[plus] in size nat_fix.
Adam Chlipala's avatar
Adam Chlipala committed
187 188 189 190 191 192 193
(** %\vspace{-.15in}% [[
     = fix F (n : nat) : nat := match n with
                                | 0 => 1
                                | S n' => F n' + 1
                                end
     : nat -> nat
]] *)
Adam Chlipala's avatar
Adam Chlipala committed
194 195 196 197

Definition list_fix (A : Type) : fixDenote (list A) (list_dt A) :=
  fun R cases => fix F (ls : list A) : R :=
    match ls with
198 199
      | nil => (hhd cases) tt INil
      | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
Adam Chlipala's avatar
Adam Chlipala committed
200 201
    end.
Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
Adam Chlipala's avatar
Adam Chlipala committed
202 203 204 205 206 207 208 209 210
(** %\vspace{-.15in}% [[
     = fun A : Type =>
       fix F (ls : list A) : nat :=
         match ls with
         | nil => 1
         | _ :: ls' => F ls' + 1
         end
     : forall A : Type, list A -> nat
]] *)
Adam Chlipala's avatar
Adam Chlipala committed
211 212 213 214

Definition tree_fix (A : Type) : fixDenote (tree A) (tree_dt A) :=
  fun R cases => fix F (t : tree A) : R :=
    match t with
215 216
      | Leaf x => (hhd cases) x INil
      | Node t1 t2 => (hhd (htl cases)) tt (ICons (F t1) (ICons (F t2) INil))
Adam Chlipala's avatar
Adam Chlipala committed
217 218
    end.
Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
Adam Chlipala's avatar
Adam Chlipala committed
219 220 221 222 223 224 225 226 227
(** %\vspace{-.15in}% [[
     = fun A : Type =>
       fix F (t : tree A) : nat :=
         match t with
         | Leaf _ => 1
         | Node t1 t2 => F t1 + (F t2 + 1)
         end
     : forall A : Type, tree A -> n
]] *)
Adam Chlipala's avatar
Adam Chlipala committed
228
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
229 230 231 232


(** ** Pretty-Printing *)

Adam Chlipala's avatar
Adam Chlipala committed
233 234
(* EX: Define a generic pretty-printing function. *)

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

Adam Chlipala's avatar
Adam Chlipala committed
237
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
238 239 240 241 242
Record print_constructor (c : constructor) : Type := PI {
  printName : string;
  printNonrec : nonrecursive c -> string
}.

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

Adam Chlipala's avatar
Adam Chlipala committed
245 246
Notation "^" := (PI (Con _ _)).

Adam Chlipala's avatar
Adam Chlipala committed
247 248
(** As in earlier examples, we define the type of metadata for a datatype to be a heterogeneous list type collecting metadata for each constructor. *)

Adam Chlipala's avatar
Adam Chlipala committed
249 250
Definition print_datatype := hlist print_constructor.

Adam Chlipala's avatar
Adam Chlipala committed
251 252 253 254 255 256 257 258 259 260 261 262 263
(** We will be doing some string manipulation here, so we import the notations associated with strings. *)

Local Open Scope string_scope.

(** Now it is easy to implement our generic printer, using another function from [DepList.] *)

Check hmap.
(** %\vspace{-.15in}% [[
  hmap
     : forall (A : Type) (B1 B2 : A -> Type),
       (forall x : A, B1 x -> B2 x) ->
       forall ls : list A, hlist B1 ls -> hlist B2 ls
]] *)
Adam Chlipala's avatar
Adam Chlipala committed
264 265 266 267 268

Definition print T dt (pr : print_datatype dt) (fx : fixDenote T dt) : T -> string :=
  fx string (hmap (B1 := print_constructor) (B2 := constructorDenote string)
    (fun _ pc x r => printName pc ++ "(" ++ printNonrec pc x
      ++ foldr (fun s acc => ", " ++ s ++ acc) ")" r) pr).
Adam Chlipala's avatar
Adam Chlipala committed
269
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
270

Adam Chlipala's avatar
Adam Chlipala committed
271 272
(** Some simple tests establish that [print] gets the job done. *)

273
Eval compute in print HNil Empty_set_fix.
Adam Chlipala's avatar
Adam Chlipala committed
274 275 276 277 278 279
(** %\vspace{-.15in}% [[
     = fun emp : Empty_set => match emp return string with
                              end
     : Empty_set -> string
     ]] *)

280
Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
Adam Chlipala's avatar
Adam Chlipala committed
281 282 283 284 285
(** %\vspace{-.15in}% [[
     = fun _ : unit => "tt()"
     : unit -> string
   ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
286 287
Eval compute in print (^ "true" (fun _ => "")
  ::: ^ "false" (fun _ => "")
288
  ::: HNil) bool_fix.
Adam Chlipala's avatar
Adam Chlipala committed
289 290 291 292
(** %\vspace{-.15in}% [[
   = fun b : bool => if b then "true()" else "false()"
   : bool -> s
   ]] *)
Adam Chlipala's avatar
Adam Chlipala committed
293 294 295

Definition print_nat := print (^ "O" (fun _ => "")
  ::: ^ "S" (fun _ => "")
296
  ::: HNil) nat_fix.
Adam Chlipala's avatar
Adam Chlipala committed
297
Eval cbv beta iota delta -[append] in print_nat.
Adam Chlipala's avatar
Adam Chlipala committed
298 299 300 301 302 303 304 305 306
(** %\vspace{-.15in}% [[
     = fix F (n : nat) : string :=
         match n with
         | 0%nat => "O" ++ "(" ++ "" ++ ")"
         | S n' => "S" ++ "(" ++ "" ++ ", " ++ F n' ++ ")"
         end
     : nat -> string
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
307
Eval simpl in print_nat 0.
Adam Chlipala's avatar
Adam Chlipala committed
308 309 310 311 312
(** %\vspace{-.15in}% [[
     = "O()"
     : string
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
313
Eval simpl in print_nat 1.
Adam Chlipala's avatar
Adam Chlipala committed
314 315 316 317 318
(** %\vspace{-.15in}% [[
     = "S(, O())"
     : string
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
319
Eval simpl in print_nat 2.
Adam Chlipala's avatar
Adam Chlipala committed
320 321 322 323
(** %\vspace{-.15in}% [[
     = "S(, S(, O()))"
     : string
     ]] *)
Adam Chlipala's avatar
Adam Chlipala committed
324 325 326 327

Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
  print (^ "nil" (fun _ => "")
  ::: ^ "cons" pr
328
  ::: HNil) (@list_fix A).
Adam Chlipala's avatar
Adam Chlipala committed
329 330 331 332 333 334 335 336 337 338
(** %\vspace{-.15in}% [[
     = fun (A : Type) (pr : A -> string) =>
       fix F (ls : list A) : string :=
         match ls with
         | nil => "nil" ++ "(" ++ "" ++ ")"
         | x :: ls' => "cons" ++ "(" ++ pr x ++ ", " ++ F ls' ++ ")"
         end
     : forall A : Type, (A -> string) -> list A -> string
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
339 340 341
Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
  print (^ "Leaf" pr
  ::: ^ "Node" (fun _ => "")
342
  ::: HNil) (@tree_fix A).
Adam Chlipala's avatar
Adam Chlipala committed
343 344 345 346 347 348 349 350 351 352
(** %\vspace{-.15in}% [[
     = fun (A : Type) (pr : A -> string) =>
       fix F (t : tree A) : string :=
         match t with
         | Leaf x => "Leaf" ++ "(" ++ pr x ++ ")"
         | Node t1 t2 =>
             "Node" ++ "(" ++ "" ++ ", " ++ F t1 ++ ", " ++ F t2 ++ ")"
         end
     : forall A : Type, (A -> string) -> tree A -> string
     ]] *)
Adam Chlipala's avatar
Adam Chlipala committed
353 354 355 356


(** ** Mapping *)

Adam Chlipala's avatar
Adam Chlipala committed
357 358
(* EX: Define a generic [map] function. *)

Adam Chlipala's avatar
Adam Chlipala committed
359 360
(** By this point, we have developed enough machinery that it is old hat to define a generic function similar to the list [map] function. *)

Adam Chlipala's avatar
Adam Chlipala committed
361
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
362 363
Definition map T dt (dd : datatypeDenote T dt) (fx : fixDenote T dt) (f : T -> T)
  : T -> T :=
Adam Chlipala's avatar
Adam Chlipala committed
364 365
  fx T (hmap (B1 := constructorDenote T) (B2 := constructorDenote T)
    (fun _ c x r => f (c x r)) dd).
Adam Chlipala's avatar
Adam Chlipala committed
366
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
367 368

Eval compute in map Empty_set_den Empty_set_fix.
Adam Chlipala's avatar
Adam Chlipala committed
369 370 371 372 373 374 375
(** %\vspace{-.15in}% [[
     = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) =>
       match emp return Empty_set with
       end
     : (Empty_set -> Empty_set) -> Empty_set -> Empty_set
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
376
Eval compute in map unit_den unit_fix.
Adam Chlipala's avatar
Adam Chlipala committed
377 378 379 380 381
(** %\vspace{-.15in}% [[
     = fun (f : unit -> unit) (_ : unit) => f tt
     : (unit -> unit) -> unit -> unit
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
382
Eval compute in map bool_den bool_fix.
Adam Chlipala's avatar
Adam Chlipala committed
383 384 385 386 387
(** %\vspace{-.15in}% [[
     = fun (f : bool -> bool) (b : bool) => if b then f true else f false
     : (bool -> bool) -> bool -> bool
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
388
Eval compute in map nat_den nat_fix.
Adam Chlipala's avatar
Adam Chlipala committed
389 390 391 392 393 394 395 396 397 398
(** %\vspace{-.15in}% [[
     = fun f : nat -> nat =>
       fix F (n : nat) : nat :=
         match n with
         | 0%nat => f 0%nat
         | S n' => f (S (F n'))
         end
     : (nat -> nat) -> nat -> nat
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
399
Eval compute in fun A => map (list_den A) (@list_fix A).
Adam Chlipala's avatar
Adam Chlipala committed
400 401 402 403 404 405 406 407 408 409
(** %\vspace{-.15in}% [[
     = fun (A : Type) (f : list A -> list A) =>
       fix F (ls : list A) : list A :=
         match ls with
         | nil => f nil
         | x :: ls' => f (x :: F ls')
         end
     : forall A : Type, (list A -> list A) -> list A -> list A
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
410
Eval compute in fun A => map (tree_den A) (@tree_fix A).
Adam Chlipala's avatar
Adam Chlipala committed
411 412 413 414 415 416 417 418 419
(** %\vspace{-.15in}% [[
     = fun (A : Type) (f : tree A -> tree A) =>
       fix F (t : tree A) : tree A :=
         match t with
         | Leaf x => f (Leaf x)
         | Node t1 t2 => f (Node (F t1) (F t2))
         end
     : forall A : Type, (tree A -> tree A) -> tree A -> tree A
     ]] *)
Adam Chlipala's avatar
Adam Chlipala committed
420 421 422

Definition map_nat := map nat_den nat_fix.
Eval simpl in map_nat S 0.
Adam Chlipala's avatar
Adam Chlipala committed
423 424 425 426 427
(** %\vspace{-.15in}% [[
     = 1%nat
     : nat
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
428
Eval simpl in map_nat S 1.
Adam Chlipala's avatar
Adam Chlipala committed
429 430 431 432 433
(** %\vspace{-.15in}% [[
     = 3%nat
     : nat
     ]] *)

Adam Chlipala's avatar
Adam Chlipala committed
434
Eval simpl in map_nat S 2.
Adam Chlipala's avatar
Adam Chlipala committed
435 436 437 438
(** %\vspace{-.15in}% [[
     = 5%nat
     : nat
     ]] *)
Adam Chlipala's avatar
Adam Chlipala committed
439 440 441 442


(** * Proving Theorems about Recursive Definitions *)

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

Adam Chlipala's avatar
Adam Chlipala committed
445
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
446 447 448 449 450 451 452
Section ok.
  Variable T : Type.
  Variable dt : datatype.

  Variable dd : datatypeDenote T dt.
  Variable fx : fixDenote T dt.

Adam Chlipala's avatar
Adam Chlipala committed
453 454
  (** 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]. *)

Adam Chlipala's avatar
Adam Chlipala committed
455 456 457
  Definition datatypeDenoteOk :=
    forall P : T -> Prop,
      (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
Adam Chlipala's avatar
Adam Chlipala committed
458
        (forall i : fin (recursive c), P (get r i))
Adam Chlipala's avatar
Adam Chlipala committed
459 460 461
        -> P ((hget dd m) x r))
      -> forall v, P v.

Adam Chlipala's avatar
Adam Chlipala committed
462 463 464 465
  (** 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.

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

Adam Chlipala's avatar
Adam Chlipala committed
466 467 468 469
  Definition fixDenoteOk :=
    forall (R : Type) (cases : datatypeDenote R dt)
      c (m : member c dt)
      (x : nonrecursive c) (r : ilist T (recursive c)),
470 471
      fx cases ((hget dd m) x r)
      = (hget cases m) x (imap (fx cases) r).
Adam Chlipala's avatar
Adam Chlipala committed
472 473 474

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

Adam Chlipala's avatar
Adam Chlipala committed
475 476
End ok.

Adam Chlipala's avatar
Adam Chlipala committed
477
(** We are now ready to prove that the [size] function we defined earlier always returns positive results.  First, we establish a simple lemma. *)
Adam Chlipala's avatar
Adam Chlipala committed
478 479 480

Lemma foldr_plus : forall n (ils : ilist nat n),
  foldr plus 1 ils > 0.
481
  induction ils; crush.
Adam Chlipala's avatar
Adam Chlipala committed
482
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
483
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
484

Adam Chlipala's avatar
Adam Chlipala committed
485 486 487
Theorem size_positive : forall T dt
  (dd : datatypeDenote T dt) (fx : fixDenote T dt)
  (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
Adam Chlipala's avatar
Adam Chlipala committed
488 489
  (v : T),
  size fx v > 0.
Adam Chlipala's avatar
Adam Chlipala committed
490
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572
  unfold size; intros.
  (** [[
  ============================
   fx nat
     (hmake
        (fun (x : constructor) (_ : nonrecursive x)
           (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0
 
    ]]
      
    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.

    [[
  apply dok.

Error: Impossible to unify "datatypeDenoteOk dd" with
 "fx nat
    (hmake
       (fun (x : constructor) (_ : nonrecursive x)
          (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0".
 
    ]]

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

  pattern v.

  (** [[
  ============================
   (fun t : T =>
    fx nat
      (hmake
         (fun (x : constructor) (_ : nonrecursive x)
            (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) t > 0) v
 
      ]] *)

  apply dok; crush.
  (** [[
  H : forall i : fin (recursive c),
      fx nat
        (hmake
           (fun (x : constructor) (_ : nonrecursive x)
              (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt)
        (get r i) > 0
  ============================
   hget
     (hmake
        (fun (x0 : constructor) (_ : nonrecursive x0)
           (r0 : ilist nat (recursive x0)) => foldr plus 1%nat r0) dt) m x
     (imap
        (fx nat
           (hmake
              (fun (x0 : constructor) (_ : nonrecursive x0)
                 (r0 : ilist nat (recursive x0)) => 
               foldr plus 1%nat r0) dt)) r) > 0
 
    ]]

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

  rewrite hget_hmake.
  (** [[
  ============================
   foldr plus 1%nat
     (imap
        (fx nat
           (hmake
              (fun (x0 : constructor) (_ : nonrecursive x0)
                 (r0 : ilist nat (recursive x0)) => 
               foldr plus 1%nat r0) dt)) r) > 0
 
    ]]

    The lemma we proved earlier finishes the proof. *)

  apply foldr_plus.

  (** Using hints, we can redo this proof in a nice automated form. *)

  Restart.

Adam Chlipala's avatar
Adam Chlipala committed
573 574 575
  Hint Rewrite hget_hmake : cpdt.
  Hint Resolve foldr_plus.
 
Adam Chlipala's avatar
Adam Chlipala committed
576 577
  unfold size; intros; pattern v; apply dok; crush.
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
578
(* end thide *)
Adam Chlipala's avatar
Adam Chlipala committed
579

Adam Chlipala's avatar
Adam Chlipala committed
580 581 582 583
(** 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.

   In particular, it ought to be the case that generic [map] applied to an identity function is itself an identity function. *)

Adam Chlipala's avatar
Adam Chlipala committed
584 585 586 587 588
Theorem map_id : forall T dt
  (dd : datatypeDenote T dt) (fx : fixDenote T dt)
  (dok : datatypeDenoteOk dd) (fok : fixDenoteOk dd fx)
  (v : T),
  map dd fx (fun x => x) v = v.
Adam Chlipala's avatar
Adam Chlipala committed
589
(* begin thide *)
Adam Chlipala's avatar
Adam Chlipala committed
590 591
  (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *)

Adam Chlipala's avatar
Adam Chlipala committed
592 593 594
  Hint Rewrite hget_hmap : cpdt.

  unfold map; intros; pattern v; apply dok; crush.
Adam Chlipala's avatar
Adam Chlipala committed
595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614
  (** [[
  H : forall i : fin (recursive c),
      fx T
        (hmap
           (fun (x : constructor) (c : constructorDenote T x)
              (x0 : nonrecursive x) (r : ilist T (recursive x)) => 
            c x0 r) dd) (get r i) = get r i
  ============================
   hget dd m x
     (imap
        (fx T
           (hmap
              (fun (x0 : constructor) (c0 : constructorDenote T x0)
                 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
               c0 x1 r0) dd)) r) = hget dd m x r
 
    ]]

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

Adam Chlipala's avatar
Adam Chlipala committed
615
  f_equal.
Adam Chlipala's avatar
Adam Chlipala committed
616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707
  (** [[
  ============================
   imap
     (fx T
        (hmap
           (fun (x0 : constructor) (c0 : constructorDenote T x0)
              (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
            c0 x1 r0) dd)) r = r
 
    ]]

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

  induction r; crush.

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

     [[
  H : forall i : fin (S n),
      fx T
        (hmap
           (fun (x : constructor) (c : constructorDenote T x)
              (x0 : nonrecursive x) (r : ilist T (recursive x)) => 
            c x0 r) dd)
        (match i in (fin n') return ((fin (pred n') -> T) -> T) with
         | First n => fun _ : fin n -> T => a
         | Next n idx' => fun get_ls' : fin n -> T => get_ls' idx'
         end (get r)) =
      match i in (fin n') return ((fin (pred n') -> T) -> T) with
      | First n => fun _ : fin n -> T => a
      | Next n idx' => fun get_ls' : fin n -> T => get_ls' idx'
      end (get r)
  IHr : (forall i : fin n,
         fx T
           (hmap
              (fun (x : constructor) (c : constructorDenote T x)
                 (x0 : nonrecursive x) (r : ilist T (recursive x)) => 
               c x0 r) dd) (get r i) = get r i) ->
        imap
          (fx T
             (hmap
                (fun (x : constructor) (c : constructorDenote T x)
                   (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
                 c x0 r) dd)) r = r
  ============================
   ICons
     (fx T
        (hmap
           (fun (x0 : constructor) (c0 : constructorDenote T x0)
              (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
            c0 x1 r0) dd) a)
     (imap
        (fx T
           (hmap
              (fun (x0 : constructor) (c0 : constructorDenote T x0)
                 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
               c0 x1 r0) dd)) r) = ICons a r
 
    ]]

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

  f_equal.
  apply (H First).
  (** [[
  ============================
   imap
     (fx T
        (hmap
           (fun (x0 : constructor) (c0 : constructorDenote T x0)
              (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) => 
            c0 x1 r0) dd)) r = r
 
    ]]

    Now the goal matches the inner IH [IHr]. *)

  apply IHr; crush.

  (** [[
  i : fin n
  ============================
   fx T
     (hmap
        (fun (x0 : constructor) (c0 : constructorDenote T x0)
           (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) => 
         c0 x1 r0) dd) (get r i) = get r i
 
    ]]

    We can finish the proof by applying the outer IH again, specialized to a different [fin] value. *)

708
  apply (H (Next i)).
Adam Chlipala's avatar
Adam Chlipala committed
709
Qed.
Adam Chlipala's avatar
Adam Chlipala committed
710
(* end thide *)