comparison src/Generic.v @ 358:6cc9a3bbc2c6

Pass over Generic
author Adam Chlipala <adam@chlipala.net>
date Mon, 31 Oct 2011 14:24:16 -0400
parents ad315efc3b6b
children 059c51227e69
comparison
equal deleted inserted replaced
357:b01c7b3122cc 358:6cc9a3bbc2c6
16 (* end hide *) 16 (* end hide *)
17 17
18 18
19 (** %\chapter{Generic Programming}% *) 19 (** %\chapter{Generic Programming}% *)
20 20
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. 21 (** %\index{generic programming}\textit{%#<i>#Generic programming#</i>#%}% 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, 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}\emph{%#<i>#datatype-generic programming#</i>#%}% much more cleanly with dependent types. Thanks to the expressive power of CIC, we need no special language support.
22 22
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. *) 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. *)
24 24
25 (** * Reflecting Datatype Definitions *) 25 (** * Reflecting Datatype Definitions *)
26 26
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. 27 (** The key to generic programming with dependent types is %\index{universe types}\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.
28 28
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. 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.
30 30
31 The first step is to define a representation for constructors of our datatypes. *) 31 The first step is to define a representation for constructors of our datatypes. *)
32 32
33 (* EX: Define a reflected representation of simple algebraic datatypes. *) 33 (* EX: Define a reflected representation of simple algebraic datatypes. *)
34 34
50 Definition unit_dt : datatype := Con unit 0 :: nil. 50 Definition unit_dt : datatype := Con unit 0 :: nil.
51 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil. 51 Definition bool_dt : datatype := Con unit 0 :: Con unit 0 :: nil.
52 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil. 52 Definition nat_dt : datatype := Con unit 0 :: Con unit 1 :: nil.
53 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil. 53 Definition list_dt (A : Type) : datatype := Con unit 0 :: Con A 1 :: nil.
54 54
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]. 55 (** 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 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].
56 56
57 As a further example, we can do the same encoding for a generic binary tree type. *) 57 As a further example, we can do the same encoding for a generic binary tree type. *)
58 58
59 (* end thide *) 59 (* end thide *)
60 60
75 Variable T : Type. 75 Variable T : Type.
76 (** This variable stands for the concrete datatype that we are interested in. *) 76 (** This variable stands for the concrete datatype that we are interested in. *)
77 77
78 Definition constructorDenote (c : constructor) := 78 Definition constructorDenote (c : constructor) :=
79 nonrecursive c -> ilist T (recursive c) -> T. 79 nonrecursive c -> ilist T (recursive c) -> T.
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 8. *) 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 %\index{Gallina terms!ilist}%[ilist] that we met in Chapter 8. *)
81 81
82 Definition datatypeDenote := hlist constructorDenote. 82 Definition datatypeDenote := hlist constructorDenote.
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]. *) 83 (** 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]. *)
84 84
85 End denote. 85 End denote.
86 (* end thide *) 86 (* end thide *)
87 87
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$.% *) 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$.% *)
107 [!, ! ~> nil] ::: [x, r ~> x :: hd r] ::: HNil. 107 [!, ! ~> nil] ::: [x, r ~> x :: hd r] ::: HNil.
108 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) := 108 Definition tree_den (A : Type) : datatypeDenote (tree A) (tree_dt A) :=
109 [v, ! ~> Leaf v] ::: [!, r ~> Node (hd r) (hd (tl r))] ::: HNil. 109 [v, ! ~> Leaf v] ::: [!, r ~> Node (hd r) (hd (tl r))] ::: HNil.
110 (* end thide *) 110 (* end thide *)
111 111
112 (** Recall that the [hd] and [tl] calls above operate on richly typed lists, where type indices tell us the lengths of lists, guaranteeing the safety of operations like [hd]. The type annotation attached to each definition provides enough information for Coq to infer list lengths at appropriate points. *)
113
112 114
113 (** * Recursive Definitions *) 115 (** * Recursive Definitions *)
114 116
115 (* EX: Define a generic [size] function. *) 117 (* EX: Define a generic [size] function. *)
116 118
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. *) 119 (** 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 %\index{recursion schemes}\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. *)
118 120
119 (* begin thide *) 121 (* begin thide *)
120 Definition fixDenote (T : Type) (dt : datatype) := 122 Definition fixDenote (T : Type) (dt : datatype) :=
121 forall (R : Type), datatypeDenote R dt -> (T -> R). 123 forall (R : Type), datatypeDenote R dt -> (T -> R).
122 124
126 128
127 Check hmake. 129 Check hmake.
128 (** %\vspace{-.15in}% [[ 130 (** %\vspace{-.15in}% [[
129 hmake 131 hmake
130 : forall (A : Type) (B : A -> Type), 132 : forall (A : Type) (B : A -> Type),
131 (forall x : A, B x) -> forall ls : list A, hlist B l 133 (forall x : A, B x) -> forall ls : list A, hlist B ls
132
133 ]] 134 ]]
134 135
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. *) 136 The function [hmake] is a kind of [map] alternative that goes from a regular [list] to an [hlist]. We can use it to define a generic size function that counts the number of constructors used to build a value in a datatype. *)
136 137
137 Definition size T dt (fx : fixDenote T dt) : T -> nat := 138 Definition size T dt (fx : fixDenote T dt) : T -> nat :=
138 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt). 139 fx nat (hmake (B := constructorDenote nat) (fun _ _ r => foldr plus 1 r) dt).
139 140
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. 141 (** Our definition is parameterized over a recursion scheme [fx]. We instantiate [fx] by passing it the function result type and a set of function cases, where we build the latter with [hmake]. The function argument to [hmake] takes three arguments: the representation of a constructor, its non-recursive arguments, and the results of recursive calls on all of its recursive arguments. We only need the recursive call results here, so we call them [r] and bind the other two inputs with wildcards. The actual case body is simple: we add together the recursive call results and increment the result by one (to account for the current constructor). This [foldr] function is an [hlist]-specific version defined in the [DepList] module.
146 Eval compute in size Empty_set_fix. 147 Eval compute in size Empty_set_fix.
147 (** %\vspace{-.15in}% [[ 148 (** %\vspace{-.15in}% [[
148 = fun emp : Empty_set => match emp return nat with 149 = fun emp : Empty_set => match emp return nat with
149 end 150 end
150 : Empty_set -> nat 151 : Empty_set -> nat
151
152 ]] 152 ]]
153 153
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. *) 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. *)
155 155
156 Definition unit_fix : fixDenote unit unit_dt := 156 Definition unit_fix : fixDenote unit unit_dt :=
157 fun R cases _ => (hhd cases) tt INil. 157 fun R cases _ => (hhd cases) tt INil.
158 Eval compute in size unit_fix. 158 Eval compute in size unit_fix.
159 (** %\vspace{-.15in}% [[ 159 (** %\vspace{-.15in}% [[
160 = fun _ : unit => 1 160 = fun _ : unit => 1
161 : unit -> nat 161 : unit -> nat
162
163 ]] 162 ]]
164 163
165 Again normalization gives us the natural function definition. We see this pattern repeated for our other example types. *) 164 Again normalization gives us the natural function definition. We see this pattern repeated for our other example types. *)
166 165
167 Definition bool_fix : fixDenote bool bool_dt := 166 Definition bool_fix : fixDenote bool bool_dt :=
363 end 362 end
364 : forall A : Type, (A -> string) -> tree A -> string 363 : forall A : Type, (A -> string) -> tree A -> string
365 ]] 364 ]]
366 *) 365 *)
367 366
367 (** 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. *)
368
368 369
369 (** ** Mapping *) 370 (** ** Mapping *)
370 371
371 (* EX: Define a generic [map] function. *) 372 (* EX: Define a generic [map] function. *)
372 373
436 end 437 end
437 : forall A : Type, (tree A -> tree A) -> tree A -> tree A 438 : forall A : Type, (tree A -> tree A) -> tree A -> tree A
438 ]] 439 ]]
439 *) 440 *)
440 441
442 (** These [map] functions are just as easy to use as those we write by hand. Can you figure out the input-output pattern that [map_nat S] displays in these examples? *)
443
441 Definition map_nat := map nat_den nat_fix. 444 Definition map_nat := map nat_den nat_fix.
442 Eval simpl in map_nat S 0. 445 Eval simpl in map_nat S 0.
443 (** %\vspace{-.15in}% [[ 446 (** %\vspace{-.15in}% [[
444 = 1%nat 447 = 1%nat
445 : nat 448 : nat
457 (** %\vspace{-.15in}% [[ 460 (** %\vspace{-.15in}% [[
458 = 5%nat 461 = 5%nat
459 : nat 462 : nat
460 ]] 463 ]]
461 *) 464 *)
465
466 (** We get [map_nat S n] = [2 * n + 1], because the mapping process adds an extra [S] at every level of the inductive tree that defines a natural, including at the last level, the [O] constructor. *)
462 467
463 468
464 (** * Proving Theorems about Recursive Definitions *) 469 (** * Proving Theorems about Recursive Definitions *)
465 470
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. *) 471 (** We would like to be able to prove theorems about our generic functions. To do so, we need to establish additional well-formedness properties that must hold of pieces of evidence. *)
480 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)), 485 (forall c (m : member c dt) (x : nonrecursive c) (r : ilist T (recursive c)),
481 (forall i : fin (recursive c), P (get r i)) 486 (forall i : fin (recursive c), P (get r i))
482 -> P ((hget dd m) x r)) 487 -> P ((hget dd m) x r))
483 -> forall v, P v. 488 -> forall v, P v.
484 489
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. 490 (** 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.
486 491
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. *) 492 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. *)
488 493
489 Definition fixDenoteOk := 494 Definition fixDenoteOk :=
490 forall (R : Type) (cases : datatypeDenote R dt) 495 forall (R : Type) (cases : datatypeDenote R dt)
516 ============================ 521 ============================
517 fx nat 522 fx nat
518 (hmake 523 (hmake
519 (fun (x : constructor) (_ : nonrecursive x) 524 (fun (x : constructor) (_ : nonrecursive x)
520 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0 525 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0
521
522 ]] 526 ]]
523 527
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. 528 Our goal is an inequality over a particular call to [size], with its definition expanded. How can we proceed here? We cannot use [induction] directly, because there is no way for Coq to know that [T] is an inductive type. Instead, we need to use the induction principle encoded in our hypothesis [dok] of type [datatypeDenoteOk dd]. Let us try applying it directly.
525
526 [[ 529 [[
527 apply dok. 530 apply dok.
528 531 ]]
532 %\vspace{-.3in}%
533 <<
529 Error: Impossible to unify "datatypeDenoteOk dd" with 534 Error: Impossible to unify "datatypeDenoteOk dd" with
530 "fx nat 535 "fx nat
531 (hmake 536 (hmake
532 (fun (x : constructor) (_ : nonrecursive x) 537 (fun (x : constructor) (_ : nonrecursive x)
533 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0". 538 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0".
534 539 >>
535 ]]
536 540
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. *) 541 Matching the type of [dok] with the type of our conclusion requires more than simple first-order unification, so [apply] is not up to the challenge. We can use the [pattern] tactic to get our goal into a form that makes it apparent exactly what the induction hypothesis is. *)
538 542
539 pattern v. 543 pattern v.
540 544 (** %\vspace{-.15in}%[[
541 (** [[
542 ============================ 545 ============================
543 (fun t : T => 546 (fun t : T =>
544 fx nat 547 fx nat
545 (hmake 548 (hmake
546 (fun (x : constructor) (_ : nonrecursive x) 549 (fun (x : constructor) (_ : nonrecursive x)
547 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) t > 0) v 550 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) t > 0) v
548
549 ]] 551 ]]
550 *) 552 *)
551 553
552 apply dok; crush. 554 apply dok; crush.
553 (** [[ 555 (** %\vspace{-.15in}%[[
554 H : forall i : fin (recursive c), 556 H : forall i : fin (recursive c),
555 fx nat 557 fx nat
556 (hmake 558 (hmake
557 (fun (x : constructor) (_ : nonrecursive x) 559 (fun (x : constructor) (_ : nonrecursive x)
558 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) 560 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt)
566 (fx nat 568 (fx nat
567 (hmake 569 (hmake
568 (fun (x0 : constructor) (_ : nonrecursive x0) 570 (fun (x0 : constructor) (_ : nonrecursive x0)
569 (r0 : ilist nat (recursive x0)) => 571 (r0 : ilist nat (recursive x0)) =>
570 foldr plus 1%nat r0) dt)) r) > 0 572 foldr plus 1%nat r0) dt)) r) > 0
571
572 ]] 573 ]]
573 574
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]. *) 575 An induction hypothesis [H] is generated, but we turn out not to need it for this example. We can simplify the goal using a library theorem about the composition of [hget] and [hmake]. *)
575 576
576 rewrite hget_hmake. 577 rewrite hget_hmake.
577 (** [[ 578 (** %\vspace{-.15in}%[[
578 ============================ 579 ============================
579 foldr plus 1%nat 580 foldr plus 1%nat
580 (imap 581 (imap
581 (fx nat 582 (fx nat
582 (hmake 583 (hmake
583 (fun (x0 : constructor) (_ : nonrecursive x0) 584 (fun (x0 : constructor) (_ : nonrecursive x0)
584 (r0 : ilist nat (recursive x0)) => 585 (r0 : ilist nat (recursive x0)) =>
585 foldr plus 1%nat r0) dt)) r) > 0 586 foldr plus 1%nat r0) dt)) r) > 0
586
587 ]] 587 ]]
588 588
589 The lemma we proved earlier finishes the proof. *) 589 The lemma we proved earlier finishes the proof. *)
590 590
591 apply foldr_plus. 591 apply foldr_plus.
614 (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *) 614 (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *)
615 615
616 Hint Rewrite hget_hmap : cpdt. 616 Hint Rewrite hget_hmap : cpdt.
617 617
618 unfold map; intros; pattern v; apply dok; crush. 618 unfold map; intros; pattern v; apply dok; crush.
619 (** [[ 619 (** %\vspace{-.15in}%[[
620 H : forall i : fin (recursive c), 620 H : forall i : fin (recursive c),
621 fx T 621 fx T
622 (hmap 622 (hmap
623 (fun (x : constructor) (c : constructorDenote T x) 623 (fun (x : constructor) (c : constructorDenote T x)
624 (x0 : nonrecursive x) (r : ilist T (recursive x)) => 624 (x0 : nonrecursive x) (r : ilist T (recursive x)) =>
629 (fx T 629 (fx T
630 (hmap 630 (hmap
631 (fun (x0 : constructor) (c0 : constructorDenote T x0) 631 (fun (x0 : constructor) (c0 : constructorDenote T x0)
632 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) => 632 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
633 c0 x1 r0) dd)) r) = hget dd m x r 633 c0 x1 r0) dd)) r) = hget dd m x r
634
635 ]] 634 ]]
636 635
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. *) 636 Our goal is an equality whose two sides begin with the same function call and initial arguments. We believe that the remaining arguments are in fact equal as well, and the [f_equal] tactic applies this reasoning step for us formally. *)
638 637
639 f_equal. 638 f_equal.
640 (** [[ 639 (** %\vspace{-.15in}%[[
641 ============================ 640 ============================
642 imap 641 imap
643 (fx T 642 (fx T
644 (hmap 643 (hmap
645 (fun (x0 : constructor) (c0 : constructorDenote T x0) 644 (fun (x0 : constructor) (c0 : constructorDenote T x0)
646 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) => 645 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
647 c0 x1 r0) dd)) r = r 646 c0 x1 r0) dd)) r = r
648
649 ]] 647 ]]
650 648
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.*) 649 At this point, it is helpful to proceed by an inner induction on the heterogeneous list [r] of recursive call results. We could arrive at a cleaner proof by breaking this step out into an explicit lemma, but here we will do the induction inline to save space.*)
652 650
653 induction r; crush. 651 induction r; crush.
654 652
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). 653 (** 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).
656
657 [[ 654 [[
658 H : forall i : fin (S n), 655 H : forall i : fin (S n),
659 fx T 656 fx T
660 (hmap 657 (hmap
661 (fun (x : constructor) (c : constructorDenote T x) 658 (fun (x : constructor) (c : constructorDenote T x)
692 (fx T 689 (fx T
693 (hmap 690 (hmap
694 (fun (x0 : constructor) (c0 : constructorDenote T x0) 691 (fun (x0 : constructor) (c0 : constructorDenote T x0)
695 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) => 692 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
696 c0 x1 r0) dd)) r) = ICons a r 693 c0 x1 r0) dd)) r) = ICons a r
697
698 ]] 694 ]]
699 695
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. *) 696 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. *)
701 697
702 f_equal. 698 f_equal.
703 apply (H First). 699 apply (H First).
704 (** [[ 700 (** %\vspace{-.15in}%[[
705 ============================ 701 ============================
706 imap 702 imap
707 (fx T 703 (fx T
708 (hmap 704 (hmap
709 (fun (x0 : constructor) (c0 : constructorDenote T x0) 705 (fun (x0 : constructor) (c0 : constructorDenote T x0)
710 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) => 706 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
711 c0 x1 r0) dd)) r = r 707 c0 x1 r0) dd)) r = r
712
713 ]] 708 ]]
714 709
715 Now the goal matches the inner IH [IHr]. *) 710 Now the goal matches the inner IH [IHr]. *)
716 711
717 apply IHr; crush. 712 apply IHr; crush.
718 713 (** %\vspace{-.15in}%[[
719 (** [[
720 i : fin n 714 i : fin n
721 ============================ 715 ============================
722 fx T 716 fx T
723 (hmap 717 (hmap
724 (fun (x0 : constructor) (c0 : constructorDenote T x0) 718 (fun (x0 : constructor) (c0 : constructorDenote T x0)
725 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) => 719 (x1 : nonrecursive x0) (r0 : ilist T (recursive x0)) =>
726 c0 x1 r0) dd) (get r i) = get r i 720 c0 x1 r0) dd) (get r i) = get r i
727
728 ]] 721 ]]
729 722
730 We can finish the proof by applying the outer IH again, specialized to a different [fin] value. *) 723 We can finish the proof by applying the outer IH again, specialized to a different [fin] value. *)
731 724
732 apply (H (Next i)). 725 apply (H (Next i)).
733 Qed. 726 Qed.
734 (* end thide *) 727 (* end thide *)
728
729 (** The proof involves complex subgoals, but, still, few steps are required, and then we may reuse our work across a variety of datatypes. *)