Instrucciones
Determina si un número es perfecto, abundante o deficiente según el esquema de clasificación de Nicómaco (60 - 120 d. C.) para los enteros positivos.
El matemático griego Nicómaco ideó un esquema de clasificación de los enteros positivos en el que cada uno pertenece de forma ú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 propio número.
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 devuelto sea un tipo inductivo Classification que debes definir.
Este tipo debe tener una instancia de BEq, es decir, admite una prueba de igualdad de valores 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 concreto que cumplen un predicado.
Positive representa los elementos de Nat que son mayores que 0.
Cualquier elemento de un subtipo se puede ver como un par formado por un valor del tipo subyacente y una demostración, en el sentido matemático, de que ese valor cumple el predicado correspondiente.
Los subtipos imponen invariantes a nivel de tipo, lo que garantiza que no se puedan construir valores mal formados.
