Geek Answers Handbook

How to make a “negative” match in Ltac?

I want to apply the rule when some hypothesis is present and the other is not. How can I check this condition?

For instance:

Variable X Y : Prop.
Axiom A: X -> Y.
Axiom B: X -> Z.

Ltac more_detail :=
    match goal with
     |[H1:X,<not H2:Y>|-_]  =>
      let H' := fresh "DET" in assert Y as H'
                                   by (apply A;assumption)
     |[H1:X,<not H2:Z>|-_]  =>
      let H' := fresh "DET" in assert Z as H'
                                   by (apply B;assumption)
    end.

Thus, for this purpose:

> Goal X->True. intros.

H:X
=====
True

more_detail. will present the second DET hypothesis:

H:X
DET:Y
DET0:Z
=====
True

And the serial call more_detail.will fail.

However, more_detail.it must always guarantee that both Y, and Z, i.e. if only one of them is present, it should run a rule for the other:

Goal X->Y->True. intros.

H:X
H1:Y
=====
True

> more_detail.

H:X
H1:Y
DET:Z
=====
True

and

> Goal X->Z->True. intros.

H:X
H0:Z
=====
True

> more_detail.

H:X
H0:Z
DET:Y
=====
True
+4
source share
1 answer

This is a generic Ltac template. You can use tactics failto avoid branch execution when any condition matches:

Variable X Y Z : Prop.
Hypothesis A : X -> Y.
Hypothesis B : X -> Z.

Ltac does_not_have Z :=
  match goal with
  | _ : Z |- _ => fail 1
  | |- _ => idtac
  end.

Ltac more_detail :=
  match goal with
  | H : X |- _ =>
    first [ does_not_have Y;
            let DET := fresh "DET" in
            assert (DET := A H)
          | does_not_have Z;
            let DET := fresh "DET" in
            assert (DET := B H) ]
  end.

Goal X -> True.
intros X. more_detail. more_detail.
(* This fails *)
more_detail.
Abort.

does_not_have : , . , : H : Z , . fail fail 0 , Ltac match. fail 1 . H : Z , , Coq . , match.

more_detail first does_not_have; first , , match .

+7

More articles:


All Articles