--- a/src/Match.v	Wed Oct 22 14:32:41 2008 -0400
+++ b/src/Match.v	Sun Oct 26 10:28:00 2008 -0400
@@ -28,9 +28,67 @@
 
    The [ring] tactic solves goals by appealing to the axioms of rings or semi-rings (as in algebra), depending on the type involved.  Coq developments may declare new types to be parts of rings and semi-rings by proving the associated axioms.  There is a simlar tactic [field] for simplifying values in fields by conversion to fractions over rings.  Both [ring] and [field] can only solve goals that are equalities.  The [fourier] tactic uses Fourier's method to prove inequalities over real numbers, which are axiomatized in the Coq standard library.
 
-   The %\textit{%#<i>#setoid#</i>#%}% facility makes it possible to register new equivalence relations to be understood by tactics like [rewrite].  For instance, [Prop] is registered as a setoid with the equivalence relation "if and only if."  The ability to register new setoids can be very useful in proofs of a kind common in math, where all reasoning is done after "modding out by a relation."
+   The %\textit{%#<i>#setoid#</i>#%}% facility makes it possible to register new equivalence relations to be understood by tactics like [rewrite].  For instance, [Prop] is registered as a setoid with the equivalence relation "if and only if."  The ability to register new setoids can be very useful in proofs of a kind common in math, where all reasoning is done after "modding out by a relation." *)
 
-   We have seen [auto] and [eauto] put to good use.  Both are based on databases of hints to be applied in Prolog-style logic programming.  The most general form of [auto] hint is [Hint Extern], which takes the form [Hint Extern num pattern => tactic : db].  This command asks to apply [tactic] during an [auto] or [eauto] proof search with database [db], whenever the conclusion matches the pattern.  The pattern may bind variables to be used in the tactic.  The argument [num] assigns a cost to this rule.  When [auto] finds multiple applicable rules at some point during proof search, it tries them in increasing order of cost.  A normal [Hint Resolve lemma] adds [eapply lemma] as a hint with a cost equal to the number of subgoals that would be introduced.
 
-   We have also seen many uses of [autorewrite], which is based on databases of quantified equalities for rewriting.  One feature which we have not focused on, but that is worth mentioning, is that each [Rewrite] hint may specify a tactic to use to discharge any subgoals required by the rewrite lemma.  By choosing a tactic like [solve [ trivial ]], which fails if [trivial] fails to prove the goal completely, we can prevent [autorewrite] from "going down the wrong path." *)
+(** * Hint Databases *)
 
+(** 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.
+
+The basic hints for [auto] and [eauto] are [Hint Immediate lemma], asking to try solving a goal immediately by applying the premise-free lemma; [Resolve lemma], which does the same but may add new premises that are themselves to be subjects of proof search; [Constructor 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.
+
+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. *)
+
+Theorem bool_neq : true <> false.
+  auto.
+  (** [crush] would have discharged this goal, but the default hint database for [auto] contains no hint that applies. *)
+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. *)
+
+Hint Extern 1 (_ <> _) => congruence.
+
+Theorem bool_neq : true <> false.
+  auto.
+Qed.
+
+(** 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]. *)
+
+Section forall_and.
+  Variable A : Set.
+  Variables P Q : A -> Prop.
+
+  Hypothesis both : forall x, P x /\ Q x.
+
+  Theorem forall_and : forall z, P z.
+    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. *)
+
+    Hint Extern 1 (P ?X) =>
+      match goal with
+        | [ H : forall x, P x /\ _ |- _ ] => apply (proj1 (H X))
+      end.
+
+    auto.
+  Qed.
+
+  (** 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]. *)
+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
+    ]]
+
+    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].
+
+    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 later sections of the chapter. *)