Instruções
Um número racional é definido como o quociente de dois inteiros a e b, chamados de numerador e denominador, respectivamente, onde b != 0.
Observe que, matematicamente, o denominador não pode ser zero.
No entanto, em muitas implementações de números racionais, você vai encontrar o denominador podendo ser zero, com um comportamento semelhante ao infinito positivo ou negativo em números de ponto flutuante.
Nesses casos, o denominador e o numerador geralmente ainda não podem 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₂ dá 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), onde m = |n|.
Elevar um número racional r = a/b a um número real (de ponto 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), onde root(p, q) é a raiz q-ésima de p.
Implemente as seguintes operações:
- adição, subtração, multiplicação e divisão de dois números racionais,
- valor absoluto, exponenciação de um número racional dado a uma potência inteira, exponenciação de um número racional dado a uma potência real (de ponto flutuante), exponenciação de um número real a um número racional.
Sua 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, divida a e b pelo máximo divisor comum (mdc) de a e b.
Então, por exemplo, gcd(12, 8) = 4, logo 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 inteiro positivo).
Se houver um denominador com um inteiro negativo, multiplique o numerador e o denominador por -1 para garantir que a forma padrão seja alcançada.
Por exemplo, 3/-4 deve ser reduzido a -3/4
Considere que a linguagem de programação que você está usando não tem uma implementação de números racionais.
Provando propriedades
Neste exercício, você deve definir um tipo RationalNumber que representa um número racional válido e totalmente reduzido.
Isso é garantido diretamente por uma propriedade que faz parte do próprio tipo.
Codificar especificações e restrições diretamente no nível do tipo torna os estados inválidos efetivamente irrepresentáveis.
No entanto, isso também impõe um fardo adicional a quem programa, que precisa provar que a propriedade sempre se mantém.
Este capítulo oferece uma boa introdução à prova de teoremas em Lean.
Para um mergulho mais profundo, este livro está listado como recurso oficial no site do Lean.
Você também pode querer consultar uma referência da linguagem.
