دستورالعمل‌ها
بر اساس طرح طبقه‌بندی نیکوماخوس (۶۰ تا ۱۲۰ میلادی) برای اعداد صحیح مثبت، مشخص کنید که یک عدد perfect است، abundant است یا deficient.
ریاضیدان یونانی، نیکوماخوس، طرحی برای طبقه‌بندی اعداد صحیح مثبت ابداع کرد که هر عدد را به‌طور یکتا در یکی از دسته‌های 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 هستند
Task
راهی پیاده‌سازی کنید تا مشخص شود یک عدد داده‌شده perfect است یا نه.
بسته به مسیر زبان شما، ممکن است لازم باشد راهی هم پیاده‌سازی کنید تا مشخص شود آن عدد abundant یا deficient است.
تعریف یک نوع استقرایی
این تمرین انتظار دارد که مقدار بازگشتی یک نوع استقرایی به اسم Classification باشد که باید خودتان آن را تعریف کنید.
این نوع باید یک نمونه از BEq داشته باشد، یعنی آزمون برابری منطقی را می‌پذیرد، و یک نمونه از Repr، یعنی مقادیر این نوع می‌توانند برای نمایش قالب‌بندی شوند.
می‌توانید به این صفحه درباره‌ی اعلان نمونه‌ها مراجعه کنید.
Lean می‌تواند به‌طور خودکار برای بسیاری از کلاس‌ها نمونه بسازد.
زیرنوع‌ها
آرگومان تابع classify یک زیرنوع به اسم Positive است:
def Positive := { x : Nat // x > 0 }
زیرنوع‌ها عنصرهایی از یک نوع خاص را نمایش می‌دهند که یک محمول را برآورده می‌کنند.
Positive عنصرهای Nat را نمایش می‌دهد که بزرگ‌تر از 0 هستند.
هر عنصر از یک زیرنوع را می‌توان به‌صورت یک جفت در نظر گرفت که از یک مقدار از نوع زیرین و یک اثبات، به معنای ریاضی، تشکیل شده است که آن مقدار محمول متناظر را برآورده می‌کند.
زیرنوع‌ها ناورداها را در سطح نوع اعمال می‌کنند و تضمین می‌کنند که مقادیر بدشکل ساخته نشوند.
