Instruções
Determine se um número é perfect, abundant ou deficient, com base no esquema de classificação de Nicômaco (60 - 120 d.C.) para os números inteiros positivos.
O matemático grego Nicômaco criou um esquema de classificação para os números inteiros positivos, identificando cada um como pertencente de forma única às categorias perfect, abundant ou deficient, com base na sua soma dos divisores próprios.
A soma dos divisores próprios é definida como a soma dos divisores 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.
Perfect
Um número é perfect quando é igual à sua soma dos divisores próprios.
Por exemplo:
-
6 é um número perfect porque 1 + 2 + 3 = 6
-
28 é um número perfect porque 1 + 2 + 4 + 7 + 14 = 28
Abundant
Um número é abundant quando é menor que a sua soma dos divisores próprios.
Por exemplo:
-
12 é um número abundant porque 1 + 2 + 3 + 4 + 6 = 16
-
24 é um número abundant porque 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Deficient
Um número é deficient quando é maior que a sua soma dos divisores próprios.
Por exemplo:
-
8 é um número deficient porque 1 + 2 + 4 = 7
- Números primos são deficient
Tarefa
Implemente uma forma de determinar se um dado número é perfect.
Dependendo da sua trilha de linguagem, você também pode precisar implementar uma forma de determinar se um dado número é abundant ou deficient.
Definindo um tipo indutivo
Este exercício espera que o valor de retorno seja um tipo indutivo Classification que você deve definir.
Esse tipo deve ter uma instância de BEq, ou seja, ele admite um teste de igualdade Boolean, e uma instância de Repr, ou seja, valores do tipo podem ser formatados para exibição.
Você pode consultar esta página sobre declarações de instância.
O Lean pode gerar instâncias automaticamente para muitas classes.
Subtipos
O argumento da função classify é um subtipo chamado Positive:
def Positive := { x : Nat // x > 0 }
Subtipos representam elementos de um determinado tipo que satisfazem um predicado.
Positive representa 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.
Subtipos impõem invariantes no nível do tipo, garantindo que valores mal formados não possam ser construídos.
