Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Hints and the crush tactic


chronological Thread 
  • From: Michael Day <mikeday AT yeslogic.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Hints and the crush tactic
  • Date: Mon, 29 Mar 2010 22:18:10 +1100

Hi,

In my proofs there are often introduced hypotheses like this:

    H : tl1 ++ tl2 = nil

To make progress it is necessary to perform the following steps:

    apply app_eq_nil in H ; destruct H ; subst.

This introduces equalities tl1=nil and tl2=nil and substitutes this into the goal and any other assumptions.

Is it possible to use a hint to encourage the crush tactic to perform such substitutions automatically?

Best regards,

Michael

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



Archive powered by MhonArc 2.6.16.

Top of Page