Coq

Question

对"the sum of two naturals is odd if one of them is even and the other odd"进行非常简单的证明：

Require Import Arith.
Require Import Coq.omega.Omega.

Definition even (n: nat) := exists k, n = 2 * k.
Definition odd  (n: nat) := exists k, n = 2 * k + 1.

Lemma sum_odd_even : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. left.
  destruct H. firstorder.

此代码块末尾的状态是：

2 subgoals
n, m, x : nat
H : n + m = 2 * x + 1
______________________________________(1/2)
odd n
______________________________________(2/2)
even m

按我的理解，它是告诉我需要通过假设向它证明我有一个奇数n和一个偶数m？即使我已经说过 n 是奇数而 m 是偶数？我该如何从这里开始？

更新：

经过一些烦躁（根据评论），我想我必须做这样的事情？

Lemma even_or_odd: forall (n: nat), even n \/ odd n.
Proof.
  induction n as [|n IHn].
  (* Base Case *)
  left. unfold even. exists 0. firstorder.
  (* step case *)
  destruct IHn as [IHeven | IHodd].
  right. unfold even in IHeven. destruct IHeven as [k Heq].
  unfold odd. exists k. firstorder.
  left. unfold odd in IHodd. destruct IHodd as [k Heq].
  unfold even. exists (k + 1). firstorder.
Qed.

也就是说现在：

Lemma sum_odd : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. left. destruct H. firstorder.
  pose proof (even_or_odd n). pose proof (even_or_odd m).

结果：

    2 subgoals
n, m, x : nat
H : n + m = 2 * x + 1
H0 : even n \/ odd n
H1 : even m \/ odd m
______________________________________(1/2)
odd n
______________________________________(2/2)
even m

凭直觉，我所做的就是说明每个数字不是偶数就是奇数。现在我必须告诉 coq 我的奇数和偶数确实是奇数和偶数（我猜？）。

更新 2：

顺便说一句，这个问题只用一阶就可以解决：

Lemma sum_odd : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. firstorder.
  pose proof (even_or_odd n). pose proof (even_or_odd m).
  destruct H0 as [Even_n | Odd_n]. destruct H1 as [Even_m | Odd_m].
  exfalso. firstorder.
  right. auto.
  destruct H1. left. auto.
  exfalso. firstorder.
Qed.

Answer 1

您对 left 的使用仍然不正确，使您无法完成证明。您将其应用于以下目标：

odd (n + m) -> odd n /\ even m \/ even n /\ odd m

它给出：

H : odd (n + m)
______________________________________(1/1)
odd n /\ even m

你要证明如果n + m是奇数，那么n是奇数，m是偶数。但这是不正确：n 可能是奇数，而 m 可能是偶数。只有当你在上下文中有足够的信息来确定你想证明哪一个时，才应用 left 或 right。

所以让我们在没有 left 的情况下重新开始:

Lemma sum_odd : forall n m, odd (n + m) -> odd n /\ even m \/ even n /\ odd m.
Proof.
  intros n. intros m. firstorder.
  pose proof (even_or_odd n). pose proof (even_or_odd m).

此时我们处于：

H : n + m = 2 * x + 1
H0 : even n \/ odd n
H1 : even m \/ odd m
______________________________________(1/1)
odd n /\ even m \/ even n /\ odd m

现在你想从析取中证明一些东西。为了证明 Coq 构造逻辑中 A \/ B -> C 形式的东西，您必须证明 A -> C 和 B -> C。您可以通过对 A \/ B 进行案例分析（使用 destruct 或其他策略）来执行此操作。在这种情况下，我们有两个析取要分解：

  destruct H0 as [Even_n | Odd_n], H1 as [Even_m | Odd_m].

这给出了四种情况。我给你看前两个，后两个是对称的。

拳头案例：

H : n + m = 2 * x + 1
Even_n : even n
Even_m : even m
______________________________________(1/1)
odd n /\ even m \/ even n /\ odd m

假设是矛盾的：如果n和m都是偶数，那么H就不能成立。我们可以证明如下：

  - exfalso. destruct Even_n, Even_m. omega.

（逐步了解会发生什么！）exfalso 并不是真正必要的，但它是很好的文档，表明我们正在通过证明假设相互矛盾来进行证明。

第二种情况：

H : n + m = 2 * x + 1
Even_n : even n
Odd_m : odd m
______________________________________(1/1)
odd n /\ even m \/ even n /\ odd m

现在，知道适用于这种情况的假设，我们可以承诺正确析取。这就是为什么您的 left 阻碍您取得进步的原因！

  - right.

还有待证明的是：

Even_n : even n
Odd_m : odd m
______________________________________(1/1)
even n /\ odd m

而 auto 可以解决这个问题。

Coq - 证明已经定义的东西？

Coq - proving something which has already been defined?

proof