2

我想要一个 Ltac 策略来完成 Disjunction Commutavity 的工作。主要是，如果我P \/ Q在某个假设的某个地方有一个子项H，Ltac Com H则会在上下文中添加Q \/ P另一个假设。

我尝试通过一个公理和apply它来提供交换规则；但它只适用于简单的假设，例如失败R -> (P \/ Q)；它应该添加到上下文中R -> (Q \/ P)。

4

1 回答 1

4

您可以使用 setoid 重写库，它允许您使用除相等之外的关系进行重写。以下片段显示了如何在假设中A \/ B替换为：B \/ A

Require Import Setoid.

Variables A B C : Prop.

Goal ~ (A \/ B -> C).
intros H.
rewrite or_comm in H.
Abort.

为了实现你想要的策略，我们只需要复制假设并重写它。注意fresh策略的使用，它会生成一个新的假设名称。

Ltac Comm H :=
  let H' := fresh "H" in
  pose proof H as H';
  rewrite or_comm in H'.

这是一个实际操作的演示Comm。

Goal ~ (A \/ B -> C).
intros H.
Comm H.
Abort.

编辑Coq 手册中有一个关于 setoid 重写的部分。粗略地说，您可以用假设中的任何关系重写R，前提是您证明该假设中出现的操作与该关系兼容。例如，如果我们认为R是<->，上述重写是有效的，因为标准库中有引理表明逻辑等价是通过暗示得到尊重的。

请注意，我通常建议不要让 Coq 自己命名假设：这些名称往往非常不稳定，这通常会导致证明脚本中断。根据经验，如果您正在编写完全自动化的证明脚本，那么您应该让 Coq 自己选择名称，它从不引用自动选择的名称。Comm这是避免此问题的另一个版本。

Ltac Comm' H H' :=
  pose proof H as H';
  rewrite or_comm in H'.

Goal ~ (A \/ B -> C).
intros H.
Comm H H'.
Abort.
于 2018-10-24T02:18:27.873 回答