coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [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,
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.