عالقة حتى مع وجودها

Question

أنا عالق في lemma "اليسار كتمرين" من هذه المحاضرة.تسير الأمور على هذا النحو:

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) كشاهد وجودي لهدفك.
• ثم يعمل البعض على إثبات صحة المساواة.