存在する偶数の補題に引っかかる

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

導入ステップが終了したら、2 つの目標を設定する必要があります。

最初のもの (基本ケース) even0）証明するのは簡単なはずです。存在の証人は次のように選ばれるべきです 0, 、その後、反射性によって目標が保持されるはずです。

2番目のケース（ 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) あなたの目標の実存の証人として。
• 次に、等価性が成り立つことを証明するためにいくつかの作業が行われます。