Coq：nと（S n）の積が偶数であることを証明する

Question

手順evenが与えられると、すべての自然数がnであることを証明したいと思います。

誘導を使用すると、これは、n = 0の場合、容易にtrueであることがわかります。しかし、ケース(S n) * (S (S n))は単純化するのが難しいです。

私は補題を証明すると考えていますが、それはeven (m * n) = even m /\ even nですが、これは簡単ではないようです。

また、even n = true iffの場合は分かりやすいです。 even (S n) = false。

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

誰かがコックの「初心者」のサブセットを使用してこれを証明する方法についてのヒントを与えることはできますか？

Answer 1

@ ejgallegoの答えの精神で、別のバージョンです。 偶数述語について別の定義をしましょう。これは簡単な誘導で簡単な証明を行うためのもので、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. 

Answer 2

これは、より進歩した誘導原理が有用な場合である。簡単にはthis answerに記載されています。

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. 

簡単です誰かがコックの「初心者」のサブセットを使用してこれを証明する方法についてのヒントを与えることはできますか？

考えられるプルーフの一般的な構造を明らかにしているので、これはヒントと考えることができます。自動戦術は、rewrite、apply、destructなどのような「手動」戦術に置き換えることができます。私はmathcomp libにを使用して短い証明貢献したいと思います

Answer 3

：

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によって証明されます。

Answer 4

標準ライブラリの使用可能ショートバージョン：それは価値がある何のため

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. 

Answer 5

は、ここに解決策が私の感想です。基本的な考え方は、述語P nを証明するのではなく、代わりにP n /\ P (S n)と証明します。これは同等ですが、2番目の形式では簡単な誘導を使用することができます。 - >でも（N×m個） `（すべての 'M'のために）私は証明開始する

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.