nat

-- 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).
infixl 6 +
def + : ℕ → ℕ → ℕ ≔ λx. λy. ℕ-elim (n. _) x (n ih. S ih) y
infixl 7 *
def * : ℕ → ℕ → ℕ ≔ λx. λy. ℕ-elim (n. _) Z (n ih. x + ih) y

def plusZeroId : (n : ℕ) → n + Z ≡ n ∈ _ ≔ λn. ⋆
def plusSucId : (n : ℕ) (m : ℕ) → n + S m ≡ S (n + m) ∈ _ ≔ λn. λm. ⋆
def zeroPlusId : (n : ℕ) → Z + n ≡ n ∈ ℕ ≔ λn. ℕ-elim (k. Z + k ≡ k ∈ _) ⋆ (k ih. ⋆) n
def sucPlus : (n : ℕ) (m : ℕ) → S n + m ≡ S (n + m) ∈ ℕ ≔ λn. λm. ℕ-elim (k. S n + k ≡ S (n + k) ∈ _) ⋆ (k ih. ⋆) m
def plusComm : (n : ℕ) (m : ℕ) → m + n ≡ n + m ∈ ℕ ≔ λn. λm. ℕ-elim (k. k + n ≡ n + k ∈ _) ⋆ (k ih. ⋆) m
def plusAssoc : (n : ℕ) (m : ℕ) (k : ℕ) → n + m + k ≡ n + (m + k) ∈ _ ≔
  λn. λm. λk. ℕ-elim (j. n + m + j ≡ n + (m + j) ∈ _) ⋆ (j ih. ⋆) k

-- a + (b + c) ≡ b + (a + c) — permutative, used by whole-equation match
def swapLeft : (a : ℕ) (b : ℕ) (c : ℕ) → a + (b + c) ≡ b + (a + c) ∈ _ ≔
  λa. λb. λc. ℕ-elim (k. a + (b + k) ≡ b + (a + k) ∈ _) ⋆ (k ih. ⋆) c

def multZeroId : (n : ℕ) → n * Z ≡ Z ∈ _ ≔ λn. ⋆
def multSucId : (n : ℕ) (m : ℕ) → n * S m ≡ n + n * m ∈ _ ≔ λn. λm. ⋆
def zeroMult : (n : ℕ) → Z * n ≡ Z ∈ ℕ ≔ λn. ℕ-elim (k. Z * k ≡ Z ∈ _) ⋆ (k ih. ⋆) n
def sucMult : (n : ℕ) (m : ℕ) → S n * m ≡ m + n * m ∈ _ ≔
  λn. λm. ℕ-elim (k. S n * k ≡ k + n * k ∈ _) ⋆ (k ih. ⋆) m
def multComm : (n : ℕ) (m : ℕ) → m * n ≡ n * m ∈ _ ≔
  λn. λm. ℕ-elim (k. k * n ≡ n * k ∈ _) ⋆ (k ih. ⋆) m
def multDistrib : (n : ℕ) (m : ℕ) (k : ℕ) → n * (m + k) ≡ n * m + n * k ∈ _ ≔
  λn. λm. λk. ℕ-elim (j. n * (m + j) ≡ n * m + n * j ∈ _) ⋆ (j ih. ⋆) k
def multAssoc : (n : ℕ) (m : ℕ) (k : ℕ) → n * m * k ≡ n * (m * k) ∈ _ ≔
  λn. λm. λk. ℕ-elim (j. n * m * j ≡ n * (m * j) ∈ _) ⋆ (j ih. ⋆) k