Utasítások
Döntsd el egy számról, hogy Nikomakhosz (i. sz. 60–120) pozitív egészekre vonatkozó osztályozási rendszere alapján tökéletes, bővelkedő vagy hiányos-e.
A görög matematikus, Nikomakhosz a pozitív egészek osztályozására dolgozott ki egy rendszert, amelyben minden szám a valódi osztók összege alapján egyértelműen a tökéletes, a bővelkedő vagy a hiányos kategóriák valamelyikébe tartozik.
A valódi osztók összege a szám önmagát nem tartalmazó osztóinak összege.
Például a 15 esetében a valódi osztók összege 1 + 3 + 5 = 9.
Tökéletes
Egy szám akkor tökéletes, ha megegyezik a valódi osztóinak összegével.
Például:
- A
6 tökéletes szám, mert 1 + 2 + 3 = 6
- A
28 tökéletes szám, mert 1 + 2 + 4 + 7 + 14 = 28
Bővelkedő
Egy szám akkor bővelkedő, ha kisebb a valódi osztóinak összegénél.
Például:
- A
12 bővelkedő szám, mert 1 + 2 + 3 + 4 + 6 = 16
- A
24 bővelkedő szám, mert 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Hiányos
Egy szám akkor hiányos, ha nagyobb a valódi osztóinak összegénél.
Például:
- A
8 hiányos szám, mert 1 + 2 + 4 = 7
- A prímszámok hiányosak.
Feladat
Készíts egy megoldást, amely meghatározza, hogy egy adott szám tökéletes-e.
A kurzustól függően arra is szükség lehet, hogy megállapítsd egy adott számról, bővelkedő-e vagy hiányos.
Induktív típus definiálása
Ez a feladat elvárja, hogy a visszatérési érték egy induktív típus Classification legyen, amelyet neked kell definiálnod.
Ennek a típusnak rendelkeznie kell egy BEq példánnyal, azaz lehetővé kell tennie a Boolean egyenlőségvizsgálatot, és egy Repr példánnyal, azaz a típus értékei formázhatók megjelenítéshez.
A példánydeklarációkról ezen az oldalon olvashatsz.
A Lean sok osztályhoz automatikusan tud példányokat generálni.
Altípusok
A classify függvény argumentuma egy Positive nevű altípus:
def Positive := { x : Nat // x > 0 }
Az altípusok egy adott típus azon elemeit reprezentálják, amelyek kielégítenek egy predikátumot.
A Positive a Nat 0-nál nagyobb elemeit reprezentálja.
Egy altípus bármely eleme tekinthető egy párnak, amely az alaptípus egy értékéből és egy bizonyításból áll; a bizonyítás matematikai értelemben azt igazolja, hogy ez az érték kielégíti a megfelelő predikátumot.
Az altípusok a típus szintjén kényszerítik ki az invariánsokat, biztosítva, hogy hibás formájú értékeket ne lehessen létrehozni.
