Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Hints and the crush tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Hints and the crush tactic


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page