Mercurial > cpdt > repo
comparison src/Coinductive.v @ 475:1fd4109f7b31
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 22 Oct 2012 14:23:52 -0400 |
| parents | 51a8472aca68 |
| children | f02b698aadb1 |
comparison
equal
deleted
inserted
replaced
| 474:d9e1fb184672 | 475:1fd4109f7b31 |
|---|---|
| 175 ]] | 175 ]] |
| 176 %\vspace{-.15in}%We get another error message about an unguarded recursive call. *) | 176 %\vspace{-.15in}%We get another error message about an unguarded recursive call. *) |
| 177 | 177 |
| 178 End map'. | 178 End map'. |
| 179 | 179 |
| 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. *) | 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 by defining a standard function for taking the tail of a stream. Since streams are infinite, this operation is total. *) |
| 181 | 181 |
| 182 Definition tl A (s : stream A) : stream A := | 182 Definition tl A (s : stream A) : stream A := |
| 183 match s with | 183 match s with |
| 184 | Cons _ s' => s' | 184 | Cons _ s' => s' |
| 185 end. | 185 end. |
| 404 (** 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}%. *) | 404 (** 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}%. *) |
| 405 | 405 |
| 406 Section stream_eq_coind. | 406 Section stream_eq_coind. |
| 407 Variable A : Type. | 407 Variable A : Type. |
| 408 Variable R : stream A -> stream A -> Prop. | 408 Variable R : stream A -> stream A -> Prop. |
| 409 | |
| 409 (** This relation generalizes the theorem we want to prove, defining a set of pairs of streams that we must eventually prove contains the particular pair we care about. *) | 410 (** This relation generalizes the theorem we want to prove, defining a set of pairs of streams that we must eventually prove contains the particular pair we care about. *) |
| 410 | 411 |
| 411 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2. | 412 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2. |
| 412 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2). | 413 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2). |
| 414 | |
| 413 (** Two hypotheses characterize what makes a good choice of [R]: it enforces equality of stream heads, and it is %``%#<i>#hereditary#</i>#%''% in the sense that an [R] stream pair passes on "[R]-ness" to its tails. An established technical term for such a relation is%\index{bisimulation}% _bisimulation_. *) | 415 (** Two hypotheses characterize what makes a good choice of [R]: it enforces equality of stream heads, and it is %``%#<i>#hereditary#</i>#%''% in the sense that an [R] stream pair passes on "[R]-ness" to its tails. An established technical term for such a relation is%\index{bisimulation}% _bisimulation_. *) |
| 414 | 416 |
| 415 (** Now it is straightforward to prove the principle, which says that any stream pair in [R] is equal. The reader may wish to step through the proof script to see what is going on. *) | 417 (** Now it is straightforward to prove the principle, which says that any stream pair in [R] is equal. The reader may wish to step through the proof script to see what is going on. *) |
| 416 | 418 |
| 417 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2. | 419 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2. |