Rat.invOrder

-- ORDER FACTS ABOUT ℚ's RECIPROCAL.
--
-- rationalAlgInv gives qInv and the one equation qMulInvR: u · u⁻¹ = 1
-- for u ≠ 0. It says nothing about ORDER, and the reciprocal's
-- convergence estimate is entirely about order — |1/a − 1/b| is small
-- because a and b are bounded AWAY from zero. This module supplies
-- the missing half.
--
-- The chain has to be walked in the right order, because the obvious
-- route is circular: cancelling by a positive c wants 0 ≤ c⁻¹, and the
-- usual proof of 0 ≤ c⁻¹ wants cancellation. It is broken by proving
-- 0 ≤ c⁻¹ directly from a SIGN case split: if c⁻¹ were negative then
-- c · c⁻¹ would be ≤ 0, and it is 1.

import Core.prop (⊥, ¬, ⊃, impIntro, impApply, absurdP)
import Rat (Q, +, *, qNeg, qZero, qOne, qAddZeroL, qAddZeroR, qAddComm, qAddAssoc, qAddNegR, qNegNeg, qMulComm, qMulAssoc, qMulOneL, qMulOneR, qDistribR)
import Rat.order (Sign, sPos, sNeg, sZero, sgnQ, NonNegS, ≤, sgnCases, leQTrans, leQMulMono, leQAntisym, leQOfEq, sZeroNotPos)
import Rat.bound (leQNegFlip, leQZeroOfNonNeg, leQZeroOfPos, qNegZeroQ)
import Rat.abs (leQZeroMul, qNegMulR, sgnQNegOfNeg)
import Rat.lt (sgnQAddPosNonNeg)
import Rat.sqrt (qMulSwap3)
import Rat.algInv (qInv, qMulInvR, qInvUniqueVal)
import Real (qInvNat, qInvNatPos)
import Core.equality (trans, sym, cong, transport, transportP)
import Core.id (Id, idToEq, eqToId)

sgnQZeroEq : sgnQ qZero ≡ sZero using (Rat.order.sgnQZero)
sgnQZeroEq = ⋆

-- qOne IS qInvNat Z, so its sign comes from Real.qInvNatPos
qInvNatZeroEq : qInvNat Z ≡ qOne
  using (Real.qInvNat.eq,
    Rat.qOne.eq,
    Rat.qcls.eq,
    Rat.frac.mkRat.eq,
    Int.intOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.ratOne.eq,
    Rat.frac.ratOfInt.eq,
    Rat.frac.nzOne.eq)
qInvNatZeroEq = ⋆

sgnQOneEq : sgnQ qOne ≡ sPos
sgnQOneEq = transportP (λw. sgnQ w ≡ sPos) qInvNatZeroEq (qInvNatPos Z)

leQZeroOne : qZero ≤ qOne
leQZeroOne = leQZeroOfPos _ sgnQOneEq

qNeZeroOfPos : {u : Q} → (sgnQ u ≡ sPos) → ¬ (u ≡ qZero) using (Core.prop.¬.eq)
qNeZeroOfPos =
  λu hp. impIntro
    {u ≡ qZero}
    {⊥}
    λhz. 𝟘-elim
      sZeroNotPos
        trans _ _ _ (sym _ _ (trans _ _ _ (cong (λw. Sign) (λw. sgnQ w) hz) sgnQZeroEq)) hp

qMulInvPos : {c : Q} → (sgnQ c ≡ sPos) → c * qInv c ≡ qOne
qMulInvPos = λc hp. qMulInvR (qNeZeroOfPos hp)

-- a negative sign is a value at most zero
leQZeroOfNeg : {u : Q} → Id _ (sgnQ u) sNeg → u ≤ qZero
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQZeroOfNeg =
  λu hn. transport
    λw. NonNegS (sgnQ w)
    sym _ _ (qAddZeroL (qNeg u))
    inj₂ (eqToId _ _ (sgnQNegOfNeg hn))

-- nonnegative times nonpositive is nonpositive
leQMulNonPos : {a b : Q} → qZero ≤ a → b ≤ qZero → a * b ≤ qZero
leQMulNonPos =
  λa b ha hb. transport
    λw. w ≤ qZero
    qNegNeg (a * b)
    transport
      λw. qNeg w ≤ qZero
      qNegMulR a b
      transport
        λw. qNeg (a * qNeg b) ≤ w
        qNegZeroQ
        leQNegFlip _ _ (leQZeroMul ha (transport (λw. w ≤ qNeg b) qNegZeroQ (leQNegFlip _ _ hb)))

-- THE circle-breaker: the reciprocal of a positive is nonnegative.
-- If it were negative, c · c⁻¹ would be ≤ 0; but it is 1, and 0 ≤ 1,
-- so 1 = 0 and the signs collide.
leQZeroInv : {c : Q} → (sgnQ c ≡ sPos) → qZero ≤ qInv c
  using (Rat.order.≤.unfold, Rat.order.NonNegS.unfold)
leQZeroInv =
  λc hp. ⊎-elim
    nn. leQZeroOfNonNeg _ nn
    hn. 𝟘-elim
      sZeroNotPos
        trans
          _
          _
          _
          sym
            _
            _
            trans
              _
              _
              _
              cong
                λw. Sign
                λw. sgnQ w
                leQAntisym
                  transport
                    λw. w ≤ qZero
                    qMulInvPos hp
                    leQMulNonPos (leQZeroOfNonNeg c (inj₂ (eqToId _ _ hp))) (leQZeroOfNeg hn)
                  leQZeroOne
              sgnQZeroEq
          sgnQOneEq
    sgnCases (sgnQ (qInv c))

-- ===== cancellation, and what follows =====
cancelR : {z c : Q} → (sgnQ c ≡ sPos) → z * c * qInv c ≡ z
cancelR =
  λz c hp. trans
    _
    _
    _
    qMulAssoc z c (qInv c)
    trans _ _ _ (cong (λw. Q) (λw. z * w) (qMulInvPos hp)) (qMulOneR z)

leQMulCancel : {x y : Q} (c : Q) → (sgnQ c ≡ sPos) → x * c ≤ y * c → x ≤ y
leQMulCancel =
  λx y c hp h. transport
    {Q}
    λw. w ≤ y
    {x * c * qInv c}
    {x}
    cancelR hp
    transport
      {Q}
      λw. x * c * qInv c ≤ w
      {y * c * qInv c}
      {y}
      cancelR hp
      leQMulMono _ _ h (leQZeroInv hp)

qAddSubCancel : {c u : Q} → c + (u + qNeg c) ≡ u
qAddSubCancel =
  λc u. trans
    _
    _
    _
    trans
      _
      _
      _
      sym _ _ (qAddAssoc c u (qNeg c))
      trans _ _ _ (cong (λw. Q) (λw. w + qNeg c) (qAddComm c u)) (qAddAssoc u c (qNeg c))
    trans _ _ _ (cong (λw. Q) (λw. u + w) (qAddNegR c)) (qAddZeroR u)

-- anything above a positive is positive
sgnQPosOfLe : (c : Q) {u : Q} → (sgnQ c ≡ sPos) → c ≤ u → sgnQ u ≡ sPos using (Rat.order.≤.unfold)
sgnQPosOfLe =
  λc u hp h. transportP
    {Q}
    λw. sgnQ w ≡ sPos
    {c + (u + qNeg c)}
    {u}
    qAddSubCancel
    sgnQAddPosNonNeg hp h

-- the reciprocal is antitone on the positives: cancel by c, then by u
leQInvAnti : {c u : Q} → (sgnQ c ≡ sPos) → c ≤ u → qInv u ≤ qInv c
leQInvAnti =
  λc u hp h. leQMulCancel
    _
    hp
    transport
      λw. qInv u * c ≤ w
      sym _ _ (trans _ _ _ (qMulComm (qInv c) c) (qMulInvPos hp))
      leQMulCancel
        _
        sgnQPosOfLe _ hp h
        transport
          λw. w ≤ qOne * u
          sym
            _
            _
            trans
              _
              _
              _
              qMulSwap3 (qInv u) c u
              trans
                _
                _
                _
                cong
                  λw. Q
                  λw. w * c
                  trans _ _ _ (qMulComm (qInv u) u) (qMulInvPos (sgnQPosOfLe _ hp h))
                qMulOneL c
          transport (λw. c ≤ w) (sym _ _ (qMulOneL u)) h

-- ...so a reciprocal is bounded by any M inverse to a lower bound
leQInvBound : (c : Q) {u M : Q} → (sgnQ c ≡ sPos) → c ≤ u → (c * M ≡ qOne) → qInv u ≤ M
leQInvBound =
  λc u M hp h hm. transport
    λw. qInv u ≤ w
    sym _ _ (qInvUniqueVal _ hm (qMulInvPos hp))
    leQInvAnti hp h

-- ===== the difference identity =====
--
--   1/a − 1/b = (b − a)·(1/a)·(1/b)
--
-- This is what turns "a and b are close and bounded away from zero"
-- into "their reciprocals are close": the factor (b − a) carries the
-- closeness and the two reciprocals carry the bound.
negMulL : {x y : Q} → qNeg x * y ≡ qNeg (x * y)
negMulL =
  λx y. trans
    _
    _
    _
    qMulComm (qNeg x) y
    trans _ _ _ (qNegMulR y x) (cong (λw. Q) (λw. qNeg w) (qMulComm y x))

invFirst : (a b : Q) → (sgnQ b ≡ sPos) → b * qInv a * qInv b ≡ qInv a
invFirst =
  λa b hb. trans
    _
    _
    _
    qMulSwap3 b (qInv a) (qInv b)
    trans _ _ _ (cong (λw. Q) (λw. w * qInv a) (qMulInvPos hb)) (qMulOneL (qInv a))

invSecond : (a b : Q) → (sgnQ a ≡ sPos) → qNeg a * qInv a * qInv b ≡ qNeg (qInv b)
invSecond =
  λa b ha. trans
    _
    _
    _
    cong
      λw. Q
      λw. w * qInv b
      trans (qNeg a * qInv a) _ _ negMulL (cong (λw. Q) (λw. qNeg w) (qMulInvPos ha))
    trans (qNeg qOne * qInv b) _ _ negMulL (cong (λw. Q) (λw. qNeg w) (qMulOneL (qInv b)))

qInvDiff : {a b : Q}
  → (sgnQ a ≡ sPos) → (sgnQ b ≡ sPos) → (b + qNeg a) * qInv a * qInv b ≡ qInv a + qNeg (qInv b)
qInvDiff =
  λa b ha hb. (b + qNeg a) * qInv a * qInv b
    ≡⟨ cong (λw. Q) (λw. w * qInv b) (qDistribR (qInv a) b (qNeg a)) ⟩
      (b * qInv a + qNeg a * qInv a) * qInv b
    ≡⟨ qDistribR (qInv b) (b * qInv a) (qNeg a * qInv a) ⟩
      b * qInv a * qInv b + qNeg a * qInv a * qInv b
    ≡⟨ cong (λw. Q) (λw. w + qNeg a * qInv a * qInv b) (invFirst a _ hb) ⟩
      qInv a + qNeg a * qInv a * qInv b
    ≡⟨ cong (λw. Q) (λw. qInv a + w) (invSecond _ b ha) ⟩ qInv a + qNeg (qInv b)