Coq: Proving that the product of n and (S n) is even

Link:: https://stackoverflow.com/q/40791863

Display all goals and responses

Question

Given the procedure even, I want to prove that even (n * (S n)) = true for all natural numbers n.

Using induction, this is easily seen to be true for the case n = 0. However, the case (S n) * (S (S n)) is hard to simplify.

I've considered proving the lemma that even (m * n) = even m /\ even n, but this doesn't seem to be easier.

Also, it is easy to see that if 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.

Can someone give a hint on how to prove this using a "beginner's" subset of Coq?

Answer (Anton Trunov)

This is a case where a more advanced induction principle can be useful. It is briefly described in 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.P: nat -> Prop
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S n) -> P (S (S n))) ->
forall n : nat, P n
Proof.P: nat -> Prop
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S n) -> P (S (S n))) ->
forall n : nat, P n
  intros ? ? ? n.P: nat -> Prop
H: P 0
H0: P 1
H1: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
P n enough (P n /\ P (S n)) by tauto.P: nat -> Prop
H: P 0
H0: P 1
H1: forall n : nat, P n -> P (S n) -> P (S (S n))
n: nat
P n /\ P (S n)
  induction n; intuition.
Qed.

Now, let's define several helper lemmas. They are obvious and can be easily proved using the pair_induction principle and some proof automation.

Lemma even_mul2 : forall n, Nat.even (2 * n) = true.forall n : nat, Nat.even (2 * n) = true
Proof.forall n : nat, Nat.even (2 * n) = true
  induction n; auto.n: nat
IHn: Nat.even (2 * n) = true
Nat.even (2 * S n) = true
  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.forall m n : nat,
Nat.even m = true -> Nat.even (m + n) = Nat.even n
Proof.forall m n : nat,
Nat.even m = true -> Nat.even (m + n) = Nat.even n
  now induction m using pair_induction; auto.
Qed.

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

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

The following lemma shows how to "distribute" even over multiplication. It plays an important role in the proof of our main goal. As almost always generalization helps a lot.

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

Now, the proof of the goal is trivial

Goal forall n, Nat.even (n * (S n)) = true.forall n : nat, Nat.even (n * S n) = true
  intros n.n: nat
Nat.even (n * S n) = true 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?

You can consider this a hint, since it reveals the general structure of a possible proof. The automatic tactics may be replaced by the "manual" tactics like with rewrite, apply, destruct and so on.

Answer (ejgallego)

I'd like to contribute a shorter proof using the mathcomp lib:

From mathcomp Require Import all_ssreflect.Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ ^ _" was already used in scope nat_scope.
[notation-overridden,parsing]

Lemma P n : ~~ odd (n * n.+1).n: nat
~~ odd (n * n.+1)
Proof.n: nat
~~ odd (n * n.+1) by rewrite oddM andbN. Qed.

oddM is proved by simple induction, as well as oddD.

A: The definition of odd here has different structure comparing to even in the question, that's why simple induction works well in this case.

Answer (Anton Trunov)

Another version, in the spirit of @ejgallego's answer. Let's give another definition for the even predicate. The purpose of this is to make proofs by simple induction easy, so there is no need of using pair_induction. The main idea is that we are going to prove some properties of even2 and then we'll use the fact that Nat.even and even2 are extensionally equal to transfer the properties of even2 onto Nat.even.

Require Import Coq.Bool.Bool.

Fixpoint even2 (n : nat) : bool :=
  match n with
  | O => true
  | S n' => negb (even2 n')
  end.

Let's show that Nat.even and even2 are extensionally equal.

Lemma even_S n :
  Nat.even (S n) = negb (Nat.even n).n: nat
Nat.even (S n) = negb (Nat.even n)
Proof.n: nat
Nat.even (S n) = negb (Nat.even n) induction n; auto.n: nat
IHn: Nat.even (S n) = negb (Nat.even n)
Nat.even (S (S n)) = negb (Nat.even (S n)) apply negb_sym; assumption. Qed.

Lemma even_equiv_even2 n :
  Nat.even n = even2 n.n: nat
Nat.even n = even2 n
Proof.n: nat
Nat.even n = even2 n induction n; auto.n: nat
IHn: Nat.even n = even2 n
Nat.even (S n) = even2 (S n) now rewrite even_S, IHn. Qed.

Some distribution lemmas for even2:

Lemma even2_distr_add m n :
  even2 (m + n) = negb (xorb (even2 m) (even2 n)).m, n: nat
even2 (m + n) = negb (xorb (even2 m) (even2 n))
Proof.m, n: nat
even2 (m + n) = negb (xorb (even2 m) (even2 n))
  induction m; simpl.n: nat
even2 n = negb (if even2 n then false else true)
m, n: nat
IHm: even2 (m + n) = negb (xorb (even2 m) (even2 n))
negb (even2 (m + n)) =
negb (xorb (negb (even2 m)) (even2 n))
  -n: nat
even2 n = negb (if even2 n then false else true) now destruct (even2 n).
  -m, n: nat
IHm: even2 (m + n) = negb (xorb (even2 m) (even2 n))
negb (even2 (m + n)) =
negb (xorb (negb (even2 m)) (even2 n)) rewrite IHm.m, n: nat
IHm: even2 (m + n) = negb (xorb (even2 m) (even2 n))
negb (negb (xorb (even2 m) (even2 n))) =
negb (xorb (negb (even2 m)) (even2 n)) now destruct (even2 m); destruct (even2 n).
Qed.

Lemma even2_distr_mult m n :
  even2 (m * n) = even2 m || even2 n.m, n: nat
even2 (m * n) = even2 m || even2 n
Proof.m, n: nat
even2 (m * n) = even2 m || even2 n
  induction m; auto; simpl.m, n: nat
IHm: even2 (m * n) = even2 m || even2 n
even2 (n + m * n) = negb (even2 m) || even2 n
  rewrite even2_distr_add, IHm.m, n: nat
IHm: even2 (m * n) = even2 m || even2 n
negb (xorb (even2 n) (even2 m || even2 n)) =
negb (even2 m) || even2 n
  now destruct (even2 m); destruct (even2 n).
Qed.

Finally, we are able to prove our goal, using the equality between Nat.even and even2.

Goal forall n, Nat.even (n * (S n)) = true.forall n : nat, Nat.even (n * S n) = true
  intros n.n: nat
Nat.even (n * S n) = true
  now rewrite even_equiv_even2, even2_distr_mult, orb_negb_r.
Qed.

Answer (Anton Trunov)

A short version that makes use of the standard library:

Require Import Coq.Arith.Arith.

Goal forall n, Nat.even (n * (S n)) = true.forall n : nat, Nat.even (n * S n) = true
  intros n.n: nat
Nat.even (n * S n) = true
  now rewrite Nat.even_mul, Nat.even_succ, Nat.orb_even_odd.
Qed.

Answer (Olivier Verdier)

For what it's worth, here is my take on the solution. The essential idea is, instead of proving a predicate P n, prove instead P n /\ P (S n), which is equivalent, but the second formulation allows to use simple induction.

Here is the complete proof:

Require Import Nat.
Require Import Lia.

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.forall n m : nat,
even n = true -> even (n + 2 * m) = true
Proof.forall n m : nat,
even n = true -> even (n + 2 * m) = true
  intros.n, m: nat
H: even n = true
even (n + 2 * m) = true induction m.n: nat
H: even n = true
even (n + 2 * 0) = true
n, m: nat
H: even n = true
IHm: even (n + 2 * m) = true
even (n + 2 * S m) = true
  -n: nat
H: even n = true
even (n + 2 * 0) = true simpl.n: nat
H: even n = true
even (n + 0) = true replace (n + 0) with n; intuition.
  -n, m: nat
H: even n = true
IHm: even (n + 2 * m) = true
even (n + 2 * S m) = true replace (n + 2 * S m) with (S (S (n + 2 * m))); [intuition | lia].
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))).forall n : nat,
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.forall n : nat,
S (S n) * S (S (S n)) = S n * S (S n) + 2 * S (S n)
  intro.n: nat
S (S n) * S (S (S n)) = S n * S (S n) + 2 * S (S n)
  replace (S (S (S n))) with ((S n) + 2) by lia.n: nat
S (S n) * (S n + 2) = S n * S (S n) + 2 * S (S n)
  remember (S (S n)) as m.n, m: nat
Heqm: m = S (S n)
m * (S n + 2) = S n * m + 2 * m
  replace (m * (S n + 2)) with ((S n + 2) * m) by lia.n, m: nat
Heqm: m = S (S n)
(S n + 2) * m = S n * m + 2 * m
  intuition.
Qed.

(* The claim to be proved by simple induction *)
Lemma nsn : forall n, claim n /\ claim (S n).forall n : nat, claim n /\ claim (S n)
Proof.forall n : nat, claim n /\ claim (S n)
  intros.n: nat
claim n /\ claim (S n)
  unfold claim.n: nat
even (n * S n) = true /\ even (S n * S (S n)) = true
  induction n.even (0 * 1) = true /\ even (1 * 2) = true
n: nat
IHn: even (n * S n) = true /\ even (S n * S (S n)) = true
even (S n * S (S n)) = true /\
even (S (S n) * S (S (S n))) = true
  -even (0 * 1) = true /\ even (1 * 2) = true intuition.
  -n: nat
IHn: even (n * S n) = true /\ even (S n * S (S n)) = true
even (S n * S (S n)) = true /\
even (S (S n) * S (S (S n))) = true intuition.n: nat
H: even (n * S n) = true
H0: even (S n * S (S n)) = true
even (S (S n) * S (S (S n))) = true rewrite ident.n: nat
H: even (n * S n) = true
H0: even (S n * S (S n)) = true
even (S n * S (S n) + 2 * S (S n)) = true apply tech; auto.
Qed.