comparison src/Coinductive.v @ 63:fe7d37dfbd26

Co-equality
author Adam Chlipala <adamc@hcoop.net>
date Tue, 30 Sep 2008 17:07:57 -0400
parents 437cc4857e2a
children 739c2818d6e2
comparison
equal deleted inserted replaced
62:437cc4857e2a 63:fe7d37dfbd26
141 (** We get another error message about an unguarded recursive call. This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls. The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion. 141 (** We get another error message about an unguarded recursive call. This is because we are violating the second guardedness condition, which says that, not only must co-recursive calls be arguments to constructors, there must also %\textit{%#<i>#not be anything but [match]es and calls to constructors of the same co-inductive type#</i>#%}% wrapped around these immediate uses of co-recursive calls. The actual implemented rule for guardedness is a little more lenient than what we have just stated, but you can count on the illegality of any exception that would enhance the expressive power of co-recursion.
142 142
143 Why enforce a rule like this? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Perhaps this other function might be defined mutually with [map']. It might deconstruct its first argument, retrieving [map' s] from within [Cons (f h) (map' s)]. Next it might try a [match] on this retrieved value, which amounts to deconstructing [map' s]. To figure out how this [match] turns out, we need to know the top-level structure of [map' s], but this is exactly what we started out trying to determine! We run into a loop in the evaluation process, and we have reached a witness of inconsistency if we are evaluating [approx (map' s) 1] for any [s]. *) 143 Why enforce a rule like this? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Perhaps this other function might be defined mutually with [map']. It might deconstruct its first argument, retrieving [map' s] from within [Cons (f h) (map' s)]. Next it might try a [match] on this retrieved value, which amounts to deconstructing [map' s]. To figure out how this [match] turns out, we need to know the top-level structure of [map' s], but this is exactly what we started out trying to determine! We run into a loop in the evaluation process, and we have reached a witness of inconsistency if we are evaluating [approx (map' s) 1] for any [s]. *)
144 End map'. 144 End map'.
145 145
146
147 (** * Infinite Proofs *)
148
149 (** Let us say we want to give two different definitions of a stream of all ones, and then we want to prove that they are equivalent. *)
150
151 CoFixpoint ones : stream nat := Cons 1 ones.
152 Definition ones' := map S zeroes.
153
154 (** The obvious statement of the equality is this: *)
155
156 Theorem ones_eq : ones = ones'.
157
158 (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved. In fact, it is unprovable. The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments. To prove this equivalence, we will need to introduce a new relation. *)
159 Abort.
160
161 (** 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.
162
163 We are ready for our first co-inductive predicate. *)
164
165 Section stream_eq.
166 Variable A : Set.
167
168 CoInductive stream_eq : stream A -> stream A -> Prop :=
169 | Stream_eq : forall h t1 t2,
170 stream_eq t1 t2
171 -> stream_eq (Cons h t1) (Cons h t2).
172 End stream_eq.
173
174 (** We say that two streams are equal if and only if they have the same heads and their tails are equal. We use the normal finite-syntactic equality for the heads, and we refer to our new equality recursively for the tails.
175
176 We can try restating the theorem with [stream_eq]. *)
177
178 Theorem ones_eq : stream_eq ones ones'.
179 (** Coq does not support tactical co-inductive proofs as well as it supports tactical inductive proofs. The usual starting point is the [cofix] tactic, which asks to structure this proof as a co-fixpoint. *)
180 cofix.
181 (** [[
182
183 ones_eq : stream_eq ones ones'
184 ============================
185 stream_eq ones ones'
186 ]] *)
187
188 (** It looks like this proof might be easier than we expected! *)
189
190 assumption.
191 (** [[
192
193 Proof completed. *)
194
195 (** Unfortunately, we are due for some disappointment in our victory lap. *)
196
197 (** [[
198 Qed.
199
200 Error:
201 Recursive definition of ones_eq is ill-formed.
202
203 In environment
204 ones_eq : stream_eq ones ones'
205
206 unguarded recursive call in "ones_eq" *)
207
208 (** Via the Curry-Howard correspondence, the same guardedness condition applies to our co-inductive proofs as to our co-inductive data structures. We should be grateful that this proof is rejected, because, if it were not, the same proof structure could be used to prove any co-inductive theorem vacuously, by direct appeal to itself!
209
210 Thinking about how Coq would generate a proof term from the proof script above, we see that the problem is that we are violating the first part of the guardedness condition. During our proofs, Coq can help us check whether we have yet gone wrong in this way. We can run the command [Guarded] in any context to see if it is possible to finish the proof in a way that will yield a properly guarded proof term.
211
212 [[
213 Guarded.
214
215 Running [Guarded] here gives us the same error message that we got when we tried to run [Qed]. In larger proofs, [Guarded] can be helpful in detecting problems %\textit{%#<i>#before#</i>#%}% we think we are ready to run [Qed].
216
217 We need to start the co-induction by applying one of [stream_eq]'s constructors. To do that, we need to know that both arguments to the predicate are [Cons]es. Informally, this is trivial, but [simpl] is not able to help us. *)
218
219 Undo.
220 simpl.
221 (** [[
222
223 ones_eq : stream_eq ones ones'
224 ============================
225 stream_eq ones ones'
226 ]] *)
227
228 (** It turns out that we are best served by proving an auxiliary lemma. *)
229 Abort.
230
231 (** First, we need to define a function that seems pointless on first glance. *)
232
233 Definition frob A (s : stream A) : stream A :=
234 match s with
235 | Cons h t => Cons h t
236 end.
237
238 (** Next, we need to prove a theorem that seems equally pointless. *)
239
240 Theorem frob_eq : forall A (s : stream A), s = frob s.
241 destruct s; reflexivity.
242 Qed.
243
244 (** But, miraculously, this theorem turns out to be just what we needed. *)
245
246 Theorem ones_eq : stream_eq ones ones'.
247 cofix.
248
249 (** We can use the theorem to rewrite the two streams. *)
250 rewrite (frob_eq ones).
251 rewrite (frob_eq ones').
252 (** [[
253
254 ones_eq : stream_eq ones ones'
255 ============================
256 stream_eq (frob ones) (frob ones')
257 ]] *)
258
259 (** Now [simpl] is able to reduce the streams. *)
260
261 simpl.
262 (** [[
263
264 ones_eq : stream_eq ones ones'
265 ============================
266 stream_eq (Cons 1 ones)
267 (Cons 1
268 ((cofix map (s : stream nat) : stream nat :=
269 match s with
270 | Cons h t => Cons (S h) (map t)
271 end) zeroes))
272 ]] *)
273
274 (** Since we have exposed the [Cons] structure of each stream, we can apply the constructor of [stream_eq]. *)
275
276 constructor.
277 (** [[
278
279 ones_eq : stream_eq ones ones'
280 ============================
281 stream_eq ones
282 ((cofix map (s : stream nat) : stream nat :=
283 match s with
284 | Cons h t => Cons (S h) (map t)
285 end) zeroes)
286 ]] *)
287
288 (** Now, modulo unfolding of the definition of [map], we have matched our assumption. *)
289 assumption.
290 Qed.
291
292 (** Why did this silly-looking trick help? The answer has to do with the constraints placed on Coq's evaluation rules by the need for termination. The [cofix]-related restriction that foiled our first attempt at using [simpl] is dual to a restriction for [fix]. In particular, an application of an anonymous [fix] only reduces when the top-level structure of the recursive argument is known. Otherwise, we would be unfolding the recursive definition ad infinitum.
293
294 Fixpoints only reduce when enough is known about the %\textit{%#<i>#definitions#</i>#%}% of their arguments. Dually, co-fixpoints only reduce when enough is known about %\textit{%#<i>#how their results will be used#</i>#%}%. In particular, a [cofix] is only expanded when it is the discriminee of a [match]. Rewriting with our superficially silly lemma wrapped new [match]es around the two [cofix]es, triggering reduction.
295
296 If [cofix]es reduced haphazardly, it would be easy to run into infinite loops in evaluation, since we are, after all, building infinite objects.
297
298 One common source of difficulty with co-inductive proofs is bad interaction with standard Coq automation machinery. If we try to prove [ones_eq'] with automation, like we have in previous inductive proofs, we get an invalid proof. *)
299
300 Theorem ones_eq' : stream_eq ones ones'.
301 cofix; crush.
302 (** [[
303
304 Guarded. *)
305 Abort.
306
307 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with "hiding" the co-inductive hypothesis. We will see examples of effective co-inductive proving in later chapters. *)