Instruções
Determina se um número é perfeito, abundante ou deficiente, com base no esquema de classificação de Nicómaco (60 - 120 d.C.) para números inteiros positivos.
O matemático grego Nicómaco concebeu um esquema de classificação para os números inteiros positivos, identificando cada um como pertencendo de forma única às categorias de perfeito, abundante ou deficiente, com base na sua soma dos divisores próprios.
A soma dos divisores próprios é definida como a soma dos fatores de um número, sem incluir o próprio número.
Por exemplo, a soma dos divisores próprios de 15 é 1 + 3 + 5 = 9.
Perfeito
Um número é perfeito quando é igual à sua soma dos divisores próprios.
Por exemplo:
-
6 é um número perfeito porque 1 + 2 + 3 = 6
-
28 é um número perfeito porque 1 + 2 + 4 + 7 + 14 = 28
Abundante
Um número é abundante quando é menor do que a sua soma dos divisores próprios.
Por exemplo:
-
12 é um número abundante porque 1 + 2 + 3 + 4 + 6 = 16
-
24 é um número abundante porque 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Deficiente
Um número é deficiente quando é maior do que a sua soma dos divisores próprios.
Por exemplo:
-
8 é um número deficiente porque 1 + 2 + 4 = 7
- Os números primos são deficientes
Tarefa
Implementa uma forma de determinar se um determinado número é perfeito.
Dependendo da linguagem que estás a aprender, podes também ter de implementar uma forma de determinar se um determinado número é abundante ou deficiente.
Definir um tipo indutivo
Este exercício espera que o valor devolvido seja um tipo indutivo Classification que tens de definir.
Este tipo tem de ter uma instância de BEq, ou seja, tem de admitir um teste de igualdade Boolean, e uma instância de Repr, ou seja, os valores do tipo podem ser formatados para apresentação.
Podes consultar esta página sobre declarações de instâncias.
O Lean consegue gerar instâncias automaticamente para muitas classes.
Subtipos
O argumento da função classify é um subtipo chamado Positive:
def Positive := { x : Nat // x > 0 }
Os subtipos representam elementos de um determinado tipo que satisfazem um predicado.
Positive representa os elementos de Nat que são maiores que 0.
Qualquer elemento de um subtipo pode ser visto como um par formado por um valor do tipo subjacente e uma prova, no sentido matemático, de que esse valor satisfaz o predicado correspondente.
Os subtipos impõem invariantes ao nível do tipo, garantindo que não é possível construir valores mal formados.
