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

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?

I would start proving that `even n -> even (n * m)` (for all `m`). Then since `even n <-> (even (S n) = false)` and `n*m = m*n` you should be able to prove that `even (n * (S n))`. Not sure whether this simplies anything though... — Bakuriu, Nov 24 '16 at 17:33
Do you think "even n -> even (n * m)" would be easy to prove? — Shuzheng, Nov 24 '16 at 18:07
Maybe. consider that: `n * (S m') = n + n * m'` by inductive hypothesis `n*m'` is even and `even n /\ even m -> even (n+m)` which yields the thesis. — Bakuriu, Nov 24 '16 at 18:13
Thanks, but then "even (n + m)" seems hard to prove (although easy at first sight). — Shuzheng, Nov 24 '16 at 18:17
Why? If `n = O` then using `simpl` gets you `n+m = m` which is even by hypothesis. If `n = (S (S n'))` then using `simpl` you get `S (S (n' + m))` which by inductive hypothesis + the fact that `even n <-> even (S ( S n))` yields the thesis. You just need `even n -> (n = O \/ n = S (S n') /\ even n')` which doesn't seem hard to prove inductively. — Bakuriu, Nov 24 '16 at 19:37

score 5 · Answer 1 · edited May 23 '17 at 12:13

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.
Proof.
  intros ? ? ? n. enough (P n /\ P (S n)) by tauto.
  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.
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.

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.
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.

Now, the proof of the goal is trivial

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?

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.

(1) You can issue this query: `Print orb.` to check what it is. It's boolean "or". Of course you can do it without pair induction -- remember, it's user-defined, it's not some hidden Coq mechanism. It's just a method of strengthening the induction hypothesis. — Anton Trunov, Nov 25 '16 at 06:15
@Shuzheng I've simplified the proof of the goal. The proofs could be simpler if you defined `even` as `Fixpoint even (n: nat) : bool := match n with | O => true | S n' => negb (even n') end.` — Anton Trunov, Nov 25 '16 at 06:23

score 3 · Answer 2 · answered Nov 25 '16 at 02:18

3

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

From mathcomp Require Import all_ssreflect all_algebra.

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

odd_mul is proved by simple induction, as well as odd_add.

answered Nov 25 '16 at 02:18

ejgallego

6,709
1
14
29

The definition of `odd` here has different structure comparing to `even` in the question, that's why simple induction works well in this case. – Anton Trunov Nov 25 '16 at 05:57

score 2 · Accepted Answer · answered Nov 25 '16 at 08:18

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).
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.

Some distribution lemmas for 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.

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.
  intros n.
  now rewrite even_equiv_even2, even2_distr_mult, orb_negb_r.
Qed.

I'm in deep trouble proving "even_add_even". I've attached my partial proof in the question. Here "nat_ind2" is your "pair_induction". Can you give me a hint how to proceed? — Shuzheng, Nov 25 '16 at 12:54

score 2 · Answer 4 · answered Nov 25 '16 at 19:07

2

A short version that makes use of the standard library:

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.

answered Nov 25 '16 at 19:07

Anton Trunov

15,074
2
23
43

score 1 · Answer 5 · answered Dec 02 '16 at 12:54

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 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.

Thanks, it is a nice proof :-) – Shuzheng Dec 03 '16 at 15:05 — Shuzheng, Dec 03 '16 at 15:05

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

5 Answers5