العمل على البديهيات في بانو في AGDA وضرب قليلاً من نقطة ملتصقة

Question

PA6 : ∀{m n} -> m ≡ n -> n ≡ m

هل البديهية التي أحاول حلها ودعمها ، لقد حاولت استخدام Cong (من المكتبة الأساسية) ولكنني أواجه مشكلات مع مُنشئ Cong

PA6 = cong

لا يحصل على أي مكان ، وأنا أعلم بالنسبة لـ Cong ، فأنا مطالب بتزويده بالمساواة ونوع ، لكنني لست متأكدًا من النوع الذي من المفترض أن أقدمه. أفكار؟

هذا لمهمة صغيرة في الجامعة ، لذلك أفضل أن يوضح شخص ما ما فاتني بدلاً من كتابة الإجابة الحادة ، لكنني أقدر أي درجة من الدعم.

Answer 1

من خلال طبيعة النظام الذي أنشأته ، كان علي أن أدرك أن لديّ معادلين وبالتالي كنت بحاجة لاستخدام طريقة التكافؤ

وبالتالي فإن إرضاء نوع التوقيع الخاص بي قد تم قبول AGDA: PA6 refl = refl

امل ان يساعد

Answer 2

يقول PA6 الخاص بك أن ≡ هو متماثل.

يمكن العثور على ذلك في المكتبة القياسية من وحدة العلاقة.

sym : ∀ {a} {A : Set a} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

(هذا السؤال قديم جدًا ، لكنني أنشر لصالح القراء المستقبليين الذين يتعثرون عليه.)