Mercurial > cpdt > repo
comparison src/Coinductive.v @ 471:51a8472aca68
Batch of changes based on proofreader feedback
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 08 Oct 2012 16:04:49 -0400 |
parents | f28bdd8414e0 |
children | 1fd4109f7b31 |
comparison
equal
deleted
inserted
replaced
470:0df6dde807ab | 471:51a8472aca68 |
---|---|
55 (* end thide *) | 55 (* end thide *) |
56 (* end hide *) | 56 (* end hide *) |
57 | 57 |
58 (** The definition is surprisingly simple. Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive]. We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite. | 58 (** The definition is surprisingly simple. Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive]. We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite. |
59 | 59 |
60 How do we write down a stream constant? Obviously simple application of constructors is not good enough, since we could only denote finite objects that way. Rather, whereas recursive definitions were necessary to _use_ values of recursive inductive types effectively, here we find that we need%\index{co-recursive definitions}% _co-recursive definitions_ to _build_ values of co-inductive types effectively. | 60 How do we write down a stream constant? Obviously, simple application of constructors is not good enough, since we could only denote finite objects that way. Rather, whereas recursive definitions were necessary to _use_ values of recursive inductive types effectively, here we find that we need%\index{co-recursive definitions}% _co-recursive definitions_ to _build_ values of co-inductive types effectively. |
61 | 61 |
62 We can define a stream consisting only of zeroes.%\index{Vernacular commands!CoFixpoint}% *) | 62 We can define a stream consisting only of zeroes.%\index{Vernacular commands!CoFixpoint}% *) |
63 | 63 |
64 CoFixpoint zeroes : stream nat := Cons 0 zeroes. | 64 CoFixpoint zeroes : stream nat := Cons 0 zeroes. |
65 | 65 |
189 CoFixpoint bad : stream nat := tl (Cons 0 bad). | 189 CoFixpoint bad : stream nat := tl (Cons 0 bad). |
190 ]] | 190 ]] |
191 | 191 |
192 Imagine that Coq had accepted our definition, and consider how we might evaluate [approx bad 1]. We would be trying to calculate the first element in the stream [bad]. However, it is not hard to see that the definition of [bad] "begs the question": unfolding the definition of [tl], we see that we essentially say "define [bad] to equal itself"! Of course such an equation admits no single well-defined solution, which does not fit well with the determinism of Gallina reduction. | 192 Imagine that Coq had accepted our definition, and consider how we might evaluate [approx bad 1]. We would be trying to calculate the first element in the stream [bad]. However, it is not hard to see that the definition of [bad] "begs the question": unfolding the definition of [tl], we see that we essentially say "define [bad] to equal itself"! Of course such an equation admits no single well-defined solution, which does not fit well with the determinism of Gallina reduction. |
193 | 193 |
194 Since Coq can be considered to check definitions after inlining and simplification of previously defined identifiers, the basic guardedness condition rules out our definition of [bad]. Such an inlining reduces [bad] to: | 194 Coq's complete rule for co-recursive definitions includes not just the basic guardedness condition, but also a requirement about where co-recursive calls may occur. In particular, a co-recursive call must be a direct argument to a constructor, _nested only inside of other constructor calls or [fun] or [match] expressions_. In the definition of [bad], we erroneously nested the co-recursive call inside a call to [tl], and we nested inside a call to [interleave] in the definition of [map']. |
195 | |
196 Coq helps the user out a little by performing the guardedness check after using computation to simplify terms. For instance, any co-recursive function definition can be expanded by inserting extra calls to an identity function, and this change preserves guardedness. However, in other cases computational simplification can reveal why definitions are dangerous. Consider what happens when we inline the definition of [tl] in [bad]: | |
195 [[ | 197 [[ |
196 CoFixpoint bad : stream nat := bad. | 198 CoFixpoint bad : stream nat := bad. |
197 ]] | 199 ]] |
198 This is the same looping definition we rejected earlier. A similar inlining process reveals the way that Coq saw our failed definition of [map']: | 200 This is the same looping definition we rejected earlier. A similar inlining process reveals an alternate view on our failed definition of [map']: |
199 [[ | 201 [[ |
200 CoFixpoint map' (s : stream A) : stream B := | 202 CoFixpoint map' (s : stream A) : stream B := |
201 match s with | 203 match s with |
202 | Cons h t => Cons (f h) (Cons (f h) (interleave (map' t) (map' t))) | 204 | Cons h t => Cons (f h) (Cons (f h) (interleave (map' t) (map' t))) |
203 end. | 205 end. |
382 ]] | 384 ]] |
383 %\vspace{-.25in}% | 385 %\vspace{-.25in}% |
384 *) | 386 *) |
385 Abort. | 387 Abort. |
386 | 388 |
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. | 389 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. A correct proof strategy for a theorem like this usually starts 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 | 390 |
389 %\medskip% | 391 %\medskip% |
390 | 392 |
391 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}% _co-induction principles_. Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq']. | 393 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}% _co-induction principles_. Let us take that tack here, so that we can arrive at an [induction x; crush]-style proof for [ones_eq']. |
392 | 394 |
402 (** 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}%. *) |
403 | 405 |
404 Section stream_eq_coind. | 406 Section stream_eq_coind. |
405 Variable A : Type. | 407 Variable A : Type. |
406 Variable R : stream A -> stream A -> Prop. | 408 Variable R : stream A -> stream A -> Prop. |
407 (** This relation generalizes the theorem we want to prove, characterizing exactly which two arguments to [stream_eq] we want to consider. *) | 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. *) |
408 | 410 |
409 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2. | 411 Hypothesis Cons_case_hd : forall s1 s2, R s1 s2 -> hd s1 = hd s2. |
410 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2). | 412 Hypothesis Cons_case_tl : forall s1 s2, R s1 s2 -> R (tl s1) (tl s2). |
411 (** 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_. *) | 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_. *) |
412 | 414 |
492 (** %\vspace{-.15in}%[[ | 494 (** %\vspace{-.15in}%[[ |
493 = 1 :: 2 :: 6 :: 24 :: 120 :: nil | 495 = 1 :: 2 :: 6 :: 24 :: 120 :: nil |
494 : list nat | 496 : list nat |
495 ]] | 497 ]] |
496 | 498 |
497 Now, to prove that the two versions are equivalent, it is helpful to prove (and add as a proof hint) a quick lemma about the computational behavior of [fact]. *) | 499 Now, to prove that the two versions are equivalent, it is helpful to prove (and add as a proof hint) a quick lemma about the computational behavior of [fact]. (I intentionally skip explaining its proof at this point.) *) |
498 | 500 |
499 (* begin thide *) | 501 (* begin thide *) |
500 Lemma fact_def : forall x n, | 502 Lemma fact_def : forall x n, |
501 fact_iter' x (fact n * S n) = fact_iter' x (fact (S n)). | 503 fact_iter' x (fact n * S n) = fact_iter' x (fact (S n)). |
502 simpl; intros; f_equal; ring. | 504 simpl; intros; f_equal; ring. |
545 | 547 |
546 (** * Simple Modeling of Non-Terminating Programs *) | 548 (** * Simple Modeling of Non-Terminating Programs *) |
547 | 549 |
548 (** We close the chapter with a quick motivating example for more complex uses of co-inductive types. We will define a co-inductive semantics for a simple imperative programming language and use that semantics to prove the correctness of a trivial optimization that removes spurious additions by 0. We follow the technique of%\index{co-inductive big-step operational semantics}% _co-inductive big-step operational semantics_ %\cite{BigStep}%. | 550 (** We close the chapter with a quick motivating example for more complex uses of co-inductive types. We will define a co-inductive semantics for a simple imperative programming language and use that semantics to prove the correctness of a trivial optimization that removes spurious additions by 0. We follow the technique of%\index{co-inductive big-step operational semantics}% _co-inductive big-step operational semantics_ %\cite{BigStep}%. |
549 | 551 |
550 We define a suggestive synonym for [nat], as we will consider programs with infinitely many variables, represented as [nat]s. *) | 552 We define a suggestive synonym for [nat], as we will consider programs over infinitely many variables, represented as [nat]s. *) |
551 | 553 |
552 Definition var := nat. | 554 Definition var := nat. |
553 | 555 |
554 (** We define a type [vars] of maps from variables to values. To define a function [set] for setting a variable's value in a map, we use the standard library function [beq_nat] for comparing natural numbers. *) | 556 (** We define a type [vars] of maps from variables to values. To define a function [set] for setting a variable's value in a map, we use the standard library function [beq_nat] for comparing natural numbers. *) |
555 | 557 |
576 Inductive cmd : Set := | 578 Inductive cmd : Set := |
577 | Assign : var -> exp -> cmd | 579 | Assign : var -> exp -> cmd |
578 | Seq : cmd -> cmd -> cmd | 580 | Seq : cmd -> cmd -> cmd |
579 | While : exp -> cmd -> cmd. | 581 | While : exp -> cmd -> cmd. |
580 | 582 |
581 (** We could define an inductive relation to characterize the results of command evaluation. However, such a relation would not capture _nonterminating_ executions. With a co-inductive relation, we can capture both cases. The parameters of the relation are an initial state, a command, and a final state. A program that does not terminate in a particular initial state is related to _any_ final state. *) | 583 (** We could define an inductive relation to characterize the results of command evaluation. However, such a relation would not capture _nonterminating_ executions. With a co-inductive relation, we can capture both cases. The parameters of the relation are an initial state, a command, and a final state. A program that does not terminate in a particular initial state is related to _any_ final state. For more realistic languages than this one, it is often possible for programs to _crash_, in which case a semantics would generally relate their executions to no final states; so relating safely non-terminating programs to all final states provides a crucial distinction. *) |
582 | 584 |
583 CoInductive evalCmd : vars -> cmd -> vars -> Prop := | 585 CoInductive evalCmd : vars -> cmd -> vars -> Prop := |
584 | EvalAssign : forall vs v e, evalCmd vs (Assign v e) (set vs v (evalExp vs e)) | 586 | EvalAssign : forall vs v e, evalCmd vs (Assign v e) (set vs v (evalExp vs e)) |
585 | EvalSeq : forall vs1 vs2 vs3 c1 c2, evalCmd vs1 c1 vs2 | 587 | EvalSeq : forall vs1 vs2 vs3 c1 c2, evalCmd vs1 c1 vs2 |
586 -> evalCmd vs2 c2 vs3 | 588 -> evalCmd vs2 c2 vs3 |