Coincé même sur le lemme avec existe

Question

Je suis bloqué sur un lemme "laissé en exercice" de cette conférence.Ça va comme ça:

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

Où even est un prédicat inductif défini comme ceci :

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

Aidez-moi, s'il vous plaît?je finis toujours par (S (S p) = 2 ou similaire.

MODIFIER

Quelques lemmes et tactiques que j'ai utilisés (preuve non complète) :

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

Answer 1

Après votre étape d’intégration, vous devriez avoir deux objectifs.

Le premier (scénario de base pour even0) devrait être facile à prouver.Le témoin existentiel doit être choisi pour être 0, après quoi l'objectif doit être retenu par réflexivité.

Le deuxième cas (pour evenS) ressemblerait à :

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

IHeven dit qu'il existe un nombre (appelons-le k1) tel que p = 2 * k1.

Votre objectif est d'exposer un nombre (disons, k2) de telle sorte que vous puissiez prouver S (S p) = 2 * k2.

Si tu fais le calcul, tu devrais voir ça (S k1) serait le candidat idéal.

Donc, pour continuer, vous pouvez utiliser les tactiques suivantes :

• destruct détruire IHeven séparer un témoin k1 et une preuve que p = 2 * k1.
• exists exposer (S k1) comme témoin existentiel de votre objectif.
• puis certains travaillent pour prouver que l'égalité est vraie.