Как сделать "отрицательный" матч в Ltac?

Question

Я хочу применить правило в случае, когда одна гипотеза присутствует, а другая нет. Как я могу проверить это условие?

Например:

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.

Такой, что для этой цели:

> Goal X->True. intros.

H:X
=====
True

more_detail. введем вторую гипотезу DET:

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

И последовательный вызов more_detail. потерпит неудачу

тем не мение more_detail. всегда следует убедиться, что оба Y а также Z есть, то есть если присутствует только один из них, он должен запустить правило для другого:

Goal X->Y->True. intros.

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

> more_detail.

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

А также:

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

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

> more_detail.

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

Answer 1

Это обычный шаблон Ltac. Вы можете использовать fail тактика, позволяющая избежать выполнения ветвления при совпадении некоторых условий:

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 с негативными узорами.