4

我想在某些假设存在而另一个假设不存在的情况下应用规则。如何检查这种情况？

例如：

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
4

1 回答 1

9

这是一种常见的 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上下文中存在，则第一个分支将匹配。简单地调用failorfail 0会导致该分支失败，但会允许 Ltac 尝试相同的其他分支match。使用fail 1会导致当前分支和整个匹配失败。如果H : Z上下文中不存在，则第一个分支永远不会匹配，Coq 将跳过它并尝试第二个分支。由于这个分支不做任何事情，执行将按照match.

在more_detail中，first战术可以用来组合几个调用does_not_have；由于如果上下文包含相应的假设，则每个分支first都会失败，因此整个构造将产生match负面模式的影响。

于 2015-02-09T15:23:10.807 回答