coq - 在 Coq 中添加完全析取假设

Question

在数学中，我们经常这样进行:“现在让我们考虑两种情况，数字 k 可以是 even 或 odd 。对于 even 的情况，我们可以说 exists k', 2k' = k .. ”

这扩展了通过将整个对象集分解为几个可用于重建原始集的不连续子集来推理整个对象集的一般思想。

考虑到我们并不总是有一个假设是我们想要解构的子集之一，那么在 coq 中如何捕捉这一推理原理？

考虑以下示例进行演示:

forall n, Nat.Even n => P n.

这里我们自然可以做inversion上Nat.Even n获取n = 2*x (以及自动错误消除的假设 n = 2*x + 1 )。但是，假设我们有以下内容:

forall n, P n

我该如何表述:“让我们考虑 even n 和 odd n s”。我需要首先证明我们有可判定的forall n : nat, even n \/ odd n ？也就是说，引入一个新的(局部或全局)引理，列出所有所需的子集？最佳实践是什么？

Answer 1

事实上，要在 Coq 中推理一类对象的拆分，您需要展示一个拆分它们的算法，除非您想进行经典推理(这没有任何问题)。

IMO，一个关键点是“免费”获得这样的可判定性假设。例如，您可以将 odd : nat -> bool 实现为 bool 函数，就像在某些库中所做的那样，然后您就可以免费进行拆分。

[编辑] 您可以使用一些稍微更方便的技术进行模式匹配，将相关案例编码为归纳式:

Require Import PeanoNat Nat Bool.

CoInductive parity_spec (n : nat) : Type :=
| parity_spec_odd : odd  n = true -> parity_spec n
| parity_spec_even: even n = true -> parity_spec n
.

Lemma parityP n : parity_spec n.
Proof.
case (even n) eqn:H; [now right|left].
now rewrite <- Nat.negb_even, H.
Qed.

Lemma test n : even n = true \/ odd n = true.
Proof. now case (parityP n); auto. Qed.