Int.mul

-- Multiplication of integers as difference pairs:
--   (a₁,a₂) · (b₁,b₂) = (a₁b₁ + a₂b₂, a₁b₂ + a₂b₁)
-- Unlike addition, both well-definedness obligations need real work:
-- the cross-sum identity has to be regrouped by DISTRIBUTIVITY before
-- the relatedness hypothesis can fire.
-- ===== nat lemmas, in the orientation the engine can use =====
--
-- Rewriting is oriented and size-decreasing, so Natural.nova's
-- distributivity — stated in the size-INCREASING direction — never
-- fires as a rewrite rule. Its flips do; each is proved by ⋆, the
-- original firing by whole-equation match on the flipped goal.

import Natural (+, *, plusZeroId, plusSucId, zeroPlusId, sucPlus, plusComm, plusAssoc, swapLeft, multZeroId, multSucId, zeroMult, sucMult, multComm, multDistrib, multAssoc)
import Int (Int, intZero, intOne, intNeg)
import Int.add (+, intAddComm, intAddAssoc)
import Core.equality (trans, cong, sym, paireta)

distribBack : {n m k : ℕ} → n * m + n * k ≡ n * (m + k) using (multDistrib)
distribBack = λn m k. ⋆

-- right distributivity: Natural.nova has only the left law, so this is
-- multComm on each factor, distribBack in the middle, multComm back
distribBackR : (m k n : ℕ) → m * n + k * n ≡ (m + k) * n using (distribBack)
distribBackR =
  λm k n. trans
    _
    _
    _
    trans
      _
      _
      _
      cong (λu. ℕ) (λw. w + k * n) (multComm n m)
      cong (λu. ℕ) (λw. n * m + w) (multComm n k)
    trans (n * m + n * k) _ _ distribBack (multComm (m + k) n)

-- the two exchanges of a four-term sum
swap4 : (p q r s : ℕ) → p + q + (r + s) ≡ p + r + (q + s)
  using (hyp.rw,
    Natural.swapMid,
    Natural.swapMid.rw,
    plusAssoc,
    plusAssoc.rw,
    swapLeft,
    swapLeft.rw)
swap4 = λp q r s. ⋆

swap4b : {p q r s : ℕ} → p + q + (r + s) ≡ p + s + (q + r)
  using (Int.add.intAddCross, swap4, plusAssoc)
swap4b =
  λp q r s. p + q + (r + s) ≡⟨ plusComm s r ⟩ p + q + (s + r) ≡⟨ swap4 p q s r ⟩ p + s + (q + r)

-- congruence of + in each argument: with h reflected the two sides
-- are judgemental, so each is one ⋆ (and unlike a rewrite step, a
-- lemma application is unconstrained by the position it lands in)
plusCongL : {x y z : ℕ} → (x ≡ y) → x + z ≡ y + z using (hyp.rw)
plusCongL = λx y z h. ⋆

plusCongR : {x y z : ℕ} → (y ≡ z) → x + y ≡ x + z
plusCongR = λx y z h. ⋆

-- x*y*z + x*u*v ≡ x*(y*z + u*v): reassociate both products, then
-- collect the common left factor
collectL : (x y z u v : ℕ) → x * y * z + x * u * v ≡ x * (y * z + u * v)
  using (distribBack, multAssoc)
collectL =
  λx y z u v. trans
    _
    _
    _
    trans
      {ℕ}
      x * y * z + x * u * v
      x * (y * z) + x * u * v
      x * (y * z) + x * (u * v)
      plusCongL (multAssoc x y z)
      plusCongR (multAssoc x u v)
    distribBack

-- the representative-level associativity identity, one component of
-- it; the other component is this one with c₁ and c₂ swapped.
-- A CALC CHAIN (docs/SearchlessElaboration.md §5.2): expand both
-- products by right distributivity, exchange the middle two summands,
-- then collect a₁ and a₂ back out — each link a named sub-equation,
-- its position and orientation found by the link-scoped engine (no
-- sym, no cong wrappers, no repeated midpoints)
assocRep : (a1 a2 b1 b2 c1 c2 : ℕ)
  → (a1 * b1 + a2 * b2) * c1 + (a1 * b2 + a2 * b1) * c2
    ≡ a1 * (b1 * c1 + b2 * c2) + a2 * (b1 * c2 + b2 * c1)
  using (hyp.rw)
assocRep =
  λa1 a2 b1 b2 c1 c2. (a1 * b1 + a2 * b2) * c1 + (a1 * b2 + a2 * b1) * c2
    ≡⟨ distribBackR (a1 * b1) (a2 * b2) c1 ⟩ a1 * b1 * c1 + a2 * b2 * c1 + (a1 * b2 + a2 * b1) * c2
    ≡⟨ distribBackR (a1 * b2) (a2 * b1) c2 ⟩
      a1 * b1 * c1 + a2 * b2 * c1 + (a1 * b2 * c2 + a2 * b1 * c2)
    ≡⟨ swap4 (a1 * b1 * c1) (a2 * b2 * c1) (a1 * b2 * c2) (a2 * b1 * c2) ⟩
      a1 * b1 * c1 + a1 * b2 * c2 + (a2 * b2 * c1 + a2 * b1 * c2)
    ≡⟨ collectL a1 b1 c1 b2 c2 ⟩ a1 * (b1 * c1 + b2 * c2) + (a2 * b2 * c1 + a2 * b1 * c2)
    ≡⟨ collectL a2 b2 c1 b1 c2 ⟩ a1 * (b1 * c1 + b2 * c2) + a2 * (b2 * c1 + b1 * c2)
    ≡⟨ plusComm (b1 * c2) (b2 * c1) ⟩ a1 * (b1 * c1 + b2 * c2) + a2 * (b1 * c2 + b2 * c1)

-- regroup a cross-sum by the LEFT factor: this is the shape the inner
-- well-definedness goal takes, and once regrouped the relatedness
-- hypothesis makes the two sides judgementally equal
sum4Distrib : (a1 a2 b1 b2 c1 c2 : ℕ)
  → a1 * b1 + a2 * b2 + (a1 * c2 + a2 * c1) ≡ a1 * (b1 + c2) + a2 * (b2 + c1)
  using (distribBack, plusAssoc)
sum4Distrib =
  λa1 a2 b1 b2 c1 c2. trans
    _
    _
    _
    swap4 (a1 * b1) (a2 * b2) (a1 * c2) (a2 * c1)
    trans
      _
      _
      _
      cong (λu. ℕ) (λw. w + (a2 * b2 + a2 * c1)) {a1 * b1 + a1 * c2} {a1 * (b1 + c2)} distribBack
      cong (λu. ℕ) (λw. a1 * (b1 + c2) + w) {a2 * b2 + a2 * c1} {a2 * (b2 + c1)} distribBack

-- and by the RIGHT factor: the shape of the OUTER well-definedness goal
sum4DistribR : (x1 x2 y1 y2 c1 c2 : ℕ)
  → x1 * c1 + x2 * c2 + (y1 * c2 + y2 * c1) ≡ (x1 + y2) * c1 + (x2 + y1) * c2
  using (distribBackR, plusAssoc)
sum4DistribR =
  λx1 x2 y1 y2 c1 c2. trans
    _
    _
    _
    swap4b
    trans
      _
      _
      _
      cong (λu. ℕ) (λw. w + (x2 * c2 + y1 * c2)) (distribBackR x1 y2 c1)
      cong (λu. ℕ) (λw. (x1 + y2) * c1 + w) (distribBackR x2 y1 c2)

-- ===== the two well-definedness lemmas =====
-- inner: y varies. Both sides regroup to a₁·t + a₂·t′ with t and t′
-- interchanged, and h makes t ≐ t′.
intMulWD : (a1 a2 b1 b2 c1 c2 : ℕ)
  (h : b1 + c2 ≡ b2 + c1)
  → a1 * b1 + a2 * b2 + (a1 * c2 + a2 * c1) ≡ a1 * b2 + a2 * b1 + (a1 * c1 + a2 * c2)
  using (distribBack, distribBackR, hyp.rw, plusAssoc, sum4Distrib)
intMulWD =
  λa1 a2 b1 b2 c1 c2 h. trans
    _
    _
    _
    sum4Distrib a1 a2 b1 b2 c1 c2
    sym _ _ (sum4Distrib a1 a2 b2 b1 c2 c1)

-- outer: x varies; the same regrouping, by the right factor
intMulWDRep : (a1 a2 b1 b2 c1 c2 : ℕ)
  (h : a1 + b2 ≡ a2 + b1)
  → a1 * c1 + a2 * c2 + (b1 * c2 + b2 * c1) ≡ a1 * c2 + a2 * c1 + (b1 * c1 + b2 * c2)
  using (distribBack, hyp.rw, plusAssoc, plusComm, sum4DistribR)
intMulWDRep =
  λa1 a2 b1 b2 c1 c2 h. trans
    _
    _
    _
    sum4DistribR a1 a2 b1 b2 c1 c2
    sym _ _ (sum4DistribR a1 a2 b1 b2 c2 c1)

-- the outer well-definedness, in the quot-elim shape the elaborator
-- actually asks for (Int/add.nova's intAddWDOuter, one level up):
-- eliminate the remaining argument and the goal becomes the nat
-- relation intMulWDRep proves
intMulWDOuter : (a b : ℕ × ℕ)
  (h : a .π₁ + b .π₂ ≡ a .π₂ + b .π₁)
  (zy : Int)
  → quot-elim (z. Int) (x. class (a .π₁ * x .π₁ + a .π₂ * x .π₂, a .π₁ * x .π₂ + a .π₂ * x .π₁)) zy
    ≡ quot-elim (x. class (b .π₁ * x .π₁ + b .π₂ * x .π₂, b .π₁ * x .π₂ + b .π₂ * x .π₁)) zy
  using (distribBack,
    distribBackR,
    Int.Int.unfold,
    Int.mul.intMulWD,
    Int.mul.intMulWDRep,
    multDistrib,
    plusAssoc,
    plusComm,
    sum4Distrib,
    sum4DistribR)
intMulWDOuter =
  λa b h zy. quot-elim
    q. quot-elim
      z. Int
      x. class (a .π₁ * x .π₁ + a .π₂ * x .π₂, a .π₁ * x .π₂ + a .π₂ * x .π₁)
      q
      ≡ quot-elim (x. class (b .π₁ * x .π₁ + b .π₂ * x .π₂, b .π₁ * x .π₂ + b .π₂ * x .π₁)) q
    c. ⋆
    zy

-- ===== multiplication =====
infixl 7 *
* : Int → Int → Int
  using (distribBackR, intMulWDOuter, Int.Int.unfold, Int.mul.intMulWD, plusAssoc, sum4Distrib)
(*) =
  λx y. quot-elim
    a. quot-elim (b. class (a .π₁ * b .π₁ + a .π₂ * b .π₂, a .π₁ * b .π₂ + a .π₂ * b .π₁)) y
    x

-- 2 · 3 = 6 and (−2) · 3 = −6
intMulTest1 : class (2, Z) * class (3, Z) ≡ class (6, Z)
  using (Int.Int.unfold, Int.mul.*.eq, Natural.*.eq, Natural.+.eq)
intMulTest1 = ⋆

intMulTest2 : class (Z, 2) * class (3, Z) ≡ class (Z, 6)
  using (Int.Int.unfold, Int.mul.*.eq, Natural.*.eq, Natural.+.eq)
intMulTest2 = ⋆

-- ===== the ring laws =====
classPairEta : (p : ℕ × ℕ) → class (p .π₁, p .π₂) ≡ class p ∈ Int using (Int.Int.unfold)
classPairEta = λp. cong (λu. Int) (λr. class r) (paireta p)

oneMult : (m : ℕ) → S Z * m ≡ m using (multComm)
oneMult = λm. S Z * m ≡⟨ sucMult Z m ⟩ m + Z * m ≡⟨ zeroMult m ⟩ m + Z ≡⟨ plusZeroId m ⟩ m

-- class (u₁,u₂) ≡ class (v₁,v₂) from the two component equations:
-- reflection makes the components judgemental, so this is one ⋆
classCong2 : {u1 u2 v1 v2 : ℕ} → (u1 ≡ v1) → (u2 ≡ v2) → class (u1, u2) ≡ class (v1, v2) ∈ Int
  using (hyp.rw, Int.Int.unfold)
classCong2 = λu1 u2 v1 v2 h1 h2. ⋆

-- multiplication by 1 on the LEFT does not compute (Natural.nova's * is
-- recursive in its SECOND argument), so oneMult/zeroMult have to fire
-- before Σ-η can close it; on the right it is all β (intMulOneR)
intMulOneL : (z : Int) → intOne * z ≡ z
  using (classPairEta,
    Int.Int.unfold,
    Int.intOne.eq,
    Int.mul.*.eq,
    oneMult,
    oneMult.rw,
    plusZeroId,
    plusZeroId.rw,
    zeroMult,
    zeroMult.rw)
intMulOneL = λz. quot-elim (p. trans (class (p .π₁, p .π₂)) _ _ ⋆ (classPairEta p)) z

intMulOneR : (z : Int) → z * intOne ≡ z
  using (classPairEta,
    Int.Int.unfold,
    Int.intOne.eq,
    Int.mul.*.eq,
    multSucId,
    multSucId.rw,
    multZeroId,
    multZeroId.rw,
    plusZeroId,
    plusZeroId.rw,
    zeroPlusId,
    zeroPlusId.rw)
intMulOneR = λz. quot-elim (p. classPairEta p) z

intMulZeroL : (z : Int) → intZero * z ≡ intZero
  using (distribBack,
    distribBack.rw,
    hyp.rw,
    Int.mul.*.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.intZero.eq,
    zeroMult,
    zeroMult.rw)
intMulZeroL = λz. quot-elim (p. ⋆) z

intMulZeroR : {z : Int} → z * intZero ≡ intZero using (Int.Int.unfold, Int.intZero.eq, Int.mul.*.eq)
intMulZeroR = λz. quot-elim (p. ⋆) z

-- u₁v₁ + u₂v₂ ≡ v₁u₁ + v₂u₂: multComm is permutative, so it never
-- rewrites — each factor has to be commuted by an explicit cong
mulComm2 : (u1 u2 v1 v2 : ℕ) → u1 * v1 + u2 * v2 ≡ v1 * u1 + v2 * u2
mulComm2 =
  λu1 u2 v1 v2. trans
    _
    _
    _
    cong (λw. ℕ) (λw. w + u2 * v2) (multComm v1 u1)
    cong (λw. ℕ) (λw. v1 * u1 + w) (multComm v2 u2)

intMulComm : (x y : Int) → x * y ≡ y * x using (Int.Int.unfold, Int.mul.*.eq, plusAssoc)
intMulComm =
  λx y. quot-elim
    a. quot-elim
      b. classCong2
        mulComm2 (a .π₁) (a .π₂) (b .π₁) (b .π₂)
        trans
          _
          _
          _
          mulComm2 (a .π₁) (a .π₂) (b .π₂) (b .π₁)
          plusComm (b .π₁ * a .π₂) (b .π₂ * a .π₁)
      y
    x

intMulAssoc : (x y z : Int) → x * y * z ≡ x * (y * z) using (assocRep, Int.Int.unfold, Int.mul.*.eq)
intMulAssoc =
  λx y z. quot-elim
    a. quot-elim
      b. quot-elim
        c. classCong2
          assocRep (a .π₁) (a .π₂) (b .π₁) (b .π₂) (c .π₁) (c .π₂)
          assocRep (a .π₁) (a .π₂) (b .π₁) (b .π₂) (c .π₂) (c .π₁)
        z
      y
    x

intMulDistribL : (x y z : Int) → x * (y + z) ≡ x * y + x * z
  using (hyp.rw,
    Int.mul.*.eq,
    Int.Int.eq,
    Int.Int.unfold,
    Int.add.+.eq,
    plusAssoc,
    plusAssoc.rw,
    sum4Distrib,
    sum4Distrib.rw)
intMulDistribL = λx y z. quot-elim (a. quot-elim (b. quot-elim (c. ⋆) z) y) x

-- congruence in both arguments, for building chains: reflection makes
-- the hypotheses judgemental, so each is one ⋆
intAddCong2 : (x y u v : Int) → (x ≡ u) → (y ≡ v) → x + y ≡ u + v using (hyp.rw, Int.Int.unfold)
intAddCong2 = λx y u v h1 h2. ⋆

intMulCong2 : (x y u v : Int) → (x ≡ u) → (y ≡ v) → x * y ≡ u * v using (hyp.rw, Int.Int.unfold)
intMulCong2 = λx y u v h1 h2. ⋆

-- distributivity on the right, from the left law by commuting thrice
intMulDistribR : (x y z : Int) → (x + y) * z ≡ x * z + y * z
intMulDistribR =
  λx y z. trans
    _
    _
    _
    trans _ _ _ (intMulComm (x + y) z) (intMulDistribL z x y)
    intAddCong2 _ _ _ _ (intMulComm z x) (intMulComm z y)

-- ===== negation =====
intNegNeg : (z : Int) → intNeg (intNeg z) ≡ z using (classPairEta, Int.Int.unfold, Int.intNeg.eq)
intNegNeg = λz. quot-elim (p. classPairEta p) z

-- z + (−z) = 0: on representatives the relation is p₁+p₂ ≡ p₂+p₁
intAddNegR : (z : Int) → z + intNeg z ≡ intZero
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intZero.eq,
    Int.zeroEq,
    Int.add.+.eq,
    plusComm,
    plusZeroId,
    plusZeroId.rw)
intAddNegR = λz. quot-elim (p. ⋆) z

intAddNegL : (z : Int) → intNeg z + z ≡ intZero
  using (Int.Int.unfold,
    Int.intNeg.eq,
    Int.intZero.eq,
    Int.zeroEq,
    Int.add.+.eq,
    plusComm,
    plusZeroId,
    plusZeroId.rw)
intAddNegL = λz. quot-elim (p. ⋆) z

-- (−x)·y = −(x·y): the two representatives differ by plusComm in each
-- component
intMulNegL : (x y : Int) → intNeg x * y ≡ intNeg (x * y)
  using (Int.Int.unfold, Int.intNeg.eq, Int.mul.*.eq)
intMulNegL =
  λx y. quot-elim
    a. quot-elim
      b. classCong2
        plusComm (a .π₁ * b .π₂) (a .π₂ * b .π₁)
        plusComm (a .π₁ * b .π₁) (a .π₂ * b .π₂)
      y
    x

intMulNegR : (x y : Int) → x * intNeg y ≡ intNeg (x * y) using (intMulNegL)
intMulNegR =
  λx y. trans
    _
    _
    _
    intMulComm x (intNeg y)
    trans _ _ _ (intMulNegL y x) (cong (λu. Int) intNeg (intMulComm y x))