Istruzioni
Determina se un numero è perfetto, abbondante o difettoso in base allo schema di classificazione dei numeri interi positivi di Nicomaco (60 - 120 d.C.).
Il matematico greco Nicomaco ideò uno schema di classificazione dei numeri interi positivi, che assegna ciascuno di essi in modo univoco a una delle categorie perfetto, abbondante o difettoso, in base alla loro somma dei divisori propri.
La somma dei divisori propri è definita come la somma dei fattori di un numero, escluso il numero stesso.
Per esempio, la somma dei divisori propri di 15 è 1 + 3 + 5 = 9.
Perfetto
Un numero è perfetto quando è uguale alla somma dei suoi divisori propri.
Per esempio:
-
6 è un numero perfetto perché 1 + 2 + 3 = 6
-
28 è un numero perfetto perché 1 + 2 + 4 + 7 + 14 = 28
Abbondante
Un numero è abbondante quando è minore della somma dei suoi divisori propri.
Per esempio:
-
12 è un numero abbondante perché 1 + 2 + 3 + 4 + 6 = 16
-
24 è un numero abbondante perché 1 + 2 + 3 + 4 + 6 + 8 + 12 = 36
Difettoso
Un numero è difettoso quando è maggiore della somma dei suoi divisori propri.
Per esempio:
-
8 è un numero difettoso perché 1 + 2 + 4 = 7
- I numeri primi sono difettosi
Compito
Implementa un modo per determinare se un numero dato è perfetto.
A seconda del track linguistico che segui, potresti anche dover implementare un modo per determinare se un numero dato è abbondante o difettoso.
Definire un tipo induttivo
Questo esercizio si aspetta che il valore restituito sia un tipo induttivo Classification che devi definire.
Questo tipo deve avere un'istanza BEq, cioè deve ammettere un test di uguaglianza booleana, e un'istanza Repr, cioè i valori del tipo devono poter essere formattati per la visualizzazione.
Puoi fare riferimento a questa pagina sulle dichiarazioni di istanza.
Lean può generare automaticamente le istanze per molte classi.
Sottotipi
L'argomento della funzione classify è un sottotipo chiamato Positive:
def Positive := { x : Nat // x > 0 }
I sottotipi rappresentano gli elementi di un tipo particolare che soddisfano un predicato.
Positive rappresenta gli elementi di Nat che sono maggiori di 0.
Ogni elemento di un sottotipo può essere pensato come una coppia formata da un valore del tipo sottostante e da una dimostrazione, nel senso matematico del termine, che questo valore soddisfa il predicato corrispondente.
I sottotipi impongono invarianti a livello di tipo, assicurando che i valori malformati non possano essere costruiti.
