coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Michael Day <mikeday AT yeslogic.com>
- To: Adam Chlipala <adam AT chlipala.net>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] crush tactic
- Date: Wed, 24 Mar 2010 00:23:18 +1100
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
- [Coq-Club] crush tactic, Michael Day
- Re: [Coq-Club] crush tactic,
Adam Chlipala
- Re: [Coq-Club] crush tactic, Michael Day
- Re: [Coq-Club] crush tactic, Adam Chlipala
- Re: [Coq-Club] crush tactic, Michael Day
- Re: [Coq-Club] crush tactic,
Adam Chlipala
Archive powered by MhonArc 2.6.16.