Mercurial > cpdt > repo
diff src/Coinductive.v @ 478:f02b698aadb1
Batch of changes based on proofreader feedback
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 11 Nov 2012 18:17:23 -0500 |
parents | 1fd4109f7b31 |
children | ed829eaa91b2 |
line wrap: on
line diff
--- a/src/Coinductive.v Sun Nov 11 13:36:17 2012 -0500 +++ b/src/Coinductive.v Sun Nov 11 18:17:23 2012 -0500 @@ -617,8 +617,7 @@ cofix; intros; destruct c. rewrite (AssignCase H); constructor. destruct (SeqCase H) as [? [? ?]]; econstructor; eauto. - destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; - [ econstructor | econstructor 4 ]; eauto. + destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto. Qed. End evalCmd_coind. @@ -644,13 +643,12 @@ Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e. induction e; crush; repeat (match goal with - | [ |- context[match ?E with Const _ => _ | Var _ => _ - | Plus _ _ => _ end] ] => destruct E + | [ |- context[match ?E with Const _ => _ | _ => _ end] ] => destruct E | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E end; crush). Qed. -Hint Rewrite optExp_correct . +Hint Rewrite optExp_correct. (** The final theorem is easy to establish, using our co-induction principle and a bit of Ltac smarts that we leave unexplained for now. Curious readers can consult the Coq manual, or wait for the later chapters of this book about proof automation. At a high level, we show inclusions between behaviors, going in both directions between original and optimized programs. *)