The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

±èÇü¼± wrote:
>
> I an wondering how to automate searching process using Ltac.
>
> Can I code a tactic to do searching for past-established theorems,
> instead of manually doing SearchAbouts.
>
> I thought "Hint Resolve" and "auto with ..." did the similar job, but
> they don't seem powerful enough in that I cannot put in keywords to
> narrow down my choices.
>

You are describing a "proof implementation" technique, which might not
be the best match for your overall goal. Perhaps you could give an
example of a class of theorems you want to prove (and some concrete
examples within it), and explain why [auto] isn't working well?