Mercurial > cpdt > repo

comparison src/Coinductive.v @ 384:eb0fa506d04c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Strengthen last theorem of Coinductive
author Adam Chlipala <adam@chlipala.net>
date Sun, 08 Apr 2012 11:11:27 -0400
parents d1276004eec9
children 4b1242b277b2
comparison
equal deleted inserted replaced
383:e2c88317611f 384:eb0fa506d04c
619 end; crush). 619 end; crush).
620 Qed. 620 Qed.
621 621
622 Hint Rewrite optExp_correct . 622 Hint Rewrite optExp_correct .
623 623
624 (** 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. *) 624 (** 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. *)
625 625
626 Theorem optCmd_correct : forall vs1 c vs2, evalCmd vs1 c vs2 626 Ltac finisher := match goal with
627 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; [])
628 || (inversion H; [|])); subst
629 end; crush; eauto 10.
630
631 Lemma optCmd_correct1 : forall vs1 c vs2, evalCmd vs1 c vs2
627 -> evalCmd vs1 (optCmd c) vs2. 632 -> evalCmd vs1 (optCmd c) vs2.
628 intros; apply (evalCmd_coind (fun vs1 c' vs2 => exists c, evalCmd vs1 c vs2 633 intros; apply (evalCmd_coind (fun vs1 c' vs2 => exists c, evalCmd vs1 c vs2
629 /\ c' = optCmd c)); eauto; crush; 634 /\ c' = optCmd c)); eauto; crush;
630 match goal with 635 match goal with
631 | [ H : _ = optCmd ?E |- _ ] => destruct E; simpl in *; discriminate 636 | [ H : _ = optCmd ?E |- _ ] => destruct E; simpl in *; discriminate
632 || injection H; intros; subst 637 || injection H; intros; subst
633 end; match goal with 638 end; finisher.
634 | [ H : evalCmd _ _ _ |- _ ] => ((inversion H; []) 639 Qed.
635 || (inversion H; [|])); subst 640
636 end; crush; eauto 10. 641 Lemma optCmd_correct2 : forall vs1 c vs2, evalCmd vs1 (optCmd c) vs2
642 -> evalCmd vs1 c vs2.
643 intros; apply (evalCmd_coind (fun vs1 c vs2 => evalCmd vs1 (optCmd c) vs2));
644 crush; finisher.
645 Qed.
646
647 Theorem optCmd_correct : forall vs1 c vs2, evalCmd vs1 (optCmd c) vs2
648 <-> evalCmd vs1 c vs2.
649 intuition; apply optCmd_correct1 || apply optCmd_correct2; assumption.
637 Qed. 650 Qed.
638 (* end thide *) 651 (* end thide *)
639 652
640 (** In this form, the theorem tells us that the optimizer preserves observable behavior of both terminating and nonterminating programs, but we did not have to do more work than for the case of terminating programs alone. We merely took the natural inductive definition for terminating executions, made it co-inductive, and applied the appropriate co-induction principle. Curious readers might experiment with adding command constructs like %\texttt{%#<tt>#if#</tt>#%}%; the same proof should continue working, after the co-induction principle is extended to the new evaluation rules. *) 653 (** In this form, the theorem tells us that the optimizer preserves observable behavior of both terminating and nonterminating programs, but we did not have to do more work than for the case of terminating programs alone. We merely took the natural inductive definition for terminating executions, made it co-inductive, and applied the appropriate co-induction principle. Curious readers might experiment with adding command constructs like %\texttt{%#<tt>#if#</tt>#%}%; the same proof script should continue working, after the co-induction principle is extended to the new evaluation rules. *)