鉴于您的第二个属性,我假设您对排他性或更高数量的定义是“这些命题中的一个是真的”(而不是“这些命题中有一个奇数是真的”或“这些命题中至少有一个是真的并且至少有一个是错误的”,这是其他可能的概括)。
此排他或不是关联属性。这意味着您不能将更高元数的 xor 定义为 xor(A1,…,An)=xor(A1,xor(A2,…))。您需要一个全局定义,这意味着类型构造函数必须采用参数列表(或其他一些数据结构,但列表是最明显的选择)。
Inductive xor : list Prop -> Prop := …
您现在有两个合理的选择:从第一原理归纳地构建 xor 的定义,或者调用列表谓词。列表谓词将是“列表中存在与该谓词匹配的唯一元素”。由于标准列表库没有定义这个谓词,并且定义它比定义 xor 稍微难一些,我们将构建 xor 归纳。
参数是一个列表,所以让我们分解案例:
- 空列表的异或总是假的;
(cons A L)
如果满足以下两个条件
之一,则列表的 xor为真:
- 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.
您要证明的属性是反转属性的简单推论:给定一个构造类型,分解可能性(如果您有 a xor
,它是 axor_t
或 a xor_f
)。这是第一个的手动证明;第二个非常相似。
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)