如何在 Coq 中定义 Xor 并证明其性质答案

【问题标题】：How to define Xor in Coq and prove its properties如何在 Coq 中定义 Xor 并证明其性质
【发布时间】：2011-07-20 15:40:45
【问题描述】：

这应该是一个简单的问题。我是 Coq 的新手。

我想在 Coq 中定义独占或（据我所知，这不是预定义的）。重要的部分是允许多个命题（例如 Xor A B C D）。

我还需要两个属性：

(Xor A1 A2 ... An)/\~A1 -> Xor A2... An
(Xor A1 A2 ... An)/\A1 -> ~A2/\.../\~An

我目前无法为未定义数量的变量定义函数。我试图为两个、三个、四个和五个变量手动定义它（这就是我需要的数量）。但是随后证明这些属性很痛苦，而且似乎效率很低。

【问题讨论】：

标签： xor coq

【解决方案1】：

鉴于您的第二个属性，我假设您对排他性或更高元数的定义是“这些命题中恰好有一个是真的”（而不是“这些命题中的奇数个是真的”或“这些命题中的至少一个是真的”是真的，至少有一个是假的”，这是其他可能的概括）。

此排他或不是关联属性。这意味着您不能将更高元数的 xor 定义为 xor(A1,…,An)=xor(A1,xor(A2,…))。您需要一个全局定义，这意味着类型构造函数必须采用参数列表（或其他一些数据结构，但列表是最明显的选择）。

Inductive xor : list Prop -> Prop := …

您现在有两个合理的选择：根据第一原则归纳地构建 xor 的定义，或者调用列表谓词。列表谓词将是“列表中存在与该谓词匹配的唯一元素”。由于标准列表库没有定义这个谓词，而且定义它比定义 xor 稍微难一些，我们将构建 xor 归纳。

参数是一个列表，所以让我们分解案例：

空列表的异或总是假的；
xor 列表(cons A L) 为真，如果满足以下两个条件之一：
- A 为真，L 中没有一个元素为真；
- A 为假，而 L 的元素之一为真。

这意味着我们需要在命题列表上定义一个辅助谓词nand，以表征假命题列表。这里有很多可能性：折叠/\ 运算符，手动归纳，或调用列表谓词（同样，不在标准列表库中）。我会手动感应，但折叠/\ 是另一个合理的选择。

Require Import List.
Inductive nand : list Prop -> Prop :=
  | nand_nil : nand nil
  | nand_cons : forall (A:Prop) L, ~A -> nand L -> nand (A::L).
Inductive xor : list Prop -> Prop :=
  | xor_t : forall (A:Prop) L, A -> nand L -> xor (A::L)
  | xor_f : forall (A:Prop) L, ~A -> xor L -> xor (A::L).
Hint Constructors nand xor.

您要证明的属性是 inversion 属性的简单推论：给定一个构造类型，分解可能性（如果您有 xor，它要么是 xor_t，要么是 @ 987654329@)。这是第一个的手动证明；第二个非常相似。

Lemma xor_tail : forall A L, xor (A::L) -> ~A -> xor L.
Proof.
  intros. inversion_clear H.
    contradiction.
    assumption.
Qed.

您可能需要的另一组属性是nand 和内置连词之间的等价关系。例如，这里证明了nand (A::nil) 等价于~A。证明nand (A::B::nil) 等价于~A/\~B 等等只是更多的相同。在正向中，这又是一个反转属性（分析nand 类型的可能构造函数）。向后看，这是构造函数的简单应用。

Lemma nand1 : forall A, nand (A::nil) <-> ~A.
Proof.
  split; intros.
    inversion_clear H. assumption.
    constructor. assumption. constructor.
Qed.

在某些时候，您可能还需要替换和重新排列属性。以下是您可能想要证明的几个关键引理（这些应该不是很难，只需归纳正确的东西即可）：

forall A1 B2 L, (A1<->A2) -> (xor (A1::L) <-> xor (A2::L))
forall K L1 L2, (xor L1 <-> xor L2) -> (xor (K++L1) <-> xor (K++L2))
forall K A B L, xor (K++A::B::L) <-> xor (K::B::A::L)
forall K L M N, xor (K++L++M++N) <-> xor (K++M++L++N)

【讨论】：

这正是我想要的。我一直在为归纳定义苦苦挣扎，但这就是我想做的。您介意解释一下构造函数在您的示例中是如何工作的吗？
@Skuge 构造函数遵循上面的英文。空列表的异或总是错误的，因此无法构造xor nil 的证明。如果你有A 的证明P 和nand L 的证明Q，那么xor (A::L) 为真，因此我们声明xor (A::L) 为真，证明为xor_t P Q。 xor_f 也是如此。由于这涵盖了证明xor(something) 的所有方法，因此这些都是xor 类型的构造函数。我建议阅读 theories/Init/Logic.v 以了解 Coq 定义熟悉的逻辑连接器的方式，例如 True、False、and 等。

【解决方案2】：

好吧，我建议你从 2 个参数的 Xor 开始并证明它的属性。

如果你想概括它，你可以定义 Xor 接受参数列表——你应该能够定义它并使用您的 2 参数 Xor 证明其属性。

我可以提供更多细节，但我认为自己做会更有趣，请告诉我进展如何：)。

【讨论】：