سؤال
أنا عالق في 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
المحلول
بعد الخطوة التعريفية، يجب أن يكون لديك هدفين.
الأول (الحالة الأساسية لـ 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)
كشاهد وجودي لهدفك.- ثم يعمل البعض على إثبات صحة المساواة.