Coq：证明n和(S n)的乘积是偶数

Question

给定程序even，我想证明even (n * (S n)) = true所有自然数n。

使用归纳法，很容易看出这种情况是true成立的n = 0。然而，案件(S n) * (S (S n))很难简单化。

我考虑过证明引理even (m * n) = even m /\ even n，但这似乎并不容易。

另外，很容易看出 if even n = trueiff 。even (S n) = false。

Fixpoint even (n: nat) : bool :=
  match n with
  | O => true
  | 1 => false
  | S (S n') => even n'
  end.

有人可以提示如何使用 Coq 的“初学者”子集来证明这一点吗？

Answer 1

在这种情况下，更先进的归纳原理可能会很有用。这个答案中对此进行了简要描述。

Require Import Coq.Arith.Arith.
Require Import Coq.Bool.Bool.    

Lemma pair_induction (P : nat -> Prop) :
  P 0 -> P 1 -> (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
  intros ? ? ? n. enough (P n /\ P (S n)) by tauto.
  induction n; intuition.
Qed.

现在，让我们定义几个辅助引理。它们是显而易见的，可以使用pair_induction原理和一些证明自动化轻松证明。

Lemma even_mul2 : forall n, Nat.even (2 * n) = true.
Proof.
  induction n; auto.
  now replace (2 * S n) with (2 + 2 * n) by ring.
Qed.

Lemma even_add_even : forall m n,
  Nat.even m = true ->
  Nat.even (m + n) = Nat.even n.
Proof.
  now induction m using pair_induction; auto.
Qed.

Lemma even_add_mul2 : forall m n,
  Nat.even (2 * m + n) = Nat.even n.
Proof.
  intros; apply even_add_even, even_mul2.
Qed.

Lemma even_S : forall n,
  Nat.even (S n) = negb (Nat.even n).
Proof.
  induction n; auto.
  simpl (Nat.even (S (S n))).   (* not necessary -- just to make things clear *)
  apply negb_sym. assumption.
Qed.

以下引理显示了如何“分配”even乘法。它在证明我们的主要目标方面发挥着重要作用。概括几乎总是有很大帮助。

Lemma even_mult : forall m n,
  Nat.even (m * n) = Nat.even m || Nat.even n.
Proof.
  induction m using pair_induction; simpl; auto.
  intros n. replace (n + (n + m * n)) with (2 * n + m * n) by ring.
  now rewrite even_add_mul2.
Qed.

现在，目标的证明是微不足道的

Goal forall n, Nat.even (n * (S n)) = true.
  intros n. now rewrite even_mult, even_S, orb_negb_r.
Qed.

有人可以提示如何使用 Coq 的“初学者”子集来证明这一点吗？

您可以将其视为一个提示，因为它揭示了可能证明的一般结构。自动策略可以被“手动”策略取代，例如rewrite、apply、destruct等等。