The Coq mailing list

["Edward Z. Yang" <ezyang AT mit.edu>]

Suppose that I would like to run a tactic, but only if some hypothesis
isn't present.  Namely, I would like to do a negated pattern match,
i.e. a red cut.  It might seem that this would work OK:

(**)
match goal with
    | [ H : P X | _ ] => fail 2
    | _ => assert (P X); [eauto|]
(**)

Unfortunately, 'fail 2' is overzealous and escapes too far:

(**)
match goal with
    | [ HF : Forall ?P ?X, H : In ?X ?XS |- _ ] =>
        match goal with
            | [ H : P X | _ ] => fail 2
            | _ => assert (P X); [eauto|]
        end
end.
(**)

The problem is when I have a context that looks like:

    A : Type
    P1 : A -> Prop
    P2 : A -> Prop
    XS : list A
    H1 : Forall P1 XS
    H2 : Forall P2 XS
    H : In X XS
    H' : P1 X
    =================================

I'd like to generate 'P2 X', but P1 is matched first and the entire
match is aborted. (I could permute the order of the hypothesis but
in general that won't work.)

Any advice?

Edward