Rat.lt

-- The STRICT order on ℚ. `LeQ` reads the difference's sign as
-- "nonnegative"; `LtQ` reads it as "positive". Everything is a
-- statement about that one sign, so every proof below is a chain in
-- `Sign` — no representative is ever opened.

import Rat (Q, +, qNeg, qZero, qAddComm, qAddZeroR, qAddNegR, qNegNeg)
import Rat.order (Sign, sZero, sPos, sNeg, sgnFlip, sgnQ, sgnQZero, sgnCases, sgnQAddPos, sgnQZeroView, sgnQNegFlip, NonNegS, ≤, leQTrans, qSubSplit, qDiffZero, qSubPlusCancel, sZeroNotPos, sNegNotPos, sPosNotNeg, qSubNeg)
import Rat.bound (leQZeroOfPos, qSubPlusCancelL)
import Rat.arch (sgnQSubFlip)
import Core.equality (trans, sym, cong, transport)
import Core.id (Id, eqToId, idToEq)

infixl 4 <
< : Q → Q → 𝕌
(<) = λx y. Id _ (sgnQ (y + qNeg x)) sPos

ltQOfSgn : (x y : Q) → (sgnQ (y + qNeg x) ≡ sPos) → x < y
  using (Core.id.Id.unfold, Rat.lt.<.unfold, Rat.Q.unfold)
ltQOfSgn = λx y h. eqToId _ _ h

sgnOfLtQ : {x y : Q} → x < y → sgnQ (y + qNeg x) ≡ sPos
  using (Core.id.Id.unfold, Rat.lt.<.unfold, Rat.Q.unfold)
sgnOfLtQ = λx y h. idToEq _ _ _ h

-- strict implies non-strict, on the nose: a positive sign IS a
-- nonnegative one
leQOfLtQ : {x y : Q} → x < y → x ≤ y
  using (Core.id.Id.unfold,
    Rat.lt.<.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.Q.unfold)
leQOfLtQ = λx y h. inj₂ h

ltQZero : (u : Q) → qZero < u → qZero ≤ u using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
ltQZero = λu h. leQOfLtQ h

-- ===== irreflexivity and asymmetry =====
ltQIrrefl : (x : Q) → x < x → 𝟘
ltQIrrefl =
  λx h. sZeroNotPos
    trans
      _
      _
      _
      sym _ _ (trans _ _ _ (cong (λw. Sign) (λw. sgnQ w) (qAddNegR x)) sgnQZero)
      sgnOfLtQ h

ltQAsym : (x y : Q) → x < y → y < x → 𝟘
  using (Core.id.Id.unfold,
    Rat.lt.<.unfold,
    Rat.order.Sign.unfold,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sgnFlip.eq,
    Rat.Q.unfold)
ltQAsym =
  λx y h1 h2. sNegNotPos
    trans
      _
      _
      _
      sym
        _
        _
        trans
          sgnQ (x + qNeg y)
          _
          _
          sgnQSubFlip
          trans _ _ sNeg (cong (λw. Sign) (λw. sgnFlip w) (sgnOfLtQ h1)) ⋆
      sgnOfLtQ h2

-- ===== transitivity, in all four mixed forms =====
-- a positive plus a NONNEGATIVE is positive: the zero case collapses
sgnQAddPosNonNeg : {a b : Q} → (sgnQ a ≡ sPos) → NonNegS (sgnQ b) → sgnQ (a + b) ≡ sPos
  using (Rat.order.NonNegS.unfold)
sgnQAddPosNonNeg =
  λa b ha hb. ⊎-elim
    h0. trans
      _
      _
      _
      cong
        λw. Sign
        λw. sgnQ w
        trans _ _ _ (cong (λw. Q) (λw. a + w) (sgnQZeroView _ (idToEq _ _ _ h0))) (qAddZeroR a)
      ha
    hp. sgnQAddPos _ _ ha (idToEq _ _ _ hp)
    hb

ltQTrans : (x y z : Q) → x < y → y < z → x < z using (Core.id.Id.unfold, Rat.lt.<.unfold)
ltQTrans =
  λx y z h1 h2. ltQOfSgn
    _
    _
    trans
      _
      _
      _
      cong (λw. Sign) (λw. sgnQ w) (sym _ _ (qSubSplit x y z))
      sgnQAddPos _ _ (sgnOfLtQ h2) (sgnOfLtQ h1)

leQLtTrans : (x y z : Q) → x ≤ y → y < z → x < z
  using (Core.id.Id.unfold,
    Rat.lt.<.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.Q.unfold)
leQLtTrans =
  λx y z h1 h2. ltQOfSgn
    _
    _
    trans
      {Sign}
      _
      _
      _
      cong (λw. Sign) (λw. sgnQ w) (sym _ _ (qSubSplit x y z))
      sgnQAddPosNonNeg (sgnOfLtQ h2) h1

ltQLeTrans : (x y z : Q) → x < y → y ≤ z → x < z
  using (Core.id.Id.unfold,
    Rat.lt.<.unfold,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.Q.unfold)
ltQLeTrans =
  λx y z h1 h2. ltQOfSgn
    _
    _
    trans
      {Sign}
      _
      _
      _
      cong
        λw. Sign
        λw. sgnQ w
        trans _ _ _ (sym _ _ (qSubSplit x y z)) (qAddComm (z + qNeg y) (y + qNeg x))
      sgnQAddPosNonNeg (sgnOfLtQ h1) h2

-- ===== trichotomy =====
ltQTrichotomy : (x y : Q) → x < y ⊎ Id _ x y ⊎ y < x
  using (Core.id.Id.eq,
    Core.id.Id.unfold,
    Rat.lt.<.eq,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.sNeg.eq,
    Rat.order.sPos.eq,
    Rat.order.sgnFlip.eq,
    Rat.order.sgnQ.eq,
    Rat.Q.unfold,
    Rat.+.eq,
    Rat.qNeg.eq)
ltQTrichotomy =
  λx y. ⊎-elim
    nn. ⊎-elim
      h0. inj₂ (inj₁ (eqToId _ _ (sym _ _ (qDiffZero (sgnQZeroView _ (idToEq _ _ _ h0))))))
      hp. inj₁ hp
      nn
    hneg. inj₂
      inj₂
        ltQOfSgn
          _
          _
          trans
            sgnQ (x + qNeg y)
            _
            _
            sgnQSubFlip
            trans _ _ sPos (cong (λw. Sign) (λw. sgnFlip w) (idToEq _ _ _ hneg)) ⋆
    sgnCases (sgnQ (y + qNeg x))

-- ===== compatibility with addition =====
ltQPlusMono : (x y w : Q) → x < y → x + w < y + w
  using (Core.id.Id.unfold, Rat.lt.<.unfold, Rat.Q.unfold)
ltQPlusMono =
  λx y w h. transport
    λs. Id _ s sPos
    sym _ _ (cong (λv. Sign) (λv. sgnQ v) (qSubPlusCancel x y w))
    h

ltQPlusMonoL : (x y w : Q) → x < y → w + x < w + y
  using (Core.id.Id.unfold, Rat.lt.<.unfold, Rat.Q.unfold)
ltQPlusMonoL =
  λx y w h. transport
    λs. Id _ s sPos
    sym _ _ (cong (λv. Sign) (λv. sgnQ v) (qSubPlusCancelL x y w))
    h