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

Question

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

我想在 Coq 中定义exclusive or in Coq(据我所知，这不是预定义的)。重要的部分是允许多个命题(例如 Xor A B C D)。

我还需要两个属性:

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

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

Answer 1

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

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

我可以提供更多细节，但我认为自己做更有趣，让我知道它是怎么回事:)。