The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael Day wrote:
> > 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.
>
> Thanks, that solves it! Sorry, I have not read up on hints yet :)
>
> So is it the case that proofs involving relatively simple inductive 
> types are more likely to be solvable using this constructors hint, 
> without accidentally introducing false goals? Or does it just depend 
> upon the proof in question?

[auto] and [eauto] never change goals; they either solve them or they don't.

> Also, is there any conceptual difference between your crush tactic and 
> the built-in auto tactic? Is it that auto will not do intros or 
> simplify things if it cannot solve the whole goal, while crush will?

My last answer works about as well as an answer to this question, too. 
;)  (Yes, your suggested answer is right.)