Mercurial > cpdt > repo
comparison 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 |
comparison
equal
deleted
inserted
replaced
477:6769ef9688f2 | 478:f02b698aadb1 |
---|---|
615 | 615 |
616 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2. | 616 Theorem evalCmd_coind : forall vs1 c vs2, R vs1 c vs2 -> evalCmd vs1 c vs2. |
617 cofix; intros; destruct c. | 617 cofix; intros; destruct c. |
618 rewrite (AssignCase H); constructor. | 618 rewrite (AssignCase H); constructor. |
619 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto. | 619 destruct (SeqCase H) as [? [? ?]]; econstructor; eauto. |
620 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; | 620 destruct (WhileCase H) as [[? ?] | [? [? [? ?]]]]; subst; econstructor; eauto. |
621 [ econstructor | econstructor 4 ]; eauto. | |
622 Qed. | 621 Qed. |
623 End evalCmd_coind. | 622 End evalCmd_coind. |
624 | 623 |
625 (** Now that we have a co-induction principle, we should use it to prove something! Our example is a trivial program optimizer that finds places to replace [0 + e] with [e]. *) | 624 (** Now that we have a co-induction principle, we should use it to prove something! Our example is a trivial program optimizer that finds places to replace [0 + e] with [e]. *) |
626 | 625 |
642 | 641 |
643 (* begin thide *) | 642 (* begin thide *) |
644 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e. | 643 Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e. |
645 induction e; crush; | 644 induction e; crush; |
646 repeat (match goal with | 645 repeat (match goal with |
647 | [ |- context[match ?E with Const _ => _ | Var _ => _ | 646 | [ |- context[match ?E with Const _ => _ | _ => _ end] ] => destruct E |
648 | Plus _ _ => _ end] ] => destruct E | |
649 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E | 647 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E |
650 end; crush). | 648 end; crush). |
651 Qed. | 649 Qed. |
652 | 650 |
653 Hint Rewrite optExp_correct . | 651 Hint Rewrite optExp_correct. |
654 | 652 |
655 (** 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. *) | 653 (** 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. *) |
656 | 654 |
657 Ltac finisher := match goal with | 655 Ltac finisher := match goal with |
658 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; []) | 656 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; []) |