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] Hints and the crush tactic
- Date: Tue, 30 Mar 2010 22:47:35 +1100
Hi Adam,
I'm pretty sure [crush] will solve any goal that [auto] can, because [crush] calls [intuition], which calls [auto]. [eauto] is a different story, which, like Adam Koprowski suggested, I leave out because it can increase proof search time dramatically.
Thanks, that makes sense. Having run into a few situations now where eauto is too eager and grabs the wrong hypothesis, perhaps it is good to have them as separate tactics.
Oh, do you have any suggestion as to how to make crush apply app_eq_nil in hypotheses using hints by any chance? :)
Best regards,
Michael
--
Print XML with Prince!
http://www.princexml.com
- [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic, Adam Chlipala
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Chlipala
- Re: [Coq-Club] Hints and the crush tactic, Matthieu Sozeau
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
Archive powered by MhonArc 2.6.16.