The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

People comparing Coq to Isabelle seem most frequently to say that 
Isabelle has much better automation.  It seems to me that what is 
missing to make Coq as easy to use "out of the box" is a 
forward-chaining version of the 'auto' family of tactics.  That is, 
there ought to be a way to register lemmas that are applied based on 
pattern matching in hypotheses rather than goals.

I think this "forward auto" could work fine without any backtracking. 
I'm envisioning adding tactics like 'inversion', 'injection', and 
'discriminate' as "forward auto" hints.  In other words, these are 
"simplifications" with no chance to "head down the wrong path."

It would also be appropriate to have analogues of 'Hint Constructors' 
that stock inversion, injection, and discrimination hints for particular 
inductive types.  The inversion Hint command would probably need to be 
the most complicated, since applying 'inversion' doesn't always lead to 
"making progress," but I'm sure some heuristic for "useful inversions" 
could handle the majority of cases.

So am I missing some canonical way of doing this kind of thing in Coq today?