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. |