coq - 如何在 Ltac 中进行 "negative"匹配？

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 尝试同一匹配的其他分支。使用 fail 1 会导致当前分支和整个匹配失败。如果 H : Z 不存在于上下文中，第一个分支将永远不会匹配，Coq 将跳过它并尝试第二个分支。由于此分支不执行任何操作，因此将按照匹配之后出现的策略继续执行。

在 more_detail 中，first 策略可用于组合多次调用 does_not_have；由于如果上下文包含相应的假设，first 的每个分支都会失败，因此整个构造将产生与否定模式匹配的效果。