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: Sep 23 2023 at 08:01 UTC