التعليمات
حدّد ما إذا كان العدد perfect أو abundant أو deficient، بناءً على مخطط التصنيف الذي وضعه نيقوماخوس (60 - 120 م) للأعداد الصحيحة الموجبة.
وضع عالم الرياضيات الإغريقي نيقوماخوس مخططًا لتصنيف الأعداد الصحيحة الموجبة، يحدّد فيه انتماء كل عدد انتماءً وحيدًا إلى إحدى فئات perfect أو abundant أو deficient، وذلك استنادًا إلى مجموع القواسم الفعلية.
ويُعرَّف مجموع القواسم الفعلية بأنه مجموع قواسم العدد، دون احتساب العدد نفسه.
على سبيل المثال، مجموع القواسم الفعلية للعدد 15 هو 1 + 3 + 5 = 9.
Perfect
العدد perfect هو الذي يساوي مجموع قواسمه الفعلية.
على سبيل المثال:
-
6 عدد perfect لأن 1 + 2 + 3 = 6
-
28 عدد perfect لأن 1 + 2 + 4 + 7 + 14 = 28
Abundant
العدد abundant هو الذي يقل عن مجموع قواسمه الفعلية.
على سبيل المثال:
-
12 عدد abundant لأن 1 + 2 + 3 + 4 + 6 = 16
-
24 عدد abundant لأن 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Deficient
العدد deficient هو الذي يزيد عن مجموع قواسمه الفعلية.
على سبيل المثال:
-
8 عدد deficient لأن 1 + 2 + 4 = 7
- الأعداد الأولية أعداد deficient
المهمة
نفّذ أسلوبًا لتحديد ما إذا كان العدد المعطى perfect.
وقد تحتاج أيضًا، حسب مسار اللغة الذي تتبعه، إلى تنفيذ أسلوب لتحديد ما إذا كان العدد المعطى abundant أو deficient.
تعريف نوع استقرائي
يتوقع هذا التمرين أن تكون قيمة الإرجاع من نوع استقرائي باسم Classification يجب عليك تعريفه.
يجب أن يمتلك هذا النوع نسخة BEq، أي أنه يقبل اختبار مساواة منطقي، ونسخة Repr، أي أنه يمكن تنسيق قيم هذا النوع للعرض.
يمكنك الرجوع إلى هذه الصفحة حول إعلانات النسخ.
يستطيع Lean تلقائيًا توليد نسخ للعديد من الأصناف.
الأنواع الفرعية
الوسيط المُمرَّر إلى دالة classify هو نوع فرعي يُسمى Positive:
def Positive := { x : Nat // x > 0 }
تمثل الأنواع الفرعية عناصر من نوع معين تحقق محمولًا.
يمثل Positive عناصر Nat التي تزيد عن 0.
يمكن التفكير في أي عنصر من نوع فرعي على أنه زوج يتكون من قيمة من النوع الأساسي وبرهان، بالمعنى الرياضي، على أن هذه القيمة تحقق المحمول المقابل.
تفرض الأنواع الفرعية ثوابت على مستوى النوع، مما يضمن أنه لا يمكن بناء قيم غير سليمة البنية.
