Extern num pattern tactic
This hint type is to extend Auto with tactics other than
Apply and Unfold. For that, we must specify a
cost, a pattern and a tactic to execute. Here is an example:
Hint discr : core := Extern 4 ~(?=?) Discriminate.
Now, when the head of the goal is a disequality, Auto will
try Discriminate if it does not succeed to solve the goal
with hints with a cost less than 4.
One can even use some sub-patterns of the pattern in the tactic
script. A sub-pattern is a question mark followed by a number like
?1 or ?2. Here is an example:
Coq < Require EqDecide.
Coq < Require PolyList.
Coq < Hint eqdec1 : eqdec := Extern 5 {?1=?2}+{~ (?1=?2)}
Coq < Generalize ?1 ?2; Decide Equality.
Coq <
Coq < Goal (a,b:(list nat*nat)){a=b}+{~a=b}.
1 subgoal
============================
(a,b:(list nat*nat)){a=b}+{~a=b}
Coq < Info Auto with eqdec.
== Intro a; Intro b; Generalize a b; Decide Equality; Generalize a0 p;
Decide Equality.
Generalize y0 n0; Decide Equality.
Generalize y n; Decide Equality.
Subtree proved!