Застрял на четной лемме с exists

Question

Я застрял на лемме "оставлено в качестве упражнения" из эта лекция.Это происходит примерно так:

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

Где even определяется ли индуктивный предикат следующим образом:

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

Помогите, пожалуйста?Я всегда заканчиваю тем, что (S (S p) = 2 или что-то подобное.

Редактировать

Некоторые леммы и тактики, которые я использовал (не полное доказательство):

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

Answer 1

После вводного этапа у вас должны быть две цели.

Первый (базовый вариант для even0) должно быть легко доказать.Экзистенциальный свидетель должен быть выбран таким, чтобы быть 0, после чего цель должна удерживаться рефлексивно.

Второй случай (для 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) был бы идеальным кандидатом.

Итак, чтобы действовать дальше, вы можете использовать следующую тактику:

• destruct чтобы уничтожить IHeven чтобы отделить свидетеля k1 и доказательство того , что p = 2 * k1.
• exists выставлять напоказ (S k1) как экзистенциальный свидетель вашей цели.
• затем проделайте некоторую работу, чтобы доказать, что равенство справедливо.