Natural.more

-- Arithmetic ℕ owes the rest of the corpus: right distributivity,
-- cancellation on the left and by a non-zero factor, truncated
-- subtraction with max/min, and exponentiation. Each of these was
-- either re-derived ad hoc downstream (`distribBackR` lives in
-- Int/mul.nova, `oneMult` in Rat/frac.nova) or simply unavailable.
-- ===== distributivity on the right =====

import Natural (+, *, plusZeroId, plusSucId, zeroPlusId, sucPlus, plusComm, plusAssoc, plusCancel, sucInj, multZeroId, multSucId, zeroMult, sucMult, multComm, multDistrib, multAssoc)
import Natural.order (≤, leRefl, leTrans, leTotal, sumZeroL, sumZeroR, leAntisym)
import Core.equality (trans, sym, cong)
import Core.id (Id, idToEq, eqToId)

multDistribR : (n m k : ℕ) → (m + k) * n ≡ m * n + k * n
multDistribR =
  λn m k. (m + k) * n
    ≡⟨ multComm (m + k) n ⟩ n * (m + k)
    ≡⟨ multDistrib n m k ⟩ n * m + n * k
    ≡⟨ cong (λu. ℕ) (λw. w + n * k) (multComm m n) ⟩ m * n + n * k
    ≡⟨ cong (λu. ℕ) (λw. m * n + w) (multComm k n) ⟩ m * n + k * n

-- ===== cancellation =====
plusCancelL : (k n m : ℕ) → (k + n ≡ k + m) → n ≡ m
plusCancelL = λk n m h. plusCancel _ _ _ (trans _ _ _ (plusComm k n) (trans _ _ _ h (plusComm m k)))

-- a product with a SUCCESSOR is zero only if the other factor is
multZeroInv : (j k : ℕ) → (j * S k ≡ Z) → j ≡ Z
multZeroInv = λj k h. sumZeroL _ _ (trans _ _ _ (sym _ _ (multSucId j k)) h)

-- cancellation by S k, under the assumption that the smaller side is
-- known: the surplus times S k is zero, hence zero
multCancelLe : {n m : ℕ} (k : ℕ) → n ≤ m → (n * S k ≡ m * S k) → n ≡ m
  using (Core.id.Id.unfold, Natural.plusZeroId, Natural.order.≤.unfold)
multCancelLe =
  λn m k le h. let e : n + le .π₁ ≡ m = idToEq _ _ _ (le .π₂)
                   split : n * S k ≡ n * S k + le .π₁ * S k
                     = trans
                       _
                       _
                       _
                       h
                       trans
                         _
                         _
                         _
                         cong (λu. ℕ) (λw. w * S k) (sym _ _ e)
                         multDistribR (S k) n (le .π₁)
                   jz : le .π₁ ≡ Z
                     = multZeroInv _ _ (sym _ _ (plusCancelL (n * S k) Z (le .π₁ * S k) split))
                   trans
                     _
                     _
                     _
                     sym _ _ (trans _ _ _ (cong (λu. ℕ) (λw. n + w) jz) (plusZeroId n))
                     e

multCancelR : (n m k : ℕ) → (n * S k ≡ m * S k) → n ≡ m
multCancelR =
  λn m k h. ⊎-elim
    le. multCancelLe _ le h
    le. sym _ _ (multCancelLe _ le (sym _ _ h))
    leTotal n m

-- ===== truncated subtraction =====
pred : ℕ → ℕ
pred = λn. ℕ-elim Z (k ih. k) n

infixl 6 ∸
∸ : ℕ → ℕ → ℕ
(∸) = λa b. ℕ-elim a (k ih. pred ih) b

monusZeroR : {a : ℕ} → a ∸ Z ≡ a using (Natural.more.∸.eq)
monusZeroR = λa. ⋆

monusSucR : (a b : ℕ) → a ∸ S b ≡ pred (a ∸ b) using (Natural.more.pred.eq, Natural.more.∸.eq)
monusSucR = λa b. ⋆

zeroMonus : (b : ℕ) → Z ∸ b ≡ Z
  using (hyp.rw,
    Natural.more.monusZeroR,
    Natural.more.monusZeroR.rw,
    Natural.more.monusSucR,
    Natural.more.monusSucR.rw,
    Natural.more.pred.eq)
zeroMonus = λb. ℕ-elim ⋆ (k ih. ⋆) b

sucMonusSuc : (a b : ℕ) → S a ∸ S b ≡ a ∸ b using (Natural.more.pred.eq, Natural.more.∸.eq)
sucMonusSuc = λa b. ℕ-elim ⋆ (k ih. ⋆) b

-- (a + b) − b is a, on the nose
plusMonus : (a b : ℕ) → a + b ∸ b ≡ a
  using (hyp.rw,
    plusZeroId,
    plusZeroId.rw,
    plusSucId,
    plusSucId.rw,
    Natural.more.monusZeroR,
    Natural.more.monusZeroR.rw,
    sucMonusSuc,
    sucMonusSuc.rw)
plusMonus = λa b. ℕ-elim ⋆ (k ih. ⋆) b

-- subtracting a sum is subtracting twice
monusPlus : (a b c : ℕ) → a ∸ (b + c) ≡ a ∸ b ∸ c using (Natural.+.eq, Natural.more.∸.eq)
monusPlus = λa b c. ℕ-elim ⋆ (k ih. ⋆) c

monusSelf : {a : ℕ} → a ∸ a ≡ Z
  using (hyp.rw, Natural.more.zeroMonus, Natural.more.zeroMonus.rw, sucMonusSuc, sucMonusSuc.rw)
monusSelf = λa. ℕ-elim ⋆ (k ih. ⋆) a

-- ...so a ≤ b makes a − b vanish
monusZeroOfLe : (a b : ℕ) → a ≤ b → a ∸ b ≡ Z using (Core.id.Id.unfold, Natural.order.≤.unfold)
monusZeroOfLe =
  λa b le. a ∸ b
    ≡⟨ cong (λu. ℕ) (λw. a ∸ w) (sym _ _ (idToEq _ _ _ (le .π₂))) ⟩ a ∸ (a + le .π₁)
    ≡⟨ monusPlus a a (le .π₁) ⟩ a ∸ a ∸ le .π₁
    ≡⟨ cong (λu. ℕ) (λw. w ∸ le .π₁) {a ∸ a} {Z} monusSelf ⟩ Z ∸ le .π₁
    ≡⟨ zeroMonus (le .π₁) ⟩ Z

-- ...and a ≤ b makes the difference add back
leMonusPlus : {a b : ℕ} → a ≤ b → a + (b ∸ a) ≡ b using (Core.id.Id.unfold, Natural.order.≤.unfold)
leMonusPlus =
  λa b le. let e : a + le .π₁ ≡ b = idToEq _ _ _ (le .π₂)
               a + (b ∸ a)
                 ≡⟨ cong (λu. ℕ) (λw. a + (w ∸ a)) (sym _ _ e) ⟩ a + (a + le .π₁ ∸ a)
                 ≡⟨ cong (λu. ℕ) (λw. a + (w ∸ a)) (plusComm (le .π₁) a) ⟩ a + (le .π₁ + a ∸ a)
                 ≡⟨ cong (λu. ℕ) (λw. a + w) (plusMonus (le .π₁) a) ⟩ a + le .π₁
                 ≡⟨ e ⟩ b

-- ===== max and min =====
natMax : ℕ → ℕ → ℕ
natMax = λa b. a + (b ∸ a)

natMin : ℕ → ℕ → ℕ
natMin = λa b. a ∸ (a ∸ b)

-- a sits under the max by construction: the witness is the difference
leMaxL : (a b : ℕ) → a ≤ natMax a b using (Natural.more.natMax.eq, Natural.order.≤.unfold)
leMaxL = λa b. b ∸ a, eqToId _ _ ⋆

-- and so does b, once the two cases are settled
-- a ≤ b : the max IS b
-- b ≤ a : the max is a, and b ≤ a
leMaxR : (a b : ℕ) → b ≤ natMax a b
  using (Core.id.Id.unfold, Natural.more.natMax.eq, Natural.order.≤.unfold)
leMaxR =
  λa b. ⊎-elim
    le. Z, eqToId _ _ (trans _ _ _ (plusZeroId b) (sym (natMax a b) _ (leMonusPlus le)))
    le. (,)
      le .π₁ + (b ∸ a)
      eqToId
        _
        _
        trans
          _
          _
          natMax a b
          trans
            _
            _
            _
            sym _ _ (plusAssoc b (le .π₁) (b ∸ a))
            cong (λu. ℕ) (λw. w + (b ∸ a)) (idToEq _ _ _ (le .π₂))
          ⋆
    leTotal a b

natMaxSelf : (a : ℕ) → natMax a a ≡ a using (Natural.more.natMax.eq)
natMaxSelf = λa. trans _ _ _ (cong (λu. ℕ) (λw. a + w) {a ∸ a} {Z} monusSelf) (plusZeroId a)

natMinSelf : (a : ℕ) → natMin a a ≡ a using (Natural.more.natMin.eq)
natMinSelf = λa. trans _ _ _ (cong (λu. ℕ) (λw. a ∸ w) {a ∸ a} {Z} monusSelf) monusZeroR

-- ===== exponentiation =====
infixr 8 ^
^ : ℕ → ℕ → ℕ
(^) = λa n. ℕ-elim (S Z) (k ih. a * ih) n

expZero : (a : ℕ) → a ^ Z ≡ S Z using (Natural.more.^.eq)
expZero = λa. ⋆

expSuc : (a n : ℕ) → a ^ S n ≡ a * a ^ n using (Natural.*.eq, Natural.more.^.eq)
expSuc = λa n. ⋆

oneExp : (n : ℕ) → S Z ^ n ≡ S Z
  using (hyp.rw,
    Natural.more.expZero,
    Natural.more.expZero.rw,
    Natural.more.expSuc,
    Natural.more.expSuc.rw,
    multSucId,
    multSucId.rw,
    multZeroId,
    multZeroId.rw,
    plusZeroId,
    plusZeroId.rw)
oneExp = λn. ℕ-elim ⋆ (k ih. ⋆) n

-- x * (y * z) ≡ y * (x * z): the left-swap under associativity,
-- stated in the exact shape expPlus's step case needs
multLeftComm : (x y z : ℕ) → x * (y * z) ≡ y * (x * z)
multLeftComm =
  λx y z. x * (y * z)
    ≡⟨ multAssoc x y z ⟩ x * y * z
    ≡⟨ cong (λu. ℕ) (λw. w * z) (multComm y x) ⟩ y * x * z
    ≡⟨ multAssoc y x z ⟩ y * (x * z)

expPlus : (a m n : ℕ) → a ^ (m + n) ≡ a ^ m * a ^ n
  using (hyp.rw,
    plusZeroId,
    plusZeroId.rw,
    Natural.more.expZero,
    Natural.more.expZero.rw,
    multSucId,
    multSucId.rw,
    multZeroId,
    multZeroId.rw)
expPlus =
  λa m n. ℕ-elim
    ⋆
    k ih. a ^ (m + S k)
      ≡⟨ plusSucId m k ⟩ a ^ S (m + k)
      ≡⟨ expSuc a (m + k) ⟩ a * a ^ (m + k)
      ≡⟨ ih ⟩ a * (a ^ m * a ^ k)
      ≡⟨ multLeftComm a (a ^ m) (a ^ k) ⟩ a ^ m * (a * a ^ k)
      ≡⟨ expSuc a k ⟩ a ^ m * a ^ S k
    n

-- ===== monus and a common summand =====
monusPlusR : (a b k : ℕ) → a + k ∸ (b + k) ≡ a ∸ b
  using (hyp.rw, plusZeroId, plusZeroId.rw, plusSucId, plusSucId.rw, sucMonusSuc, sucMonusSuc.rw)
monusPlusR = λa b k. ℕ-elim ⋆ (j ih. ⋆) k

monusPlusL : {k a b : ℕ} → k + a ∸ (k + b) ≡ a ∸ b
monusPlusL =
  λk a b. trans
    _
    _
    _
    trans
      _
      _
      _
      cong (λu. ℕ) (λw. w ∸ (k + b)) (plusComm a k)
      cong (λu. ℕ) (λw. a + k ∸ w) (plusComm b k)
    monusPlusR a b k

-- the difference-pair reading: a + d ≡ b + c makes a − b and c − d
-- the same truncated difference
monusEqOfSum : {a b c d : ℕ} → (a + d ≡ b + c) → a ∸ b ≡ c ∸ d
monusEqOfSum =
  λa b c d h. trans
    _
    _
    _
    sym _ _ (monusPlusR a b d)
    trans _ _ (c ∸ d) (cong (λu. ℕ) (λw. w ∸ (b + d)) h) monusPlusL