怎么做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负面模式的效果.