在 Coq 中添加完全析取假设

Question

在数学中，我们经常这样进行："Now let us consider two cases, the number k can be even or odd. For the even case, we can say exists k', 2k' = k..."

通过将其分解为几个可用于重建原始集合的分离子集，扩展了对整个对象集进行推理的一般想法。

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

考虑以下示例进行演示：

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

这里我们自然可以在 Nat.Even n 上做 inversion 得到 n = 2*x（以及一个自动错误的消除假设 n = 2*x + 1）。但是，假设我们有以下内容：

forall n, P n

我该如何声明："let us consider even ns and odd ns"。我需要先证明我们有可判定的 forall n : nat, even n \/ odd n 吗？也就是说，引入一个新的（局部的或全局的）引理来列出所有需要的子集？最佳做法是什么？

Answer 1

确实，要在 Coq 中推理 class 个对象的拆分，你需要展示一个拆分它们的算法，除非你想 class 逻辑地推理（这没有任何问题） ).

IMO，一个关键点是得到这样的可判定性假设"for free"。例如，您可以将 odd : nat -> 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.

在 Coq 中添加完全析取假设

Adding complete disjunctive assumption in Coq

coq

theorem-proving