Real.metric

-- ℝ AS A METRIC SPACE, with the distance valued in ℝ itself:
--
--   d u v = |u − v|
--
-- symmetric, vanishing exactly on the diagonal, and satisfying the
-- triangle inequality. Every proof is one rewrite of Real/group.nova's
-- algebra composed with a fact about |·| that Real/abs.nova already
-- has — the metric axioms carry no analysis of their own.
-- ===== |u| bounds u on both sides, at the level of ℝ =====

import Rat (Q, +, qNeg, qZero)
import Rat.order (≤, leQTrans)
import Rat.half (dbl)
import Rat.abs (qAbs, bndAbs)
import Rat.bound (Bnd)
import Rat.arch (leQSubShift)
import Real (rBound, leQZeroBound, RSeq, Real, constReg, realOfQ, realZero, realOne)
import Real.neg (seqOf, rNeg, realNeg, realNegZero, realNegCls)
import Real.add (rAdd, +, realAddCls)
import Real.abs (rAbs, realAbs, realAbsCls, realAbsNeg, realAbsZero, leRZeroAbs, leRAbsTriangle)
import Real.order (RLeP, rleOf, ≤, leRAntisym, leRTrans, leQSubZero)
import Real.group (-, realSubSelf, realSubVia, realNegSub, realSubZeroInv)
import Core.equality (trans, sym, cong, transport, transportP)

leRAbsSelf : {u : Real} → u ≤ realAbs u
  using (Core.id.Id.eq,
    Rat.abs.qAbs.eq,
    Rat.bound.Bnd.unfold,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratNeg.eq,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnCases.eq,
    Rat.order.sgnQ.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Real.REq.unfold,
    Real.RSeq.unfold,
    Real.Real.unfold,
    Real.Regular.unfold,
    Real.qInvNat.eq,
    Real.rBound.eq,
    Real.abs.absSeq.eq,
    Real.abs.rAbs.eq,
    Real.abs.realAbs.eq,
    Real.neg.seqOf.eq,
    Real.order.≤.eq,
    Real.order.≤.unfold,
    Real.order.RLeP.eq)
leRAbsSelf =
  λu. quot-elim
    x. rleOf
      x
      rAbs x
      λn. leQTrans
        seqOf x n + qNeg (qAbs (seqOf x n))
        _
        _
        leQSubZero (bndAbs (seqOf x n) .π₂)
        leQZeroBound n n
    u

leRNegAbsSelf : {u : Real} → realNeg (realAbs u) ≤ u
  using (Core.id.Id.eq,
    Rat.abs.qAbs.eq,
    Rat.bound.Bnd.unfold,
    Rat.frac.ratAdd.eq,
    Rat.frac.ratNeg.eq,
    Rat.order.≤.unfold,
    Rat.order.NonNegS.unfold,
    Rat.order.Sign.eq,
    Rat.order.ratSgn.eq,
    Rat.order.sPos.eq,
    Rat.order.sZero.eq,
    Rat.order.sgnCases.eq,
    Rat.order.sgnQ.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Real.REq.unfold,
    Real.RSeq.unfold,
    Real.Real.unfold,
    Real.Regular.unfold,
    Real.qInvNat.eq,
    Real.rBound.eq,
    Real.abs.absSeq.eq,
    Real.abs.rAbs.eq,
    Real.abs.realAbs.eq,
    Real.abs.realAbs.unfold,
    Real.neg.negSeq.eq,
    Real.neg.rNeg.eq,
    Real.neg.realNeg.eq,
    Real.neg.realNeg.unfold,
    Real.neg.seqOf.eq,
    Real.order.≤.eq,
    Real.order.≤.unfold,
    Real.order.RLeP.eq)
leRNegAbsSelf =
  λu. quot-elim
    x. rleOf
      rNeg (rAbs x)
      x
      λn. leQTrans
        qNeg (qAbs (seqOf x n)) + qNeg (seqOf x n)
        _
        _
        leQSubZero (bndAbs (seqOf x n) .π₁)
        leQZeroBound n n
    u

-- ...so a vanishing absolute value names zero
realAbsZeroInv : (u : Real) → (realAbs u ≡ realZero) → u ≡ realZero
realAbsZeroInv =
  λu h. leRAntisym
    transportP (λw. u ≤ w) h leRAbsSelf
    transportP
      λw. w ≤ u
      trans _ _ _ (cong (λw. Real) (λw. realNeg w) h) realNegZero
      leRNegAbsSelf

-- ===== the distance =====
realDist : Real → Real → Real using (Real.Real.unfold)
realDist = λu v. realAbs (u - v)

-- THE BRIDGE. d on classes IS the representative-level |p − q|, and
-- naming it once is what keeps its users cheap.
--
-- Without this, a proof that states its goal at the ℝ level while
-- working at the representative level asks the kernel to see through
-- realDist → realSub → realAdd/realNeg → rAdd/rNeg → addSeq/negSeq →
-- qAdd/qNeg → mkRat → … inside a SINGLE type conversion, and the
-- licensed join has to redo that at every use. Here each layer is one
-- named lemma — realNegCls, realAddCls, realAbsCls — so the deep walk
-- happens once, at a statement small enough to be cheap.
realDistCls : (p q : RSeq) → realDist (class p) (class q) ≡ class (rAbs (rAdd p (rNeg q)))
  using (Real.metric.realDist.eq,
    Real.group.-.eq,
    Real.Real.unfold,
    Real.RSeq.unfold,
    Real.Regular.unfold)
realDistCls =
  λp q. trans
    realAbs (class p + realNeg (class q))
    _
    _
    cong (λw. Real) (λw. realAbs (class p + w)) {realNeg (class q)} {class (rNeg q)} realNegCls
    trans
      _
      _
      class (rAbs (rAdd p (rNeg q)))
      cong (λw. Real) (λw. realAbs w) (realAddCls p (rNeg q))
      realAbsCls

-- THE SECOND BRIDGE, for the element side. rleOf's argument type
-- mentions seqOf of the whole |p − q| construction, so supplying it
-- directly makes the kernel walk rAbs → rAdd/rNeg → absSeq/addSeq/
-- negSeq → seqOf at every use. Here that walk happens once, with p, q
-- and the bound ABSTRACT (D-3), and callers hand over a statement in
-- which no construction appears at all.
rleOfAbsSub : {p : RSeq}
  (q : RSeq)
  {b : Q}
  → ((j : ℕ) → qAbs (seqOf p (dbl j) + qNeg (seqOf q (dbl j))) ≤ b + rBound j j)
    → RLeP (rAbs (rAdd p (rNeg q))) ((λk. b), constReg)
  using (Real.RSeq.unfold,
    Real.Regular.unfold,
    Real.abs.rAbs.eq,
    Real.abs.absSeq.eq,
    Real.add.rAdd.eq,
    Real.add.addSeq.eq,
    Real.neg.rNeg.eq,
    Real.neg.negSeq.eq,
    Real.neg.seqOf.eq,
    Real.order.RLeP.eq)
rleOfAbsSub =
  λp q b f. rleOf _ _ (λj. leQSubShift (qAbs (seqOf p (dbl j) + qNeg (seqOf q (dbl j)))) b (f j))

realDistSelf : (u : Real) → realDist u u ≡ realZero
  using (Real.Real.unfold, Real.abs.realAbs.eq, Real.group.-.eq, Real.metric.realDist.eq)
realDistSelf =
  λu. trans _ _ _ (cong (λw. Real) (λw. realAbs w) {u - u} {realZero} realSubSelf) realAbsZero

realDistSym : (u v : Real) → realDist u v ≡ realDist v u
  using (Real.Real.unfold, Real.abs.realAbs.eq, Real.group.-.eq, Real.metric.realDist.eq)
realDistSym =
  λu v. trans
    _
    realAbs (realNeg (u - v))
    _
    sym _ _ (realAbsNeg (u - v))
    cong (λw. Real) (λw. realAbs w) {realNeg (u - v)} {v - u} realNegSub

leRZeroDist : (u v : Real) → realZero ≤ realDist u v
  using (Real.Real.unfold,
    Real.realOfQ.unfold,
    Real.realZero.eq,
    Real.realZero.unfold,
    Real.abs.realAbs.eq,
    Real.abs.realAbs.unfold,
    Real.add.+.unfold,
    Real.group.-.eq,
    Real.group.-.unfold,
    Real.metric.realDist.eq,
    Real.metric.realDist.unfold,
    Real.order.≤.eq,
    Real.order.≤.unfold)
leRZeroDist = λu v. leRZeroAbs (u - v)

-- identity of indiscernibles, via realAbsZeroInv and the group law
realDistZeroInv : (u v : Real) → (realDist u v ≡ realZero) → u ≡ v
  using (Real.Real.unfold, Real.abs.realAbs.eq, Real.group.-.eq, Real.metric.realDist.eq)
realDistZeroInv = λu v h. realSubZeroInv (realAbsZeroInv (u - v) h)

-- the triangle inequality: |·| adds along the three-term split
realDistTriangle : (u v w : Real) → realDist u w ≤ realDist u v + realDist v w
  using (Real.Real.unfold,
    Real.abs.realAbs.eq,
    Real.abs.realAbs.unfold,
    Real.add.+.eq,
    Real.add.+.unfold,
    Real.group.-.eq,
    Real.group.-.unfold,
    Real.metric.realDist.eq,
    Real.metric.realDist.unfold,
    Real.order.≤.unfold)
realDistTriangle =
  λu v w. transportP
    λt. t ≤ realAbs (u - v) + realAbs (v - w)
    {realAbs (u - v + (v - w))}
    {realDist u w}
    cong (λt. Real) (λt. realAbs t) {u - v + (v - w)} {u - w} realSubVia
    leRAbsTriangle