The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Adam,

> 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?

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?

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com