Mercurial > cpdt > repo

comparison src/Coinductive.v @ 478:f02b698aadb1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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; [])