Coq:证明 n 和 (S n) 的乘积是偶数
Coq: Proving that the product of n and (S n) is even
给定过程 even
,我想证明 even (n * (S n)) = true
对于所有自然数 n
。
使用归纳法,对于 n = 0
的情况,这很容易看出是 true
。但是,案例(S n) * (S (S n))
很难简化。
我考虑过证明 even (m * n) = even m /\ even n
的引理,但这似乎并不容易。
另外,很容易看出如果even n = true
当且仅当。 even (S n) = false
.
Fixpoint even (n: nat) : bool :=
match n with
| O => true
| 1 => false
| S (S n') => even n'
end.
有人可以提示如何使用 Coq 的 "beginner's" 子集来证明这一点吗?
在这种情况下,更高级的归纳原理可能会有用。 .
中有简要说明
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.
下面的引理展示了如何 "distribute" 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.
Can someone give a hint on how to prove this using a "beginner's" subset of Coq?
您可以将此视为提示,因为它揭示了可能证明的一般结构。自动战术可能会被 "manual" 战术取代,例如 rewrite
、apply
、destruct
等。
我想使用 mathcomp 库贡献一个更短的证明:
From mathcomp Require Import all_ssreflect all_algebra.
Lemma P n : ~~ odd (n * n.+1).
Proof. by rewrite odd_mul andbN. Qed.
odd_mul
和odd_add
.
一样用简单归纳法证明
另一个版本,本着@ejgallego 的回答精神。
让我们为 even 谓词给出另一个定义。这样做的目的是使简单归纳的证明变得容易,所以不需要使用pair_induction
。主要思想是我们要证明 even2
的一些性质,然后我们将使用 Nat.even
和 even2
外延相等的事实来传递 even2
的性质] 到 Nat.even
.
Require Import Coq.Bool.Bool.
Fixpoint even2 (n : nat) : bool :=
match n with
| O => true
| S n' => negb (even2 n')
end.
让我们证明 Nat.even
和 even2
在外延上是相等的。
Lemma even_S n :
Nat.even (S n) = negb (Nat.even n).
Proof. induction n; auto. apply negb_sym; assumption. Qed.
Lemma even_equiv_even2 n :
Nat.even n = even2 n.
Proof. induction n; auto. now rewrite even_S, IHn. Qed.
even2
的一些分布引理:
Lemma even2_distr_add m n :
even2 (m + n) = negb (xorb (even2 m) (even2 n)).
Proof.
induction m; simpl.
- now destruct (even2 n).
- rewrite IHm. now destruct (even2 m); destruct (even2 n).
Qed.
Lemma even2_distr_mult m n :
even2 (m * n) = even2 m || even2 n.
Proof.
induction m; auto; simpl.
rewrite even2_distr_add, IHm.
now destruct (even2 m); destruct (even2 n).
Qed.
最后,我们能够使用 Nat.even
和 even2
之间的等式来证明我们的目标。
Goal forall n, Nat.even (n * (S n)) = true.
intros n.
now rewrite even_equiv_even2, even2_distr_mult, orb_negb_r.
Qed.
使用标准库的简短版本:
Require Import Coq.Arith.Arith.
Goal forall n, Nat.even (n * (S n)) = true.
intros n.
now rewrite Nat.even_mul, Nat.even_succ, Nat.orb_even_odd.
Qed.
对于它的价值,这是我对解决方案的看法。基本思想是,不是证明谓词 P n
,而是证明 P n /\ P (S n)
,这是等价的,但第二个公式允许使用简单的归纳法。
这里是完整的证明:
Require Import Nat.
Require Import Omega.
Definition claim n := even (n * (S n)) = true.
(* A technical Lemma, needed in the proof *)
Lemma tech: forall n m, even n = true -> even (n + 2*m) = true.
Proof.
intros. induction m.
* simpl. replace (n+0) with n; intuition.
* replace (n + 2 * S m) with (S (S (n+2*m))); intuition.
Qed.
(* A simple identity, that Coq needs help to prove *)
Lemma ident: forall n,
(S (S n) * S (S (S n))) = (S n * S( S n) + 2*(S (S n))).
(* (n+2)*(n+3) = (n+1)*(n+2) + 2*(n+2) *)
Proof.
intro.
replace (S (S (S n))) with ((S n) + 2) by intuition.
remember (S (S n)) as m.
replace (m * (S n + 2)) with ((S n + 2) * m) by intuition.
intuition.
Qed.
(* The claim to be proved by simple induction *)
Lemma nsn: forall n, claim n /\ claim (S n).
Proof.
intros.
unfold claim.
induction n.
* intuition.
* intuition. rewrite ident. apply tech; auto.
Qed.
(* The final result is now a simple corollary *)
Theorem thm: forall n, claim n.
Proof.
apply nsn.
Qed.
给定过程 even
,我想证明 even (n * (S n)) = true
对于所有自然数 n
。
使用归纳法,对于 n = 0
的情况,这很容易看出是 true
。但是,案例(S n) * (S (S n))
很难简化。
我考虑过证明 even (m * n) = even m /\ even n
的引理,但这似乎并不容易。
另外,很容易看出如果even n = true
当且仅当。 even (S n) = false
.
Fixpoint even (n: nat) : bool :=
match n with
| O => true
| 1 => false
| S (S n') => even n'
end.
有人可以提示如何使用 Coq 的 "beginner's" 子集来证明这一点吗?
在这种情况下,更高级的归纳原理可能会有用。
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.
下面的引理展示了如何 "distribute" 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.
Can someone give a hint on how to prove this using a "beginner's" subset of Coq?
您可以将此视为提示,因为它揭示了可能证明的一般结构。自动战术可能会被 "manual" 战术取代,例如 rewrite
、apply
、destruct
等。
我想使用 mathcomp 库贡献一个更短的证明:
From mathcomp Require Import all_ssreflect all_algebra.
Lemma P n : ~~ odd (n * n.+1).
Proof. by rewrite odd_mul andbN. Qed.
odd_mul
和odd_add
.
另一个版本,本着@ejgallego 的回答精神。
让我们为 even 谓词给出另一个定义。这样做的目的是使简单归纳的证明变得容易,所以不需要使用pair_induction
。主要思想是我们要证明 even2
的一些性质,然后我们将使用 Nat.even
和 even2
外延相等的事实来传递 even2
的性质] 到 Nat.even
.
Require Import Coq.Bool.Bool.
Fixpoint even2 (n : nat) : bool :=
match n with
| O => true
| S n' => negb (even2 n')
end.
让我们证明 Nat.even
和 even2
在外延上是相等的。
Lemma even_S n :
Nat.even (S n) = negb (Nat.even n).
Proof. induction n; auto. apply negb_sym; assumption. Qed.
Lemma even_equiv_even2 n :
Nat.even n = even2 n.
Proof. induction n; auto. now rewrite even_S, IHn. Qed.
even2
的一些分布引理:
Lemma even2_distr_add m n :
even2 (m + n) = negb (xorb (even2 m) (even2 n)).
Proof.
induction m; simpl.
- now destruct (even2 n).
- rewrite IHm. now destruct (even2 m); destruct (even2 n).
Qed.
Lemma even2_distr_mult m n :
even2 (m * n) = even2 m || even2 n.
Proof.
induction m; auto; simpl.
rewrite even2_distr_add, IHm.
now destruct (even2 m); destruct (even2 n).
Qed.
最后,我们能够使用 Nat.even
和 even2
之间的等式来证明我们的目标。
Goal forall n, Nat.even (n * (S n)) = true.
intros n.
now rewrite even_equiv_even2, even2_distr_mult, orb_negb_r.
Qed.
使用标准库的简短版本:
Require Import Coq.Arith.Arith.
Goal forall n, Nat.even (n * (S n)) = true.
intros n.
now rewrite Nat.even_mul, Nat.even_succ, Nat.orb_even_odd.
Qed.
对于它的价值,这是我对解决方案的看法。基本思想是,不是证明谓词 P n
,而是证明 P n /\ P (S n)
,这是等价的,但第二个公式允许使用简单的归纳法。
这里是完整的证明:
Require Import Nat.
Require Import Omega.
Definition claim n := even (n * (S n)) = true.
(* A technical Lemma, needed in the proof *)
Lemma tech: forall n m, even n = true -> even (n + 2*m) = true.
Proof.
intros. induction m.
* simpl. replace (n+0) with n; intuition.
* replace (n + 2 * S m) with (S (S (n+2*m))); intuition.
Qed.
(* A simple identity, that Coq needs help to prove *)
Lemma ident: forall n,
(S (S n) * S (S (S n))) = (S n * S( S n) + 2*(S (S n))).
(* (n+2)*(n+3) = (n+1)*(n+2) + 2*(n+2) *)
Proof.
intro.
replace (S (S (S n))) with ((S n) + 2) by intuition.
remember (S (S n)) as m.
replace (m * (S n + 2)) with ((S n + 2) * m) by intuition.
intuition.
Qed.
(* The claim to be proved by simple induction *)
Lemma nsn: forall n, claim n /\ claim (S n).
Proof.
intros.
unfold claim.
induction n.
* intuition.
* intuition. rewrite ident. apply tech; auto.
Qed.
(* The final result is now a simple corollary *)
Theorem thm: forall n, claim n.
Proof.
apply nsn.
Qed.