Mercurial > cpdt > repo

comparison src/Coinductive.v @ 205:f05514cc6c0d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'make doc' works with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 12:15:05 -0500
parents 8caa3b3f8fc0
children d06726f49bc6
comparison
equal deleted inserted replaced
204:cbf2f74a5130 205:f05514cc6c0d
26 26
27 [[ 27 [[
28 28
29 Fixpoint bad (u : unit) : P := bad u. 29 Fixpoint bad (u : unit) : P := bad u.
30 30
31 ]]
32
31 This would leave us with [bad tt] as a proof of [P]. 33 This would leave us with [bad tt] as a proof of [P].
32 34
33 There are also algorithmic considerations that make universal termination very desirable. We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules. Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps. It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem. 35 There are also algorithmic considerations that make universal termination very desirable. We have seen how tactics like [reflexivity] compare terms up to equivalence under computational rules. Calls to recursive, pattern-matching functions are simplified automatically, with no need for explicit proof steps. It would be very hard to hold onto that kind of benefit if it became possible to write non-terminating programs; we would be running smack into the halting problem.
34 36
35 One solution is to use types to contain the possibility of non-termination. For instance, we can create a "non-termination monad," inside which we must write all of our general-recursive programs. In later chapters, we will spend some time on this idea and its applications. For now, we will just say that it is a heavyweight solution, and so we would like to avoid it whenever possible. 37 One solution is to use types to contain the possibility of non-termination. For instance, we can create a "non-termination monad," inside which we must write all of our general-recursive programs. In later chapters, we will spend some time on this idea and its applications. For now, we will just say that it is a heavyweight solution, and so we would like to avoid it whenever possible.
93 95
94 The restriction for co-inductive types shows up as the %\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts. First, consider this stream definition, which would be legal in Haskell. 96 The restriction for co-inductive types shows up as the %\textit{%#<i>#guardedness condition#</i>#%}%, and it can be broken into two parts. First, consider this stream definition, which would be legal in Haskell.
95 97
96 [[ 98 [[
97 CoFixpoint looper : stream nat := looper. 99 CoFixpoint looper : stream nat := looper.
100
101 ]]
102
98 [[ 103 [[
99 Error: 104 Error:
100 Recursive definition of looper is ill-formed. 105 Recursive definition of looper is ill-formed.
101 In environment 106 In environment
102 looper : stream nat 107 looper : stream nat
103 108
104 unguarded recursive call in "looper" 109 unguarded recursive call in "looper"
110 ]]
111
105 *) 112 *)
106 113
107 114
108 (** 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. 115 (** 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.
109 116
143 150
144 CoFixpoint map' (s : stream A) : stream B := 151 CoFixpoint map' (s : stream A) : stream B :=
145 match s with 152 match s with
146 | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s)) 153 | Cons h t => interleave (Cons (f h) (map' s)) (Cons (f h) (map' s))
147 end. 154 end.
155
156 ]]
148 *) 157 *)
149 158
150 (** 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. 159 (** 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.
151 160
152 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]. *) 161 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]. *)
199 (** It looks like this proof might be easier than we expected! *) 208 (** It looks like this proof might be easier than we expected! *)
200 209
201 assumption. 210 assumption.
202 (** [[ 211 (** [[
203 212
204 Proof completed. *) 213 Proof completed.
214
215 ]] *)
205 216
206 (** Unfortunately, we are due for some disappointment in our victory lap. *) 217 (** Unfortunately, we are due for some disappointment in our victory lap. *)
207 218
208 (** [[ 219 (** [[
209 Qed. 220 Qed.
212 Recursive definition of ones_eq is ill-formed. 223 Recursive definition of ones_eq is ill-formed.
213 224
214 In environment 225 In environment
215 ones_eq : stream_eq ones ones' 226 ones_eq : stream_eq ones ones'
216 227
217 unguarded recursive call in "ones_eq" *) 228 unguarded recursive call in "ones_eq"
229
230 ]] *)
218 231
219 (** 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! 232 (** 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!
220 233
221 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. 234 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.
222 235
223 [[ 236 [[
224 Guarded. 237 Guarded.
238
239 ]]
225 240
226 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]. 241 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].
227 242
228 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. *) 243 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. *)
229 244
310 325
311 Theorem ones_eq' : stream_eq ones ones'. 326 Theorem ones_eq' : stream_eq ones ones'.
312 cofix; crush. 327 cofix; crush.
313 (** [[ 328 (** [[
314 329
315 Guarded. *) 330 Guarded.
331
332 ]] *)
316 Abort. 333 Abort.
317 (* end thide *) 334 (* end thide *)
318 335
319 (** 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. *) 336 (** 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. *)
320 337