-- Natural-number algebra
-- Part of the Grace17 proof assistant for mathematics based on set theory.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Core.Nat.Algebra
namespace Grace.Core.Nat.Algebra
import Grace.Core.Nat
export open Grace.Core.Nat.Algebra

theorem add.right_unit (n : Nat)
  shows add(n, 0) = n
proof
  induction n
  | zero => settle with add
  | succ(k) using ih => settle with add, ih

theorem add.succ_right (m : Set, n : Nat)
  shows add(n, succ(m)) = succ(add(n, m))
proof
  induction n
  | zero => settle with add
  | succ(k) using ih => settle with add, ih

theorem add.right_one (n : Nat)
  shows add(n, 1) = succ(n)
proof
  simp [add.succ_right, add.right_unit]

theorem add.associative (y z : Set, n : Nat)
  shows add(add(n, y), z) = add(n, add(y, z))
proof
  induction n
  | zero => settle with add
  | succ(k) using ih => settle with add, ih

theorem add.associative_reverse (y z : Set, n : Nat)
  shows add(n, add(y, z)) = add(add(n, y), z)
proof
  simp [add.associative]

theorem add.commutative (y n : Nat)
  shows add(n, y) = add(y, n)
proof
  induction n
  | zero => settle with add, add.right_unit
  | succ(k) using ih => settle with add, add.succ_right, ih

theorem add.successor_shift (a k : Nat)
  shows add(a, succ(k)) = add(succ(a), k)
proof
  simp [add.succ_right, add]

theorem add.swap (b : Nat, c : Set, a : Nat)
  shows add(a, add(b, c)) = add(b, add(a, c))
proof
  induction a
  | zero => settle with add
  | succ(k) using ih => settle with add, add.succ_right, ih

theorem add.closed (y : Nat, x : Nat)
  shows Nat(add(x, y))
proof
  induction x
  | zero => settle with add
  | succ(k) using ih => settle with add, Naturals.constructor.succ, ih

theorem mul.right_zero (n : Nat)
  shows mul(n, 0) = 0
proof
  induction n
  | zero => settle with mul
  | succ(k) using ih => settle with mul, add, ih

theorem mul.left_unit (n : Nat)
  shows mul(1, n) = n
proof
  simp [mul, add, add.right_unit]

theorem mul.right_unit (n : Nat)
  shows mul(n, 1) = n
proof
  induction n
  | zero => settle with mul
  | succ(k) using ih => settle with mul, add, ih

theorem mul.succ_right (y n : Nat)
  shows mul(n, succ(y)) = add(n, mul(n, y))
proof
  induction n
  | zero => settle with mul, add
  | succ(k) using ih => settle with mul, add, add.swap, ih

theorem mul.commutative (y n : Nat)
  shows mul(n, y) = mul(y, n)
proof
  induction n
  | zero => settle with mul, mul.right_zero
  | succ(k) using ih => settle with mul, mul.succ_right, ih

theorem mul.closed (y : Nat, x : Nat)
  shows Nat(mul(x, y))
proof
  induction x
  | zero => settle with mul, Naturals.constructor.zero
  | succ(k) using ih => settle with mul, add.closed, ih

theorem mul.distributes_right (y z : Nat, n : Nat)
  shows mul(add(n, y), z) = add(mul(n, z), mul(y, z))
proof
  induction n
  | zero => settle with add, mul
  | succ(k) using ih => settle with add, mul, add.associative, ih

theorem mul.distributes_left (y z : Nat, x : Nat)
  shows mul(x, add(y, z)) = add(mul(x, y), mul(x, z))
proof
  induction x
  | zero => settle with add, mul
  | succ(k) using ih => settle with mul, add.associative, add.swap, mul.closed, ih

theorem mul.associative (y z : Nat, x : Nat)
  shows mul(mul(x, y), z) = mul(x, mul(y, z))
proof
  induction x
  | zero => settle with mul
  | k + 1 using ih => settle with mul, mul.distributes_right, mul.closed, ih

end Grace.Core.Nat.Algebra