Mercurial > cpdt > repo

comparison src/Coinductive.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents 549d604c3d16
children eb0fa506d04c
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
617 | Plus _ _ => _ end] ] => destruct E 617 | Plus _ _ => _ end] ] => destruct E
618 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E 618 | [ |- context[match ?E with O => _ | S _ => _ end] ] => destruct E
619 end; crush). 619 end; crush).
620 Qed. 620 Qed.
621 621
622 Hint Rewrite optExp_correct : cpdt. 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. *)
625 625
626 Theorem optCmd_correct : forall vs1 c vs2, evalCmd vs1 c vs2 626 Theorem optCmd_correct : forall vs1 c vs2, evalCmd vs1 c vs2
627 -> evalCmd vs1 (optCmd c) vs2. 627 -> evalCmd vs1 (optCmd c) vs2.