Natural

-- Natural-number addition and multiplication (both recursing on the
-- second argument) and their basic equational theory. The operators
-- ARE the definitions' names (docs/NovaElaboration.txt).

import Core.equality (sym, cong, trans)

infixl 6 +
+ : ℕ → ℕ → ℕ
(+) = λx y. ℕ-elim x (n ih. S ih) y

infixl 7 *
* : ℕ → ℕ → ℕ
(*) = λx y. ℕ-elim Z (n ih. x + ih) y

plusZeroId : (n : ℕ) → n + Z ≡ n using (Natural.+.eq)
plusZeroId = λn. ⋆

plusSucId : (n m : ℕ) → n + S m ≡ S (n + m) using (Natural.+.eq)
plusSucId = λn m. ⋆

zeroPlusId : (n : ℕ) → Z + n ≡ n using (+.eq, Natural.plusZeroId)
zeroPlusId = λn. ℕ-elim ⋆ (k ih. ⋆) n

sucPlus : (n m : ℕ) → S n + m ≡ S (n + m) using (Natural.+.eq)
sucPlus = λn m. ℕ-elim ⋆ (k ih. ⋆) m

plusComm : (n m : ℕ) → m + n ≡ n + m
plusComm =
  λn m. ℕ-elim
    Z + n ≡⟨ zeroPlusId n ⟩ n ≡⟨ plusZeroId n ⟩ n + Z
    k ih. S k + n ≡⟨ sucPlus k n ⟩ S (k + n) ≡⟨ ih ⟩ S (n + k) ≡⟨ plusSucId n k ⟩ n + S k
    m

plusAssoc : (n m k : ℕ) → n + m + k ≡ n + (m + k) using (Natural.+.eq)
plusAssoc = λn m k. ℕ-elim ⋆ (j ih. ⋆) k

-- a + (b + c) ≡ b + (a + c) — permutative, used by whole-equation match
swapLeft : (a b c : ℕ) → a + (b + c) ≡ b + (a + c) using (plusComm)
swapLeft =
  λa b c. ℕ-elim
    a + (b + Z) ≡⟨ plusZeroId b ⟩ a + b ≡⟨ plusComm b a ⟩ b + a ≡⟨ plusZeroId a ⟩ b + (a + Z)
    k ih. ⋆ using (Natural.+.eq)
    c

-- congruence in each summand — one ⋆ each: reflecting the hypothesis
-- makes the two sides the same term
plusCongL : {a b : ℕ} (c : ℕ) → (a ≡ b) → a + c ≡ b + c
plusCongL = λa b c h. cong (λu. ℕ) (λu. u + c) h

plusCongR : (a : ℕ) {b c : ℕ} → (b ≡ c) → a + b ≡ a + c
plusCongR = λa b c h. ⋆

-- (x+y)+(z+w) ≡ (x+w)+(z+y) — the inner summands swap. Discharged by
-- whole-equation matching against plusAssoc/plusComm/swapLeft above
swapMid : {x y z w : ℕ} → x + y + (z + w) ≡ x + w + (z + y)
swapMid =
  λx y z w. x + y + (z + w)
    ≡⟨ plusAssoc x y (z + w) ⟩ x + (y + (z + w))
    ≡⟨ swapLeft y z w ⟩ x + (z + (y + w))
    ≡⟨ plusComm w y ⟩ x + (z + (w + y))
    ≡⟨ swapLeft z w y ⟩ x + (w + (z + y))
    ≡⟨ plusAssoc x w (z + y) ⟩ x + w + (z + y)

-- S is injective — the kernel's suc selector, named. Bare ⋆: reflecting
-- the hypothesis gives S n ≐ S m, whose suc-component the selector
-- reads off (docs/NovaKernel.txt §5)
sucInj : (n m : ℕ) → (S n ≡ S m) → n ≡ m
sucInj = λn m h. ⋆

-- CANCELLATION: (· + k) is injective, i.e. a common right summand
-- cancels. Induction on the cancelled summand — each step peels one
-- successor off both sides (n + S j ≜ S (n + j)) and hands it to sucInj
plusCancel : (n m k : ℕ) → (n + k ≡ m + k) → n ≡ m using (+.eq, Natural.plusSucId)
plusCancel = λn m k. ℕ-elim (λh. ⋆) (j ih. λh. ih (sucInj _ _ h)) k

multZeroId : (n : ℕ) → n * Z ≡ Z using (Natural.*.eq)
multZeroId = λn. ⋆

multSucId : (n m : ℕ) → n * S m ≡ n + n * m using (Natural.*.eq, Natural.+.eq)
multSucId = λn m. ⋆

zeroMult : (n : ℕ) → Z * n ≡ Z using (Natural.multZeroId)
zeroMult =
  λn. ℕ-elim ⋆ (k ih. Z * S k ≡⟨ multSucId Z k ⟩ Z + Z * k ≡⟨ ih ⟩ Z + Z ≡⟨ zeroPlusId Z ⟩ Z) n

sucMult : (n m : ℕ) → S n * m ≡ m + n * m
sucMult =
  λn m. ℕ-elim
    S n * Z ≡⟨ multZeroId (S n) ⟩ Z ≡⟨ multZeroId n ⟩ n * Z ≡⟨ zeroPlusId (n * Z) ⟩ Z + n * Z
    k ih. S n * S k
      ≡⟨ multSucId (S n) k ⟩ S n + S n * k
      ≡⟨ ih ⟩ S n + (k + n * k)
      ≡⟨ swapLeft (S n) k (n * k) ⟩ k + (S n + n * k)
      ≡⟨ sucPlus n (n * k) ⟩ k + S (n + n * k)
      ≡⟨ plusSucId k (n + n * k) ⟩ S (k + (n + n * k))
      ≡⟨ sucPlus k (n + n * k) ⟩ S k + (n + n * k)
      ≡⟨ multSucId n k ⟩ S k + n * S k
    m

multComm : (n m : ℕ) → m * n ≡ n * m
multComm =
  λn m. ℕ-elim
    Z * n ≡⟨ zeroMult n ⟩ Z ≡⟨ multZeroId n ⟩ n * Z
    k ih. S k * n ≡⟨ sucMult k n ⟩ n + k * n ≡⟨ ih ⟩ n + n * k ≡⟨ multSucId n k ⟩ n * S k
    m

multDistrib : (n m k : ℕ) → n * (m + k) ≡ n * m + n * k
multDistrib =
  λn m k. ℕ-elim
    n * (m + Z)
      ≡⟨ plusZeroId m ⟩ n * m
      ≡⟨ plusZeroId (n * m) ⟩ n * m + Z
      ≡⟨ multZeroId n ⟩ n * m + n * Z
    j ih. n * (m + S j)
      ≡⟨ plusSucId m j ⟩ n * S (m + j)
      ≡⟨ multSucId n (m + j) ⟩ n + n * (m + j)
      ≡⟨ ih ⟩ n + (n * m + n * j)
      ≡⟨ swapLeft n (n * m) (n * j) ⟩ n * m + (n + n * j)
      ≡⟨ multSucId n j ⟩ n * m + n * S j
    k

multAssoc : (n m k : ℕ) → n * m * k ≡ n * (m * k)
multAssoc =
  λn m k. ℕ-elim
    n * m * Z ≡⟨ multZeroId (n * m) ⟩ Z ≡⟨ multZeroId n ⟩ n * Z ≡⟨ multZeroId m ⟩ n * (m * Z)
    j ih. n * m * S j
      ≡⟨ multSucId (n * m) j ⟩ n * m + n * m * j
      ≡⟨ ih ⟩ n * m + n * (m * j)
      ≡⟨ multDistrib n m (m * j) ⟩ n * (m + m * j)
      ≡⟨ multSucId m j ⟩ n * (m * S j)
    k