### annotate src/Generic.v @ 534:ed829eaa91b2

Builds with Coq 8.5beta2
author Adam Chlipala Wed, 05 Aug 2015 14:46:55 -0400 04177dd1b133
rev   line source
adamc@193 10 (* begin hide *)
adamc@195 11 Require Import String List.
adam@534 13 Require Import Cpdt.CpdtTactics Cpdt.DepList.
adamc@193 17 (* end hide *)
adam@408 19 (** printing ~> $\leadsto$ *)
adamc@219 22 (** %\chapter{Generic Programming}% *)
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@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. *)
adam@457 28 (** * Reifying Datatype Definitions *)
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.
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.
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. *)
adam@457 36 (* EX: Define a reified representation of simple algebraic datatypes. *)
adamc@198 38 (* begin thide *)
adamc@193 39 Record constructor : Type := Con {
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.
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@193 48 Definition datatype := list constructor.
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@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.
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 60 As a further example, we can do the same encoding for a generic binary tree type. *)
adamc@198 62 (* end thide *)
adamc@193 65 Variable A : Type.
adamc@193 67 Inductive tree : Type :=
adamc@193 68 | Leaf : A -> tree
adamc@193 69 | Node : tree -> tree -> tree.
adamc@198 72 (* begin thide *)
adamc@193 73 Definition tree_dt (A : Type) : datatype := Con A 0 :: Con unit 2 :: nil.
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@193 78 Variable T : Type.
adamc@219 79 (** This variable stands for the concrete datatype that we are interested in. *)
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 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@198 89 (* end thide *)
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 93 Notation "[ v , r ~> x ]" := ((fun v r => x) : constructorDenote _ (Con _ _)).
adamc@198 95 (* begin thide *)
adamc@193 96 Definition Empty_set_den : datatypeDenote Empty_set Empty_set_dt :=
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 *)
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. *)
adamc@195 113 (** * Recursive Definitions *)
adamc@198 115 (* EX: Define a generic [size] function. *)
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@198 119 (* begin thide *)
adamc@194 120 Definition fixDenote (T : Type) (dt : datatype) :=
adamc@194 121 forall (R : Type), datatypeDenote R dt -> (T -> R).
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 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 130 : forall (A : Type) (B : A -> Type),
adam@358 131 (forall x : A, B x) -> forall ls : list A, hlist B ls
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@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).
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 141 It is instructive to build [fixDenote] values for our example types and see what specialized [size] functions result from them. *)
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 147 = fun emp : Empty_set => match emp return nat with
adamc@219 149 : Empty_set -> nat
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 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 158 = fun _ : unit => 1
adamc@219 159 : unit -> nat
adamc@219 162 Again normalization gives us the natural function definition. We see this pattern repeated for our other example types. *)
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 170 = fun b : bool => if b then 1 else 1
adamc@219 171 : bool -> nat
adamc@194 175 Definition nat_fix : fixDenote nat nat_dt :=
adamc@194 176 fun R cases => fix F (n : nat) : R :=
adamc@216 178 | O => (hhd cases) tt INil
adamc@216 179 | S n' => (hhd (htl cases)) tt (ICons (F n') INil)
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@194 184 Eval cbv beta iota delta -[plus] in size nat_fix.
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 190 : nat -> nat
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@216 197 | nil => (hhd cases) tt INil
adamc@216 198 | x :: ls' => (hhd (htl cases)) x (ICons (F ls') INil)
adamc@194 200 Eval cbv beta iota delta -[plus] in fun A => size (@list_fix A).
adamc@219 202 = fun A : Type =>
adamc@219 203 fix F (ls : list A) : nat :=
adamc@219 205 | nil => 1
adamc@219 206 | _ :: ls' => F ls' + 1
adamc@219 208 : forall A : Type, list A -> nat
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@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 218 Eval cbv beta iota delta -[plus] in fun A => size (@tree_fix A).
adamc@219 220 = fun A : Type =>
adamc@219 221 fix F (t : tree A) : nat :=
adamc@219 223 | Leaf _ => 1
adamc@219 224 | Node t1 t2 => F t1 + (F t2 + 1)
adamc@219 226 : forall A : Type, tree A -> n
adamc@198 229 (* end thide *)
adam@457 231 (** As our examples show, even recursive datatypes are mapped to normal-looking size functions. *)
adamc@195 234 (** ** Pretty-Printing *)
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@195 238 Record print_constructor (c : constructor) : Type := PI {
adamc@195 240 printNonrec : nonrecursive c -> string
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@195 245 Notation "^" := (PI (Con _ _)).
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@195 249 Definition print_datatype := hlist print_constructor.
adamc@219 251 (** We will be doing some string manipulation here, so we import the notations associated with strings. *)
adamc@219 253 Local Open Scope string_scope.
adamc@219 255 (** Now it is easy to implement our generic printer, using another function from [DepList.] *)
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
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@219 271 (** Some simple tests establish that [print] gets the job done. *)
adamc@216 273 Eval compute in print HNil Empty_set_fix.
adamc@219 275 = fun emp : Empty_set => match emp return string with
adamc@219 277 : Empty_set -> string
adamc@216 281 Eval compute in print (^ "tt" (fun _ => "") ::: HNil) unit_fix.
adamc@219 283 = fun _ : unit => "tt()"
adamc@219 284 : unit -> string
adamc@195 288 Eval compute in print (^ "true" (fun _ => "")
adamc@195 289 ::: ^ "false" (fun _ => "")
adamc@219 292 = fun b : bool => if b then "true()" else "false()"
adam@488 293 : bool -> string
adamc@195 297 Definition print_nat := print (^ "O" (fun _ => "")
adamc@195 298 ::: ^ "S" (fun _ => "")
adamc@195 300 Eval cbv beta iota delta -[append] in print_nat.
adamc@219 302 = fix F (n : nat) : string :=
adamc@219 304 | 0%nat => "O" ++ "(" ++ "" ++ ")"
adamc@219 305 | S n' => "S" ++ "(" ++ "" ++ ", " ++ F n' ++ ")"
adamc@219 307 : nat -> string
adamc@195 311 Eval simpl in print_nat 0.
adamc@195 318 Eval simpl in print_nat 1.
adamc@195 325 Eval simpl in print_nat 2.
adamc@219 327 = "S(, S(, O()))"
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 337 = fun (A : Type) (pr : A -> string) =>
adamc@219 338 fix F (ls : list A) : string :=
adamc@219 340 | nil => "nil" ++ "(" ++ "" ++ ")"
adamc@219 341 | x :: ls' => "cons" ++ "(" ++ pr x ++ ", " ++ F ls' ++ ")"
adamc@219 343 : forall A : Type, (A -> string) -> list A -> string
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 352 = fun (A : Type) (pr : A -> string) =>
adamc@219 353 fix F (t : tree A) : string :=
adamc@219 355 | Leaf x => "Leaf" ++ "(" ++ pr x ++ ")"
adamc@219 356 | Node t1 t2 =>
adamc@219 357 "Node" ++ "(" ++ "" ++ ", " ++ F t1 ++ ", " ++ F t2 ++ ")"
adamc@219 359 : forall A : Type, (A -> string) -> tree A -> string
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@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. *)
adamc@196 372 (** ** Mapping *)
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 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 381 Eval compute in map Empty_set_den Empty_set_fix.
adamc@219 383 = fun (_ : Empty_set -> Empty_set) (emp : Empty_set) =>
adamc@219 384 match emp return Empty_set with
adamc@219 386 : (Empty_set -> Empty_set) -> Empty_set -> Empty_set
adamc@196 390 Eval compute in map unit_den unit_fix.
adamc@219 392 = fun (f : unit -> unit) (_ : unit) => f tt
adamc@219 393 : (unit -> unit) -> unit -> unit
adamc@196 397 Eval compute in map bool_den bool_fix.
adamc@219 399 = fun (f : bool -> bool) (b : bool) => if b then f true else f false
adamc@219 400 : (bool -> bool) -> bool -> bool
adamc@196 404 Eval compute in map nat_den nat_fix.
adamc@219 406 = fun f : nat -> nat =>
adamc@219 407 fix F (n : nat) : nat :=
adamc@219 409 | 0%nat => f 0%nat
adamc@219 410 | S n' => f (S (F n'))
adamc@219 412 : (nat -> nat) -> nat -> nat
adamc@196 416 Eval compute in fun A => map (list_den A) (@list_fix A).
adamc@219 418 = fun (A : Type) (f : list A -> list A) =>
adamc@219 419 fix F (ls : list A) : list A :=
adamc@219 421 | nil => f nil
adamc@219 422 | x :: ls' => f (x :: F ls')
adamc@219 424 : forall A : Type, (list A -> list A) -> list A -> list A
adamc@196 428 Eval compute in fun A => map (tree_den A) (@tree_fix A).
adamc@219 430 = fun (A : Type) (f : tree A -> tree A) =>
adamc@219 431 fix F (t : tree A) : tree A :=
adamc@219 433 | Leaf x => f (Leaf x)
adamc@219 434 | Node t1 t2 => f (Node (F t1) (F t2))
adamc@219 436 : forall A : Type, (tree A -> tree A) -> tree A -> tree A
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? *)
adamc@196 442 Definition map_nat := map nat_den nat_fix.
adamc@196 443 Eval simpl in map_nat S 0.
adamc@196 450 Eval simpl in map_nat S 1.
adamc@196 457 Eval simpl in map_nat S 2.
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. *)
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@196 472 Variable T : Type.
adamc@196 473 Variable dt : datatype.
adamc@196 475 Variable dd : datatypeDenote T dt.
adamc@196 476 Variable fx : fixDenote T dt.
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@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.
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 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@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 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 502 (** We are now ready to prove that the [size] function we defined earlier always returns positive results. First, we establish a simple lemma. *)
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@198 509 (* end thide *)
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 515 size fx v > 0.
adamc@198 516 (* begin thide *)
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 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 532 Error: Impossible to unify "datatypeDenoteOk dd" with
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@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 544 (fun t : T =>
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
adamc@219 554 H : forall i : fin (recursive c),
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 563 (fun (x0 : constructor) (_ : nonrecursive x0)
adamc@219 564 (r0 : ilist nat (recursive x0)) => foldr plus 1%nat r0) dt) m x
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 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 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 587 The lemma we proved earlier finishes the proof. *)
adamc@219 591 (** Using hints, we can redo this proof in a nice automated form. *)
adamc@197 598 unfold size; intros; pattern v; apply dok; crush.
adamc@198 600 (* end thide *)
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 604 In particular, it ought to be the case that generic [map] applied to an identity function is itself an identity function. *)
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 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@197 616 unfold map; intros; pattern v; apply dok; crush.
adamc@219 618 H : forall i : fin (recursive c),
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 625 hget dd m x
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 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 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 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.*)
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@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 659 H : forall i : fin (S n),
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 673 IHr : (forall i : fin n,
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 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 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 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 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 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 714 Now the goal matches the inner IH [IHr]. *)
adamc@219 718 i : fin n