Stuck on even lemma with exists

Question

I'm stuck on a lemma "left as an exercise" from this lecture. It goes like this:

Lemma even_double : forall n, even n -> exists k, n = 2 * k.
Proof.
  intros n H.
  induction H.
  ...

Where even is an inductive predicate defined like this:

Inductive even : nat -> Prop :=
| even0 : even 0
| evenS : forall p:nat, even p -> even (S (S p).

Help, please? I always end up with (S (S p) = 2 or similar.

EDIT

Some lemmas and tactics I used (not complete proof):

destruct IHeven
exists (S x)
rewrite mult_succ_l
apply eq_S
apply plus_n_Sm

Answer 1

After your induction step, you should have two goals.

The first one (base case for even0) should be easy to prove. The existential witness should be picked to be 0, after which the goal should hold by reflexivity.

The second case (for evenS) would look like:

p : nat
H : even p
IHeven : exists k : nat, p = 2 * k
============================
 exists k : nat, S (S p) = 2 * k

IHeven says that there exists a number (let's name it k1) such that p = 2 * k1.

Your goal is to exhibit a number (say, k2) such that you can prove S (S p) = 2 * k2.

If you do the math, you should see that (S k1) would be the perfect candidate.

So to proceed you can use the following tactics:

• destruct to destruct IHeven to separate a witness k1 and a proof that p = 2 * k1.
• exists to exhibit (S k1) as the existential witness for you goal.
• then some work to prove that the equality holds.