Mercurial > cpdt > repo

comparison src/StackMachine.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 7e57c909f0f2
children cc8d0503619f
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
846 (** This one goes through completely automatically. 846 (** This one goes through completely automatically.
847 847
848 Some code behind the scenes registers [app_assoc_reverse] for use by [crush]. We must register [tconcat_correct] similarly to get the same effect:%\index{Vernacular commands!Hint Rewrite}% *) 848 Some code behind the scenes registers [app_assoc_reverse] for use by [crush]. We must register [tconcat_correct] similarly to get the same effect:%\index{Vernacular commands!Hint Rewrite}% *)
849 849
850 (* begin hide *) 850 (* begin hide *)
851 Hint Rewrite tconcat_correct : cpdt. 851 Hint Rewrite tconcat_correct.
852 (* end hide *) 852 (* end hide *)
853 (** %\noindent%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [tconcat_correct : cpdt.] *) 853 (** %\noindent%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [tconcat_correct.] *)
854 854
855 (** Here we meet the pervasive concept of a %\emph{%#<i>#hint#</i>#%}%. Many proofs can be found through exhaustive enumerations of combinations of possible proof steps; hints provide the set of steps to consider. The tactic [crush] is applying such brute force search for us silently, and it will consider more possibilities as we add more hints. This particular hint asks that the lemma be used for left-to-right rewriting, and we ask for the hint to be added to the hint database called [cpdt], which is the database used by [crush]. In general, segragating hints into different databases is helpful to control the performance of proof search, in cases where domain knowledge allows us to narrow the set of proof steps to be considered in brute force search. Part III of this book considers such pragmatic aspects of proof search in much more detail. 855 (** Here we meet the pervasive concept of a %\emph{%#<i>#hint#</i>#%}%. Many proofs can be found through exhaustive enumerations of combinations of possible proof steps; hints provide the set of steps to consider. The tactic [crush] is applying such brute force search for us silently, and it will consider more possibilities as we add more hints. This particular hint asks that the lemma be used for left-to-right rewriting, and we ask for the hint to be added to the hint database called [cpdt], which is the database used by [crush]. In general, segragating hints into different databases is helpful to control the performance of proof search, in cases where domain knowledge allows us to narrow the set of proof steps to be considered in brute force search. Part III of this book considers such pragmatic aspects of proof search in much more detail.
856 856
857 Now we are ready to return to [tcompile_correct'], proving it automatically this time. *) 857 Now we are ready to return to [tcompile_correct'], proving it automatically this time. *)
858 858
862 Qed. 862 Qed.
863 863
864 (** We can register this main lemma as another hint, allowing us to prove the final theorem trivially. *) 864 (** We can register this main lemma as another hint, allowing us to prove the final theorem trivially. *)
865 865
866 (* begin hide *) 866 (* begin hide *)
867 Hint Rewrite tcompile_correct' : cpdt. 867 Hint Rewrite tcompile_correct'.
868 (* end hide *) 868 (* end hide *)
869 (** %\noindent%[Hint ]%\coqdockw{%#<tt>#Rewrite#</tt>#%}%[ tcompile_correct' : cpdt.] *) 869 (** %\noindent%[Hint ]%\coqdockw{%#<tt>#Rewrite#</tt>#%}%[ tcompile_correct'.] *)
870 870
871 Theorem tcompile_correct : forall t (e : texp t), 871 Theorem tcompile_correct : forall t (e : texp t),
872 tprogDenote (tcompile e nil) tt = (texpDenote e, tt). 872 tprogDenote (tcompile e nil) tt = (texpDenote e, tt).
873 crush. 873 crush.
874 Qed. 874 Qed.