Rat.frac

-- Rationals over Int.nova's Int, with a STRUCTURALLY non-zero
-- denominator.
--
-- Why not `(d : Int) × (d ≢ 0)`: has no 𝕌-code (there is no
-- code for Ω or for p in 𝕌 — NovaFoundation.txt's Ω section says
-- so outright), so a Σ carrying a proof cannot be a code and Rat would
-- be a large `type`: no Rat, no generic (A : 𝕌) combinators, no use
-- as a code anywhere. Worse, it would be practically uninhabited —
-- writing ½ needs a proof of an Int DISEQUALITY. (When this was
-- written nothing inverted el-quot-eq at all; Int/effective.nova now
-- gives IntR back from a class equation, so the disequality is cheap —
-- but the encoding below is still the one that keeps Rat a 𝕌-code.)
--
-- So the denominator ranges over NZ, whose elements ARE the non-zero
-- integers by construction: inj₁ n and inj₂ n denote +(n+1) and
-- -(n+1). Everything stays small, elements are free, and nzToInt
-- embeds NZ back into Int.
-- ===== the non-zero integers =====

import Natural (+, *, plusZeroId, zeroPlusId, plusComm, plusAssoc, swapLeft, multZeroId, zeroMult, sucMult, multComm, multDistrib)
import Int (Int, intZero, intOne, intNeg)
import Int.add (+, intAddComm)
import Core.equality (trans, cong)

NZ : 𝕌
NZ = ℕ ⊎ ℕ

-- +(n+1)
nzPos : ℕ → NZ using (Rat.frac.NZ.unfold)
nzPos = λn. inj₁ n

-- -(n+1)
nzNeg : ℕ → NZ using (Rat.frac.NZ.unfold)
nzNeg = λn. inj₂ n

nzOne : NZ using (Rat.frac.NZ.unfold)
nzOne = nzPos Z

nzToInt : NZ → Int using (Int.Int.unfold, Rat.frac.NZ.unfold)
nzToInt = λd. ⊎-elim (n. class (S n, Z)) (n. class (Z, S n)) d

-- the magnitudes multiply: (m+1)(k+1) = m*k + m + k + 1, so the stored
-- (magnitude − 1) of the product is m*k + m + k; the sign is the usual
-- product of signs. Closure of NZ under multiplication is therefore
-- definitional — there is no side condition to discharge.
nzMul : NZ → NZ → NZ using (Rat.frac.NZ.unfold)
nzMul =
  λx y. ⊎-elim
    m. ⊎-elim (k. nzPos (m * k + m + k)) (k. nzNeg (m * k + m + k)) y
    m. ⊎-elim (k. nzNeg (m * k + m + k)) (k. nzPos (m * k + m + k)) y
    x

nzMulOneL : {y : NZ} → nzMul nzOne y ≡ y
  using (nzMul.eq,
    nzNeg.eq,
    nzOne.eq,
    nzPos.eq,
    plusZeroId.rw,
    Rat.frac.NZ.unfold,
    zeroMult,
    zeroMult.rw,
    zeroPlusId,
    zeroPlusId.rw)
nzMulOneL = λy. ⊎-elim (k. ⋆) (k. ⋆) y

nzMulOneR : {x : NZ} → nzMul x nzOne ≡ x
  using (multZeroId.rw,
    nzMul.eq,
    nzNeg.eq,
    nzOne.eq,
    nzPos.eq,
    plusZeroId.rw,
    Rat.frac.NZ.unfold,
    zeroPlusId,
    zeroPlusId.rw)
nzMulOneR = λx. ⊎-elim (m. ⋆) (m. ⋆) x

-- ===== nat lemmas, in the orientation the engine can use =====
--
-- Rewriting is ORIENTED and size-decreasing, so Natural.nova's
-- distributivity and successor-multiplication laws — both stated in
-- the size-INCREASING direction — never fire as rewrite rules. Their
-- flips do; each is proved by ⋆, the original firing by
-- whole-equation match on the flipped goal.
distribBack : (n m k : ℕ) → n * m + n * k ≡ n * (m + k) using (multDistrib)
distribBack = λn m k. ⋆

sucMultBack : (n m : ℕ) → m + n * m ≡ S n * m using (sucMult)
sucMultBack = λn m. ⋆

oneMult : (m : ℕ) → S Z * m ≡ m using (multComm)
oneMult = λm. S Z * m ≡⟨ sucMult Z m ⟩ m + Z * m ≡⟨ zeroMult m ⟩ m + Z ≡⟨ plusZeroId m ⟩ m

-- ===== scaling an integer by a non-zero integer =====
--
-- Rational addition needs num · den, i.e. multiplication in Int. A
-- general intMul owes a quotient well-definedness proof in BOTH
-- arguments (the (a₁−a₂)(b₁−b₂) cross-sum identity). But one factor is
-- always a DENOMINATOR — an NZ, i.e. a SIGN and a NAT — so it suffices
-- to scale by a nat and negate: n · (a, b) = (n*a, n*b), whose
-- well-definedness is one application of distributivity.
intAddZeroL : (z : Int) → intZero + z ≡ z
  using (hyp.rw,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intZero.eq,
    Int.add.+.eq,
    plusComm,
    plusComm.rw,
    zeroPlusId,
    zeroPlusId.rw)
intAddZeroL = λz. quot-elim (p. ⋆) z

intAddZeroR : (z : Int) → z + intZero ≡ z
  using (hyp.rw,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intZero.eq,
    Int.add.+.eq,
    plusComm,
    plusComm.rw,
    plusZeroId,
    plusZeroId.rw,
    zeroPlusId,
    zeroPlusId.rw)
intAddZeroR = λz. quot-elim (p. ⋆) z

intScaleN : ℕ → Int → Int using (distribBack, distribBack.rw, hyp.rw, Int.Int.unfold)
intScaleN = λn z. quot-elim (p. class (n * p .π₁, n * p .π₂)) z

intScaleNZero : (n : ℕ) → intScaleN n intZero ≡ intZero
  using (Int.Int.unfold, Int.intZero.eq, Rat.frac.intScaleN.eq)
intScaleNZero = λn. ⋆

intScaleNOne : (z : Int) → intScaleN (S Z) z ≡ z
  using (hyp.rw,
    intScaleN.eq,
    Int.Int.eq,
    Int.Int.unfold,
    oneMult,
    oneMult.rw,
    plusComm,
    plusComm.rw)
intScaleNOne = λz. quot-elim (p. ⋆) z

-- scaling by n+1 really is n+1 iterated additions — the definition by
-- representatives agrees with the recursive one
intScaleNSuc : (n : ℕ) (z : Int) → intScaleN (S n) z ≡ z + intScaleN n z
  using (hyp.rw,
    intScaleN.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.add.+.eq,
    sucMultBack,
    sucMultBack.rw)
intScaleNSuc = λn z. quot-elim (p. ⋆) z

intScale : NZ → Int → Int using (Int.Int.unfold, Rat.frac.NZ.unfold)
intScale = λd z. ⊎-elim (n. intScaleN (S n) z) (n. intNeg (intScaleN (S n) z)) d

intScaleOne : {z : Int} → intScale nzOne z ≡ z
  using (intScale.eq, intScaleNOne, Int.Int.unfold, nzOne.eq, nzPos.eq)
intScaleOne = λz. ⋆

intScaleZero : (d : NZ) → intScale d intZero ≡ intZero
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intZero.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq)
intScaleZero = λd. ⊎-elim (n. ⋆) (n. ⋆) d

-- Adding a scaled zero. Both arguments of intAdd are quot-elim
-- SCRUTINEE positions, and a rewrite may not land in one unless the
-- subterm is ⇒ᴺ-inferable (NovaKernel.txt §6, the neutral-subterm
-- rule) — which a stuck ⊎-elim like `intScale d intZero` is not. So
-- the ⊎-elim on d is done here, where each branch closes at the ROOT
-- (a type-determined position) against intAddZeroL/R, and the other
-- summand is kept a VARIABLE so there is nothing to rewrite in it.
-- Callers compose with trans rather than ask the engine to rewrite
-- these in place.
intAddScaleZeroL : {d : NZ} {y : Int} → intScale d intZero + y ≡ y
  using (intAddZeroL,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intNeg.eq,
    Int.intZero.eq,
    Int.add.+.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq)
intAddScaleZeroL = λd y. ⊎-elim (n. intAddZeroL y) (n. intAddZeroL y) d

intAddScaleZeroR : {d : NZ} {y : Int} → y + intScale d intZero ≡ y
  using (intAddZeroR, Int.Int.unfold, Rat.frac.NZ.unfold, Rat.frac.intScaleZero)
intAddScaleZeroR = λd y. ⊎-elim (n. intAddZeroR y) (n. intAddZeroR y) d

-- scaling by d agrees with multiplying by d's image in Int
intScaleToInt : {d : NZ} → intScale d (class (S Z, Z)) ≡ nzToInt d
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.nzToInt.eq)
intScaleToInt = λd. ⊎-elim (n. ⋆) (n. ⋆) d

-- ===== the rationals =====
Rat : 𝕌
Rat = Int × NZ

mkRat : Int → NZ → Rat using (Rat.frac.Rat.unfold)
mkRat = λn d. n, d

num : Rat → Int using (Int.Int.unfold, Rat.frac.Rat.unfold)
num = λq. q .π₁

den : Rat → NZ using (Rat.frac.NZ.unfold, Rat.frac.Rat.unfold)
den = λq. q .π₂

denInt : Rat → Int using (Int.Int.unfold, Rat.frac.Rat.unfold)
denInt = λq. nzToInt (q .π₂)

ratOfInt : Int → Rat using (Rat.frac.Rat.unfold)
ratOfInt = λz. mkRat z nzOne

ratZero : Rat using (Rat.frac.Rat.unfold)
ratZero = ratOfInt intZero

ratOne : Rat using (Rat.frac.Rat.unfold)
ratOne = ratOfInt intOne

-- n₁/d₁ + n₂/d₂ = (n₁·d₂ + n₂·d₁) / (d₁·d₂). Rat is a plain Σ-code —
-- pair construction, nothing to discharge. (Once Rat is quotiented by
-- cross-multiplication, ratAdd will owe a descent proof; that is the
-- next step, not this one.)
ratAdd : Rat → Rat → Rat using (Rat.frac.Rat.unfold)
ratAdd = λp q. mkRat (intScale (den q) (num p) + intScale (den p) (num q)) (nzMul (den p) (den q))

-- ½ + ½ = 4/4, unreduced, as the raw representation demands
half : Rat using (Rat.frac.Rat.unfold)
half = mkRat intOne (nzPos (S Z))

ratAddTest : ratAdd half half ≡ mkRat (class (4, Z)) (nzPos 3)
  using (Int.Int.unfold,
    Int.intOne.eq,
    Int.add.+.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.half.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratAdd.eq)
ratAddTest = ⋆

-- ⅓ + (−⅓) = 0/(−9): numerator cancels, denominator keeps its sign
third : Rat using (Rat.frac.Rat.unfold)
third = mkRat intOne (nzPos 2)

negThird : Rat using (Rat.frac.Rat.unfold)
negThird = mkRat intOne (nzNeg 2)

-- the numerator's cancellation, at the root where the quotient join is
-- available (under the test's pair it is a component position, which
-- the strict engine reaches only by whole-equation match)
threeCancel : class (3, 3) ≡ intZero using (Int.Int.unfold, Int.intZero.eq)
threeCancel = ⋆

ratAddTest2 : ratAdd third negThird ≡ mkRat intZero (nzNeg 8)
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intOne.eq,
    Int.add.+.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.negThird.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.third.eq,
    threeCancel)
ratAddTest2 = trans _ _ _ ⋆ (cong (λu. Rat) (λx. mkRat x (nzNeg 8)) threeCancel)

-- ===== 0/1 is a unit =====
-- componentwise first: the numerator collapses by the scaled-zero
-- unit followed by intScaleOne, the denominator by nzMulOne
ratAddZeroLNum : {q : Rat} → intScale (den q) intZero + intScale nzOne (num q) ≡ num q
  using (intScaleNOne)
ratAddZeroLNum = λq. trans _ (intScale nzOne (num q)) _ intAddScaleZeroL intScaleOne

ratAddZeroRNum : {q : Rat} → intScale nzOne (num q) + intScale (den q) intZero ≡ num q
  using (intScaleNOne)
ratAddZeroRNum = λq. trans _ (intScale nzOne (num q)) _ intAddScaleZeroR intScaleOne

-- Σ-η, as a step of its own: el-sigma-eta is judgemental in the
-- theory but the kernel's normal forms do not contract (t.π₁ , t.π₂),
-- so the last hop has to be named
ratEta : {q : Rat} → mkRat (num q) (den q) ≡ q
  using (den.eq,
    Int.Int.unfold,
    mkRat.eq,
    num.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    sigma.eta)
ratEta = λq. ⋆

-- and then the pair, one component at a time
ratAddZeroL : {q : Rat} → ratAdd ratZero q ≡ q
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intZero.eq,
    Int.add.+.eq,
    nzMulOneL,
    ratEta,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.eq,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq)
ratAddZeroL =
  λq. trans
    _
    _
    _
    trans
      ratAdd ratZero q
      _
      q .π₁, q .π₂
      cong
        λw. Rat
        λx. mkRat x (nzMul nzOne (den q))
        {intScale (den q) intZero + intScale nzOne (num q)}
        {num q}
        ratAddZeroLNum
      cong (λw. Rat) (λd. mkRat (num q) d) {nzMul nzOne (den q)} {den q} nzMulOneL
    ratEta

ratAddZeroR : {q : Rat} → ratAdd q ratZero ≡ q
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intZero.eq,
    Int.add.+.eq,
    nzMulOneR,
    ratEta,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.eq,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.intScaleN.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq)
ratAddZeroR =
  λq. trans
    _
    _
    _
    trans
      ratAdd q ratZero
      _
      q .π₁, q .π₂
      cong
        λw. Rat
        λx. mkRat x (nzMul (den q) nzOne)
        {intScale nzOne (num q) + intScale (den q) intZero}
        {num q}
        ratAddZeroRNum
      cong (λw. Rat) (λd. mkRat (num q) d) {nzMul (den q) nzOne} {den q} nzMulOneR
    ratEta

-- ===== commutativity =====
-- (x + m) + k ≡ (x + k) + m: the addends the cross-sum needs swapped
plusSwapRight : {x m k : ℕ} → x + m + k ≡ x + k + m
  using (hyp.rw, plusAssoc, plusAssoc.rw, plusComm, plusComm.rw, swapLeft, swapLeft.rw)
plusSwapRight = λx m k. ⋆

-- the magnitude arithmetic of nzMul is symmetric: multComm on the
-- product, then the swap above on the two summands
mulPlusComm : {m k : ℕ} → m * k + m + k ≡ k * m + k + m using (plusAssoc)
mulPlusComm = λm k. trans _ _ _ (cong (λu. ℕ) (λw. w + m + k) (multComm k m)) plusSwapRight

nzMulComm : {x y : NZ} → nzMul x y ≡ nzMul y x
  using (plusAssoc, Rat.frac.NZ.unfold, Rat.frac.nzMul.eq, Rat.frac.nzNeg.eq, Rat.frac.nzPos.eq)
nzMulComm =
  λx y. ⊎-elim
    m. ⊎-elim
      w. nzMul (nzPos m) w ≡ nzMul w (nzPos m)
      k. cong (λu. NZ) nzPos {m * k + m + k} {k * m + k + m} mulPlusComm
      k. cong (λu. NZ) nzNeg {m * k + m + k} {k * m + k + m} mulPlusComm
      y
    m. ⊎-elim
      w. nzMul (nzNeg m) w ≡ nzMul w (nzNeg m)
      k. cong (λu. NZ) nzNeg {m * k + m + k} {k * m + k + m} mulPlusComm
      k. cong (λu. NZ) nzPos {m * k + m + k} {k * m + k + m} mulPlusComm
      y
    x

-- p + q ≡ q + p: intAddComm on the numerator, nzMulComm on the
-- denominator (the middle term of the trans spelled out — the
-- elaborator has nothing else to pin it against)
ratAddComm : (p q : Rat) → ratAdd p q ≡ ratAdd q p
  using (Int.Int.unfold,
    Int.add.+.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.intScale.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.ratAdd.eq)
ratAddComm =
  λp q. trans
    _
    mkRat (intScale (den p) (num q) + intScale (den q) (num p)) (nzMul (den p) (den q))
    _
    cong
      λu. Rat
      λx. mkRat x (nzMul (den p) (den q))
      intAddComm (intScale (den q) (num p)) (intScale (den p) (num q))
    cong
      λu. Rat
      λd. mkRat (intScale (den p) (num q) + intScale (den q) (num p)) d
      {nzMul (den p) (den q)}
      {nzMul (den q) (den p)}
      nzMulComm

-- ===== negation =====
-- negate the numerator, keep the denominator
ratNeg : Rat → Rat using (Rat.frac.Rat.unfold)
ratNeg = λp. mkRat (intNeg (num p)) (den p)

ratNegHalf : ratNeg half ≡ mkRat (class (Z, S Z)) (nzPos (S Z))
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intOne.eq,
    Rat.frac.Rat.unfold,
    Rat.frac.den.eq,
    Rat.frac.half.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratNeg.eq)
ratNegHalf = ⋆