-- Executable signed natural fractions and their quotient-rational meaning.
-- A fraction(a,b,d) represents (a-b)/d when d is nonzero.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Rat.Computable
import Operations
import Nat.Mod

datatype RationalCell(A : Set)
  | fraction(positive negative denominator : A)

namespace RationalCellOps

def zero : RationalCell(ℕ) := RationalCell.fraction(0, 0, 1)
def one : RationalCell(ℕ) := RationalCell.fraction(1, 0, 1)

def addTo (a b m : Nat, y : RationalCell(ℕ)) → RationalCell(ℕ)
  | a, b, m, RationalCell.fraction(c, d, n) =>
    RationalCell.fraction(Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(n, a), Grace.Core.Nat.Rec.mul(m, c)),
      Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(n, b), Grace.Core.Nat.Rec.mul(m, d)),
      Grace.Core.Nat.Rec.mul(m, n))

def cellAdd (x : RationalCell(ℕ), y : RationalCell(ℕ)) → RationalCell(ℕ)
  | RationalCell.fraction(a, b, m), y => addTo(a, b, m, y)

def cellNeg (x : RationalCell(ℕ)) → RationalCell(ℕ)
  | RationalCell.fraction(a, b, m) => RationalCell.fraction(b, a, m)

def sub (x y : RationalCell(ℕ)) : RationalCell(ℕ) := cellAdd(x, cellNeg(y))

def multiplyBy (a b m : Nat, y : RationalCell(ℕ)) → RationalCell(ℕ)
  | a, b, m, RationalCell.fraction(c, d, n) =>
    RationalCell.fraction(Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(a, c), Grace.Core.Nat.Rec.mul(b, d)),
      Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(a, d), Grace.Core.Nat.Rec.mul(b, c)),
      Grace.Core.Nat.Rec.mul(m, n))

def cellMul (x : RationalCell(ℕ), y : RationalCell(ℕ)) → RationalCell(ℕ)
  | RationalCell.fraction(a, b, m), y => multiplyBy(a, b, m, y)

def isZero (x : RationalCell(ℕ)) → Bool
  | RationalCell.fraction(a, b, m) => equalNat(a, b)

def less (a b : Nat) → Bool
  | zero, b => BoolOps.not(Grace.Cumulus.Nat.Mod.isZero(b))
  | succ(a), b => BoolOps.and(BoolOps.not(Grace.Cumulus.Nat.Mod.isZero(b)), less(a, predecessor(b)))

def minus (a b : Nat) → Nat
  | zero, b => 0
  | succ(a), b => chooseNat(Grace.Cumulus.Nat.Mod.isZero(b), succ(a), minus(a, predecessor(b)))

theorem minus.truncated_at_zero
  shows minus(0, 3) = 0
proof
  compute

theorem minus.large_ground
  shows minus(1000000000000, 999999999997) = 3
proof
  compute

-- Public executable carrier check. A zero denominator is not a rational.
def valid (x : RationalCell(ℕ)) → Bool
  | RationalCell.fraction(a, b, m) => BoolOps.not(Grace.Cumulus.Nat.Mod.isZero(m))

-- Cross multiplication tests equality without reducing or selecting a
-- canonical quotient representative.
def equivalentTo (a b m : Nat, y : RationalCell(ℕ)) → Bool
  | a, b, m, RationalCell.fraction(c, d, n) =>
    equalNat(Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(n, a), Grace.Core.Nat.Rec.mul(m, d)),
      Grace.Core.Nat.Rec.add(Grace.Core.Nat.Rec.mul(m, c), Grace.Core.Nat.Rec.mul(n, b)))

def sameValue (x : RationalCell(ℕ), y : RationalCell(ℕ)) → Bool
  | RationalCell.fraction(a, b, m), y => equivalentTo(a, b, m, y)

-- The caller establishes nonzero numerator. The zero case is totalized;
-- it produces denominator zero and must never be used as a rational pivot.
def inverseNumerator (negative : Bool, a b m : Nat) → RationalCell(ℕ)
  | Bool.true, a, b, m => RationalCell.fraction(0, m, minus(b, a))
  | Bool.false, a, b, m => RationalCell.fraction(m, 0, minus(a, b))

def inverse (x : RationalCell(ℕ)) → RationalCell(ℕ)
  | RationalCell.fraction(a, b, m) => inverseNumerator(less(a, b), a, b, m)

-- The semantics map is a set-theoretic quotient class. Execution stays on
-- constructor data; proofs can pass through this map to Cumulus rationals.
def meaning (x : RationalCell(ℕ)) → Set
  | RationalCell.fraction(a, b, m) => rationalClass(a, b, m)

theorem add.represents (a b m c d n : Nat)
  shows meaning(cellAdd(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =
    rationalClassSum(a, b, m, c, d, n)
proof
  unfold cellAdd
  unfold addTo
  unfold meaning
  unfold rationalClassSum
  rfl

theorem mul.represents (a b m c d n : Nat)
  shows meaning(cellMul(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =
    rationalClassMul(a, b, m, c, d, n)
proof
  unfold cellMul
  unfold multiplyBy
  unfold meaning
  unfold rationalClassMul
  rfl

theorem neg.represents (a b m : Nat)
  shows meaning(cellNeg(RationalCell.fraction(a, b, m))) = rationalClassNeg(a, b, m)
proof
  unfold cellNeg
  unfold meaning
  unfold rationalClassNeg
  rfl

theorem meaning.rational (a b m : Nat)
  requires positive : m ≠ 0
  shows Rational(meaning(RationalCell.fraction(a, b, m)))
proof
  unfold meaning
  exact rationalClass.rational with positive

theorem add.sound (a b m c d n : Nat)
  requires positiveM : m ≠ 0
  requires positiveN : n ≠ 0
  shows meaning(cellAdd(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =
    rationalAddValue(rationalClass(a, b, m), rationalClass(c, d, n))
proof
  have concrete := add.represents at a, b, m, c, d, n
  have quotient := rationalAddValue.classes at a, b, m, c, d, n with positiveM, positiveN
  rw [concrete, quotient]
  rfl

theorem mul.sound (a b m c d n : Nat)
  requires positiveM : m ≠ 0
  requires positiveN : n ≠ 0
  shows meaning(cellMul(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n))) =
    rationalMulValue(rationalClass(a, b, m), rationalClass(c, d, n))
proof
  have concrete := mul.represents at a, b, m, c, d, n
  have quotient := rationalMulValue.classes at a, b, m, c, d, n with positiveM, positiveN
  rw [concrete, quotient]
  rfl

theorem neg.sound (a b m : Nat)
  requires positive : m ≠ 0
  shows meaning(cellNeg(RationalCell.fraction(a, b, m))) =
    rationalNegValue(rationalClass(a, b, m))
proof
  have concrete := neg.represents at a, b, m
  have quotient := rationalNegValue.classes at a, b, m with positive
  rw [concrete, quotient]
  rfl

-- The decision used by elimination is faithful to quotient equality.
theorem isZero.true_iff_numerators (a b m : Nat)
  shows isZero(RationalCell.fraction(a, b, m)) = Bool.true ↔ a = b
proof
  have characterization := equalNat.true_iff at a, b with *
  constructor
  . intro h
    simp [isZero] at h
    exact characterization.forward with h
  . intro h
    have equal := characterization.backward with h
    rw h
    have reflexive := equalNat.reflexive at b
    simp [isZero, reflexive]

theorem isZero.sound (a b m : Nat)
  requires nonzero : m ≠ 0
  requires zeroTest : isZero(RationalCell.fraction(a, b, m)) = Bool.true
  shows meaning(RationalCell.fraction(a, b, m)) = rationalZero
proof
  have equal := isZero.true_iff_numerators.forward with zeroTest
  unfold meaning
  unfold rationalZero
  apply rationalClass.eq
  . exact nonzero
  . intro h
    have distinct := Naturals.disjoint.zero.succ at 0
    apply distinct
    rw h
    rfl
  . ring

theorem isZero.complete (a b m : Nat)
  requires nonzero : m ≠ 0
  requires quotientZero : meaning(RationalCell.fraction(a, b, m)) = rationalZero
  shows isZero(RationalCell.fraction(a, b, m)) = Bool.true
proof
  unfold meaning at quotientZero
  unfold rationalZero at quotientZero
  have oneNonzero : 1 ≠ 0
    intro h
    have distinct := Naturals.disjoint.zero.succ at 0
    apply distinct
    rw h
    rfl
  have cross := rationalClass.equivalent_of_eq with nonzero, oneNonzero, quotientZero
  have equal : a = b
    simpa [mul.left_unit, mul.right_zero, add.right_unit,
      add.left_unit] using cross
  exact isZero.true_iff_numerators.backward with equal

theorem isZero.quotient_iff (a b m : Nat)
  requires nonzero : m ≠ 0
  shows isZero(RationalCell.fraction(a, b, m)) = Bool.true ↔
    meaning(RationalCell.fraction(a, b, m)) = rationalZero
proof
  constructor
  . intro h
    exact isZero.sound with nonzero, h
  . intro h
    exact isZero.complete with nonzero, h

theorem valid.fraction_iff (a b m : Nat)
  shows valid(RationalCell.fraction(a, b, m)) = Bool.true ↔ m ≠ 0
proof
  induction m
  | zero =>
    have value : valid(RationalCell.fraction(a, b, 0)) = Bool.false
      settle with valid, Grace.Cumulus.Nat.Mod.isZero, BoolOps.not
    rw value
    have boolDistinct := Bool.inductive.disjoint.false.true
    have self : 0 = 0 by rfl
    tauto
  | succ(k) using ih =>
    have value : valid(RationalCell.fraction(a, b, succ(k))) = Bool.true
      settle with valid, Grace.Cumulus.Nat.Mod.isZero, BoolOps.not
    rw value
    have distinct := Naturals.disjoint.zero.succ at k
    constructor
    . intros h equal
      apply distinct
      rw equal
      rfl
    . intro h
      rfl

theorem sameValue.quotient_iff (a b m c d n : Nat)
  requires first : m ≠ 0
  requires second : n ≠ 0
  shows sameValue(RationalCell.fraction(a, b, m), RationalCell.fraction(c, d, n)) = Bool.true ↔
    meaning(RationalCell.fraction(a, b, m)) = meaning(RationalCell.fraction(c, d, n))
proof
  have test := equalNat.true_iff at
    n * a + m * d, m * c + n * b with *{2}
  constructor
  . intro yes
    simp [sameValue, equivalentTo] at yes
    have cross := test.forward with yes
    unfold meaning
    exact rationalClass.eq with first, second, cross
  . intro equal
    unfold meaning at equal
    have cross := rationalClass.equivalent_of_eq with first, second, equal
    have yes := test.backward with cross
    simp [sameValue, equivalentTo, yes, equalNat.reflexive]

theorem sameValue.reflexive (a b m : Nat)
  shows sameValue(RationalCell.fraction(a, b, m), RationalCell.fraction(a, b, m)) = Bool.true
proof
  have cross : m * a + m * b = m * a + m * b by rfl
  have yes := equalNat.true_iff.backward with cross
  simp [sameValue, equivalentTo, yes, equalNat.reflexive]

-- Ground equality uses native arbitrary-precision integers; the general
-- sameValue.quotient_iff theorem transfers this decision to quotient ℚ.
theorem sameValue.large_ground
  shows sameValue(
    RationalCell.fraction(1000000000000000000000000000000, 0, 3),
    RationalCell.fraction(2000000000000000000000000000000, 0, 6)) = Bool.true
proof
  compute

-- The quotient criterion is checked as a constant-size ground proof, even
-- though its explicit instantiation at huge numerals would expand a proof.
theorem rationalClass.large_ground
  shows rationalClass(1000000000000000000000000000000, 0, 3) =
    rationalClass(2000000000000000000000000000000, 0, 6)
proof
  compute

end RationalCellOps