Grace/Cumulus/Rat/Computable.g17

Open in Workbench Download source

Imports

Operations · Nat.Mod

Declarations

Source

1-- Executable signed natural fractions and their quotient-rational meaning.2-- A fraction(a,b,d) represents (a-b)/d when d is nonzero.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Rat.Computable9import Operations10import Nat.Mod1112datatype RationalCell(A : Set)13  | fraction(positive negative denominator : A)1415namespace RationalCellOps1617def zero : RationalCell(ℕ) := RationalCell.fraction(0, 0, 1)18def one : RationalCell(ℕ) := RationalCell.fraction(1, 0, 1)1920def addTo (a b m : Nat, y : RationalCell(ℕ)) → RationalCell(ℕ)21  | a, b, m, RationalCell.fraction(c, d, n) =>22    RationalCell.fraction(Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(n, a), Grace.Core.Nat.Rec.mul(m, c)),23      Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(n, b), Grace.Core.Nat.Rec.mul(m, d)),24      Grace.Core.Nat.Rec.mul(m, n))2526def cellAdd (x : RationalCell(ℕ), y : RationalCell(ℕ)) → RationalCell(ℕ)27  | RationalCell.fraction(a, b, m), y => addTo(a, b, m, y)2829def cellNeg (x : RationalCell(ℕ)) → RationalCell(ℕ)30  | RationalCell.fraction(a, b, m) => RationalCell.fraction(b, a, m)3132def sub (x y : RationalCell(ℕ)) : RationalCell(ℕ) := cellAdd(x, cellNeg(y))3334def multiplyBy (a b m : Nat, y : RationalCell(ℕ)) → RationalCell(ℕ)35  | a, b, m, RationalCell.fraction(c, d, n) =>36    RationalCell.fraction(Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(a, c), Grace.Core.Nat.Rec.mul(b, d)),37      Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(a, d), Grace.Core.Nat.Rec.mul(b, c)),38      Grace.Core.Nat.Rec.mul(m, n))3940def cellMul (x : RationalCell(ℕ), y : RationalCell(ℕ)) → RationalCell(ℕ)41  | RationalCell.fraction(a, b, m), y => multiplyBy(a, b, m, y)4243def isZero (x : RationalCell(ℕ)) → Bool44  | RationalCell.fraction(a, b, m) => equalNat(a, b)4546def less (a b : Nat) → Bool47  | zero, b => BoolOps.not(Grace.Cumulus.Nat.Mod.isZero(b))48  | succ(a), b => BoolOps.and(BoolOps.not(Grace.Cumulus.Nat.Mod.isZero(b)), less(a, predecessor(b)))4950def minus (a b : Nat) → Nat51  | zero, b => 052  | succ(a), b => chooseNat(Grace.Cumulus.Nat.Mod.isZero(b), succ(a), minus(a, predecessor(b)))5354theorem minus.truncated_at_zero55  shows minus(0, 3) = 056proof57  compute5859theorem minus.large_ground60  shows minus(1000000000000, 999999999997) = 361proof62  compute6364-- Public executable carrier check. A zero denominator is not a rational.65def valid (x : RationalCell(ℕ)) → Bool66  | RationalCell.fraction(a, b, m) => BoolOps.not(Grace.Cumulus.Nat.Mod.isZero(m))6768-- Cross multiplication tests equality without reducing or selecting a69-- canonical quotient representative.70def equivalentTo (a b m : Nat, y : RationalCell(ℕ)) → Bool71  | a, b, m, RationalCell.fraction(c, d, n) =>72    equalNat(Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(n, a), Grace.Core.Nat.Rec.mul(m, d)),73      Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(m, c), Grace.Core.Nat.Rec.mul(n, b)))7475def sameValue (x : RationalCell(ℕ), y : RationalCell(ℕ)) → Bool76  | RationalCell.fraction(a, b, m), y => equivalentTo(a, b, m, y)7778-- The caller establishes nonzero numerator. The zero case is totalized;79-- it produces denominator zero and must never be used as a rational pivot.80def inverseNumerator (negative : Bool, a b m : Nat) → RationalCell(ℕ)81  | Bool.true, a, b, m => RationalCell.fraction(0, m, minus(b, a))82  | Bool.false, a, b, m => RationalCell.fraction(m, 0, minus(a, b))8384def inverse (x : RationalCell(ℕ)) → RationalCell(ℕ)85  | RationalCell.fraction(a, b, m) => inverseNumerator(less(a, b), a, b, m)8687-- The semantics map is a set-theoretic quotient class. Execution stays on88-- constructor data; proofs can pass through this map to Cumulus rationals.89def meaning (x : RationalCell(ℕ)) → Set90  | RationalCell.fraction(a, b, m) => rationalClass(a, b, m)9192theorem add.represents (a b m c d n : Nat)93  shows meaning(cellAdd(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =94    rationalClassSum(a, b, m, c, d, n)95proof96  unfold cellAdd97  unfold addTo98  unfold meaning99  unfold rationalClassSum100  rfl101102theorem mul.represents (a b m c d n : Nat)103  shows meaning(cellMul(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =104    rationalClassMul(a, b, m, c, d, n)105proof106  unfold cellMul107  unfold multiplyBy108  unfold meaning109  unfold rationalClassMul110  rfl111112theorem neg.represents (a b m : Nat)113  shows meaning(cellNeg(RationalCell.fraction(a, b, m))) = rationalClassNeg(a, b, m)114proof115  unfold cellNeg116  unfold meaning117  unfold rationalClassNeg118  rfl119120theorem meaning.rational (a b m : Nat)121  requires positive : m ≠ 0122  shows Rational(meaning(RationalCell.fraction(a, b, m)))123proof124  unfold meaning125  exact rationalClass.rational with positive126127theorem add.sound (a b m c d n : Nat)128  requires positiveM : m ≠ 0129  requires positiveN : n ≠ 0130  shows meaning(cellAdd(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =131    rationalAddValue(rationalClass(a, b, m), rationalClass(c, d, n))132proof133  have concrete := add.represents at a, b, m, c, d, n134  have quotient := rationalAddValue.classes at a, b, m, c, d, n with positiveM, positiveN135  rw [concrete, quotient]136  rfl137138theorem mul.sound (a b m c d n : Nat)139  requires positiveM : m ≠ 0140  requires positiveN : n ≠ 0141  shows meaning(cellMul(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =142    rationalMulValue(rationalClass(a, b, m), rationalClass(c, d, n))143proof144  have concrete := mul.represents at a, b, m, c, d, n145  have quotient := rationalMulValue.classes at a, b, m, c, d, n with positiveM, positiveN146  rw [concrete, quotient]147  rfl148149theorem neg.sound (a b m : Nat)150  requires positive : m ≠ 0151  shows meaning(cellNeg(RationalCell.fraction(a, b, m))) =152    rationalNegValue(rationalClass(a, b, m))153proof154  have concrete := neg.represents at a, b, m155  have quotient := rationalNegValue.classes at a, b, m with positive156  rw [concrete, quotient]157  rfl158159-- The decision used by elimination is faithful to quotient equality.160theorem isZero.true_iff_numerators (a b m : Nat)161  shows isZero(RationalCell.fraction(a, b, m)) = Bool.true ↔ a = b162proof163  have characterization := equalNat.true_iff at a, b with *164  constructor165  . intro h166    simp [isZero] at h167    exact characterization.forward with h168  . intro h169    have equal := characterization.backward with h170    rw h171    have reflexive := equalNat.reflexive at b172    simp [isZero, reflexive]173174theorem isZero.sound (a b m : Nat)175  requires nonzero : m ≠ 0176  requires zeroTest : isZero(RationalCell.fraction(a, b, m)) = Bool.true177  shows meaning(RationalCell.fraction(a, b, m)) = rationalZero178proof179  have equal := isZero.true_iff_numerators.forward with zeroTest180  unfold meaning181  unfold rationalZero182  apply rationalClass.eq183  . exact nonzero184  . intro h185    have distinct := Naturals.disjoint.zero.succ at 0186    apply distinct187    rw h188    rfl189  . ring190191theorem isZero.complete (a b m : Nat)192  requires nonzero : m ≠ 0193  requires quotientZero : meaning(RationalCell.fraction(a, b, m)) = rationalZero194  shows isZero(RationalCell.fraction(a, b, m)) = Bool.true195proof196  unfold meaning at quotientZero197  unfold rationalZero at quotientZero198  have oneNonzero : 1 ≠ 0199    intro h200    have distinct := Naturals.disjoint.zero.succ at 0201    apply distinct202    rw h203    rfl204  have cross := rationalClass.equivalent_of_eq with nonzero, oneNonzero, quotientZero205  have equal : a = b206    simpa [mul.left_unit, mul.right_zero, add.right_unit,207      add.left_unit] using cross208  exact isZero.true_iff_numerators.backward with equal209210theorem isZero.quotient_iff (a b m : Nat)211  requires nonzero : m ≠ 0212  shows isZero(RationalCell.fraction(a, b, m)) = Bool.true ↔213    meaning(RationalCell.fraction(a, b, m)) = rationalZero214proof215  constructor216  . intro h217    exact isZero.sound with nonzero, h218  . intro h219    exact isZero.complete with nonzero, h220221theorem valid.fraction_iff (a b m : Nat)222  shows valid(RationalCell.fraction(a, b, m)) = Bool.true ↔ m ≠ 0223proof224  induction m225  | zero =>226    have value : valid(RationalCell.fraction(a, b, 0)) = Bool.false227      settle with valid, Grace.Cumulus.Nat.Mod.isZero, BoolOps.not228    rw value229    have boolDistinct := Bool.inductive.disjoint.false.true230    have self : 0 = 0 by rfl231    tauto232  | succ(k) using ih =>233    have value : valid(RationalCell.fraction(a, b, succ(k))) = Bool.true234      settle with valid, Grace.Cumulus.Nat.Mod.isZero, BoolOps.not235    rw value236    have distinct := Naturals.disjoint.zero.succ at k237    constructor238    . intros h equal239      apply distinct240      rw equal241      rfl242    . intro h243      rfl244245theorem sameValue.quotient_iff (a b m c d n : Nat)246  requires first : m ≠ 0247  requires second : n ≠ 0248  shows sameValue(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n)) = Bool.true ↔249    meaning(RationalCell.fraction(a, b, m)) = meaning(RationalCell.fraction(c, d, n))250proof251  have test := equalNat.true_iff at252    n * a + m * d, m * c + n * b with *{2}253  constructor254  . intro yes255    simp [sameValue, equivalentTo] at yes256    have cross := test.forward with yes257    unfold meaning258    exact rationalClass.eq with first, second, cross259  . intro equal260    unfold meaning at equal261    have cross := rationalClass.equivalent_of_eq with first, second, equal262    have yes := test.backward with cross263    simp [sameValue, equivalentTo, yes, equalNat.reflexive]264265theorem sameValue.reflexive (a b m : Nat)266  shows sameValue(RationalCell.fraction(a, b, m), RationalCell.fraction(a, b, m)) = Bool.true267proof268  have cross : m * a + m * b = m * a + m * b by rfl269  have yes := equalNat.true_iff.backward with cross270  simp [sameValue, equivalentTo, yes, equalNat.reflexive]271272-- Ground equality uses native arbitrary-precision integers; the general273-- sameValue.quotient_iff theorem transfers this decision to quotient ℚ.274theorem sameValue.large_ground275  shows sameValue(276    RationalCell.fraction(1000000000000000000000000000000, 0, 3),277    RationalCell.fraction(2000000000000000000000000000000, 0, 6)) = Bool.true278proof279  compute280281-- The quotient criterion is checked as a constant-size ground proof, even282-- though its explicit instantiation at huge numerals would expand a proof.283theorem rationalClass.large_ground284  shows rationalClass(1000000000000000000000000000000, 0, 3) =285    rationalClass(2000000000000000000000000000000, 0, 6)286proof287  compute288289end RationalCellOps290