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