Вказівки
Раціональне число визначається як частка двох цілих чисел a і b, які називаються відповідно чисельником і знаменником, де b != 0.
Зауважмо, що математично знаменник не може дорівнювати нулю.
Однак у багатьох реалізаціях раціональних чисел знаменник може бути нулем, а поведінка при цьому подібна до додатної чи відʼємної нескінченності в числах з плаваючою комою.
У таких випадках знаменник і чисельник зазвичай усе одно не можуть бути нулями одночасно.
Абсолютна величина |r| раціонального числа r = a/b дорівнює |a|/|b|.
Сума двох раціональних чисел r₁ = a₁/b₁ і r₂ = a₂/b₂ дорівнює r₁ + r₂ = a₁/b₁ + a₂/b₂ = (a₁ * b₂ + a₂ * b₁) / (b₁ * b₂).
Різниця двох раціональних чисел r₁ = a₁/b₁ і r₂ = a₂/b₂ дорівнює r₁ - r₂ = a₁/b₁ - a₂/b₂ = (a₁ * b₂ - a₂ * b₁) / (b₁ * b₂).
Добуток (множення) двох раціональних чисел r₁ = a₁/b₁ і r₂ = a₂/b₂ дорівнює r₁ * r₂ = (a₁ * a₂) / (b₁ * b₂).
Ділення раціонального числа r₁ = a₁/b₁ на інше r₂ = a₂/b₂ дає r₁ / r₂ = (a₁ * b₂) / (a₂ * b₁), якщо a₂ не дорівнює нулю.
Піднесення раціонального числа r = a/b до невідʼємного цілого степеня n дає r^n = (a^n)/(b^n).
Піднесення раціонального числа r = a/b до відʼємного цілого степеня n дає r^n = (b^m)/(a^m), де m = |n|.
Піднесення раціонального числа r = a/b до дійсного (з плаваючою комою) числа x дає частку (a^x)/(b^x), яка є дійсним числом.
Піднесення дійсного числа x до раціонального числа r = a/b дає x^(a/b) = root(x^a, b), де root(p, q) позначає корінь q-го степеня з p.
Реалізуйте такі операції:
- додавання, віднімання, множення та ділення двох раціональних чисел;
- абсолютну величину, піднесення заданого раціонального числа до цілого степеня, піднесення заданого раціонального числа до дійсного (з плаваючою комою) степеня, піднесення дійсного числа до раціонального степеня.
Реалізація раціональних чисел завжди повинна бути зведена до нескоротного вигляду.
Наприклад, 4/4 має зводитися до 1/1, 30/60 має зводитися до 1/2, 12/8 має зводитися до 3/2 тощо.
Щоб скоротити раціональне число r = a/b, треба поділити a і b на найбільший спільний дільник (НСД) чисел a і b.
Так, наприклад, gcd(12, 8) = 4, тому r = 12/8 можна звести до (12/4)/(8/4) = 3/2.
Зведена форма раціонального числа має бути в «стандартному вигляді» (знаменник завжди має бути додатним цілим числом).
Якщо знаменник є відʼємним цілим числом, треба помножити і чисельник, і знаменник на -1, щоб досягти стандартного вигляду.
Наприклад, 3/-4 має бути зведено до -3/4
Вважайте, що в мові програмування, з якою ми працюємо, немає реалізації раціональних чисел.
Доведення властивостей
У цій вправі визначте тип RationalNumber, який представляє повністю скорочене коректне раціональне число.
Це забезпечується безпосередньо властивістю, яка є частиною самого типу.
Кодування специфікацій та обмежень безпосередньо на рівні типу практично унеможливлює некоректні стани.
Однак це також покладає додатковий тягар на програміста, який має довести, що властивість завжди виконується.
Цей розділ дає гарний вступ до доведення теорем у Lean.
Для глибшого занурення цю книгу зазначено як офіційний ресурс на сайті Lean.
Також можна звернутися до довідки з мови.
