Rat.abs

-- ABSOLUTE VALUE on ℚ. The order is decidable (`sgnCases`), so this is
-- an honest function, not a squashed existence claim — and because
-- `sgnQ` is already a function on the QUOTIENT, no well-definedness
-- obligation arises anywhere below.
--
-- The organising fact is that |u| is the LEAST two-sided bound of u:
--
--   bndAbs      :  Bnd (qAbs u) u          -- it IS a bound
--   absLeOfBnd  :  Bnd b u → qAbs u ≤ b    -- and the least one
--
-- Every other law — involutivity under negation, the triangle
-- inequality, the reverse triangle inequality — follows from those two
-- by antisymmetry, with no further case analysis. This is the payoff
-- of Rat/bound.nova's decision to make two-sided bounds primitive
-- (D-7): |·| is defined in terms of Bnd rather than the other way
-- round.

import Rat (Q, +, *, qNeg, qZero, qAddComm, qAddAssoc, qAddZeroR, qAddNegR, qNegNeg, qMulComm, qMulZeroL)
import Rat.order (Sign, sZero, sPos, sNeg, sgnFlip, sgnQ, sgnQNegFlip, sgnCases, NonNegS, ≤, leQRefl, leQTrans, leQPlusMono, leQAntisym, qPlusNegCancelR, leQMulMono, qNegMulL)
import Rat.bound (Bnd, bndAdd, bndNeg, bndEq, bndZero, bndWeaken, bndOfBothLe, qNegZeroQ, leQZeroOfPos, leQZeroOfNonNeg, leQNegFlip)
import Core.equality (trans, sym, cong, transport)
import Core.id (Id, eqToId, idToEq)

qAbs : Q → Q using (Rat.Q.unfold)
qAbs = λu. ⊎-elim (nn. u) (hn. qNeg u) (sgnCases (sgnQ u))

-- ===== the two characterising facts =====
-- a negative sign flips to a positive one, so −u is nonnegative there
sgnQNegOfNeg : {u : Q} → Id _ (sgnQ u) sNeg → sgnQ (qNeg u) ≡ sPos
  using (Core.id.Id.unfold,
    Rat.order.Sign.unfold,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sgnFlip.eq,
    Rat.Q.unfold)
sgnQNegOfNeg =
  λu hn. trans
    _
    _
    _
    sgnQNegFlip
    trans _ _ sPos (cong (λw. Sign) (λw. sgnFlip w) (idToEq _ _ _ hn)) ⋆

bndAbs : (u : Q) → Bnd (qAbs u) u
  using (Core.id.Id.eq,
    Rat.abs.qAbs.eq,
    Rat.bound.Bnd.unfold,
    Rat.order.Sign.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnCases.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.+.eq,
    Rat.qNeg.eq)
bndAbs =
  λu. ⊎-elim
    w. Bnd (⊎-elim (nn. u) (hn. qNeg u) w) u
    nn. leQTrans _ _ _ (bndZero _ (leQZeroOfNonNeg _ nn) .π₁) (leQZeroOfNonNeg _ nn), leQRefl _
    hn. (,)
      transport (λw. w ≤ u) (sym _ _ (qNegNeg u)) (leQRefl u)
      leQTrans
        _
        _
        _
        transport (λw. w ≤ qZero) (qNegNeg u) (bndZero _ (leQZeroOfPos _ (sgnQNegOfNeg hn)) .π₁)
        leQZeroOfPos _ (sgnQNegOfNeg hn)
    sgnCases (sgnQ u)

absLeOfBnd : {b u : Q} → Bnd b u → qAbs u ≤ b
  using (Core.id.Id.eq,
    Rat.abs.qAbs.eq,
    Rat.bound.Bnd.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnCases.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.+.eq,
    Rat.qNeg.eq)
absLeOfBnd =
  λb u h. ⊎-elim
    w. ⊎-elim (nn. u) (hn. qNeg u) w ≤ b
    nn. h .π₂
    hn. bndNeg _ _ h .π₂
    sgnCases (sgnQ u)

-- ...and the converse: a bound on |u| is a two-sided bound on u
bndOfAbsLe : {b u : Q} → qAbs u ≤ b → Bnd b u using (Rat.bound.Bnd.unfold)
bndOfAbsLe = λb u le. bndWeaken _ _ _ le (bndAbs u)

-- ===== the laws =====
leQZeroAbs : (u : Q) → qZero ≤ qAbs u
  using (Core.id.Id.eq,
    Rat.abs.qAbs.eq,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnCases.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.+.eq,
    Rat.qNeg.eq,
    Rat.qZero.eq)
leQZeroAbs =
  λu. ⊎-elim
    w. qZero ≤ ⊎-elim (nn. u) (hn. qNeg u) w
    nn. leQZeroOfNonNeg _ nn
    hn. leQZeroOfPos _ (sgnQNegOfNeg hn)
    sgnCases (sgnQ u)

qAbsNeg : (u : Q) → qAbs (qNeg u) ≡ qAbs u
qAbsNeg =
  λu. leQAntisym
    absLeOfBnd (bndNeg _ _ (bndAbs u))
    absLeOfBnd (bndEq _ _ (qNegNeg u) (bndNeg _ _ (bndAbs (qNeg u))))

-- the triangle inequality is bndAdd, read through leastness
qAbsTriangle : (u v : Q) → qAbs (u + v) ≤ qAbs u + qAbs v
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
qAbsTriangle = λu v. absLeOfBnd (bndAdd (bndAbs u) (bndAbs v))

-- (a + b) − b ≡ a — the mirror of rationalOrder's qPlusNegCancelR
qAddSubCancel : {a b : Q} → a + b + qNeg b ≡ a using (Rat.Q.unfold)
qAddSubCancel =
  λa b. a + b + qNeg b
    ≡⟨ qAddAssoc a b (qNeg b) ⟩ a + (b + qNeg b)
    ≡⟨ cong (λw. Q) (λw. a + w) (qAddNegR b) ⟩ a + qZero
    ≡⟨ qAddZeroR a ⟩ a

-- a ≤ b + c gives a − c ≤ b
leQSubOfLeAdd : {a b c : Q} → a ≤ b + c → a + qNeg c ≤ b
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQSubOfLeAdd =
  λa b c le. transport
    λw. a + qNeg c ≤ w
    {b + c + qNeg c}
    {b}
    qAddSubCancel
    leQPlusMono (qNeg c) le

-- ===== the reverse triangle inequality =====
-- |u| − |v| ≤ |u − v| : split u as (u − v) + v and use leastness
qAbsSubLe : (u v : Q) → qAbs u + qNeg (qAbs v) ≤ qAbs (u + qNeg v)
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
qAbsSubLe =
  λu v. leQSubOfLeAdd
    transport
      λw. qAbs w ≤ qAbs (u + qNeg v) + qAbs v
      qPlusNegCancelR u v
      qAbsTriangle (u + qNeg v) v

-- ...so | |u| − |v| | ≤ |u − v|, and a bound on u − v bounds the
-- difference of the absolute values
bndAbsSub : (b u v : Q) → Bnd b (u + qNeg v) → Bnd b (qAbs u + qNeg (qAbs v))
  using (Rat.bound.Bnd.unfold)
bndAbsSub =
  λb u v h. bndWeaken
    _
    _
    _
    absLeOfBnd h
    bndOfBothLe
      _
      _
      qAbsSubLe u v
      transport
        λw. qAbs v + qNeg (qAbs u) ≤ w
        trans
          _
          _
          _
          sym _ _ (qAbsNeg (v + qNeg u))
          cong (λw. Q) (λw. qAbs w) (Rat.bound.qSubFlip v u)
        qAbsSubLe v u

-- ===== a nonnegative rational is its own absolute value =====
bndSelfOfNonNeg : {u : Q} → qZero ≤ u → Bnd u u using (Rat.bound.Bnd.unfold)
bndSelfOfNonNeg = λu nn. leQTrans _ _ _ (bndZero _ nn .π₁) nn, leQRefl _

qAbsOfNonNeg : {u : Q} → qZero ≤ u → qAbs u ≡ u using (Rat.bound.Bnd.unfold)
qAbsOfNonNeg = λu nn. leQAntisym (absLeOfBnd (bndSelfOfNonNeg nn)) (bndAbs u .π₂)

qAbsAbs : (u : Q) → qAbs (qAbs u) ≡ qAbs u
qAbsAbs = λu. qAbsOfNonNeg (leQZeroAbs u)

qAbsZero : qAbs qZero ≡ qZero
qAbsZero = qAbsOfNonNeg (leQRefl qZero)

-- ===== |·| is multiplicative =====
--
-- |u| is characterised by being nonnegative and being ±u, so it is
-- enough to show that |u|·|v| is nonnegative and is ±(u·v) — the sign
-- case analysis then happens once, on the two factors, and never on
-- the product.
qAbsEqOfNonNeg : {z : Q} (w : Q) → qZero ≤ w → (w ≡ z) → qAbs z ≡ w
qAbsEqOfNonNeg = λz w nn e. trans _ _ _ (cong (λt. Q) (λt. qAbs t) (sym _ _ e)) (qAbsOfNonNeg nn)

qAbsEqOfNonNegNeg : {z : Q} (w : Q) → qZero ≤ w → (w ≡ qNeg z) → qAbs z ≡ w
qAbsEqOfNonNegNeg = λz w nn e. trans _ _ _ (sym _ _ (qAbsNeg z)) (qAbsEqOfNonNeg _ nn e)

leQZeroMul : {a b : Q} → qZero ≤ a → qZero ≤ b → qZero ≤ a * b
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQZeroMul =
  λa b ha hb. transport (λw. w ≤ a * b) {qZero * b} {qZero} qMulZeroL (leQMulMono _ _ ha hb)

qNegMulR : (x c : Q) → x * qNeg c ≡ qNeg (x * c)
qNegMulR =
  λx c. trans
    _
    _
    _
    trans _ _ _ (qMulComm x (qNeg c)) (qNegMulL c x)
    cong (λw. Q) (λw. qNeg w) (qMulComm c x)

qAbsMul : (u v : Q) → qAbs (u * v) ≡ qAbs u * qAbs v
  using (Core.id.Id.unfold,
    Rat.abs.qAbs.eq,
    Rat.order.NonNegS.unfold,
    Rat.order.sgnCases.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.*.eq,
    Rat.qNeg.eq)
qAbsMul =
  λu v. ⊎-elim
    w. qAbs (u * v) ≡ ⊎-elim (nn. u) (hn. qNeg u) w * qAbs v
    nu. ⊎-elim
      w. qAbs (u * v) ≡ u * ⊎-elim (nn. v) (hn. qNeg v) w
      nv. qAbsEqOfNonNeg _ (leQZeroMul (leQZeroOfNonNeg _ nu) (leQZeroOfNonNeg _ nv)) ⋆
      hv. qAbsEqOfNonNegNeg
        _
        leQZeroMul (leQZeroOfNonNeg _ nu) (leQZeroOfPos _ (sgnQNegOfNeg hv))
        qNegMulR u v
      sgnCases (sgnQ v)
    hu. ⊎-elim
      w. qAbs (u * v) ≡ qNeg u * ⊎-elim (nn. v) (hn. qNeg v) w
      nv. qAbsEqOfNonNegNeg
        _
        leQZeroMul (leQZeroOfPos _ (sgnQNegOfNeg hu)) (leQZeroOfNonNeg _ nv)
        qNegMulL u v
      hv. qAbsEqOfNonNeg
        _
        leQZeroMul (leQZeroOfPos _ (sgnQNegOfNeg hu)) (leQZeroOfPos _ (sgnQNegOfNeg hv))
        trans
          _
          _
          _
          trans _ _ _ (qNegMulL u (qNeg v)) (cong (λw. Q) (λw. qNeg w) (qNegMulR u v))
          qNegNeg (u * v)
      sgnCases (sgnQ v)
    sgnCases (sgnQ u)

-- ===== the product of two bounds =====
bndMul : {a b u v : Q} → qZero ≤ a → qZero ≤ b → Bnd a u → Bnd b v → Bnd (a * b) (u * v)
  using (Rat.bound.Bnd.unfold)
bndMul =
  λa b u v ha hb hu hv. bndOfAbsLe
    transport
      λw. w ≤ a * b
      sym _ _ (qAbsMul u v)
      leQTrans
        _
        _
        _
        leQMulMono _ _ (absLeOfBnd hu) (leQZeroAbs v)
        transport
          λw. w ≤ a * b
          qMulComm (qAbs v) a
          transport (λw. qAbs v * a ≤ w) (qMulComm b a) (leQMulMono _ _ (absLeOfBnd hv) ha)