Instruções
Um número racional é definido como o quociente de dois números inteiros a e b, chamados numerador e denominador, respetivamente, em que b != 0.
Repara que, matematicamente, o denominador não pode ser zero.
No entanto, em muitas implementações de números racionais, vais encontrar casos em que o denominador pode ser zero, com um comportamento semelhante ao infinito positivo ou negativo nos números de vírgula flutuante.
Nesses casos, o denominador e o numerador, em geral, continuam a não poder ser ambos zero ao mesmo tempo.
O valor absoluto |r| do número racional r = a/b é igual a |a|/|b|.
A soma de dois números racionais r₁ = a₁/b₁ e r₂ = a₂/b₂ é r₁ + r₂ = a₁/b₁ + a₂/b₂ = (a₁ * b₂ + a₂ * b₁) / (b₁ * b₂).
A diferença de dois números racionais r₁ = a₁/b₁ e r₂ = a₂/b₂ é r₁ - r₂ = a₁/b₁ - a₂/b₂ = (a₁ * b₂ - a₂ * b₁) / (b₁ * b₂).
O produto (multiplicação) de dois números racionais r₁ = a₁/b₁ e r₂ = a₂/b₂ é r₁ * r₂ = (a₁ * a₂) / (b₁ * b₂).
Dividir um número racional r₁ = a₁/b₁ por outro r₂ = a₂/b₂ é r₁ / r₂ = (a₁ * b₂) / (a₂ * b₁) se a₂ não for zero.
Elevar um número racional r = a/b a uma potência inteira não negativa n dá r^n = (a^n)/(b^n).
Elevar um número racional r = a/b a uma potência inteira negativa n dá r^n = (b^m)/(a^m), em que m = |n|.
Elevar um número racional r = a/b a um número real (de vírgula flutuante) x dá o quociente (a^x)/(b^x), que é um número real.
Elevar um número real x a um número racional r = a/b dá x^(a/b) = root(x^a, b), em que root(p, q) é a raiz de índice q de p.
Implementa as seguintes operações:
- adição, subtração, multiplicação e divisão de dois números racionais,
- valor absoluto, exponenciação de um determinado número racional a uma potência inteira, exponenciação de um determinado número racional a uma potência real (de vírgula flutuante), exponenciação de um número real a um número racional.
A tua implementação de números racionais deve estar sempre reduzida à forma mais simples.
Por exemplo, 4/4 deve ser reduzido a 1/1, 30/60 deve ser reduzido a 1/2, 12/8 deve ser reduzido a 3/2, etc.
Para reduzir um número racional r = a/b, divide a e b pelo máximo divisor comum (mdc) de a e b.
Assim, por exemplo, gcd(12, 8) = 4, pelo que r = 12/8 pode ser reduzido a (12/4)/(8/4) = 3/2.
A forma reduzida de um número racional deve estar na "forma padrão" (o denominador deve ser sempre um número inteiro positivo).
Se houver um denominador com um número inteiro negativo, multiplica tanto o numerador como o denominador por -1, para garantir que se chega à forma padrão.
Por exemplo, 3/-4 deve ser reduzido a -3/4
Assume que a linguagem de programação que estás a usar não tem uma implementação de números racionais.
Provar propriedades
Neste exercício, tens de definir um tipo RationalNumber que representa um número racional válido e totalmente reduzido.
Isto é imposto diretamente por uma propriedade que faz parte do próprio tipo.
Codificar especificações e restrições diretamente ao nível do tipo torna os estados inválidos efetivamente irrepresentáveis.
No entanto, isto também coloca um peso adicional sobre o programador, que tem de provar que a propriedade se verifica sempre.
Este capítulo é uma boa introdução à prova de teoremas em Lean.
Para um estudo mais aprofundado, este livro está listado como recurso oficial no site do Lean.
Também podes consultar uma referência da linguagem.
