Finish pass over LogicProg; change [crush] to take advantage of new [Hint...

Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default

src/Coinductive.v

@@ -619,7 +619,7 @@ Lemma optExp_correct : forall vs e, evalExp vs (optExp e) = evalExp vs e.
             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. *)
 

src/CpdtTactics.v

@@ -81,11 +81,11 @@ Ltac rewriteHyp :=
     | [ 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 @@ Require Import JMeq.
 
 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 @@ Ltac crush' lemmas invOne :=
                       || (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

src/DataStruct.v

@@ -838,7 +838,7 @@ Qed.
 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;

src/GeneralRec.v

@@ -696,7 +696,7 @@ Lemma TBind_Answer : forall (A B : Type) (v : A) (m2 : A -> thunk B),
     simpl; findDestr; reflexivity.
 Qed.
 
-Hint Rewrite TBind_Answer : cpdt.
+Hint Rewrite TBind_Answer.
 
 (** printing exists $\exists$ *)
 
@@ -723,7 +723,7 @@ Inductive eval A : thunk A -> A -> Prop :=
 | 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

src/Generic.v

@@ -586,7 +586,7 @@ Error: Impossible to unify "datatypeDenoteOk dd" with
 
   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 @@ Theorem map_id : forall T dt
 (* 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}%[[

src/InductiveTypes.v

@@ -420,9 +420,9 @@ Theorem nsize_nsplice : forall tr1 tr2 : nat_btree, nsize (nsplice tr1 tr2)
   = 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 @@ Theorem ntsize_ntsplice : forall tr1 tr2 : nat_tree, ntsize (ntsplice tr1 tr2)
   = 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. *)
 

src/Large.v

@@ -208,7 +208,7 @@ Qed.
 
 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 @@ Theorem confounder : forall e1 e2 e3,
   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 @@ Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
   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 @@ Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
 
   (** 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 @@ Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
   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)).

src/MoreDep.v

@@ -860,7 +860,7 @@ Lemma substring_none : forall s n,
   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 @@ Qed.
 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 @@ Lemma app_empty_end : forall s, s ++ "" = s.
   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 @@ Lemma substring_empty : forall s n m,
   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 @@ Lemma substring_suffix_emp : forall s n m,
 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 @@ Lemma plus_n_Sm' : forall n m : nat, S (n + m) = m + S n.
   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 @@ Section dec_star.
     \/ 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

src/Predicates.v

@@ -364,9 +364,9 @@ We see that there are two ways to prove a disjunction: prove the first disjunct
     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 @@ Theorem even_4 : even 4.
 (* 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 @@ Lemma even_contra' : forall n', even n' -> forall n, n' = S (n + n) -> False.
 (** %\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

src/StackMachine.v

@@ -848,9 +848,9 @@ Qed.
 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 @@ Qed.
 (** 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).