Mercurial > cpdt > repo
changeset 375:d1276004eec9
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 | f3146d40c2a1 |
| children | 3b36b1e05b4e |
| files | src/Coinductive.v src/CpdtTactics.v src/DataStruct.v src/GeneralRec.v src/Generic.v src/InductiveTypes.v src/Large.v src/LogicProg.v src/MoreDep.v src/Predicates.v src/StackMachine.v |
| diffstat | 11 files changed, 81 insertions(+), 75 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Coinductive.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/Coinductive.v Mon Mar 26 16:55:59 2012 -0400 @@ -619,7 +619,7 @@ end; crush). Qed. -Hint Rewrite optExp_correct : cpdt. +Hint Rewrite optExp_correct . (** 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. *)
--- a/src/CpdtTactics.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/CpdtTactics.v Mon Mar 26 16:55:59 2012 -0400 @@ -81,11 +81,11 @@ | [ H : _ |- _ ] => rewrite H; auto; [idtac] end. -Ltac rewriterP := repeat (rewriteHyp; autorewrite with cpdt in *). +Ltac rewriterP := repeat (rewriteHyp; autorewrite with core in *). -Ltac rewriter := autorewrite with cpdt in *; rewriterP. +Ltac rewriter := autorewrite with core in *; rewriterP. -Hint Rewrite app_ass : cpdt. +Hint Rewrite app_ass. Definition done (T : Type) (x : T) := True. @@ -130,7 +130,7 @@ Ltac crush' lemmas invOne := let sintuition := simpl in *; intuition; try subst; repeat (simplHyp invOne; intuition; try subst); try congruence in - let rewriter := autorewrite with cpdt in *; + let rewriter := autorewrite with core in *; repeat (match goal with | [ H : ?P |- _ ] => match P with @@ -139,7 +139,7 @@ || (rewrite H; [ | solve [ crush' lemmas invOne ] ]) || (rewrite H; [ | solve [ crush' lemmas invOne ] | solve [ crush' lemmas invOne ] ]) end - end; autorewrite with cpdt in *) + end; autorewrite with core in *) in (sintuition; rewriter; match lemmas with | false => idtac
--- a/src/DataStruct.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/DataStruct.v Mon Mar 26 16:55:59 2012 -0400 @@ -838,7 +838,7 @@ Theorem cfold_correct : forall t (e : exp' t), exp'Denote (cfold e) = exp'Denote e. (* begin thide *) - Hint Rewrite cfoldCond_correct : cpdt. + Hint Rewrite cfoldCond_correct. Hint Resolve cond_ext. induction e; crush;
--- a/src/GeneralRec.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/GeneralRec.v Mon Mar 26 16:55:59 2012 -0400 @@ -696,7 +696,7 @@ simpl; findDestr; reflexivity. Qed. -Hint Rewrite TBind_Answer : cpdt. +Hint Rewrite TBind_Answer. (** printing exists $\exists$ *) @@ -723,7 +723,7 @@ | EvalAnswer : forall x, eval (Answer x) x | EvalThink : forall m x, eval m x -> eval (Think m) x. -Hint Rewrite frob_eq : cpdt. +Hint Rewrite frob_eq. Lemma eval_frob : forall A (c : thunk A) x, eval (frob c) x
--- a/src/Generic.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/Generic.v Mon Mar 26 16:55:59 2012 -0400 @@ -586,7 +586,7 @@ Restart. - Hint Rewrite hget_hmake : cpdt. + Hint Rewrite hget_hmake. Hint Resolve foldr_plus. unfold size; intros; pattern v; apply dok; crush. @@ -605,7 +605,7 @@ (* begin thide *) (** Let us begin as we did in the last theorem, after adding another useful library equality as a hint. *) - Hint Rewrite hget_hmap : cpdt. + Hint Rewrite hget_hmap. unfold map; intros; pattern v; apply dok; crush. (** %\vspace{-.15in}%[[
--- a/src/InductiveTypes.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/InductiveTypes.v Mon Mar 26 16:55:59 2012 -0400 @@ -420,9 +420,9 @@ = plus (nsize tr2) (nsize tr1). (* begin thide *) (* begin hide *) - Hint Rewrite n_plus_O plus_assoc : cpdt. + Hint Rewrite n_plus_O plus_assoc. (* end hide *) - (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [n_plus_O plus_assoc : cpdt.] *) + (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [n_plus_O plus_assoc.] *) induction tr1; crush. Qed. @@ -1125,9 +1125,9 @@ = plus (ntsize tr2) (ntsize tr1). (* begin thide *) (* begin hide *) - Hint Rewrite plus_S : cpdt. + Hint Rewrite plus_S. (* end hide *) - (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [plus_S : cpdt.] *) + (** [Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [plus_S.] *) (** We know that the standard induction principle is insufficient for the task, so we need to provide a %\index{tactics!using}%[using] clause for the [induction] tactic to specify our alternate principle. *)
--- a/src/Large.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/Large.v Mon Mar 26 16:55:59 2012 -0400 @@ -208,7 +208,7 @@ Reset eval_times. -Hint Rewrite mult_plus_distr_l : cpdt. +Hint Rewrite mult_plus_distr_l. Theorem eval_times : forall k e, eval (times k e) = k * eval e. @@ -421,7 +421,7 @@ crush. Qed. -Hint Rewrite confounder : cpdt. +Hint Rewrite confounder. Theorem reassoc_correct : forall e, eval (reassoc e) = eval e. (* begin thide *) @@ -468,19 +468,19 @@ Undo. info t. (** %\vspace{-.15in}%[[ - == simpl in *; intuition; subst; autorewrite with cpdt in *; - simpl in *; intuition; subst; autorewrite with cpdt in *; + == simpl in *; intuition; subst; autorewrite with core in *; + simpl in *; intuition; subst; autorewrite with core in *; simpl in *; intuition; subst; destruct (reassoc e2). simpl in *; intuition. simpl in *; intuition. - simpl in *; intuition; subst; autorewrite with cpdt in *; + simpl in *; intuition; subst; autorewrite with core in *; refine (eq_ind_r (fun n : nat => n * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2) _ IHe1); - autorewrite with cpdt in *; simpl in *; intuition; - subst; autorewrite with cpdt in *; simpl in *; + autorewrite with core in *; simpl in *; intuition; + subst; autorewrite with core in *; simpl in *; intuition; subst. ]] @@ -491,15 +491,15 @@ (** We arbitrarily split the script into chunks. The first few seem not to do any harm. *) - simpl in *; intuition; subst; autorewrite with cpdt in *. - simpl in *; intuition; subst; autorewrite with cpdt in *. + simpl in *; intuition; subst; autorewrite with core in *. + simpl in *; intuition; subst; autorewrite with core in *. simpl in *; intuition; subst; destruct (reassoc e2). simpl in *; intuition. simpl in *; intuition. (** The next step is revealed as the culprit, bringing us to the final unproved subgoal. *) - simpl in *; intuition; subst; autorewrite with cpdt in *. + simpl in *; intuition; subst; autorewrite with core in *. (** We can split the steps further to assign blame. *) @@ -508,13 +508,13 @@ simpl in *. intuition. subst. - autorewrite with cpdt in *. + autorewrite with core in *. (** It was the final of these four tactics that made the rewrite. We can find out exactly what happened. The [info] command presents hierarchical views of proof steps, and we can zoom down to a lower level of detail by applying [info] to one of the steps that appeared in the original trace. *) Undo. - info autorewrite with cpdt in *. + info autorewrite with core in *. (** %\vspace{-.15in}%[[ == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _ (confounder (reassoc e1) e3 e4)).
--- a/src/LogicProg.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/LogicProg.v Mon Mar 26 16:55:59 2012 -0400 @@ -781,11 +781,11 @@ (** * More on [auto] Hints *) -(** Another class of built-in tactics includes [auto], [eauto], and [autorewrite]. These are based on %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. These tactics are important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments. +(** Let us stop at this point and take stock of the possibilities for [auto] and [eauto] hints. Hints are contained within %\textit{%#<i>#hint databases#</i>#%}%, which we have seen extended in many examples so far. When no hint database is specified, a default database is used. Hints in the default database are always used by [auto] or [eauto]. The chance to extend hint databases imperatively is important, because, in Ltac programming, we cannot create %``%#"#global variables#"#%''% whose values can be extended seamlessly by different modules in different source files. We have seen the advantages of hints so far, where [crush] can be defined once and for all, while still automatically applying the hints we add throughout developments. In fact, [crush] is defined in terms of [auto], which explains how we achieve this extensibility. Other user-defined tactics can take similar advantage of [auto] and [eauto]. -The basic hints for [auto] and [eauto] are [Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; [Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; [Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and [Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db]. This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5. +The basic hints for [auto] and [eauto] are %\index{Vernacular commands!Hint Immediate}%[Hint Immediate lemma], asking to try solving a goal immediately by applying a lemma and discharging any hypotheses with a single proof step each; %\index{Vernacular commands!Hint Resolve}%[Resolve lemma], which does the same but may add new premises that are themselves to be subjects of nested proof search; %\index{Vernacular commands!Hint Constructors}%[Constructors type], which acts like [Resolve] applied to every constructor of an inductive type; and %\index{Vernacular commands!Hint Unfold}%[Unfold ident], which tries unfolding [ident] when it appears at the head of a proof goal. Each of these [Hint] commands may be used with a suffix, as in [Hint Resolve lemma : my_db]. This adds the hint only to the specified database, so that it would only be used by, for instance, [auto with my_db]. An additional argument to [auto] specifies the maximum depth of proof trees to search in depth-first order, as in [auto 8] or [auto 8 with my_db]. The default depth is 5. -All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few examples should do best to explain how [Hint Extern] works. *) +All of these [Hint] commands can be issued alternatively with a more primitive hint kind, [Extern]. A few more examples of [Hint Extern] should illustrate more of the possibilities. *) Theorem bool_neq : true <> false. (* begin thide *) @@ -795,7 +795,7 @@ Abort. -(** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove. Luckily, a simpler form suffices. *) +(** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove. Luckily, a simpler form suffices, by appealing to the built-in tactic %\index{tactics!congruence}%[congruence], a complete procedure for the theory of equality, uninterpreted functions, and datatype constructors. *) Hint Extern 1 (_ <> _) => congruence. @@ -804,9 +804,7 @@ Qed. (* end thide *) -(** Our hint says: %``%#"#whenever the conclusion matches the pattern [_ <> _], try applying [congruence].#"#%''% The [1] is a cost for this rule. During proof search, whenever multiple rules apply, rules are tried in increasing cost order, so it pays to assign high costs to relatively expensive [Extern] hints. - -[Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *) +(** [Extern] hints may be implemented with the full Ltac language. This example shows a case where a hint uses a [match]. *) Section forall_and. Variable A : Set. @@ -818,7 +816,7 @@ (* begin thide *) crush. - (** [crush] makes no progress beyond what [intros] would have accomplished. [auto] will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal. However, we can teach [auto] to handle this kind of goal. *) + (** The [crush] invocation makes no progress beyond what [intros] would have accomplished. An [auto] invocation will not apply the hypothesis [both] to prove the goal, because the conclusion of [both] does not unify with the conclusion of the goal. However, we can teach [auto] to handle this kind of goal. *) Hint Extern 1 (P ?X) => match goal with @@ -829,32 +827,38 @@ Qed. (* end thide *) - (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. [proj1] is a function from the standard library for extracting a proof of [R] from a proof of [R /\ S]. *) + (** We see that an [Extern] pattern may bind unification variables that we use in the associated tactic. The function [proj1] is from the standard library, for extracting a proof of [R] from a proof of [R /\ S]. *) End forall_and. (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P]. - [[ Hint Extern 1 (?P ?X) => match goal with | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X)) end. +]] +<< +User error: Bound head variable +>> -User error: Bound head variable - - ]] + Coq's [auto] hint databases work as tables mapping %\index{head symbol}\textit{%#<i>#head symbols#</i>#%}% to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P]. - Coq's [auto] hint databases work as tables mapping %\textit{%#<i>#head symbols#</i>#%}% to lists of tactics to try. Because of this, the constant head of an [Extern] pattern must be determinable statically. In our first [Extern] hint, the head symbol was [not], since [x <> y] desugars to [not (eq x y)]; and, in the second example, the head symbol was [P]. + Fortunately, a more basic form of [Hint Extern] also applies. We may simply leave out the pattern to the left of the [=>], incorporating the corresponding logic into the Ltac script. *) - This restriction on [Extern] hints is the main limitation of the [auto] mechanism, preventing us from using it for general context simplifications that are not keyed off of the form of the conclusion. This is perhaps just as well, since we can often code more efficient tactics with specialized Ltac programs, and we will see how in the next chapter. *) +Hint Extern 1 => + match goal with + | [ H : forall x, ?P x /\ _ |- ?P ?X ] => apply (proj1 (H X)) + end. + +(** Be forewarned that a [Hint Extern] of this kind will be applied at %\emph{%#<i>#every#</i>#%}% node of a proof tree, so an expensive Ltac script may slow proof search significantly. *) (** * Rewrite Hints *) - (** We have used [Hint Rewrite] in many examples so far. [crush] uses these hints by calling [autorewrite]. Our rewrite hints have taken the form [Hint Rewrite lemma : cpdt], adding them to the [cpdt] rewrite database. This is because, in contrast to [auto], [autorewrite] has no default database. Thus, we set the convention that [crush] uses the [cpdt] database. +(** Another dimension of extensibility with hints is rewriting with quantified equalities. We have used the associated command %\index{Vernacular commands!Hint Rewrite}%[Hint Rewrite] in many examples so far. The [crush] tactic uses these hints by calling the built-in tactic %\index{tactics!autorewrite}%[autorewrite]. Our rewrite hints have taken the form [Hint Rewrite lemma], which by default adds them to the default hint database [core]; but alternate hint databases may also be specified just as with, e.g., [Hint Resolve]. - This example shows a direct use of [autorewrite]. *) + The next example shows a direct use of [autorewrite]. Note that, while [Hint Rewrite] uses a default database, [autorewrite] requires that a database be named. *) Section autorewrite. Variable A : Set. @@ -862,10 +866,10 @@ Hypothesis f_f : forall x, f (f x) = f x. - Hint Rewrite f_f : my_db. + Hint Rewrite f_f. Lemma f_f_f : forall x, f (f (f x)) = f x. - intros; autorewrite with my_db; reflexivity. + intros; autorewrite with core; reflexivity. Qed. (** There are a few ways in which [autorewrite] can lead to trouble when insufficient care is taken in choosing hints. First, the set of hints may define a nonterminating rewrite system, in which case invocations to [autorewrite] may not terminate. Second, we may add hints that %``%#"#lead [autorewrite] down the wrong path.#"#%''% For instance: *) @@ -873,10 +877,10 @@ Section garden_path. Variable g : A -> A. Hypothesis f_g : forall x, f x = g x. - Hint Rewrite f_g : my_db. + Hint Rewrite f_g. Lemma f_f_f' : forall x, f (f (f x)) = f x. - intros; autorewrite with my_db. + intros; autorewrite with core. (** [[ ============================ g (g (g x)) = g x @@ -889,16 +893,16 @@ Reset garden_path. - (** [autorewrite] also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *) + (** The [autorewrite] tactic also works with quantified equalities that include additional premises, but we must be careful to avoid similar incorrect rewritings. *) Section garden_path. Variable P : A -> Prop. Variable g : A -> A. Hypothesis f_g : forall x, P x -> f x = g x. - Hint Rewrite f_g : my_db. + Hint Rewrite f_g. Lemma f_f_f' : forall x, f (f (f x)) = f x. - intros; autorewrite with my_db. + intros; autorewrite with core. (** [[ ============================ @@ -926,35 +930,37 @@ Variable g : A -> A. Hypothesis f_g : forall x, P x -> f x = g x. (* begin thide *) - Hint Rewrite f_g using assumption : my_db. + Hint Rewrite f_g using assumption. (* end thide *) Lemma f_f_f' : forall x, f (f (f x)) = f x. (* begin thide *) - intros; autorewrite with my_db; reflexivity. + intros; autorewrite with core; reflexivity. Qed. (* end thide *) - (** [autorewrite] will still use [f_g] when the generated premise is among our assumptions. *) + (** We may still use [autorewrite] to apply [f_g] when the generated premise is among our assumptions. *) Lemma f_f_f_g : forall x, P x -> f (f x) = g x. (* begin thide *) - intros; autorewrite with my_db; reflexivity. + intros; autorewrite with core; reflexivity. (* end thide *) Qed. End garden_path. (** remove printing * *) - (** It can also be useful to use the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *) + (** It can also be useful to apply the [autorewrite with db in *] form, which does rewriting in hypotheses, as well as in the conclusion. *) (** printing * $*$ *) Lemma in_star : forall x y, f (f (f (f x))) = f (f y) -> f x = f (f (f y)). (* begin thide *) - intros; autorewrite with my_db in *; assumption. + intros; autorewrite with core in *; assumption. (* end thide *) Qed. End autorewrite. + +(** Many proofs can be automated in pleasantly modular ways with deft combination of [auto] and [autorewrite]. *)
--- a/src/MoreDep.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/MoreDep.v Mon Mar 26 16:55:59 2012 -0400 @@ -860,7 +860,7 @@ induction s; substring. Qed. -Hint Rewrite substring_all substring_none : cpdt. +Hint Rewrite substring_all substring_none. Lemma substring_split : forall s m, substring 0 m s ++ substring m (length s - m) s = s. @@ -883,12 +883,12 @@ Lemma substring_app_snd : forall s2 s1 n, length s1 = n -> substring n (length (s1 ++ s2) - n) (s1 ++ s2) = s2. - Hint Rewrite <- minus_n_O : cpdt. + Hint Rewrite <- minus_n_O. induction s1; crush. Qed. -Hint Rewrite substring_app_fst substring_app_snd using solve [trivial] : cpdt. +Hint Rewrite substring_app_fst substring_app_snd using solve [trivial]. (* end hide *) (** A few auxiliary functions help us in our final matcher definition. The function [split] will be used to implement the regexp concatenation case. *) @@ -946,7 +946,7 @@ induction s; crush. Qed. -Hint Rewrite app_empty_end : cpdt. +Hint Rewrite app_empty_end. Lemma substring_self : forall s n, n <= 0 @@ -960,12 +960,12 @@ induction s; substring. Qed. -Hint Rewrite substring_self substring_empty using omega : cpdt. +Hint Rewrite substring_self substring_empty using omega. Lemma substring_split' : forall s n m, substring n m s ++ substring (n + m) (length s - (n + m)) s = substring n (length s - n) s. - Hint Rewrite substring_split : cpdt. + Hint Rewrite substring_split. induction s; substring. Qed. @@ -1020,7 +1020,7 @@ Qed. Hint Rewrite substring_stack substring_stack' substring_suffix - using omega : cpdt. + using omega. Lemma minus_minus : forall n m1 m2, m1 + m2 <= n @@ -1032,7 +1032,7 @@ intros; omega. Qed. -Hint Rewrite minus_minus using omega : cpdt. +Hint Rewrite minus_minus using omega. (* end hide *) (** One more helper function will come in handy: [dec_star], for implementing another linear search through ways of splitting a string, this time for implementing the Kleene star. *) @@ -1098,7 +1098,7 @@ \/ exists l, l < length s - n /\ P (substring n (S l) s) /\ star P (substring (n + S l) (length s - (n + S l)) s). - Hint Rewrite plus_n_Sm' : cpdt. + Hint Rewrite plus_n_Sm'. intros; match goal with
--- a/src/Predicates.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/Predicates.v Mon Mar 26 16:55:59 2012 -0400 @@ -364,9 +364,9 @@ length ls1 = length ls2 \/ length ls1 + length ls2 = 6 -> length (ls1 ++ ls2) = 6 \/ length ls1 = length ls2. (* begin hide *) - Hint Rewrite app_length : cpdt. + Hint Rewrite app_length. (* end hide *) -(** %\hspace{.075in}%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [app_length : cpdt.] *) +(** %\hspace{.075in}%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [app_length.] *) crush. Qed. @@ -637,7 +637,7 @@ (* end thide *) Qed. -(** It is not hard to see that sequences of constructor applications like the above can get tedious. We can avoid them using Coq's hint facility, with a new [Hint] variant that asks to consider all constructors of an inductive type during proof search. Note that this sort of hint may be placed in a default database, such that a command has no equivalent to the [: cpdt] from our earlier rewrite hints.%\index{Hint Constructirs}% The tactic %\index{tactics!auto}%[auto] performs exhaustive proof search up to a fixed depth, considering only the proof steps we have registered as hints. *) +(** It is not hard to see that sequences of constructor applications like the above can get tedious. We can avoid them using Coq's hint facility, with a new [Hint] variant that asks to consider all constructors of an inductive type during proof search. The tactic %\index{tactics!auto}%[auto] performs exhaustive proof search up to a fixed depth, considering only the proof steps we have registered as hints. *) (* begin thide *) (* begin hide *) @@ -872,9 +872,9 @@ (** %\hspace{-.075in}\coqdockw{%#<tt>#Restart#</tt>#%}%[.] *) (* begin hide *) - Hint Rewrite <- plus_n_Sm : cpdt. + Hint Rewrite <- plus_n_Sm. (* end hide *) -(** %\hspace{-.075in}%[Hint] %\noindent\coqdockw{%#<tt>#Rewrite#</tt>#%}% [<- plus_n_sm : cpdt.] *) +(** %\hspace{-.075in}%[Hint] %\noindent\coqdockw{%#<tt>#Rewrite#</tt>#%}% [<- plus_n_sm.] *) induction 1; crush; match goal with
--- a/src/StackMachine.v Mon Mar 26 16:24:19 2012 -0400 +++ b/src/StackMachine.v Mon Mar 26 16:55:59 2012 -0400 @@ -848,9 +848,9 @@ 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}% *) (* begin hide *) -Hint Rewrite tconcat_correct : cpdt. +Hint Rewrite tconcat_correct. (* end hide *) -(** %\noindent%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [tconcat_correct : cpdt.] *) +(** %\noindent%[Hint] %\coqdockw{%#<tt>#Rewrite#</tt>#%}% [tconcat_correct.] *) (** 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. @@ -864,9 +864,9 @@ (** We can register this main lemma as another hint, allowing us to prove the final theorem trivially. *) (* begin hide *) -Hint Rewrite tcompile_correct' : cpdt. +Hint Rewrite tcompile_correct'. (* end hide *) -(** %\noindent%[Hint ]%\coqdockw{%#<tt>#Rewrite#</tt>#%}%[ tcompile_correct' : cpdt.] *) +(** %\noindent%[Hint ]%\coqdockw{%#<tt>#Rewrite#</tt>#%}%[ tcompile_correct'.] *) Theorem tcompile_correct : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt).