The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael Day wrote:
> I do have one question: could the crush tactic be extended to call 
> constructor? In several proofs I've ended up with situations like this:
>
> crush ; constructor.
>
> And I thought that constructor was a relatively "safe" tactic that 
> crush could probably try just to see if it works. Is this not the case?

If you change that to:
    crush; try solve [constructor].
then this would certainly be "safe," with the only potential downside 
that I can think of being a performance cost.  If you don't enforce that 
the constructor solves the goal, then you can easily replace a true goal 
with a false goal, since multiple constructors can apply to the same goal.

In each case, have you run [Hint Constructors] for the inductive type in 
question?  I would expect that would lead [crush] to solve these goals 
as-is.