RationalComputeStarter

Public executable rational interface, independent of linear algebra

Open in Workbench View on GitHub

1-- Public executable rational interface, independent of linear algebra.2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module RationalComputeStarter7import Grace.Cumulus.Rat89theorem addition_means_rational_addition (a b m c d n : Nat)10  requires first : m ≠ 011  requires second : n ≠ 012  shows RationalCellOps.meaning(RationalCellOps.cellAdd(13      RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =14    rationalAddValue(rationalClass(a, b, m), rationalClass(c, d, n))15proof16  show RationalCellOps.meaning(RationalCellOps.cellAdd(17      RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =18    rationalAddValue(rationalClass(a, b, m), rationalClass(c, d, n)) :=19      RationalCellOps.add.sound at a, b, m, c, d, n with first, second2021theorem pivot_zero_iff_rational_zero (a b m : Nat)22  requires valid : m ≠ 023  shows RationalCellOps.isZero(RationalCell.fraction(a, b, m)) = Bool.true ↔24    RationalCellOps.meaning(RationalCell.fraction(a, b, m)) = rationalZero25proof26  exact RationalCellOps.isZero.quotient_iff with valid2728theorem reverse_representative_equality (a b m c d n : Nat)29  requires first : m ≠ 030  requires second : n ≠ 031  requires same : rationalClass(a, b, m) = rationalClass(c, d, n)32  shows rationalClass(c, d, n) = rationalClass(a, b, m)33proof34  simp3536theorem two_halves_equal_one37  shows RationalCellOps.sameValue(RationalCell.fraction(2, 0, 2),38    RationalCell.fraction(1, 0, 1)) = Bool.true39proof40  compute4142theorem two_halves_quotient_one43  shows RationalCellOps.meaning(RationalCell.fraction(2, 0, 2)) =44    RationalCellOps.meaning(RationalCell.fraction(1, 0, 1))45proof46  have nonzeroTwo : 2 ≠ 047    intro h48    have distinct := Naturals.disjoint.zero.succ at 149    apply distinct50    rw h51    rfl52  have nonzeroOne : 1 ≠ 053    intro h54    have distinct := Naturals.disjoint.zero.succ at 055    apply distinct56    rw h57    rfl58  have iff := RationalCellOps.sameValue.quotient_iff at 2, 0, 2, 1, 0, 1 with59    *60  exact iff.forward with two_halves_equal_one61