The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

   Dear Michael,

 

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?

 How about:

  Hint Extern 3 =>
    match goal with
    | H : ?X ++ ?Y = nil |- _ => 
      apply app_eq_nil in H; destruct H; subst
    end : cpdt.

  in general this variant of Hint Extern allows you to register an arbitrary tactic to be executed (after matching the goal).

  Best,

  Adam

-- 
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]