Rat.bound

-- Two-sided bounds on ℚ, stated WITHOUT an absolute value: `Bnd b u`
-- says −b ≤ u ≤ b. This is the shape every regularity/closeness
-- condition in Real.nova already has, and the shape the triangle
-- inequality wants — |u + v| ≤ |u| + |v| becomes bndAdd, with no
-- case split on signs anywhere, because the two halves of a two-sided
-- bound add independently.
--
-- Everything here is order algebra over Rat/order.nova; nothing
-- below inspects a representative.
-- ===== order lemmas the bound algebra needs =====
-- negation reverses ≤ : the two differences are the same rational

import Rat (Q, +, qNeg, qZero, qAddComm, qAddAssoc, qAddZeroL, qAddZeroR, qAddNegL, qAddNegR, qNegNeg)
import Rat.order (Sign, sPos, sNeg, sZero, sgnQ, NonNegS, ≤, leQRefl, leQOfEq, leQTrans, sZeroNotNeg, sPosNotNeg, sZeroNotPos, leQPlusMono, leQPlusMonoL, qNegAdd, qPairSwap, qSubSplit, qSubPlusCancel)
import Core.equality (trans, sym, cong, transport, pairext)
import Core.id (Id, eqToId, idToEq)
import Core.uip (uip)

leQNegFlip : (x y : Q) → x ≤ y → qNeg y ≤ qNeg x
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQNegFlip =
  λx y h. transport
    λw. NonNegS (sgnQ w)
    {y + qNeg x}
    {qNeg x + qNeg (qNeg y)}
    y + qNeg x
      ≡⟨ qAddComm y (qNeg x) ⟩ qNeg x + y
      ≡⟨ cong (λw. Q) (λw. qNeg x + w) (sym _ _ (qNegNeg y)) ⟩ qNeg x + qNeg (qNeg y)
    h

-- ...and back: (−y) ≤ (−x) gives x ≤ y, by flipping once more
leQNegFlipBack : (x y : Q) → qNeg y ≤ qNeg x → x ≤ y
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQNegFlipBack =
  λx y h. transport
    λw. w ≤ y
    qNegNeg x
    transport (λw. qNeg (qNeg x) ≤ w) (qNegNeg y) (leQNegFlip _ _ h)

-- ≤ adds in BOTH arguments — two monotonicity steps and a hop
leQAdd : (x y z w : Q) → x ≤ y → z ≤ w → x + z ≤ y + w
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQAdd = λx y z w h1 h2. leQTrans _ _ _ (leQPlusMono z h1) (leQPlusMonoL _ _ y h2)

-- ===== the bound relation =====
Bnd : Q → Q → 𝕌
Bnd = λb u. qNeg b ≤ u × u ≤ b

bndLo : (b u : Q) → Bnd b u → qNeg b ≤ u
  using (Rat.bound.Bnd.unfold, Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
bndLo = λb u h. h .π₁

bndHi : (b u : Q) → Bnd b u → u ≤ b
  using (Rat.bound.Bnd.unfold, Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
bndHi = λb u h. h .π₂

-- the triangle inequality, in two-sided form
bndAdd : {a b u v : Q} → Bnd a u → Bnd b v → Bnd (a + b) (u + v) using (Rat.bound.Bnd.unfold)
bndAdd =
  λa b u v hu hv. (,)
    transport (λw. w ≤ u + v) (sym _ _ (qNegAdd a b)) (leQAdd _ _ _ _ (hu .π₁) (hv .π₁))
    leQAdd _ _ _ _ (hu .π₂) (hv .π₂)

-- a bound on u bounds −u, with the same b
bndNeg : (b u : Q) → Bnd b u → Bnd b (qNeg u) using (Rat.bound.Bnd.unfold)
bndNeg =
  λb u h. leQNegFlip _ _ (h .π₂), transport (λw. qNeg u ≤ w) (qNegNeg b) (leQNegFlip _ _ (h .π₁))

-- a bound transports along an equality of the bounded rational
bndEq : {b : Q} (u v : Q) → (u ≡ v) → Bnd b u → Bnd b v using (Rat.bound.Bnd.unfold)
bndEq = λb u v e h. transport (λw. Bnd b w) e h

-- ...and along an equality of the bound
bndEqB : (a b u : Q) → (a ≡ b) → Bnd a u → Bnd b u using (Rat.bound.Bnd.unfold)
bndEqB = λa b u e h. transport (λw. Bnd w u) e h

-- a bound weakens to any larger bound
bndWeaken : (a b u : Q) → a ≤ b → Bnd a u → Bnd b u using (Rat.bound.Bnd.unfold)
bndWeaken = λa b u le h. leQTrans _ _ _ (leQNegFlip _ _ le) (h .π₁), leQTrans _ _ _ (h .π₂) le

-- ===== zero =====
qNegZeroQ : qNeg qZero ≡ qZero
  using (Int.intNeg.eq,
    Int.intZero.eq,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.ratNeg.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.ratZero.eq,
    Rat.Q.unfold,
    Rat.qNeg.eq,
    Rat.qZero.eq,
    Rat.qcls.eq)
qNegZeroQ = ⋆

-- 0 is bounded by every nonnegative b
bndZero : (b : Q) → qZero ≤ b → Bnd b qZero using (Rat.bound.Bnd.unfold)
bndZero = λb le. transport (λw. qNeg b ≤ w) qNegZeroQ (leQNegFlip _ _ le), le

-- a difference of EQUAL rationals is bounded by every nonnegative b
bndSubEq : (b u v : Q) → qZero ≤ b → (u ≡ v) → Bnd b (u + qNeg v) using (Rat.bound.Bnd.unfold)
bndSubEq =
  λb u v le e. bndEq
    _
    _
    sym _ _ (trans _ _ _ (cong (λw. Q) (λw. w + qNeg v) e) (qAddNegR v))
    bndZero _ le

-- ===== reassociating a difference =====
-- (u − w) ≡ (u − v) + (v − w): the standard three-term split, so a
-- bound on a difference follows from bounds on the two legs
qSubVia : (u v w : Q) → u + qNeg v + (v + qNeg w) ≡ u + qNeg w
qSubVia = λu v w. qSubSplit _ _ _

-- the triangle inequality for differences, through a midpoint
bndVia : (a b u v w : Q) → Bnd a (u + qNeg v) → Bnd b (v + qNeg w) → Bnd (a + b) (u + qNeg w)
  using (Rat.bound.Bnd.unfold)
bndVia = λa b u v w h1 h2. bndEq _ _ (qSubVia u v w) (bndAdd h1 h2)

-- −(u − v) ≡ v − u, so a bound on one difference bounds the other
qSubFlip : (u v : Q) → qNeg (u + qNeg v) ≡ v + qNeg u using (Rat.Q.unfold)
qSubFlip =
  λu v. qNeg (u + qNeg v)
    ≡⟨ qNegAdd u (qNeg v) ⟩ qNeg u + qNeg (qNeg v)
    ≡⟨ cong (λz. Q) (λz. qNeg u + z) (qNegNeg v) ⟩ qNeg u + v
    ≡⟨ qAddComm (qNeg u) v ⟩ v + qNeg u

bndSubSym : (b u v : Q) → Bnd b (u + qNeg v) → Bnd b (v + qNeg u) using (Rat.bound.Bnd.unfold)
bndSubSym = λb u v h. bndEq _ _ (qSubFlip u v) (bndNeg _ _ h)

-- ===== differences of sums =====
-- (a − b) + (c − d) ≡ (a + c) − (b + d): the two differences of a
-- componentwise sum add. This is what makes bndAdd applicable to a
-- difference of SUMS, which is every well-definedness goal for +.
qSubAdd : (a b c d : Q) → a + qNeg b + (c + qNeg d) ≡ a + c + qNeg (b + d) using (Rat.Q.unfold)
qSubAdd =
  λa b c d. a + qNeg b + (c + qNeg d)
    ≡⟨ qPairSwap a (qNeg b) c (qNeg d) ⟩ a + c + (qNeg b + qNeg d)
    ≡⟨ cong (λw. Q) (λw. a + c + w) (sym _ _ (qNegAdd b d)) ⟩ a + c + qNeg (b + d)

-- a common LEFT summand cancels from a difference (rationalOrder has
-- the right-summand version)
qSubPlusCancelL : (x y w : Q) → w + y + qNeg (w + x) ≡ y + qNeg x using (Rat.Q.unfold)
qSubPlusCancelL =
  λx y w. w + y + qNeg (w + x)
    ≡⟨ cong (λv. Q) (λv. v + qNeg (w + x)) (qAddComm w y) ⟩ y + w + qNeg (w + x)
    ≡⟨ cong (λv. Q) (λv. y + w + qNeg v) (qAddComm w x) ⟩ y + w + qNeg (x + w)
    ≡⟨ qSubPlusCancel x y w ⟩ y + qNeg x

-- ===== nonnegativity from a positive sign =====
-- u − 0 is u : the one rewriting step every 0 ≤ u proof needs
qSubZeroR : {u : Q} → u + qNeg qZero ≡ u
qSubZeroR = λu. trans _ _ _ (cong (λv. Q) (λv. u + v) qNegZeroQ) (qAddZeroR u)

-- 0 ≤ u whenever u's sign is nonnegative
leQZeroOfNonNeg : (u : Q) → NonNegS (sgnQ u) → qZero ≤ u
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQZeroOfNonNeg =
  λu h. transport NonNegS (sym _ _ (cong (λv. Sign) (λv. sgnQ v) {u + qNeg qZero} {u} qSubZeroR)) h

-- 0 ≤ u whenever u's sign is positive: the difference u − 0 is u
leQZeroOfPos : (u : Q) → (sgnQ u ≡ sPos) → qZero ≤ u
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQZeroOfPos =
  λu h. inj₂
    eqToId _ _ (trans _ _ _ (cong (λv. Sign) (λv. sgnQ v) {u + qNeg qZero} {u} qSubZeroR) h)

-- ===== growing a bound by a nonnegative amount =====
leQSelfAdd : (a : Q) {b : Q} → qZero ≤ b → a ≤ a + b
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQSelfAdd = λa b le. transport (λw. w ≤ a + b) (qAddZeroR a) (leQPlusMonoL _ _ a le)

leQSelfAddL : {a b : Q} → qZero ≤ b → a ≤ b + a using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQSelfAddL = λa b le. transport (λw. a ≤ w) (qAddComm a b) (leQSelfAdd a le)

-- the ONE-SIDED triangle inequality: a difference splits through a
-- midpoint and the two upper bounds add
leQVia : {a b u : Q} (v : Q) {w : Q} → u + qNeg v ≤ a → v + qNeg w ≤ b → u + qNeg w ≤ a + b
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQVia = λa b u v w h1 h2. transport (λz. z ≤ a + b) (qSubVia u v w) (leQAdd _ _ _ _ h1 h2)

-- an upper bound on the reversed difference is a lower bound on it
bndOfBothLe : {b : Q} (u v : Q) → u + qNeg v ≤ b → v + qNeg u ≤ b → Bnd b (u + qNeg v)
  using (Rat.bound.Bnd.unfold)
bndOfBothLe = λb u v h1 h2. transport (λw. qNeg b ≤ w) (qSubFlip v u) (leQNegFlip _ _ h2), h1

-- a nonnegative sign is not the negative one — the refutation every
-- decision branch needs
nonNegNotNeg : (s : Sign) → NonNegS s → Id _ s sNeg → 𝟘 using (Rat.order.NonNegS.unfold)
nonNegNotNeg =
  λs nn hn. ⊎-elim
    h0. sZeroNotNeg (trans _ _ _ (sym _ _ (idToEq _ _ _ h0)) (idToEq _ _ _ hn))
    hp. sPosNotNeg (trans _ _ _ (sym _ _ (idToEq _ _ _ hp)) (idToEq _ _ _ hn))
    nn

-- ===== order verdicts are unique =====
--
-- `LeQ x y` is DATA — a `⊎` of two `Id`s — but it carries no
-- information: `sgnQ` is a function, so which injection is inhabited
-- is determined by x and y, and `uip` says the `Id` payload is unique.
-- So ≤ behaves like a proposition after all, and anything built from
-- it (a `Bnd`, a regularity witness) inherits that.
nonNegIsProp : (s : Sign) (p q : NonNegS s) → p ≡ q
  using (Core.id.Id.unfold, Rat.order.NonNegS.unfold, Rat.order.Sign.unfold)
nonNegIsProp =
  λs p q. ⊎-elim
    a. ⊎-elim
      b. cong (λv. NonNegS s) (λw. inj₁ w) {a} {b} uip
      b. 𝟘-elim (sZeroNotPos (trans _ _ _ (sym _ _ (idToEq _ _ _ a)) (idToEq _ _ _ b)))
      q
    a. ⊎-elim
      b. 𝟘-elim (sZeroNotPos (trans _ _ _ (sym _ _ (idToEq _ _ _ b)) (idToEq _ _ _ a)))
      b. cong (λv. NonNegS s) (λw. inj₂ w) {a} {b} uip
      q
    p

leQIsProp : (x y : Q) (p q : x ≤ y) → p ≡ q
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
leQIsProp = λx y. nonNegIsProp (sgnQ (y + qNeg x))

bndIsProp : (b u : Q) (p q : Bnd b u) → p ≡ q
  using (Rat.bound.Bnd.unfold, Rat.order.≤.unfold, Rat.order.NonNegS.unfold, Rat.Q.unfold)
bndIsProp = λb u p q. pairext (leQIsProp _ _ (p .π₁) (q .π₁)) (leQIsProp _ _ (p .π₂) (q .π₂))