Real.lt

-- The STRICT order on ℝ. Bishop states it on representatives — some
-- index where y_n beats x_n by more than the modulus — and then owes a
-- proof that the statement survives REq. Stating it one level UP
-- instead,
--
--   u < v  ≜  ∃k. u + 1/(k+1) ≤ v
--
-- makes invariance free: everything on the right already lives on ℝ.
-- The existential is squashed, which is exactly right — the witness k
-- is not determined by u and v — and costs nothing, because LtR is
-- itself a proposition, so squash-elimination always lands where it is
-- allowed.
--
-- The two nontrivial facts are irreflexivity, which needs ℝ's group
-- structure to strip u and then ℚ ↪ ℝ's order-reflection to reach a
-- contradiction in ℚ, and ltROfQ, which is where Rat/arch.nova's
-- Archimedean witness is spent.

import Rat (Q, +, qNeg, qZero, qOne, qAddComm)
import Rat.order (Sign, sPos, sgnQ, ≤, leQAntisym, leQPlusMono, qPlusNegCancelR)
import Rat.lt (<, sgnOfLtQ, ltQOfSgn, leQOfLtQ)
import Rat.half (leQZeroInvNat)
import Rat.arch (ArchWit, qArch, qInvNatNotZero)
import Real (qInvNat, Real, realOfQ, realZero, realOne)
import Real.add (+, realAddComm, realAddAssoc, realAddZeroR, realAddNegR, realAddOfQ)
import Real.neg (realNeg)
import Real.order (≤, leRRefl, leRTrans, leRAddMono, leROfQ, leQOfLeR, leQZeroOne)
import Core.prop (⊥)
import Core.equality (trans, sym, cong, transport, transportP)

infixl 4 <
< : Real → Real → Ω
(<) = λu v. ∥(k : ℕ) × u + realOfQ (qInvNat k) ≤ v∥

ltROf : (u v : Real) (k : ℕ) → u + realOfQ (qInvNat k) ≤ v → u < v using (Real.lt.<.unfold)
ltROf = λu v k h. ⋆ (k, h)

-- ===== ℝ group algebra the proofs need =====
realAddNegCancel : (u q : Real) → u + q + realNeg u ≡ q using (Real.Real.unfold)
realAddNegCancel =
  λu q. u + q + realNeg u
    ≡⟨ cong (λw. Real) (λw. w + realNeg u) (realAddComm u q) ⟩ q + u + realNeg u
    ≡⟨ realAddAssoc q u (realNeg u) ⟩ q + (u + realNeg u)
    ≡⟨ cong (λw. Real) (λw. q + w) (realAddNegR u) ⟩ q + realZero
    ≡⟨ realAddZeroR q ⟩ q

realAddSwapR : (u q w : Real) → u + q + w ≡ u + w + q using (Real.Real.unfold)
realAddSwapR =
  λu q w. u + q + w
    ≡⟨ realAddAssoc u q w ⟩ u + (q + w)
    ≡⟨ cong (λv. Real) (λv. u + v) (realAddComm q w) ⟩ u + (w + q)
    ≡⟨ sym _ _ (realAddAssoc u w q) ⟩ u + w + q

-- 0 ≤ 1/(k+1), lifted
leRZeroInv : (k : ℕ) → realZero ≤ realOfQ (qInvNat k)
  using (Rat.qZero.eq,
    Real.qInvNat.eq,
    Real.realOfQ.eq,
    Real.realOfQ.unfold,
    Real.realZero.eq,
    Real.realZero.unfold,
    Real.order.≤.eq,
    Real.order.≤.unfold,
    Real.order.RLeP.unfold)
leRZeroInv = λk. leROfQ _ _ (leQZeroInvNat k)

-- u ≤ u + 1/(k+1)
leRSelfInv : (u : Real) (k : ℕ) → u ≤ u + realOfQ (qInvNat k) using (Real.order.≤.unfold)
leRSelfInv =
  λu k. transportP
    λw. w ≤ u + realOfQ (qInvNat k)
    Real.add.realAddZeroL u
    transportP
      {Real}
      λw. realZero + u ≤ w
      {realOfQ (qInvNat k) + u}
      realAddComm (realOfQ (qInvNat k)) u
      leRAddMono (leRZeroInv k)

-- ===== the order laws =====
leROfLtR : (u v : Real) → u < v → u ≤ v using (Real.lt.<.unfold, Real.order.≤.unfold)
leROfLtR = λu v h. squash-elim h (w. leRTrans _ _ _ (leRSelfInv u (w .π₁)) (w .π₂))

ltRTrans : (u v t : Real) → u < v → v < t → u < t using (Real.lt.<.unfold)
ltRTrans = λu v t h1 h2. squash-elim h1 (w. ltROf _ _ _ (leRTrans _ _ _ (w .π₂) (leROfLtR _ _ h2)))

leRLtTrans : (u v t : Real) → u ≤ v → v < t → u < t using (Real.lt.<.unfold)
leRLtTrans =
  λu v t h1 h2. squash-elim
    h2
    w. ltROf
      _
      _
      _
      leRTrans
        u + realOfQ (qInvNat (w .π₁))
        v + realOfQ (qInvNat (w .π₁))
        _
        leRAddMono h1
        w .π₂

ltRLeTrans : (u v t : Real) → u < v → v ≤ t → u < t using (Real.lt.<.unfold)
ltRLeTrans = λu v t h1 h2. squash-elim h1 (w. ltROf _ _ _ (leRTrans _ _ _ (w .π₂) h2))

-- irreflexivity: strip u from both sides, then read the result off in ℚ
ltRIrrefl : (u : Real) → u < u → ⊥
  using (Core.prop.⊥.unfold,
    Rat.qZero.eq,
    Real.Real.unfold,
    Real.realOfQ.eq,
    Real.realZero.eq,
    Real.add.+.unfold,
    Real.lt.<.unfold,
    Real.order.≤.unfold)
ltRIrrefl =
  λu h. squash-elim
    h
    w. ⋆
      qInvNatNotZero
        _
        leQAntisym
          leQOfLeR
            qZero
            transportP
              λt. t ≤ realZero
              realAddNegCancel u (realOfQ (qInvNat (w .π₁)))
              transportP
                {Real}
                λt. u + realOfQ (qInvNat (w .π₁)) + realNeg u ≤ t
                {u + realNeg u}
                realAddNegR u
                leRAddMono (w .π₂)
          leQZeroInvNat (w .π₁)

-- ===== ℚ ↪ ℝ preserves and reflects the strict order =====
-- p < q in ℚ: the Archimedean witness supplies the index, and the
-- squash it comes in is absorbed by LtR's own
ltROfQ : {p q : Q} → p < q → realOfQ p < realOfQ q using (Rat.arch.ArchWit.unfold, Real.lt.<.unfold)
ltROfQ =
  λp q h. squash-elim
    qArch _ (sgnOfLtQ h)
    w. ltROf
      _
      _
      _
      transportP
        λt. t ≤ realOfQ q
        sym _ _ (realAddOfQ p (qInvNat (w .π₁)))
        leROfQ
          _
          _
          transport
            λt. t ≤ q
            qAddComm (qInvNat (w .π₁)) p
            transport (λt. qInvNat (w .π₁) + p ≤ t) (qPlusNegCancelR q p) (leQPlusMono p (w .π₂))

ltRZeroOne : realZero < realOne
  using (Rat.bound.qNegZeroQ.rw,
    Rat.order.Sign.unfold,
    Rat.qAddZeroR.rw,
    Real.realOfQ.eq,
    Real.realOne.eq,
    Real.realZero.eq,
    Real.lt.<.eq,
    Real.lt.<.unfold,
    Real.order.sgnQOnePos)
ltRZeroOne = ltROfQ (ltQOfSgn qZero qOne ⋆)

-- ===== compatibility with addition =====
ltRAddMono : (u v t : Real) → u < v → u + t < v + t using (Real.lt.<.unfold)
ltRAddMono =
  λu v t h. squash-elim
    h
    w. ltROf
      _
      _
      _
      transportP
        {Real}
        λs. s ≤ v + t
        {u + realOfQ (qInvNat (w .π₁)) + t}
        realAddSwapR u (realOfQ (qInvNat (w .π₁))) t
        leRAddMono (w .π₂)