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 Koprowski <adam.koprowski AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Hints and the crush tactic
  • Date: Tue, 30 Mar 2010 20:06:55 +1100

Hi Adam,

Note that auto must solve the goal completely or else it will not change the goal in any way. When you apply this tactic directly does it solve the goal completely? Or just "work" giving a new obligation? Can this new obligation be solved by auto?

Right, it isn't sufficient to solve the whole goal, I was just hoping to unpack the hypothesis and subst the equalities with crush and then use other tactics to make further progress.

The crush tactic seems to use autorewrite hints, but I don't see how to trigger this kind of extern hint in this way.

In the meantime, I can always bind it to a new Ltac tactic and call that manually, which would still be shorter than typing out the whole line each time :)

Cheers,

Michael

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



Archive powered by MhonArc 2.6.16.

Top of Page