Real.mul

-- MULTIPLICATION on ℝ. Like addition it samples deeper than the index
-- asked for, but where addition's factor is the constant 2, the
-- product's is a BOUND on the two factors:
--
--   (x ⊗ y)_m = x_{φ m} · y_{φ m},   φ m + 1 = C·(m + 1),  C = A + B
--
-- with A, B the naturals Real/bound.nova computes for the two regular
-- sequences. The estimate is the classical one,
--
--   |x_a y_a − x_b y_b| ≤ |x_a|·|y_a − y_b| + |y_b|·|x_a − x_b|
--                       ≤ (A + B)·rBound a b
--
-- and C·rBound (φ m) (φ n) is rBound m n on the nose — the sampling
-- depth is chosen to make that an equality, exactly as qInvHalf makes
-- addition's an equality.
-- ===== the sampling index =====
-- φ with S (φ c m) = (c+1)·(m+1)

import Natural (+, *, plusZeroId, zeroPlusId, sucPlus, plusSucId, plusComm, sucMult, multComm)
import Int (Int, intOne)
import Int.mul (*, intMulOneL, intMulOneR)
import Int.order (intOfNat, intOfNatMul)
import Rat.frac (NZ, nzOne, nzPos, nzToInt, nzMul, nzMulOneL, Rat, mkRat)
import Rat (Q, qcls, +, *, qNeg, qZero, qOne, qAddComm, qAddAssoc, qMulComm, qMulCls, qDistribL, qDistribR, clsEqOfRel, RatR, ratMul)
import Rat.order (≤, leQRefl, qPairSwap, qSubSplit)
import Rat.bound (Bnd, bndAdd, bndEq, bndEqB, bndWeaken, bndVia)
import Rat.abs (bndMul, qNegMulR)
import Rat.nat (qOfNat, qOfNatAdd, leQOfNat)
import Rat.ceil (qNatBound)
import Rat.arch (bndOfArch)
import Real (qInvNat, rBound, leQZeroBound, Regular, RSeq, REq, Real, constReg, realOfQ)
import Real.neg (seqOf, regOf, regBnd, bndReg, reqOf, realEqOfREq)
import Real.seq (rseqEq, wdOuterOfComm, realEqOfSeqEq)
import Real.bound (seqBound, bndSeqBound, seqBoundPos)
import Core.equality (trans, sym, cong, transport, transportP)

mulIdx : ℕ → ℕ → ℕ
mulIdx = λc m. m + c * S m

sucMulIdx : (c m : ℕ) → S (mulIdx c m) ≡ S c * S m
  using (Natural.*.eq, Natural.+.eq, Real.mul.mulIdx.eq)
sucMulIdx =
  λc m. trans (S (m + c * S m)) _ _ (sym _ _ (sucPlus m (c * S m))) (sym _ _ (sucMult c (S m)))

-- (c+1) · 1/((c+1)(m+1)) = 1/(m+1) : cross-multiplication is the
-- successor identity above. Split into the two sides, because a
-- single nested term at this depth is unreadable and easy to
-- mis-parenthesise.
qMulIdxNum : {c m : ℕ} → intOfNat (S c) * intOne * nzToInt (nzPos m) ≡ intOfNat (S c * S m)
  using (Rat.half.nzPosInt)
qMulIdxNum =
  λc m. trans
    _
    intOfNat (S c) * intOfNat (S m)
    _
    cong (λv. Int) (λv. v * nzToInt (nzPos m)) (intMulOneR (intOfNat (S c)))
    intOfNatMul (S c) (S m)

qMulIdxDen : (c m : ℕ) → intOne * nzToInt (nzMul nzOne (nzPos (mulIdx c m))) ≡ intOfNat (S c * S m)
  using (Rat.half.nzPosInt)
qMulIdxDen =
  λc m. trans
    _
    _
    _
    trans
      _
      _
      intOfNat (S (mulIdx c m))
      intMulOneL (nzToInt (nzMul nzOne (nzPos (mulIdx c m))))
      cong
        λv. Int
        λv. nzToInt v
        {nzMul nzOne (nzPos (mulIdx c m))}
        {nzPos (mulIdx c m)}
        nzMulOneL
    cong (λu. Int) (λw. intOfNat w) (sucMulIdx c m)

qMulIdxRel : (c m : ℕ)
  → RatR
    ratMul (mkRat (intOfNat (S c)) nzOne) (mkRat intOne (nzPos (mulIdx c m)))
    mkRat intOne (nzPos m)
  using (Int.order.intOfNat.eq,
    Int.Int.eq,
    Int.intOne.eq,
    Int.mul.*.eq,
    Natural.*.eq,
    Natural.+.eq,
    Rat.frac.den.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.num.eq,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.frac.nzToInt.eq,
    Rat.RatR.eq,
    Rat.dInt.eq,
    Rat.ratMul.eq,
    Real.mul.mulIdx.eq)
qMulIdxRel =
  λc m. trans
    {Int}
    intOfNat (S c) * intOne * nzToInt (nzPos m)
    _
    _
    qMulIdxNum
    sym _ _ (qMulIdxDen c m)

qMulInvIdx : {c m : ℕ} → qOfNat (S c) * qInvNat (mulIdx c m) ≡ qInvNat m
  using (Int.order.intOfNat.eq,
    Int.intOne.eq,
    Rat.nat.qOfNat.eq,
    Rat.frac.mkRat.eq,
    Rat.frac.nzOne.eq,
    Rat.frac.nzPos.eq,
    Rat.*.eq,
    Rat.qcls.eq,
    Rat.ratMul.eq,
    Real.qInvNat.eq,
    Real.mul.mulIdx.eq)
qMulInvIdx =
  λc m. trans
    _
    qcls (ratMul (mkRat (intOfNat (S c)) nzOne) (mkRat intOne (nzPos (mulIdx c m))))
    _
    qMulCls (mkRat (intOfNat (S c)) nzOne) (mkRat intOne (nzPos (mulIdx c m)))
    clsEqOfRel _ _ (qMulIdxRel c m)

-- the same, with the factor given as a natural and its successor
-- shape as an explicit equation. Without this the elaborator has to
-- CONVERT `qOfNat (S (mulPred p q))` to `qOfNat (seqBound p + seqBound q)`
-- at every use, and those terms unfold through divN's fuel recursion:
-- the item stops finishing. As an argument the equation is proved once,
-- generically, where every symbol is a variable.
qMulInvIdxC : {C c m : ℕ} → (C ≡ S c) → qOfNat C * qInvNat (mulIdx c m) ≡ qInvNat m
qMulInvIdxC =
  λC c m h. transportP (λw. qOfNat w * qInvNat (mulIdx c m) ≡ qInvNat m) (sym _ _ h) qMulInvIdx

-- ...so the factor turns the deep bound into the shallow one exactly
qMulRBoundIdx : (c m n : ℕ) → qOfNat (S c) * rBound (mulIdx c m) (mulIdx c n) ≡ rBound m n
  using (Rat.+.eq, Real.qInvNat.eq, Real.rBound.eq, Real.mul.mulIdx.eq)
qMulRBoundIdx =
  λc m n. trans
    _
    _
    _
    qDistribL (qOfNat (S c)) (qInvNat (mulIdx c m)) (qInvNat (mulIdx c n))
    trans
      _
      _
      rBound m n
      cong
        λw. Q
        λw. w + qOfNat (S c) * qInvNat (mulIdx c n)
        {qOfNat (S c) * qInvNat (mulIdx c m)}
        {qInvNat m}
        qMulInvIdx
      cong (λw. Q) (λw. qInvNat m + w) {qOfNat (S c) * qInvNat (mulIdx c n)} {qInvNat n} qMulInvIdx

-- ===== the product-difference identity =====
qMulSubL : (x y y' : Q) → x * (y + qNeg y') ≡ x * y + qNeg (x * y')
qMulSubL =
  λx y y'. trans _ _ _ (qDistribL x y (qNeg y')) (cong (λw. Q) (λw. x * y + w) (qNegMulR x y'))

qMulSubR : {y' x x' : Q} → y' * (x + qNeg x') ≡ x * y' + qNeg (x' * y')
qMulSubR =
  λy' x x'. trans
    _
    _
    _
    qDistribL y' x (qNeg x')
    trans
      _
      _
      _
      cong (λw. Q) (λw. w + y' * qNeg x') (qMulComm y' x)
      cong
        λw. Q
        λw. x * y' + w
        trans _ _ _ (qNegMulR y' x') (cong (λw. Q) (λw. qNeg w) (qMulComm y' x'))

-- x·y − x′·y′ ≡ x·(y − y′) + y′·(x − x′)
qMulDiff : (x y x' y' : Q) → x * (y + qNeg y') + y' * (x + qNeg x') ≡ x * y + qNeg (x' * y')
qMulDiff =
  λx y x' y'. trans
    _
    _
    _
    trans
      _
      _
      _
      cong (λw. Q) (λw. w + y' * (x + qNeg x')) (qMulSubL x y y')
      cong
        λw. Q
        λw. x * y + qNeg (x * y') + w
        {y' * (x + qNeg x')}
        {x * y' + qNeg (x' * y')}
        qMulSubR
    qSubSplit (x' * y') (x * y') (x * y)

-- ===== the factor and the sequence =====
-- C − 1, written so that S (mulPred p q) IS seqBound p + seqBound q
mulPred : RSeq → RSeq → ℕ
mulPred = λp q. seqBound p + S (qNatBound (seqOf q Z))

mulSeq : RSeq → RSeq → ℕ → Q
mulSeq = λp q m. seqOf p (mulIdx (mulPred p q) m) * seqOf q (mulIdx (mulPred p q) m)

qMulSumBound : (A B : ℕ) (r : Q) → qOfNat A * r + qOfNat B * r ≡ qOfNat (A + B) * r
qMulSumBound =
  λA B r. sym
    _
    _
    trans
      _
      _
      _
      cong (λw. Q) (λw. w * r) (sym _ _ (qOfNatAdd A B))
      qDistribR r (qOfNat A) (qOfNat B)

-- PRODUCTS OF CLOSE, BOUNDED RATIONALS ARE CLOSE. Everything the ring
-- laws need about multiplication factors through this one estimate:
-- if |x| ≤ A, |y'| ≤ B, and both |y − y'| and |x − x'| are under d,
-- then |xy − x'y'| is under (A + B)·d. The modulus d is arbitrary —
-- it is rBound a b for regularity, but the ring laws need it to be a
-- multiple of rBound m m instead.
-- ...with the two differences allowed DIFFERENT moduli and the two
-- bounds arbitrary rationals. Associativity needs both: the bound on
-- the left factor is a product of two ceilings, and the left
-- difference is itself a product-difference, so it carries a bigger
-- modulus than the right one.
bndMulSubQ : {x y x' y' a b d e : Q}
  → Bnd a x
    → Bnd b y'
      → Bnd d (y + qNeg y')
        → Bnd e (x + qNeg x')
          → qZero ≤ a
            → qZero ≤ b → qZero ≤ d → qZero ≤ e → Bnd (a * d + b * e) (x * y + qNeg (x' * y'))
bndMulSubQ =
  λx y x' y' a b d e hx hy' hd he ha hb hd0 he0. bndEq
    _
    _
    qMulDiff x y x' y'
    bndAdd (bndMul ha hd0 hx hd) (bndMul hb he0 hy' he)

bndMulSub : {x y x' y' : Q}
  {A B : ℕ}
  {d : Q}
  → Bnd (qOfNat A) x
    → Bnd (qOfNat B) y'
      → Bnd d (y + qNeg y')
        → Bnd d (x + qNeg x')
          → qZero ≤ qOfNat A
            → qZero ≤ qOfNat B → qZero ≤ d → Bnd (qOfNat (A + B) * d) (x * y + qNeg (x' * y'))
bndMulSub =
  λx y x' y' A B d hx hy' hg hf hA hB hd. bndEqB
    _
    _
    _
    qMulSumBound A B d
    bndMulSubQ hx hy' hg hf hA hB hd hd

-- the estimate, at two arbitrary indices and with EVERYTHING abstract:
-- |x_a y_a − x_b y_b| ≤ (A + B)·rBound a b. Abstract because `seqBound`
-- unfolds through divN's fuel recursion, and an item that mentions it
-- twenty times does not finish elaborating (D-3, for speed).
bndMulDiffGen : (f g : ℕ → Q)
  (A B a b : ℕ)
  → Bnd (qOfNat A) (f a)
    → Bnd (qOfNat B) (g b)
      → Bnd (rBound a b) (g a + qNeg (g b))
        → Bnd (rBound a b) (f a + qNeg (f b))
          → qZero ≤ qOfNat A
            → qZero ≤ qOfNat B → Bnd (qOfNat (A + B) * rBound a b) (f a * g a + qNeg (f b * g b))
bndMulDiffGen = λf g A B a b hfa hgb hg hf hA hB. bndMulSub hfa hgb hg hf hA hB (leQZeroBound a b)

bndMulDiff : (p q : RSeq)
  (a b : ℕ)
  → Bnd
    qOfNat (seqBound p + seqBound q) * rBound a b
    seqOf p a * seqOf q a + qNeg (seqOf p b * seqOf q b)
bndMulDiff =
  λp q a b. bndMulDiffGen
    seqOf p
    seqOf q
    _
    _
    _
    _
    bndSeqBound p a
    bndSeqBound q b
    regBnd _ (regOf q) a b
    regBnd _ (regOf p) a b
    seqBoundPos
    seqBoundPos

-- ...and at the product's own sampling indices the factor cancels
mulReg : {p q : RSeq} → Regular (mulSeq p q)
  using (Natural.+.eq,
    Rat.nat.qOfNat.eq,
    Rat.+.eq,
    Rat.*.eq,
    Rat.qNeg.eq,
    Real.rBound.eq,
    Real.bound.seqBound.eq,
    Real.mul.mulIdx.eq,
    Real.mul.mulPred.eq,
    Real.mul.mulSeq.eq,
    Real.neg.seqOf.eq)
mulReg =
  λp q. bndReg
    λm n. bndEqB
      qOfNat (seqBound p + seqBound q) * rBound (mulIdx (mulPred p q) m) (mulIdx (mulPred p q) n)
      rBound m n
      seqOf p (mulIdx (mulPred p q) m) * seqOf q (mulIdx (mulPred p q) m)
        + qNeg (seqOf p (mulIdx (mulPred p q) n) * seqOf q (mulIdx (mulPred p q) n))
      qMulRBoundIdx (mulPred p q) m n
      bndMulDiff p q (mulIdx (mulPred p q) m) (mulIdx (mulPred p q) n)

rMul : RSeq → RSeq → RSeq using (Real.RSeq.unfold)
rMul = λp q. mulSeq p q, mulReg

-- ===== well-definedness =====
--
-- Two representatives of the same real get DIFFERENT sampling depths
-- (the bound is computed from the representative), so the two products
-- cannot be compared index by index. The comparison runs through a
-- third, deeper index j and the slack — everything proportional to
-- 1/(j+1) — is driven below every 1/(k+1) by ratArch's leQOfArch,
-- exactly as REq's transitivity was.
-- (a + p) + (r + (s + a)) ≡ (a + a) + (p + (r + s))
qRearr5 : (a p r s : Q) → a + p + (r + (s + a)) ≡ a + a + (p + (r + s))
qRearr5 =
  λa p r s. a + p + (r + (s + a))
    ≡⟨ cong (λw. Q) (λw. a + p + w) (sym _ _ (qAddAssoc r s a)) ⟩ a + p + (r + s + a)
    ≡⟨ cong (λw. Q) (λw. a + p + w) (qAddComm (r + s) a) ⟩ a + p + (a + (r + s))
    ≡⟨ qPairSwap a p a (r + s) ⟩ a + a + (p + (r + s))

-- C·t + ((A·t + A·t) + C″·t) ≡ (C + ((A + A) + C″))·t
qTailSum : {C A D : ℕ}
  {t : Q}
  → qOfNat C * t + (qOfNat A * t + qOfNat A * t + qOfNat D * t) ≡ qOfNat (C + (A + A + D)) * t
qTailSum =
  λC A D t. trans
    _
    _
    _
    cong
      λw. Q
      λw. qOfNat C * t + w
      trans
        _
        _
        _
        cong (λw. Q) (λw. w + qOfNat D * t) (qMulSumBound A A t)
        qMulSumBound (A + A) D t
    qMulSumBound C (A + A + D) t

-- the bound arithmetic of the three-leg comparison, stated abstractly:
-- two of the three factors collapse against the shallow index, and the
-- rest is one multiple of the deep unit fraction
wdBoundEq : {C A E n a b t k : ℕ}
  → (qOfNat C * qInvNat a ≡ qInvNat n)
    → (qOfNat E * qInvNat b ≡ qInvNat n)
      → (qOfNat (C + (A + A + E)) * qInvNat t ≡ qInvNat k)
        → qOfNat C * rBound a t + (qOfNat A * rBound t t + qOfNat E * rBound t b)
          ≡ rBound n n + qInvNat k
  using (Rat.nat.qOfNat.eq, Rat.+.eq, Rat.*.eq, Real.qInvNat.eq, Real.rBound.eq)
wdBoundEq =
  λC A E n a b t k h1 h2 h3. trans
    _
    _
    _
    trans
      _
      _
      _
      cong
        λw. Q
        λw. w + (qOfNat A * rBound t t + qOfNat E * rBound t b)
        trans
          qOfNat C * rBound a t
          _
          _
          qDistribL (qOfNat C) (qInvNat a) (qInvNat t)
          cong (λw. Q) (λw. w + qOfNat C * qInvNat t) h1
      trans
        _
        _
        _
        cong
          λw. Q
          λw. qInvNat n + qOfNat C * qInvNat t + (w + qOfNat E * rBound t b)
          {qOfNat A * rBound t t}
          {qOfNat A * qInvNat t + qOfNat A * qInvNat t}
          qDistribL (qOfNat A) (qInvNat t) (qInvNat t)
        cong
          λw. Q
          λw. qInvNat n + qOfNat C * qInvNat t + (qOfNat A * qInvNat t + qOfNat A * qInvNat t + w)
          trans
            qOfNat E * rBound t b
            _
            _
            qDistribL (qOfNat E) (qInvNat t) (qInvNat b)
            cong (λw. Q) (λw. qOfNat E * qInvNat t + w) h2
    trans
      _
      _
      rBound n n + qInvNat k
      qRearr5
        qInvNat n
        qOfNat C * qInvNat t
        qOfNat A * qInvNat t + qOfNat A * qInvNat t
        qOfNat E * qInvNat t
      cong
        λw. Q
        λw. rBound n n + w
        trans
          qOfNat C * qInvNat t
            + (qOfNat A * qInvNat t + qOfNat A * qInvNat t + qOfNat E * qInvNat t)
          _
          _
          qTailSum
          h3

-- the deep index: its factor is everything the three legs spend
wdIdx : RSeq → RSeq → RSeq → ℕ
wdIdx = λp q q'. seqBound p + seqBound q + (seqBound p + seqBound p + mulPred p q')

-- The three-leg comparison, abstract in the sequences, their bounds
-- and every index. Two representatives of the same real get different
-- sampling depths, so the two products are compared through a third,
-- deeper index t, and everything proportional to 1/(t+1) is the slack.
rMulWDGen : (f g g' : ℕ → Q)
  (A B B' : ℕ)
  (hfB : (j : ℕ) → Bnd (qOfNat A) (f j))
  (hgB : (j : ℕ) → Bnd (qOfNat B) (g j))
  (hg'B : (j : ℕ) → Bnd (qOfNat B') (g' j))
  (hfR : (i j : ℕ) → Bnd (rBound i j) (f i + qNeg (f j)))
  (hgR : (i j : ℕ) → Bnd (rBound i j) (g i + qNeg (g j)))
  (hg'R : (i j : ℕ) → Bnd (rBound i j) (g' i + qNeg (g' j)))
  (hq : (j : ℕ) → Bnd (rBound j j) (g j + qNeg (g' j)))
  (hA : qZero ≤ qOfNat A)
  (hB : qZero ≤ qOfNat B)
  (hB' : qZero ≤ qOfNat B')
  (n k a b t : ℕ)
  → (qOfNat (A + B) * qInvNat a ≡ qInvNat n)
    → (qOfNat (A + B') * qInvNat b ≡ qInvNat n)
      → (qOfNat (A + B + (A + A + (A + B'))) * qInvNat t ≡ qInvNat k)
        → Bnd (rBound n n + qInvNat k) (f a * g a + qNeg (f b * g' b))
rMulWDGen =
  λf g g' A B B' hfB hgB hg'B hfR hgR hg'R hq hA hB hB' n k a b t h1 h2 h3. bndEqB
    _
    _
    _
    wdBoundEq h1 h2 h3
    bndVia
      _
      _
      _
      _
      _
      bndMulDiffGen f g _ _ _ _ (hfB a) (hgB t) (hgR a t) (hfR a t) hA hB
      bndVia
        _
        _
        _
        _
        _
        bndEq _ _ (qMulSubL (f t) (g t) (g' t)) (bndMul hA (leQZeroBound t t) (hfB t) (hq t))
        bndMulDiffGen f g' _ _ _ _ (hfB t) (hg'B b) (hg'R t b) (hfR t b) hA hB'

-- the two successor identities the factors satisfy, each definitional
facEqPair : (p q : RSeq) → seqBound p + seqBound q ≡ S (mulPred p q)
  using (Natural.+.eq, Real.bound.seqBound.eq, Real.mul.mulPred.eq)
facEqPair = λp q. ⋆

facEqDeep : (p q q' : RSeq)
  → seqBound p + seqBound q + (seqBound p + seqBound p + (seqBound p + seqBound q'))
    ≡ S (wdIdx p q q')
  using (Natural.+.eq,
    Rat.ceil.qNatBound.eq,
    Real.bound.seqBound.eq,
    Real.mul.mulPred.eq,
    Real.mul.wdIdx.eq,
    Real.neg.seqOf.eq)
facEqDeep = λp q q'. ⋆

rMulWDStep : (p q q' : RSeq)
  (hq : (j : ℕ) → Bnd (rBound j j) (seqOf q j + qNeg (seqOf q' j)))
  (n k : ℕ)
  → Bnd (rBound n n + qInvNat k) (mulSeq p q n + qNeg (mulSeq p q' n))
  using (Rat.+.eq,
    Rat.*.eq,
    Rat.qNeg.eq,
    Real.mul.mulIdx.eq,
    Real.mul.mulPred.eq,
    Real.mul.mulSeq.eq,
    Real.neg.seqOf.eq)
rMulWDStep =
  λp q q' hq n k. rMulWDGen
    seqOf p
    seqOf q
    seqOf q'
    seqBound p
    seqBound q
    seqBound q'
    bndSeqBound p
    bndSeqBound q
    bndSeqBound q'
    regBnd _ (regOf p)
    regBnd _ (regOf q)
    regBnd _ (regOf q')
    hq
    seqBoundPos
    seqBoundPos
    seqBoundPos
    n
    k
    mulIdx (mulPred p q) n
    mulIdx (mulPred p q') n
    mulIdx (wdIdx p q q') k
    qMulInvIdxC (facEqPair p q)
    qMulInvIdxC (facEqPair p q')
    qMulInvIdxC (facEqDeep p q q')

rMulWDInner : (p : RSeq) {q q' : RSeq} → REq q q' → REq (rMul p q) (rMul p q')
  using (Rat.bound.Bnd.eq,
    Rat.order.≤.eq,
    Rat.+.eq,
    Rat.qNeg.eq,
    Real.REq.unfold,
    Real.rBound.eq,
    Real.mul.mulSeq.eq,
    Real.mul.rMul.eq,
    Real.neg.seqOf.eq)
rMulWDInner =
  λp q q' h. squash-elim
    h
    u. reqOf _ _ (λn. bndOfArch (mulSeq p q n + qNeg (mulSeq p q' n)) (λk. rMulWDStep p _ _ u n k))

-- ===== the descent =====
--
-- Under the strict engine this is the ordinary quot-elim descent, the
-- same shape realAdd uses, and the whole module elaborates in ~2 s.
-- It was NOT ordinary under the old engine. There, every type
-- mentioning `rMul p q` normalised both mulReg's proof term and
-- seqBound's unfolding through divN's fuel recursion, and these items
-- cost 3.5 minutes (rMulWDInnerCls), >6 minutes (rMulComm) and, for
-- the descent itself, more than ten — the module shipped without them.
-- Naming the δ is what made them cheap: with the unfolds licensed
-- rather than ambient, conversion only walks what is cited. B-16 in
-- docs/ProvingFeedback.md has the before/after.
--
-- One item still had to be reshaped rather than licensed: rMulComm's
-- pointwise step goes through `mulSeqCommAt`, abstract in both
-- sequences and both depths. Written inline it is 8.5 s even under the
-- strict engine, because the cong motive puts the two ceilings in the
-- conversion; abstracted, it is free and the call site cites three
-- unfolds. D-3 still earns its keep.
rMulWDInnerCls : (p q q' : RSeq) (h : REq q q') → class (rMul p q) ≡ class (rMul p q') ∈ Real
  using (Real.REq.unfold, Real.RSeq.unfold, Real.Real.unfold)
rMulWDInnerCls = λp q q' h. realEqOfREq _ _ (rMulWDInner p h)

-- ===== the sampling depth is symmetric =====
--
-- `mulPred p q` is seqBound p + S (qNatBound (seqOf q Z)) and seqBound
-- is S (S (qNatBound ·)), so both depths are a + b + 3 — but only up
-- to plusComm, not on the nose. Proved once at two naturals, so the
-- ceilings never have to be looked at.
ssAddComm : {a b : ℕ} → S (S a) + S b ≡ S (S b) + S a
ssAddComm =
  λa b. S (S a) + S b
    ≡⟨ sucPlus (S a) (S b) ⟩ S (S a + S b)
    ≡⟨ cong (λw. ℕ) (λw. S w) (sucPlus a (S b)) ⟩ S (S (a + S b))
    ≡⟨ cong (λw. ℕ) (λw. S (S w)) (plusSucId a b) ⟩ S (S (S (a + b)))
    ≡⟨ cong (λw. ℕ) (λw. S (S (S w))) (plusComm b a) ⟩ S (S (S (b + a)))
    ≡⟨ sym _ _ (cong (λw. ℕ) (λw. S (S w)) (plusSucId b a)) ⟩ S (S (b + S a))
    ≡⟨ sym _ _ (cong (λw. ℕ) (λw. S w) (sucPlus b (S a))) ⟩ S (S b + S a)
    ≡⟨ sym _ _ (sucPlus (S b) (S a)) ⟩ S (S b) + S a

mulPredComm : {p q : RSeq} → mulPred p q ≡ mulPred q p
  using (Real.bound.seqBound.eq, Real.mul.mulPred.eq)
mulPredComm = λp q. ssAddComm

-- the pointwise step, at abstract sequences and abstract depths: the
-- two products differ by qMulComm and by the depth, and the depth
-- difference is an argument. Keeping it abstract is what keeps the
-- ceilings out of the conversion (D-3).
mulSeqCommAt : (f g : ℕ → Q)
  (c d n : ℕ)
  → (c ≡ d) → f (mulIdx c n) * g (mulIdx c n) ≡ g (mulIdx d n) * f (mulIdx d n)
mulSeqCommAt =
  λf g c d n h. f (mulIdx c n) * g (mulIdx c n)
    ≡⟨ qMulComm (f (mulIdx c n)) (g (mulIdx c n)) ⟩ g (mulIdx c n) * f (mulIdx c n)
    ≡⟨ cong (λw. Q) (λw. g (mulIdx w n) * f (mulIdx w n)) h ⟩ g (mulIdx d n) * f (mulIdx d n)

-- ...and hence the product itself commutes ON REPRESENTATIVES: the two
-- sequences are pointwise equal, which rseqEq lifts to RSeq because
-- RSeq is a set
rMulComm : {x y : RSeq} → rMul x y ≡ rMul y x
  using (Real.mul.mulSeq.eq, Real.mul.rMul.eq, Real.neg.seqOf.eq)
rMulComm =
  λx y. rseqEq (λn. mulSeqCommAt (seqOf x) (seqOf y) (mulPred x y) (mulPred y x) n mulPredComm)

-- outer well-definedness, spent in one line against commutativity
rMulWDOuterCls : {x x' c : RSeq} (h : REq x x') → class (rMul x c) ≡ class (rMul x' c) ∈ Real
  using (Real.REq.unfold, Real.RSeq.unfold, Real.Real.unfold)
rMulWDOuterCls = wdOuterOfComm rMul (rMulComm {}) rMulWDInnerCls

rMulWDOuter : (x x' : RSeq)
  (h : REq x x')
  (v : Real)
  → quot-elim (w. Real) (q. class (rMul x q)) v ≡ quot-elim (q. class (rMul x' q)) v
  using (rMulWDInnerCls, Real.REq.unfold, Real.RSeq.unfold, Real.Real.unfold, Real.Regular.unfold)
rMulWDOuter =
  λx x' h v. quot-elim
    w. quot-elim (z. Real) (q. class (rMul x q)) w ≡ quot-elim (q. class (rMul x' q)) w
    c. rMulWDOuterCls h
    v

-- ===== multiplication on ℝ =====
infixl 7 *
* : Real → Real → Real
  using (rMulWDInnerCls,
    rMulWDOuter,
    Real.REq.unfold,
    Real.RSeq.unfold,
    Real.Real.unfold,
    Real.Regular.unfold)
(*) = λu v. quot-elim (p. quot-elim (q. class (rMul p q)) v) u

realMulCls : {x : RSeq} (y : RSeq) → class x * class y ≡ class (rMul x y)
  using (Real.RSeq.unfold, Real.Real.unfold, Real.Regular.unfold, Real.mul.rMul.eq, Real.mul.*.eq)
realMulCls = λx y. ⋆

realMulComm : (u v : Real) → u * v ≡ v * u
  using (Real.REq.unfold, Real.RSeq.unfold, Real.Real.unfold, Real.Regular.unfold, Real.mul.*.eq)
realMulComm =
  λu v. quot-elim
    p. quot-elim (q. cong (λw. Real) (λw. class w) {rMul p q} {rMul q p} rMulComm) v
    u

-- the embedding of ℚ is a homomorphism: both products are the constant
-- sequence at a·b, at every sampling depth
realMulOfQ : (a b : Q) → realOfQ a * realOfQ b ≡ realOfQ (a * b)
  using (Rat.Q.unfold,
    Real.RSeq.unfold,
    Real.Real.unfold,
    Real.constReg.eq,
    Real.realOfQ.eq,
    Real.mul.mulSeq.eq,
    Real.mul.rMul.eq,
    Real.mul.*.eq,
    Real.neg.seqOf.eq)
realMulOfQ =
  λa b. realEqOfSeqEq (rMul ((λn. a), constReg) ((λn. b), constReg)) ((λn. a * b), constReg) (λn. ⋆)