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

Question

以“如果其中一个是偶数而另一个是奇数，则两个自然数之和为奇数”的非常直接的证明：

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.

标签： coqproof

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

现在你想从析取中证明一些东西。为了证明A \/ B -> CCoq 构造逻辑中的某种形式，您必须同时 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可以处理这个。