Instrucciones
Determina si un número es perfecto, abundante o deficiente según el esquema de clasificación de Nicómaco (60 - 120 de la era común) para los enteros positivos.
El matemático griego Nicómaco ideó un esquema de clasificación para los enteros positivos, que identifica cada uno como perteneciente de manera única a las categorías de perfecto, abundante o deficiente según su suma alícuota.
La suma alícuota se define como la suma de los factores de un número, sin incluir el número mismo.
Por ejemplo, la suma alícuota de 15 es 1 + 3 + 5 = 9.
Perfecto
Un número es perfecto cuando es igual a su suma alícuota.
Por ejemplo:
-
6 es un número perfecto porque 1 + 2 + 3 = 6
-
28 es un número perfecto porque 1 + 2 + 4 + 7 + 14 = 28
Abundante
Un número es abundante cuando es menor que su suma alícuota.
Por ejemplo:
-
12 es un número abundante porque 1 + 2 + 3 + 4 + 6 = 16
-
24 es un número abundante porque 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Deficiente
Un número es deficiente cuando es mayor que su suma alícuota.
Por ejemplo:
-
8 es un número deficiente porque 1 + 2 + 4 = 7
- Los números primos son deficientes
Tarea
Implementa una forma de determinar si un número dado es perfecto.
Según el track de tu lenguaje, es posible que también tengas que implementar una forma de determinar si un número dado es abundante o deficiente.
Definir un tipo inductivo
Este ejercicio espera que el valor de retorno sea un tipo inductivo Classification que debes definir.
Este tipo debe tener una instancia de BEq, es decir, admite una prueba de igualdad Boolean, y una instancia de Repr, es decir, los valores del tipo se pueden formatear para mostrarlos.
Puedes consultar esta página sobre declaraciones de instancias.
Lean puede generar instancias automáticamente para muchas clases.
Subtipos
El argumento de la función classify es un subtipo llamado Positive:
def Positive := { x : Nat // x > 0 }
Los subtipos representan elementos de un tipo determinado que satisfacen un predicado.
Positive representa elementos de Nat que son mayores que 0.
Cualquier elemento de un subtipo se puede pensar como un par formado por un valor del tipo subyacente y una prueba, en el sentido matemático, de que ese valor satisface el predicado correspondiente.
Los subtipos imponen invariantes a nivel del tipo, lo que garantiza que no se puedan construir valores mal formados.
