在 Coq 中使用 AND 运算符的交换性

Question

我正在尝试使用逻辑 AND 运算符的交换性在 Coq 中证明一些东西。我编写了这个简短的例子：

Axiom ax1 : A /\ B.
Theorem th1 : B /\ A.
Proof.
  pose proof (ax1) as H.
  symmetry.
  apply H.
Qed.

我在我的证明中使用了公理 (ax1)，但我卡在了对称命令上。这是我目前的目标：

1 subgoal
H : A /\ B
______________________________________(1/1)
B /\ A

当我使用对称命令时，出现以下错误：

Tactic failure:  The relation and is not a declared symmetric relation. Maybe you need to require the Coq.Classes.RelationClasses library.

我目前的解决方案是破坏假设H，拆分目标，将正确的子假设应用于正确的子目标。这需要很多 space 并且无法使用 AND 可交换性有点令人沮丧。

所以我有一些问题：对称性是用于交换关系的正确命令吗？如果是，我该如何修复我的代码以使其正常工作？如果不是，有没有办法利用AND运算符的交换性？

Answer 1

symmetry 策略专门用于推理等式 (a = b iff b = a)。

我不知道可交换运算符的通用机制，但您可以通过以下方式找到所需的引理：

Search _ (?a /\ ?b <-> ?b /\ ?a)

（我作弊了：原来我用的是->，结果没找到就改成<->了！）

基础库中只有一个这种形式的引理，叫做and_comm。您应该可以用它来解决您剩余的证明义务：apply and_comm.

Answer 2

您可以使 symmetry 策略适用于任何关系……只要您首先证明它是对称的。这是在标准库中完成的（这就是为什么 symmetry 开箱即用），但不适用于 and。所以如果你想使用它，你必须自己动手，像这样：

Require Import RelationClasses.

Instance and_comm : Symmetric and.
Proof.
  intros A B [].
  now split.
Qed.

标准库的RelationClasses模块声明了Symmetric类型class，Coq在调用对称策略时会使用它。接下来我们证明 and 确实是对称的，并将其声明为 Symmetric class 的一个实例。完成后，symmetry 将如您所愿地工作。

Using the commutativity of the AND operator in Coq