Вказівки
Визначте, чи є число досконалим, надлишковим або недостатнім, за схемою класифікації Нікомаха (60 - 120 рр. н. е.) для додатних цілих чисел.
Грецький математик Нікомах розробив схему класифікації додатних цілих чисел, за якою кожне з них належить рівно до однієї з категорій: досконале, надлишкове або недостатнє, залежно від суми власних дільників.
Суму власних дільників визначають як суму всіх дільників числа, крім самого числа.
Наприклад, сума власних дільників числа 15 дорівнює 1 + 3 + 5 = 9.
Досконале
Число є досконалим, коли воно дорівнює сумі своїх власних дільників.
Наприклад:
-
6 є досконалим числом, бо 1 + 2 + 3 = 6
-
28 є досконалим числом, бо 1 + 2 + 4 + 7 + 14 = 28
Надлишкове
Число є надлишковим, коли воно менше за суму своїх власних дільників.
Наприклад:
-
12 є надлишковим числом, бо 1 + 2 + 3 + 4 + 6 = 16
-
24 є надлишковим числом, бо 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Недостатнє
Число є недостатнім, коли воно більше за суму своїх власних дільників.
Наприклад:
-
8 є недостатнім числом, бо 1 + 2 + 4 = 7
- Прості числа є недостатніми
Завдання
Реалізуйте спосіб визначати, чи є задане число досконалим.
Залежно від мовного треку, можливо, також потрібно реалізувати спосіб визначати, чи є задане число надлишковим або недостатнім.
Визначення індуктивного типу
У цій вправі повернене значення має бути індуктивним типом Classification, який ми маємо визначити.
Цей тип повинен мати екземпляр BEq, тобто допускати булеву перевірку на рівність, та екземпляр Repr, тобто значення цього типу можна відформатувати для відображення.
Можна звернутися до цієї сторінки про оголошення екземплярів.
Lean може автоматично генерувати екземпляри для багатьох класів.
Підтипи
Аргумент функції classify - це підтип під назвою Positive:
def Positive := { x : Nat // x > 0 }
Підтипи представляють елементи певного типу, які задовольняють предикат.
Positive представляє елементи Nat, які більші за 0.
Будь-який елемент підтипу можна уявити як пару, що складається зі значення базового типу та доведення, у математичному сенсі, що це значення задовольняє відповідний предикат.
Підтипи забезпечують інваріанти на рівні типу, завдяки чому некоректні значення неможливо створити.
