Mercurial > cpdt > repo

comparison src/Coinductive.v @ 440:f923024bd284

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Vertical spacing pass, through end of Subset
author Adam Chlipala <adam@chlipala.net>
date Mon, 30 Jul 2012 16:50:02 -0400
parents 8077352044b2
children 89c67796754e
comparison
equal deleted inserted replaced
439:393b8ed99c2f 440:f923024bd284
27 We spent some time in the last chapter discussing the %\index{Curry-Howard correspondence}%Curry-Howard isomorphism, where proofs are identified with functional programs. In such a setting, infinite loops, intended or otherwise, are disastrous. If Coq allowed the full breadth of definitions that Haskell did, we could code up an infinite loop and use it to prove any proposition vacuously. That is, the addition of general recursion would make CIC _inconsistent_. For an arbitrary proposition [P], we could write: 27 We spent some time in the last chapter discussing the %\index{Curry-Howard correspondence}%Curry-Howard isomorphism, where proofs are identified with functional programs. In such a setting, infinite loops, intended or otherwise, are disastrous. If Coq allowed the full breadth of definitions that Haskell did, we could code up an infinite loop and use it to prove any proposition vacuously. That is, the addition of general recursion would make CIC _inconsistent_. For an arbitrary proposition [P], we could write:
28 [[ 28 [[
29 Fixpoint bad (u : unit) : P := bad u. 29 Fixpoint bad (u : unit) : P := bad u.
30 ]] 30 ]]
31 31
32 This would leave us with [bad tt] as a proof of [P]. 32 %\smallskip{}%This would leave us with [bad tt] as a proof of [P].
33 33
34 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 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 35
36 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; several such approaches are surveyed in Chapter 7. This is a heavyweight solution, and so we would like to avoid it whenever possible. 36 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; several such approaches are surveyed in Chapter 7. This is a heavyweight solution, and so we would like to avoid it whenever possible.
37 37
165 165
166 Section map'. 166 Section map'.
167 Variables A B : Type. 167 Variables A B : Type.
168 Variable f : A -> B. 168 Variable f : A -> B.
169 (* begin thide *) 169 (* begin thide *)
170 (** [[ 170 (** %\vspace{-.15in}%[[
171 CoFixpoint map' (s : stream A) : stream B := 171 CoFixpoint map' (s : stream A) : stream B :=
172 match s with 172 match s with
173 | Cons h t => interleave (Cons (f h) (map' t)) (Cons (f h) (map' t)) 173 | Cons h t => interleave (Cons (f h) (map' t)) (Cons (f h) (map' t))
174 end. 174 end.
175 ]] 175 ]]
176 176 %\vspace{-.15in}%We get another error message about an unguarded recursive call. *)
177 We get another error message about an unguarded recursive call. *)
178 177
179 End map'. 178 End map'.
180 179
181 (** What is going wrong here? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Here is one simpler example demonstrating the essential pitfall. We start defining a standard function for taking the tail of a stream. Since streams are infinite, this operation is total. *) 180 (** What is going wrong here? Imagine that, instead of [interleave], we had called some other, less well-behaved function on streams. Here is one simpler example demonstrating the essential pitfall. We start defining a standard function for taking the tail of a stream. Since streams are infinite, this operation is total. *)
182 181
376 375
377 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. *) 376 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. *)
378 377
379 Theorem ones_eq' : stream_eq ones ones'. 378 Theorem ones_eq' : stream_eq ones ones'.
380 cofix; crush. 379 cofix; crush.
381 (** [[ 380 (** %\vspace{-.25in}%[[
382 Guarded. 381 Guarded.
383 ]] 382 ]]
383 %\vspace{-.25in}%
384 *) 384 *)
385 Abort. 385 Abort.
386 386
387 (** 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. 387 (** 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.
388 388