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
La solution
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étruireIHeven
séparer un témoink1
et une preuve quep = 2 * k1
.exists
exposer(S k1)
comme témoin existentiel de votre objectif.- puis certains travaillent pour prouver que l'égalité est vraie.