Mercurial > cpdt > repo
comparison src/Coinductive.v @ 392:4b1242b277b2
Typo fixes
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Fri, 20 Apr 2012 12:49:47 -0400 |
parents | eb0fa506d04c |
children | 3c941750c347 |
comparison
equal
deleted
inserted
replaced
391:fd3f1057685c | 392:4b1242b277b2 |
---|---|
360 | 360 |
361 (** 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. | 361 (** 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. |
362 | 362 |
363 %\medskip% | 363 %\medskip% |
364 | 364 |
365 Must we always be cautious with automation in proofs by co-induction? Induction seems to have dual versions the same pitfalls inherent in it, and yet we avoid those pitfalls by encapsulating safe Curry-Howard recursion schemes inside named induction principles. It turns out that we can usually do the same with %\index{co-induction principles}\emph{%#<i>#co-induction principles#</i>#%}%. Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq']. | 365 Must we always be cautious with automation in proofs by co-induction? Induction seems to have dual versions of the same pitfalls inherent in it, and yet we avoid those pitfalls by encapsulating safe Curry-Howard recursion schemes inside named induction principles. It turns out that we can usually do the same with %\index{co-induction principles}\emph{%#<i>#co-induction principles#</i>#%}%. Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq']. |
366 | 366 |
367 An induction principle is parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the inductive fact that we already know#</i>#%}%. Dually, a co-induction principle ought to be parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the arguments to the co-inductive predicate that we are trying to prove#</i>#%}%. | 367 An induction principle is parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the inductive fact that we already know#</i>#%}%. Dually, a co-induction principle ought to be parameterized over a predicate characterizing what we mean to prove, %\emph{%#<i>#as a function of the arguments to the co-inductive predicate that we are trying to prove#</i>#%}%. |
368 | 368 |
369 To state a useful principle for [stream_eq], it will be useful first to define the stream head function. *) | 369 To state a useful principle for [stream_eq], it will be useful first to define the stream head function. *) |
370 | 370 |
376 (** 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}%. *) | 376 (** 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}%. *) |
377 | 377 |
378 Section stream_eq_coind. | 378 Section stream_eq_coind. |
379 Variable A : Type. | 379 Variable A : Type. |
380 Variable R : stream A -> stream A -> Prop. | 380 Variable R : stream A -> stream A -> Prop. |
381 (** This relation generalizes the theorem we want to prove, characterizinge exactly which two arguments to [stream_eq] we want to consider. *) | 381 (** This relation generalizes the theorem we want to prove, characterizing exactly which two arguments to [stream_eq] we want to consider. *) |
382 | 382 |
383 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2. | 383 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2. |
384 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2). | 384 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2). |
385 (** 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 a [R] stream pair passes on %``%#"#[R]-ness#"#%''% to its tails. An established technical term for such a relation is %\index{bisimulation}\emph{%#<i>#bisimulation#</i>#%}%. *) | 385 (** 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}\emph{%#<i>#bisimulation#</i>#%}%. *) |
386 | 386 |
387 (** 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. *) | 387 (** 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. *) |
388 | |
388 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2. | 389 Theorem stream_eq_coind : forall s1 s2, R s1 s2 -> stream_eq s1 s2. |
389 cofix; destruct s1; destruct s2; intro. | 390 cofix; destruct s1; destruct s2; intro. |
390 generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq. | 391 generalize (Cons_case_hd H); intro Heq; simpl in Heq; rewrite Heq. |
391 constructor. | 392 constructor. |
392 apply stream_eq_coind. | 393 apply stream_eq_coind. |
393 apply (Cons_case_tl H). | 394 apply (Cons_case_tl H). |
394 Qed. | 395 Qed. |
395 End stream_eq_coind. | 396 End stream_eq_coind. |
396 | 397 |
397 (** To see why this proof is guarded, we can print it and verify that the one co-recursive call is an immediate argument to a constructor. *) | 398 (** To see why this proof is guarded, we can print it and verify that the one co-recursive call is an immediate argument to a constructor. *) |
399 | |
398 Print stream_eq_coind. | 400 Print stream_eq_coind. |
399 | 401 |
400 (** We omit the output and proceed to proving [ones_eq''] again. The only bit of ingenuity is in choosing [R], and in this case the most restrictive predicate works. *) | 402 (** We omit the output and proceed to proving [ones_eq''] again. The only bit of ingenuity is in choosing [R], and in this case the most restrictive predicate works. *) |
401 | 403 |
402 Theorem ones_eq'' : stream_eq ones ones'. | 404 Theorem ones_eq'' : stream_eq ones ones'. |