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

Question

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

我想在 Coq 中定义exclusive or in Coq（据我所知，这不是预定义的）。重要的部分是允许多个命题（例如 Xor ABCD）。

我还需要两个属性：

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

我目前在为未定义数量的变量定义函数时遇到问题。我尝试为两个、三个、四个和五个变量手动定义它（这就是我需要的数量）。但是证明这些属性很痛苦，而且效率很低。

Answer 1

给定你的第二个属性，我假设你对独占或更高数量的定义是 \xe2\x80\x9c 这些命题之一是 true\xe2\x80\x9d （而不是 \xe2\x80\x9can 这些命题的奇数是true\xe2\x80\x9d 或 \xe2\x80\x9cat 这些命题中至少一个为真，至少一个为假\xe2\x80\x9d，这是其他可能的概括）。

\n\n

这个独占属性或不是结合属性。这意味着您不能将高次异或定义为 xor(A1,\xe2\x80\xa6,An)=xor(A1,xor(A2,\xe2\x80\xa6))。您需要一个全局定义，这意味着类型构造函数必须采用参数列表（或其他一些数据结构，但列表是最明显的选择）。

\n\n

Inductive xor : list Prop -> Prop := \xe2\x80\xa6\n

\n\n

您现在有两个合理的选择：从第一原理归纳构建异或的定义，或调用列表谓词。列表谓词将是 \xe2\x80\x9c 列表中存在与此谓词\xe2\x80\x9d 匹配的唯一元素。由于标准列表库没有定义这个谓词，并且定义它比定义异或稍微困难，因此我们将归纳地构建异或。

\n\n

参数是一个列表，所以让我们分解一下情况：

\n\n

\n
• 空列表的异或总是 false；
\n
• (cons A L)当满足这两个条件之一时，列表的异或为 true:\n
  \n
  • A 为真，且 L 的所有元素均不为真；
  \n
  • A 为假，且 L 的其中一个元素为真。
  \n
\n

\n\n

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

\n\n

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

\n\n

您想要证明的属性是反转属性的简单推论：给定一个构造类型，分解可能性（如果您有 a xor，则它是 axor_t或 a xor_f）。这是第一个的手动证明；第二个非常相似。

\n\n

Lemma xor_tail : forall A L, xor (A::L) -> ~A -> xor L.\nProof.\n  intros. inversion_clear H.\n    contradiction.\n    assumption.\nQed.\n

\n\n

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

\n\n

Lemma nand1 : forall A, nand (A::nil) <-> ~A.\nProof.\n  split; intros.\n    inversion_clear H. assumption.\n    constructor. assumption. constructor.\nQed.\n

\n\n

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

\n\n

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

\n