Stream: Coq users

Topic: ✔ Proof: Sum of even nos is even

Julin S (Sep 15 2022 at 06:54):

I was trying to prove that the sum of two even numbers would be even in coq.

But didn't get much further than stating it.

Require Import Arith.

Definition even_even : forall n m:nat,
    ((Nat.Even n) /\ (Nat.Even m))
    -> Nat.Even (n+m).
  intros n m H.
  destruct H.

Goal at this point was:

1 subgoal (ID 9)

  n, m : nat
  H : Nat.Even n
  H0 : Nat.Even m
  ============================
  Nat.Even (n + m)

How can we go from here?

Induction on n is not it, right?

And would we be better off using Nat.even instead of Nat.Even somewhere?

Julin S (Sep 15 2022 at 06:58):

(Edited the goal output.)

Pierre Castéran (Sep 15 2022 at 07:14):

Nat.Evenis defined through an existential quantification.

Nat.Even = fun n : nat => exists m : nat, n = 2 * m
     : nat -> Prop

Here's a proof.

Require Import Arith Lia.

Lemma even_even : forall n m:nat,  Nat.Even n /\ Nat.Even m -> Nat.Even (n+m).
  Proof.
      intros n m [[p Hp] [q Hq]].
      exists (p + q); lia.
Qed.

Julin S (Sep 15 2022 at 08:50):

Thanks!

Julin S (Sep 15 2022 at 12:11):

unfolding the Nat.Even allowed to see the exists itself.

Notification Bot (Sep 15 2022 at 12:11):

Julin S has marked this topic as resolved.

Last updated: Sep 23 2023 at 08:01 UTC