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

score 3 · Accepted Answer

在你的归纳步骤之后，你应该有两个目标。

第一个（基本情况even0）应该很容易证明。存在的见证应该被选为0，然后目标应该通过自反性来保持。

第二种情况（for evenS）看起来像：

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

IHeven说存在一个数字（让我们命名它k1）使得p = 2 * k1.

您的目标是展示一个数字（例如k2），以便您可以证明S (S p) = 2 * k2。

如果您进行数学计算，您应该会发现那(S k1)将是完美的候选人。

因此，要继续，您可以使用以下策略：

1 回答 1