Int.order

-- Order on ℤ, same shape as natOrder's LeN: the difference between
-- two integers in the right order is a NATURAL, so x ≤ y is a nat
-- witness k with an Id-proof that x + k closes the gap. No quot-elim
-- into 𝕌 is ever needed (𝕌-equality is structural, so a code family
-- BY REPRESENTATIVES has no well-definedness proof): the family is
-- built by COMPOSITION — intAdd, intOfNat, Id — and the one place
-- representatives must be touched (deciding the order) goes through
-- the honest function intCanon.

import Natural (+, *, plusComm, zeroPlusId, zeroMult)
import Natural.order (≤, leTotal, sumZeroL)
import Int (Int, intZero, intNeg)
import Int.add (+, intAddComm, intAddAssoc)
import Int.mul (*, intMulComm, intMulDistribL, intAddNegL, intAddNegR, intNegNeg, classPairEta)
import Rat.frac (intAddZeroL, intAddZeroR)
import Int.eq (intCanon, intCanonClass)
import Int.effective (intEffective)
import Core.equality (trans, sym, cong, transport)
import Core.id (Id, idToEq, eqToId)

intOfNat : ℕ → Int using (Int.Int.unfold)
intOfNat = λn. class (n, Z)

infixl 4 ≤
≤ : Int → Int → 𝕌
(≤) = λx y. (k : ℕ) × Id _ (x + intOfNat k) y

-- ===== glue: intOfNat is an order-embedding-ready map =====
intOfNatZero : intOfNat Z ≡ intZero using (Int.order.intOfNat.eq, Int.Int.unfold, Int.intZero.eq)
intOfNatZero = ⋆

intOfNatPlus : (a b : ℕ) → intOfNat a + intOfNat b ≡ intOfNat (a + b)
  using (Int.order.intOfNat.eq, Int.Int.unfold, Int.add.+.eq, Natural.+.eq)
intOfNatPlus = λa b. ⋆

intOfNatInjZ : {k : ℕ} → (intOfNat k ≡ intZero) → k ≡ Z
  using (hyp.rw,
    Int.order.intOfNat.eq,
    Int.IntR.unfold,
    Int.intZero.eq,
    Natural.plusZeroId,
    Natural.plusZeroId.rw)
intOfNatInjZ = λk h. let r = intEffective h in ⋆

-- x + ofNat (a + b) ≡ (x + ofNat a) + ofNat b, hypothesis-free
intOfNatSplit : {x : Int} {a b : ℕ} → x + intOfNat (a + b) ≡ x + intOfNat a + intOfNat b
  using (Int.Int.unfold)
intOfNatSplit =
  λx a b. x + intOfNat (a + b)
    ≡⟨ cong (λu. Int) (λu. x + u) (sym _ _ (intOfNatPlus a b)) ⟩ x + (intOfNat a + intOfNat b)
    ≡⟨ sym _ _ (intAddAssoc x (intOfNat a) (intOfNat b)) ⟩ x + intOfNat a + intOfNat b

-- ===== additive-group plumbing =====
intNegAdd : (z w : Int) → intNeg (z + w) ≡ intNeg z + intNeg w
  using (Int.Int.unfold, Int.intNeg.eq, Int.add.+.eq)
intNegAdd = λz w. quot-elim (p. quot-elim (q. ⋆) w) z

-- −x + (x + a) ≡ a, hypothesis-free
intNegPlusCancel : (x a : Int) → intNeg x + (x + a) ≡ a using (Int.Int.unfold)
intNegPlusCancel =
  λx a. intNeg x + (x + a)
    ≡⟨ sym _ _ (intAddAssoc (intNeg x) x a) ⟩ intNeg x + x + a
    ≡⟨ cong (λu. Int) (λu. u + a) (intAddNegL x) ⟩ intZero + a
    ≡⟨ intAddZeroL a ⟩ a

intCancelL : (x a b : Int) → (x + a ≡ x + b) → a ≡ b
intCancelL =
  λx a b h. trans
    _
    _
    _
    sym _ _ (intNegPlusCancel x a)
    trans _ _ _ (cong (λu. Int) (λu. intNeg x + u) h) (intNegPlusCancel x b)

-- x + (y − x) ≡ y, and y − (y − x) ≡ x: the two rearrangements the
-- order decision below hangs on
intPlusDiff : (x y : Int) → x + (y + intNeg x) ≡ y using (Int.Int.unfold)
intPlusDiff =
  λx y. x + (y + intNeg x)
    ≡⟨ cong (λu. Int) (λu. x + u) (intAddComm y (intNeg x)) ⟩ x + (intNeg x + y)
    ≡⟨ sym _ _ (intAddAssoc x (intNeg x) y) ⟩ x + intNeg x + y
    ≡⟨ cong (λu. Int) (λu. u + y) (intAddNegR x) ⟩ intZero + y
    ≡⟨ intAddZeroL y ⟩ y

intPlusNegDiff : (x y : Int) → y + intNeg (y + intNeg x) ≡ x using (Int.Int.unfold)
intPlusNegDiff =
  λx y. y + intNeg (y + intNeg x)
    ≡⟨ cong (λu. Int) (λu. y + u) (intNegAdd y (intNeg x)) ⟩ y + (intNeg y + intNeg (intNeg x))
    ≡⟨ cong (λu. Int) (λu. y + (intNeg y + u)) (intNegNeg x) ⟩ y + (intNeg y + x)
    ≡⟨ sym _ _ (intAddAssoc y (intNeg y) x) ⟩ y + intNeg y + x
    ≡⟨ cong (λu. Int) (λu. u + x) (intAddNegR y) ⟩ intZero + x
    ≡⟨ intAddZeroL x ⟩ x

-- ===== the order =====
leZRefl : (x : Int) → x ≤ x using (Int.order.≤.unfold, Int.order.intOfNatZero, Int.Int.unfold)
leZRefl = λx. Z, eqToId _ _ (intAddZeroR x)

leZOfEq : {x y : Int} → (x ≡ y) → x ≤ y
  using (Int.order.≤.unfold, Int.order.intOfNatZero, Int.Int.unfold)
leZOfEq = λx y h. Z, eqToId _ _ (trans (x + intOfNat Z) _ _ (intAddZeroR x) h)

leZTrans : {x : Int} (y : Int) {z : Int} → x ≤ y → y ≤ z → x ≤ z using (Int.order.≤.unfold)
leZTrans =
  λx y z l1 l2. (,)
    l1 .π₁ + l2 .π₁
    eqToId
      _
      _
      trans
        x + intOfNat (l1 .π₁ + l2 .π₁)
        _
        _
        intOfNatSplit
        trans
          _
          _
          _
          cong (λu. Int) (λu. u + intOfNat (l2 .π₁)) (idToEq _ _ _ (l1 .π₂))
          idToEq _ _ _ (l2 .π₂)

leZAntisym : (x y : Int) → x ≤ y → y ≤ x → x ≡ y using (Int.order.≤.unfold)
leZAntisym =
  λx y l1 l2. let h1 = idToEq _ _ _ (l1 .π₂)
                  h2 = idToEq _ _ _ (l2 .π₂)
                  loop : x + intOfNat (l1 .π₁ + l2 .π₁) ≡ x
                    = trans
                      _
                      _
                      _
                      intOfNatSplit
                      trans _ _ _ (cong (λu. Int) (λu. u + intOfNat (l2 .π₁)) h1) h2
                  sumz : intOfNat (l1 .π₁ + l2 .π₁) ≡ intZero
                    = intCancelL _ _ _ (trans _ _ _ loop (sym _ _ (intAddZeroR x)))
                  k1z = sumZeroL _ _ (intOfNatInjZ sumz)
                  trans
                    _
                    _
                    _
                    trans
                      _
                      _
                      _
                      sym _ _ (intAddZeroR x)
                      cong
                        λu. Int
                        λu. x + u
                        sym _ _ (trans _ _ _ (cong (λu. Int) (λu. intOfNat u) k1z) intOfNatZero)
                    h1

-- ===== monotonicity =====
-- the shuffle, HYPOTHESIS-FREE (an equation hypothesis in scope can
-- rewrite inside a stuck-scrutinee position of both chain sides at
-- once; such lockstep steps are unreplayable, so keep the shuffle in
-- a helper and use the hypothesis only through cong)
intAddShiftR : {x w v : Int} → x + w + v ≡ x + v + w using (Int.Int.unfold)
intAddShiftR =
  λx w v. x + w + v
    ≡⟨ intAddAssoc x w v ⟩ x + (w + v)
    ≡⟨ cong (λu. Int) (λu. x + u) (intAddComm w v) ⟩ x + (v + w)
    ≡⟨ sym _ _ (intAddAssoc x v w) ⟩ x + v + w

leZPlusMonoR : {x y : Int} (w : Int) → x ≤ y → x + w ≤ y + w using (Int.order.≤.unfold)
leZPlusMonoR =
  λx y w le. (,)
    le .π₁
    eqToId
      _
      _
      trans
        x + w + intOfNat (le .π₁)
        _
        _
        intAddShiftR
        cong (λu. Int) (λu. u + w) (idToEq _ _ _ (le .π₂))

leZPlusMonoL : (x y w : Int) → x ≤ y → w + x ≤ w + y using (Int.order.≤.unfold)
leZPlusMonoL =
  λx y w le. leZTrans
    _
    leZOfEq (intAddComm w x)
    leZTrans _ (leZPlusMonoR w le) (leZOfEq (intAddComm y w))

-- again the shuffle first, hypothesis-free
intNegAddCancel : {x v : Int} → intNeg (x + v) + v ≡ intNeg x using (Int.Int.unfold)
intNegAddCancel =
  λx v. intNeg (x + v) + v
    ≡⟨ cong (λu. Int) (λu. u + v) (intNegAdd x v) ⟩ intNeg x + intNeg v + v
    ≡⟨ intAddAssoc (intNeg x) (intNeg v) v ⟩ intNeg x + (intNeg v + v)
    ≡⟨ cong (λu. Int) (λu. intNeg x + u) (intAddNegL v) ⟩ intNeg x + intZero
    ≡⟨ intAddZeroR (intNeg x) ⟩ intNeg x

leZNegFlip : (x y : Int) → x ≤ y → intNeg y ≤ intNeg x using (Int.order.≤.unfold)
leZNegFlip =
  λx y le. (,)
    le .π₁
    eqToId
      _
      _
      trans
        _
        _
        intNeg x
        cong (λu. Int) (λu. intNeg u + intOfNat (le .π₁)) (sym _ _ (idToEq _ _ _ (le .π₂)))
        intNegAddCancel

-- ===== the ℕ bridge =====
leZOfNat : (a b : ℕ) → a ≤ b → intOfNat a ≤ intOfNat b
  using (Int.order.≤.unfold, Natural.order.≤.unfold)
leZOfNat =
  λa b le. (,)
    le .π₁
    eqToId
      _
      _
      trans
        _
        _
        _
        intOfNatPlus a (le .π₁)
        cong (λu. Int) (λu. intOfNat u) (idToEq _ _ _ (le .π₂))

-- ===== totality: decide by the canonical form of the difference =====
-- The class-equation legs, kept ABSTRACT in the pair components
-- (ProvingFeedback D-3): instantiated at intCanon's projections the
-- engine would match against the δ-UNFOLDED canon — a bare quot-elim
-- that proof-spine inference cannot type.
-- the represented relation behind clsOfRelGe's class equation, as its
-- own lemma: k + b ≡ Z + a from b + k ≡ a
sumSwapZL : (a b k : ℕ) → (b + k ≡ a) → k + b ≡ Z + a
sumSwapZL = λa b k h. k + b ≡⟨ plusComm b k ⟩ b + k ≡⟨ h ⟩ a ≡⟨ zeroPlusId a ⟩ Z + a

clsOfRelGe : (a b k : ℕ) → (b + k ≡ a) → class (k, Z) ≡ class (a, b) ∈ Int
  using (Int.Int.unfold, plusComm, sumSwapZL, zeroPlusId)
clsOfRelGe = λa b k h. ⋆

clsOfRelLe : (a b k : ℕ) → (a + k ≡ b) → class (k, Z) ≡ class (b, a) ∈ Int
  using (Int.order.clsOfRelGe, Int.Int.unfold, plusComm, zeroPlusId)
clsOfRelLe = λa b k h. ⋆

intNegClass : (p : ℕ × ℕ) → intNeg (class p) ≡ class (p .π₂, p .π₁)
  using (Int.Int.unfold, Int.intNeg.eq)
intNegClass = λp. ⋆

leZTotal : (x y : Int) → x ≤ y ⊎ y ≤ x
  using (Core.id.Id.unfold,
    Int.order.≤.unfold,
    Int.order.intOfNat.eq,
    Int.Int.unfold,
    Int.mul.intAddCong2,
    Natural.order.≤.unfold)
leZTotal =
  λx y. let d = y + intNeg x
            hd = intCanonClass d
            ⊎-elim
              nn. let hb = idToEq _ _ _ (nn .π₂)
                      e1 : intOfNat (nn .π₁) ≡ class (intCanon d)
                        = intOfNat (nn .π₁)
                          ≡⟨ clsOfRelGe _ _ _ hb ⟩ class (intCanon d .π₁, intCanon d .π₂)
                          ≡⟨ classPairEta (intCanon d) ⟩ class (intCanon d)
                      inj₁
                        (,)
                          nn .π₁
                          eqToId
                            _
                            _
                            trans
                              _
                              _
                              y
                              cong (λu. Int) (λu. x + u) (trans _ _ _ e1 hd)
                              intPlusDiff x y
              nn. let ha = idToEq _ _ _ (nn .π₂)
                      e2 : intOfNat (nn .π₁) ≡ intNeg (class (intCanon d))
                        = intOfNat (nn .π₁)
                          ≡⟨ clsOfRelLe _ _ _ ha ⟩ class (intCanon d .π₂, intCanon d .π₁)
                          ≡⟨ sym _ _ (intNegClass (intCanon d)) ⟩ intNeg (class (intCanon d))
                      inj₂
                        (,)
                          nn .π₁
                          eqToId
                            _
                            _
                            trans
                              _
                              _
                              x
                              cong
                                λu. Int
                                λu. y + u
                                trans _ _ _ e2 (cong (λu. Int) (λu. intNeg u) hd)
                              intPlusNegDiff x y
              leTotal (intCanon d .π₂) (intCanon d .π₁)

-- ===== multiplicative order =====
-- intOfNat is multiplicative (Z·b needs one zeroMult rewrite)
intOfNatMul : (a b : ℕ) → intOfNat a * intOfNat b ≡ intOfNat (a * b)
  using (Int.order.intOfNat.eq,
    Int.mul.*.eq,
    Int.Int.eq,
    zeroMult,
    zeroMult.rw,
    Natural.multZeroId,
    Natural.multZeroId.rw,
    Natural.plusZeroId,
    Natural.plusZeroId.rw,
    zeroPlusId,
    zeroPlusId.rw)
intOfNatMul = λa b. ⋆

-- right distributivity, from the left one by commutativity
intMulDistribR : (a b c : Int) → (a + b) * c ≡ a * c + b * c using (Int.Int.unfold)
intMulDistribR =
  λa b c. (a + b) * c
    ≡⟨ intMulComm (a + b) c ⟩ c * (a + b)
    ≡⟨ intMulDistribL c a b ⟩ c * a + c * b
    ≡⟨ cong (λv. Int) (λv. v + c * b) (intMulComm c a) ⟩ a * c + c * b
    ≡⟨ cong (λv. Int) (λv. a * c + v) (intMulComm c b) ⟩ a * c + b * c

-- scaling by a NATURAL preserves the order: the witness scales
leZMultMonoNat : {x y : Int} {m : ℕ} → x ≤ y → x * intOfNat m ≤ y * intOfNat m
  using (Int.order.≤.unfold)
leZMultMonoNat =
  λx y m le. (,)
    le .π₁ * m
    eqToId
      _
      _
      trans
        _
        _
        _
        cong (λv. Int) (λv. x * intOfNat m + v) (sym _ _ (intOfNatMul (le .π₁) m))
        trans
          _
          _
          _
          sym _ _ (intMulDistribR x (intOfNat (le .π₁)) (intOfNat m))
          cong (λv. Int) (λv. v * intOfNat m) (idToEq _ _ _ (le .π₂))

-- a nonneg integer is a natural, witnessed
leZNonNegView : (c : Int) → intZero ≤ c → (m : ℕ) × intOfNat m ≡ c using (Int.order.≤.unfold)
leZNonNegView =
  λc le. le .π₁, trans _ _ _ (sym _ _ (intAddZeroL (intOfNat (le .π₁)))) (idToEq _ _ _ (le .π₂))

-- scaling by a NONNEGATIVE integer preserves the order: view the
-- scalar as a natural and TRANSPORT the scaled inequality along the
-- view — LeZ is a 𝕌-family, so transport applies to it directly
leZMultMono : (x y c : Int) → x ≤ y → intZero ≤ c → x * c ≤ y * c using (Int.order.≤.unfold)
leZMultMono =
  λx y c le lc. transport
    {Int}
    λu. x * u ≤ y * u
    {intOfNat (leZNonNegView _ lc .π₁)}
    leZNonNegView _ lc .π₂
    leZMultMonoNat le