Instructions
Détermine si un nombre est parfait, abondant ou déficient, d'après le système de classification des entiers positifs établi par Nicomaque (60 - 120 apr. J.-C.).
Le mathématicien grec Nicomaque a conçu un système de classification des entiers positifs qui range chacun d'eux dans une seule catégorie : parfait, abondant ou déficient, selon sa somme aliquote.
La somme aliquote se définit comme la somme des diviseurs d'un nombre, sans compter le nombre lui-même.
Par exemple, la somme aliquote de 15 est 1 + 3 + 5 = 9.
Parfait
Un nombre est parfait lorsqu'il est égal à sa somme aliquote.
Par exemple :
-
6 est un nombre parfait car 1 + 2 + 3 = 6
-
28 est un nombre parfait car 1 + 2 + 4 + 7 + 14 = 28
Abondant
Un nombre est abondant lorsqu'il est inférieur à sa somme aliquote.
Par exemple :
-
12 est un nombre abondant car 1 + 2 + 3 + 4 + 6 = 16
-
24 est un nombre abondant car 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Déficient
Un nombre est déficient lorsqu'il est supérieur à sa somme aliquote.
Par exemple :
-
8 est un nombre déficient car 1 + 2 + 4 = 7
- Les nombres premiers sont déficients.
Tâche
Implémente un moyen de déterminer si un nombre donné est parfait.
Selon le langage de ton parcours, tu devras peut-être aussi implémenter un moyen de déterminer si un nombre donné est abondant ou déficient.
Définir un type inductif
Cet exercice attend que la valeur de retour soit un type inductif Classification que tu dois définir.
Ce type doit posséder une instance BEq, c'est-à-dire qu'il admet un test d'égalité booléenne, ainsi qu'une instance Repr, c'est-à-dire que les valeurs de ce type peuvent être formatées pour l'affichage.
Tu peux consulter cette page sur les déclarations d'instances.
Lean peut générer automatiquement des instances pour de nombreuses classes.
Sous-types
L'argument de la fonction classify est un sous-type appelé Positive :
def Positive := { x : Nat // x > 0 }
Les sous-types représentent les éléments d'un type donné qui satisfont un prédicat.
Positive représente les éléments de Nat qui sont supérieurs à 0.
Tout élément d'un sous-type peut être vu comme un couple formé d'une valeur du type sous-jacent et d'une preuve, au sens mathématique, que cette valeur satisfait le prédicat correspondant.
Les sous-types font respecter des invariants au niveau du type, ce qui garantit que des valeurs mal formées ne peuvent pas être construites.
