The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Michael,

Le 30 mars 10 à 07:47, Michael Day a écrit :

> Hi Adam,
>
> > I'm pretty sure [crush] will solve any goal that [auto] can,  
> > because [crush] calls [intuition], which calls [auto].  [eauto] is  
> > a different story, which, like Adam Koprowski suggested, I leave  
> > out because it can increase proof search time dramatically.
>
> Thanks, that makes sense. Having run into a few situations now where  
> eauto is too eager and grabs the wrong hypothesis, perhaps it is  
> good to have them as separate tactics.
>
> Oh, do you have any suggestion as to how to make crush apply  
> app_eq_nil in hypotheses using hints by any chance? :)

The [auto] resolution tactic does not support hints that change the  
hypotheses currently.
It keeps an index of the hypotheses that can be applied at the  
beginning of a search and
updates it only when [intro]ducing new ones, not if the hypotheses  
change by other means.
This limitation is lifted in the typeclass resolution tactic  
[typeclasses eauto with ...]
where that index is rebuilt each time the hypotheses change.

Hope this helps,
-- Matthieu