Mercurial > cpdt > repo

comparison src/Coinductive.v @ 351:bb1a470c1757

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Well-founded recursion
author Adam Chlipala <adam@chlipala.net>
date Wed, 26 Oct 2011 15:12:21 -0400
parents de7db21a016c
children dc99dffdf20a
comparison
equal deleted inserted replaced
350:ad315efc3b6b 351:bb1a470c1757
39 (** * Computing with Infinite Data *) 39 (** * Computing with Infinite Data *)
40 40
41 (** Let us begin with the most basic type of infinite data, %\textit{%#<i>#streams#</i>#%}%, or lazy lists.%\index{Vernacular commands!CoInductive}% *) 41 (** Let us begin with the most basic type of infinite data, %\textit{%#<i>#streams#</i>#%}%, or lazy lists.%\index{Vernacular commands!CoInductive}% *)
42 42
43 Section stream. 43 Section stream.
44 Variable A : Set. 44 Variable A : Type.
45 45
46 CoInductive stream : Set := 46 CoInductive stream : Type :=
47 | Cons : A -> stream -> stream. 47 | Cons : A -> stream -> stream.
48 End stream. 48 End stream.
49 49
50 (** The definition is surprisingly simple. Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive]. We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite. 50 (** The definition is surprisingly simple. Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive]. We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite.
51 51
117 The rule we have run afoul of here is that %\textit{%#<i>#every co-recursive call must be guarded by a constructor#</i>#%}%; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating. It is a good thing that this rule is enforced. If the definition of [looper] were accepted, our [approx] function would run forever when passed [looper], and we would have fallen into inconsistency. 117 The rule we have run afoul of here is that %\textit{%#<i>#every co-recursive call must be guarded by a constructor#</i>#%}%; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating. It is a good thing that this rule is enforced. If the definition of [looper] were accepted, our [approx] function would run forever when passed [looper], and we would have fallen into inconsistency.
118 118
119 Some familiar functions are easy to write in co-recursive fashion. *) 119 Some familiar functions are easy to write in co-recursive fashion. *)
120 120
121 Section map. 121 Section map.
122 Variables A B : Set. 122 Variables A B : Type.
123 Variable f : A -> B. 123 Variable f : A -> B.
124 124
125 CoFixpoint map (s : stream A) : stream B := 125 CoFixpoint map (s : stream A) : stream B :=
126 match s with 126 match s with
127 | Cons h t => Cons (f h) (map t) 127 | Cons h t => Cons (f h) (map t)
131 (** This code is a literal copy of that for the list [map] function, with the [Nil] case removed and [Fixpoint] changed to [CoFixpoint]. Many other standard functions on lazy data structures can be implemented just as easily. Some, like [filter], cannot be implemented. Since the predicate passed to [filter] may reject every element of the stream, we cannot satisfy the guardedness condition. 131 (** This code is a literal copy of that for the list [map] function, with the [Nil] case removed and [Fixpoint] changed to [CoFixpoint]. Many other standard functions on lazy data structures can be implemented just as easily. Some, like [filter], cannot be implemented. Since the predicate passed to [filter] may reject every element of the stream, we cannot satisfy the guardedness condition.
132 132
133 The implications of the condition can be subtle. To illustrate how, we start off with another co-recursive function definition that %\textit{%#<i>#is#</i>#%}% legal. The function [interleave] takes two streams and produces a new stream that alternates between their elements. *) 133 The implications of the condition can be subtle. To illustrate how, we start off with another co-recursive function definition that %\textit{%#<i>#is#</i>#%}% legal. The function [interleave] takes two streams and produces a new stream that alternates between their elements. *)
134 134
135 Section interleave. 135 Section interleave.
136 Variable A : Set. 136 Variable A : Type.
137 137
138 CoFixpoint interleave (s1 s2 : stream A) : stream A := 138 CoFixpoint interleave (s1 s2 : stream A) : stream A :=
139 match s1, s2 with 139 match s1, s2 with
140 | Cons h1 t1, Cons h2 t2 => Cons h1 (Cons h2 (interleave t1 t2)) 140 | Cons h1 t1, Cons h2 t2 => Cons h1 (Cons h2 (interleave t1 t2))
141 end. 141 end.
142 End interleave. 142 End interleave.
143 143
144 (** Now say we want to write a weird stuttering version of [map] that repeats elements in a particular way, based on interleaving. *) 144 (** Now say we want to write a weird stuttering version of [map] that repeats elements in a particular way, based on interleaving. *)
145 145
146 Section map'. 146 Section map'.
147 Variables A B : Set. 147 Variables A B : Type.
148 Variable f : A -> B. 148 Variable f : A -> B.
149 (* begin thide *) 149 (* begin thide *)
150 (** [[ 150 (** [[
151 CoFixpoint map' (s : stream A) : stream B := 151 CoFixpoint map' (s : stream A) : stream B :=
152 match s with 152 match s with
208 (** Co-inductive datatypes make sense by analogy from Haskell. What we need now is a %\textit{%#<i>#co-inductive proposition#</i>#%}%. That is, we want to define a proposition whose proofs may be infinite, subject to the guardedness condition. The idea of infinite proofs does not show up in usual mathematics, but it can be very useful (unsurprisingly) for reasoning about infinite data structures. Besides examples from Haskell, infinite data and proofs will also turn out to be useful for modelling inherently infinite mathematical objects, like program executions. 208 (** Co-inductive datatypes make sense by analogy from Haskell. What we need now is a %\textit{%#<i>#co-inductive proposition#</i>#%}%. That is, we want to define a proposition whose proofs may be infinite, subject to the guardedness condition. The idea of infinite proofs does not show up in usual mathematics, but it can be very useful (unsurprisingly) for reasoning about infinite data structures. Besides examples from Haskell, infinite data and proofs will also turn out to be useful for modelling inherently infinite mathematical objects, like program executions.
209 209
210 We are ready for our first %\index{co-inductive predicates}%co-inductive predicate. *) 210 We are ready for our first %\index{co-inductive predicates}%co-inductive predicate. *)
211 211
212 Section stream_eq. 212 Section stream_eq.
213 Variable A : Set. 213 Variable A : Type.
214 214
215 CoInductive stream_eq : stream A -> stream A -> Prop := 215 CoInductive stream_eq : stream A -> stream A -> Prop :=
216 | Stream_eq : forall h t1 t2, 216 | Stream_eq : forall h t1 t2,
217 stream_eq t1 t2 217 stream_eq t1 t2
218 -> stream_eq (Cons h t1) (Cons h t2). 218 -> stream_eq (Cons h t1) (Cons h t2).
374 end. 374 end.
375 375
376 (** Now we enter a section for the co-induction principle, based on %\index{Park's principle}%Park's principle as introduced in a tutorial by Gim%\'%enez%~\cite{IT}%. *) 376 (** Now we enter a section for the co-induction principle, based on %\index{Park's principle}%Park's principle as introduced in a tutorial by Gim%\'%enez%~\cite{IT}%. *)
377 377
378 Section stream_eq_coind. 378 Section stream_eq_coind.
379 Variable A : Set. 379 Variable A : Type.
380 Variable R : stream A -> stream A -> Prop. 380 Variable R : stream A -> stream A -> Prop.
381 (** This relation generalizes the theorem we want to prove, characterizinge exactly which two arguments to [stream_eq] we want to consider. *) 381 (** This relation generalizes the theorem we want to prove, characterizinge exactly which two arguments to [stream_eq] we want to consider. *)
382 382
383 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2. 383 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2.
384 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2). 384 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2).
406 (** Note that this proof achieves the proper reduction behavior via [hd] and [tl], rather than [frob] as in the last proof. All three functions pattern match on their arguments, catalyzing computation steps. 406 (** Note that this proof achieves the proper reduction behavior via [hd] and [tl], rather than [frob] as in the last proof. All three functions pattern match on their arguments, catalyzing computation steps.
407 407
408 Compared to the inductive proofs that we are used to, it still seems unsatisfactory that we had to write out a choice of [R] in the last proof. An alternate is to capture a common pattern of co-recursion in a more specialized co-induction principle. For the current example, that pattern is: prove [stream_eq s1 s2] where [s1] and [s2] are defined as their own tails. *) 408 Compared to the inductive proofs that we are used to, it still seems unsatisfactory that we had to write out a choice of [R] in the last proof. An alternate is to capture a common pattern of co-recursion in a more specialized co-induction principle. For the current example, that pattern is: prove [stream_eq s1 s2] where [s1] and [s2] are defined as their own tails. *)
409 409
410 Section stream_eq_loop. 410 Section stream_eq_loop.
411 Variable A : Set. 411 Variable A : Type.
412 Variables s1 s2 : stream A. 412 Variables s1 s2 : stream A.
413 413
414 Hypothesis Cons_case_hd : hd s1 = hd s2. 414 Hypothesis Cons_case_hd : hd s1 = hd s2.
415 Hypothesis loop1 : tl s1 = s1. 415 Hypothesis loop1 : tl s1 = s1.
416 Hypothesis loop2 : tl s2 = s2. 416 Hypothesis loop2 : tl s2 = s2.
490 Qed. 490 Qed.
491 491
492 (** As in the case of [ones_eq'], we may be unsatisfied that we needed to write down a choice of [R] that seems to duplicate information already present in a lemma statement. We can facilitate a simpler proof by defining a co-induction principle specialized to goals that begin with single universal quantifiers, and the strategy can be extended in a straightforward way to principles for other counts of quantifiers. (Our [stream_eq_loop] principle is effectively the instantiation of this technique to zero quantifiers.) *) 492 (** As in the case of [ones_eq'], we may be unsatisfied that we needed to write down a choice of [R] that seems to duplicate information already present in a lemma statement. We can facilitate a simpler proof by defining a co-induction principle specialized to goals that begin with single universal quantifiers, and the strategy can be extended in a straightforward way to principles for other counts of quantifiers. (Our [stream_eq_loop] principle is effectively the instantiation of this technique to zero quantifiers.) *)
493 493
494 Section stream_eq_onequant. 494 Section stream_eq_onequant.
495 Variables A B : Set. 495 Variables A B : Type.
496 (** We have the types [A], the domain of the one quantifier; and [B], the type of data found in the streams. *) 496 (** We have the types [A], the domain of the one quantifier; and [B], the type of data found in the streams. *)
497 497
498 Variables f g : A -> stream B. 498 Variables f g : A -> stream B.
499 (** The two streams we compare must be of the forms [f x] and [g x], for some shared [x]. Note that this falls out naturally when [x] is a shared universally quantified variable in a lemma statement. *) 499 (** The two streams we compare must be of the forms [f x] and [g x], for some shared [x]. Note that this falls out naturally when [x] is a shared universally quantified variable in a lemma statement. *)
500 500