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?

(Edited the goal output.)

`Nat.Even`

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

Thanks!

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

Julin S has marked this topic as resolved.

Last updated: Jun 16 2024 at 02:41 UTC