Int.abs

-- The MAGNITUDE of an integer, as a natural. `intCanon` already
-- computes the canonical difference pair — one of whose components is
-- Z — so the magnitude is just the sum of the two, and needs no new
-- well-definedness: it is a function of a function.
--
-- This is the one place where ℤ has a canonical form and ℚ does not
-- (that would need gcd), which is why the same construction cannot be
-- repeated one level up.

import Natural (+, *, plusZeroId, zeroPlusId, plusComm, plusAssoc, sucPlus, multZeroId, zeroMult)
import Natural.order (sumZeroL, sumZeroR)
import Natural.more (∸, zeroMonus, monusEqOfSum)
import Int (Int, IntR, intZero, intOne, intNeg)
import Int.normalize (normPair)
import Int.order (intOfNat)
import Int.mul (*, intMulZeroL, intMulZeroR)
import Int.nonZero (nzOfInt)
import Rat.frac (NZ, nzPos, nzNeg, nzToInt, nzMul)
import Rat (nzToIntMul, sucMulSuc)
import Int.eq (intCanon, intCanonClass, normPairZR)
import Core.equality (trans, sym, cong, transportP, pairext)

intAbs : Int → ℕ
intAbs = λz. intCanon z .π₁ + intCanon z .π₂

intAbsZero : intAbs intZero ≡ Z
  using (Int.eq.intCanon.eq,
    Int.abs.intAbs.eq,
    Int.intZero.eq,
    Int.normalize.normPair.eq,
    Natural.zeroPlusId)
intAbsZero = ⋆

intAbsOne : intAbs intOne ≡ S Z
  using (Int.eq.intCanon.eq,
    Int.abs.intAbs.eq,
    Int.intOne.eq,
    Int.normalize.normPair.eq,
    Natural.plusZeroId)
intAbsOne = ⋆

-- on a natural the magnitude is the natural back
intAbsOfNat : {n : ℕ} → intAbs (intOfNat n) ≡ n
  using (Int.eq.intCanon.eq, Int.abs.intAbs.eq, Int.order.intOfNat.eq, Int.normalize.normPair.eq)
intAbsOfNat =
  λn. trans _ _ _ (cong (λu. ℕ) (λp. p .π₁ + p .π₂) {normPair n Z} {n, Z} normPairZR) (plusZeroId n)

-- zero magnitude names zero: both components of the canonical pair
-- vanish, so the class is the class of (Z , Z)
intAbsZeroInv : (z : Int) → (intAbs z ≡ Z) → z ≡ intZero
  using (Int.eq.intCanon.eq, Int.abs.intAbs.eq, Int.Int.unfold, Int.intZero.eq)
intAbsZeroInv =
  λz h. trans
    _
    _
    _
    sym _ _ (intCanonClass z)
    trans
      _
      _
      intZero
      cong
        {ℕ × ℕ}
        λu. Int
        λp. class p
        {intCanon z}
        {Z, Z}
        pairext
          sumZeroL (intCanon z .π₁) (intCanon z .π₂) h
          sumZeroR (intCanon z .π₁) (intCanon z .π₂) h
      ⋆

-- ===== negation keeps the magnitude =====
-- the canonical pair of the swapped input is the swapped canonical
-- pair, and a sum does not notice the swap
normPairSum : {a b : ℕ} → normPair b a .π₁ + normPair b a .π₂ ≡ normPair a b .π₁ + normPair a b .π₂
  using (Int.normalize.normPair.eq, plusComm, plusZeroId, zeroPlusId)
normPairSum =
  λa. ℕ-elim
    λb. trans
      _
      _
      _
      cong (λu. ℕ) (λp. p .π₁ + p .π₂) {normPair b Z} {b, Z} normPairZR
      trans _ _ _ (plusZeroId b) (sym _ _ (zeroPlusId b))
    n ih. λb. ℕ-elim ⋆ (m ihb. ih m) b
    a

intAbsNeg : {z : Int} → intAbs (intNeg z) ≡ intAbs z
  using (Int.eq.intCanon.eq,
    Int.abs.intAbs.eq,
    Int.Int.unfold,
    Int.intNeg.eq,
    Int.normalize.normPair.eq,
    Core.prop.irrel)
intAbsNeg = λz. quot-elim (p. normPairSum) z

-- ===== the magnitude is multiplicative =====
IntAbsMulAt : Int → Int → Ω
IntAbsMulAt = λx y. intAbs (x * y) ≡ intAbs x * intAbs y

-- the stored magnitude of a non-zero integer, as a natural (one less
-- than the true magnitude, matching NZ's encoding)
nzMag : NZ → ℕ using (Rat.frac.NZ.unfold)
nzMag = λd. ⊎-elim (n. n) (n. n) d

intAbsNz : (f : NZ) → intAbs (nzToInt f) ≡ S (nzMag f)
  using (Int.abs.nzMag.eq,
    Int.order.intOfNat.eq,
    Int.intNeg.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.nzToInt.eq)
intAbsNz =
  λf. ⊎-elim
    n. intAbsOfNat
    n. trans
      intAbs (intNeg (intOfNat (S n)))
      intAbs (intOfNat (S n))
      S n
      intAbsNeg
      intAbsOfNat
    f

nzMagMul : {e f : NZ} → nzMag (nzMul e f) ≡ nzMag e * nzMag f + nzMag e + nzMag f
  using (Int.abs.nzMag.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.nzMul.eq,
    Rat.frac.nzNeg.eq,
    Rat.frac.nzPos.eq)
nzMagMul =
  λe f. ⊎-elim
    m. ⊎-elim
      v. nzMag (nzMul (nzPos m) v) ≡ nzMag (nzPos m) * nzMag v + nzMag (nzPos m) + nzMag v
      k. ⋆
      k. ⋆
      f
    m. ⊎-elim
      v. nzMag (nzMul (nzNeg m) v) ≡ nzMag (nzNeg m) * nzMag v + nzMag (nzNeg m) + nzMag v
      k. ⋆
      k. ⋆
      f
    e

-- on the nose for two non-zero integers, and by collapse otherwise
intAbsMulNz : {e f : NZ} → intAbs (nzToInt e * nzToInt f) ≡ intAbs (nzToInt e) * intAbs (nzToInt f)
intAbsMulNz =
  λe f. trans
    _
    _
    _
    trans _ _ _ (cong (λv. ℕ) (λv. intAbs v) (sym _ _ (nzToIntMul e f))) (intAbsNz (nzMul e f))
    trans
      _
      _
      _
      trans
        _
        _
        _
        cong (λu. ℕ) (λw. S w) {nzMag (nzMul e f)} {nzMag e * nzMag f + nzMag e + nzMag f} nzMagMul
        sym _ _ (sucMulSuc (nzMag e) (nzMag f))
      trans
        _
        _
        _
        cong (λu. ℕ) (λw. w * S (nzMag f)) (sym _ _ (intAbsNz e))
        cong (λu. ℕ) (λw. intAbs (nzToInt e) * w) (sym _ _ (intAbsNz f))

intAbsMul : (x y : Int) → intAbs (x * y) ≡ intAbs x * intAbs y
  using (Int.abs.IntAbsMulAt.eq,
    Int.abs.intAbs.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.nzToInt.eq)
intAbsMul =
  λx y. ⊎-elim
    ex. ⊎-elim
      ey. transportP
        λv. IntAbsMulAt v y
        ex .π₂
        transportP (λv. IntAbsMulAt (nzToInt (ex .π₁)) v) (ey .π₂) intAbsMulNz
      hy. trans
        _
        _
        _
        trans
          _
          _
          _
          cong
            λv. ℕ
            λv. intAbs v
            trans _ _ intZero (cong (λv. Int) (λv. x * v) hy) intMulZeroR
          intAbsZero
        sym
          _
          _
          trans
            _
            _
            _
            cong
              λu. ℕ
              λw. intAbs x * w
              trans _ _ _ (cong (λv. ℕ) (λv. intAbs v) hy) intAbsZero
            multZeroId (intAbs x)
      nzOfInt y
    hx. trans
      _
      _
      _
      trans
        _
        _
        _
        cong (λv. ℕ) (λv. intAbs v) (trans _ _ _ (cong (λv. Int) (λv. v * y) hx) (intMulZeroL y))
        intAbsZero
      sym
        _
        _
        trans
          _
          _
          _
          cong (λu. ℕ) (λw. w * intAbs y) (trans _ _ _ (cong (λv. ℕ) (λv. intAbs v) hx) intAbsZero)
          zeroMult (intAbs y)
    nzOfInt x

-- ===== a leaner magnitude, for the discharge engine's sake =====
--
-- `intAbs` reads the magnitude off `intCanon`, which is the honest
-- canonical form but whose normal form the lemma matcher cannot see
-- into: a `using` candidate mentioning `intAbs ?N` never fires against
-- a goal mentioning `intAbs (p .π₁)`, because ?N sits inside
-- intCanon's quot-elim. `intMag` computes the same natural directly
-- from a difference pair, and matches.
magPair : ℕ × ℕ → ℕ
magPair = λr. r .π₁ ∸ r .π₂ + (r .π₂ ∸ r .π₁)

magPairWD : (r r' : ℕ × ℕ) (h : IntR r r') → magPair r ≡ magPair r'
  using (Int.abs.magPair.eq, Int.IntR.eq, Int.IntR.unfold)
magPairWD =
  λr r' h. trans
    _
    _
    _
    cong (λu. ℕ) (λw. w + (r .π₂ ∸ r .π₁)) (monusEqOfSum h)
    cong (λu. ℕ) (λw. r' .π₁ ∸ r' .π₂ + w) (monusEqOfSum (sym _ _ h))

-- the same well-definedness, stated over the REPRESENTED relation (the
-- raw sum equation) — the shape the quot-elim obligation carries its
-- hypothesis in under strict conversion
magPairWDRep : (r r' : ℕ × ℕ) → (r .π₁ + r' .π₂ ≡ r .π₂ + r' .π₁) → magPair r ≡ magPair r'
  using (Int.abs.magPair.eq)
magPairWDRep =
  λr r' h. trans
    _
    _
    _
    cong (λu. ℕ) (λw. w + (r .π₂ ∸ r .π₁)) (monusEqOfSum h)
    cong (λu. ℕ) (λw. r' .π₁ ∸ r' .π₂ + w) (monusEqOfSum (sym _ _ h))

intMag : Int → ℕ using (Int.Int.unfold, magPairWD, magPairWDRep)
intMag = λz. quot-elim (r. magPair r) z

intMagZero : intMag intZero ≡ Z
  using (Int.abs.intMag.eq, Int.abs.magPair.eq, Int.intZero.eq, Natural.+.eq, Natural.more.∸.eq)
intMagZero = ⋆

intMagOfNat : (n : ℕ) → intMag (intOfNat n) ≡ n
  using (Int.abs.intMag.eq,
    Int.abs.magPair.eq,
    Int.order.intOfNat.eq,
    Natural.more.monusZeroR,
    Natural.more.monusZeroR.rw,
    zeroMonus,
    zeroMonus.rw,
    plusZeroId,
    plusZeroId.rw)
intMagOfNat = λn. ⋆

intMagNz : (f : NZ) → intMag (nzToInt f) ≡ S (nzMag f)
  using (Int.abs.intMag.eq,
    Int.abs.magPair.eq,
    Int.abs.nzMag.eq,
    Natural.more.monusZeroR,
    Natural.more.monusZeroR.rw,
    plusZeroId,
    plusZeroId.rw,
    Rat.frac.NZ.unfold,
    Rat.frac.nzToInt.eq,
    zeroMonus,
    zeroMonus.rw,
    zeroPlusId,
    zeroPlusId.rw)
intMagNz = λf. ⊎-elim (n. ⋆) (n. ⋆) f

IntMagMulAt : Int → Int → Ω
IntMagMulAt = λx y. intMag (x * y) ≡ intMag x * intMag y

intMagMulNz : {e f : NZ} → intMag (nzToInt e * nzToInt f) ≡ intMag (nzToInt e) * intMag (nzToInt f)
intMagMulNz =
  λe f. trans
    _
    _
    _
    trans _ _ _ (cong (λv. ℕ) (λv. intMag v) (sym _ _ (nzToIntMul e f))) (intMagNz (nzMul e f))
    trans
      _
      _
      _
      trans
        _
        _
        _
        cong (λu. ℕ) (λw. S w) {nzMag (nzMul e f)} {nzMag e * nzMag f + nzMag e + nzMag f} nzMagMul
        sym _ _ (sucMulSuc (nzMag e) (nzMag f))
      trans
        _
        _
        _
        cong (λu. ℕ) (λw. w * S (nzMag f)) (sym _ _ (intMagNz e))
        cong (λu. ℕ) (λw. intMag (nzToInt e) * w) (sym _ _ (intMagNz f))

intMagMul : (x y : Int) → intMag (x * y) ≡ intMag x * intMag y
  using (Int.abs.IntMagMulAt.eq,
    Int.abs.intMag.eq,
    Int.Int.unfold,
    Int.mul.*.eq,
    Rat.frac.NZ.unfold,
    Rat.frac.nzToInt.eq)
intMagMul =
  λx y. ⊎-elim
    ex. ⊎-elim
      ey. transportP
        λv. IntMagMulAt v y
        ex .π₂
        transportP (λv. IntMagMulAt (nzToInt (ex .π₁)) v) (ey .π₂) intMagMulNz
      hy. trans
        _
        _
        _
        trans
          _
          _
          _
          cong
            λv. ℕ
            λv. intMag v
            trans _ _ intZero (cong (λv. Int) (λv. x * v) hy) intMulZeroR
          intMagZero
        sym
          _
          _
          trans
            _
            _
            _
            cong
              λu. ℕ
              λw. intMag x * w
              trans _ _ _ (cong (λv. ℕ) (λv. intMag v) hy) intMagZero
            multZeroId (intMag x)
      nzOfInt y
    hx. trans
      _
      _
      _
      trans
        _
        _
        _
        cong (λv. ℕ) (λv. intMag v) (trans _ _ _ (cong (λv. Int) (λv. v * y) hx) (intMulZeroL y))
        intMagZero
      sym
        _
        _
        trans
          _
          _
          _
          cong (λu. ℕ) (λw. w * intMag y) (trans _ _ _ (cong (λv. ℕ) (λv. intMag v) hx) intMagZero)
          zeroMult (intMag y)
    nzOfInt x

intMagNeg : {z : Int} → intMag (intNeg z) ≡ intMag z
  using (Int.abs.intMag.eq, Int.abs.magPair.eq, Int.Int.unfold, Int.intNeg.eq, Core.prop.irrel)
intMagNeg = λz. quot-elim (r. plusComm (r .π₁ ∸ r .π₂) (r .π₂ ∸ r .π₁)) z