Bloccato anche il lemma con esiste

Question

Sono bloccato su un Lemma "Sinistra come esercizio" da Questa conferenza .Va così:

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

.

Dove even è un predicato induttivo definito come questo:

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

.

Aiuto, per favore?Finisco sempre con (S (S p) = 2 o simili.

Modifica

Alcuni lemmi e tattiche che ho usato (non completo di prova):

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

.

Answer 1

Dopo il tuo passaggio di induzione, dovresti avere due gol.

Il primo (caso base per even0) dovrebbe essere facile da dimostrare. Il testimone esistenziale dovrebbe essere scelto per essere 0, dopo di che l'obiettivo dovrebbe contenere la riflessività.

Il secondo caso (per evenS) sarebbe simile a

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

.

IHeven dice che esiste un numero (chiamiamolo k1) in modo tale che p = 2 * k1.

Il tuo obiettivo è quello di mostrare un numero (dire, k2) in modo tale da poter provare S (S p) = 2 * k2.

Se fai la matematica, dovresti vedere che (S k1) sarebbe il candidato perfetto.

Pertanto per procedere è possibile utilizzare le seguenti tattiche:

.
• destruct per distruggere IHeven per separare un testimone k1 e una prova che p = 2 * k1.
• exists per mostrare (S k1) come testimone esistenziale per il tuo obiettivo.
• Quindi alcuni lavori per dimostrare che l'uguaglianza tiene.