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?
n is not it, right?
And would we be better off using
Nat.even instead of
(Edited the goal output.)
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.
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