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