Istruzioni
Un numero razionale è definito come il quoziente di due numeri interi a e b, chiamati rispettivamente numeratore e denominatore, dove b != 0.
Nota che, matematicamente, il denominatore non può essere zero.
Tuttavia, in molte implementazioni dei numeri razionali, troverai che è consentito che il denominatore sia zero, con un comportamento simile a quello dell'infinito positivo o negativo nei numeri in virgola mobile.
In quei casi, il denominatore ed il numeratore generalmente non possono comunque essere entrambi zero allo stesso tempo.
Il valore assoluto |r| del numero razionale r = a/b è uguale a |a|/|b|.
La somma di due numeri razionali r₁ = a₁/b₁ e r₂ = a₂/b₂ è r₁ + r₂ = a₁/b₁ + a₂/b₂ = (a₁ * b₂ + a₂ * b₁) / (b₁ * b₂).
La differenza di due numeri razionali r₁ = a₁/b₁ e r₂ = a₂/b₂ è r₁ - r₂ = a₁/b₁ - a₂/b₂ = (a₁ * b₂ - a₂ * b₁) / (b₁ * b₂).
Il prodotto (moltiplicazione) di due numeri razionali r₁ = a₁/b₁ e r₂ = a₂/b₂ è r₁ * r₂ = (a₁ * a₂) / (b₁ * b₂).
Dividere un numero razionale r₁ = a₁/b₁ per un altro r₂ = a₂/b₂ dà r₁ / r₂ = (a₁ * b₂) / (a₂ * b₁) se a₂ non è zero.
L'elevamento a potenza di un numero razionale r = a/b ad una potenza intera non negativa n è r^n = (a^n)/(b^n).
L'elevamento a potenza di un numero razionale r = a/b ad una potenza intera negativa n è r^n = (b^m)/(a^m), dove m = |n|.
L'elevamento a potenza di un numero razionale r = a/b ad un numero reale (in virgola mobile) x è il quoziente (a^x)/(b^x), che è un numero reale.
L'elevamento a potenza di un numero reale x ad un numero razionale r = a/b è x^(a/b) = root(x^a, b), dove root(p, q) è la radice q-esima di p.
Implementa le seguenti operazioni:
- addizione, sottrazione, moltiplicazione e divisione di due numeri razionali,
- valore assoluto, elevamento a potenza di un dato numero razionale ad una potenza intera, elevamento a potenza di un dato numero razionale ad una potenza reale (in virgola mobile), elevamento a potenza di un numero reale ad un numero razionale.
L'implementazione dei numeri razionali dovrebbe sempre essere ridotta ai minimi termini.
Per esempio, 4/4 dovrebbe ridursi a 1/1, 30/60 dovrebbe ridursi a 1/2, 12/8 dovrebbe ridursi a 3/2, ecc.
Per ridurre un numero razionale r = a/b, dividi a e b per il massimo comun divisore (gcd) di a e b.
Quindi, per esempio, gcd(12, 8) = 4, per cui r = 12/8 può essere ridotto a (12/4)/(8/4) = 3/2.
La forma ridotta di un numero razionale dovrebbe essere in «forma standard» (il denominatore dovrebbe sempre essere un numero intero positivo).
Se è presente un denominatore con un numero intero negativo, moltiplica sia il numeratore sia il denominatore per -1 per garantire che si raggiunga la forma standard.
Per esempio, 3/-4 dovrebbe essere ridotto a -3/4
Presumi che il linguaggio di programmazione che stai usando non abbia un'implementazione dei numeri razionali.
Dimostrare le proprietà
In questo esercizio dovrai definire un tipo RationalNumber che rappresenta un numero razionale valido, completamente ridotto.
Questo è imposto direttamente da una proprietà che fa parte del tipo stesso.
Codificare specifiche e vincoli direttamente a livello di tipo rende gli stati non validi di fatto non rappresentabili.
Tuttavia, questo pone anche un onere aggiuntivo sul programmatore, che deve dimostrare che la proprietà vale sempre.
Questo capitolo offre una buona introduzione alla dimostrazione di teoremi in Lean.
Per approfondire, questo libro è elencato tra le risorse ufficiali sul sito di Lean.
Potresti anche voler consultare una guida di riferimento per il linguaggio.
