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.

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 -> 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可以处理这个.