-- Core natural-number mathematics
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Nat.Core
import Core.Nat.Order

-- Arithmetic lemmas belong in Cumulus; Core retains only the bootstrap laws.
theorem one.ne_zero
  shows 1 ≠ 0
proof
  intro equal
  have distinct := Naturals.disjoint.zero.succ at 0
  apply distinct
  symm
  exact equal

theorem add.left_cancel (b c : Set, a : Nat)
  shows add(a, b) = add(a, c) → b = c
proof
  induction a
  | zero =>
    intro h
    simp [add] at h
    exact h
  | succ(k) using ih =>
    intro h
    simp [add] at h
    have inject := Naturals.injective.succ with h
    apply ih
    exact inject

theorem add.right_cancel (a b c : Nat)
  shows add(a, c) = add(b, c) → a = b
proof
  intro h
  have cancel := add.left_cancel at a, b, c
  apply cancel
  have commuteA := add.commutative at a, c
  have commuteB := add.commutative at b, c
  rewrite commuteA
  rwa commuteB

theorem add.swap_last (a b c : Nat)
  shows add(add(a, b), c) = add(add(a, c), b)
proof
  have left := add.associative at b, c, a
  have middle := add.commutative at c, b with *
  have right := add.associative at c, b, a
  simp

theorem add.four_shuffle (a b c d : Nat)
  shows add(add(a, b), add(c, d)) = add(add(a, c), add(b, d))
proof
  simp [add.associative, add.swap]

theorem add.eq_zero (b a : Nat)
  shows add(a, b) = 0 → (a = 0 ∧ b = 0)
proof
  induction a
  | zero =>
    intro h
    constructor
    rfl
    simp [add] at h
    exact h
  | succ(k) using ih =>
    intro h
    simp [add] at h
    exfalso
    have impossible := Naturals.disjoint.zero.succ at add(k, b)
    apply impossible
    simp

lemma add.zero_successor_case (b : Set, a : Nat)
  requires hbNat : Nat(b)
  shows add(a, b) = 0 → (succ(a) = 1 ∧ b = 0)
proof
  induction a
  | zero =>
    intro h
    constructor
    . rfl
    . simp [add] at h
      exact h
  | succ(k) using ih =>
    intro h
    simp [add] at h
    exfalso
    have impossible := Naturals.disjoint.zero.succ at add(k, b)
    apply impossible
    simp

theorem add.eq_one (b : Set, a : Nat)
  requires hbNat : Nat(b)
  shows add(a, b) = 1 → ((a = 0 ∧ b = 1) ∨ (a = 1 ∧ b = 0))
proof
  induction a
  | zero =>
    intro h
    left
    constructor
    . rfl
    . simp [add] at h
      exact h
  | succ(k) using ih =>
    intro h
    right
    simp [add] at h
    have inject := Naturals.injective.succ at add(k, b), 0 with h
    apply add.zero_successor_case at b, k
    . exact inject

theorem add.eq_zero_right (b : Set, a : Nat)
  requires hbNat : Nat(b)
  shows add(a, b) = 0 → b = 0
proof
  induction a
  | zero =>
    intro h
    simp [add] at h
    exact h
  | succ(k) using ih =>
    intro h
    simp [add] at h
    exfalso
    have impossible := Naturals.disjoint.zero.succ at add(k, b)
    apply impossible
    simp

theorem add.eq_zero_left (b : Set, a : Nat)
  requires hbNat : Nat(b)
  shows add(a, b) = 0 → a = 0
proof
  induction a
  | zero =>
    intro h
    rfl
  | succ(k) using ih =>
    intro h
    simp [add] at h
    exfalso
    have impossible := Naturals.disjoint.zero.succ at add(k, b)
    apply impossible
    simp

theorem mul.left_zero (n : Nat)
  shows mul(0, n) = 0
proof
  simp [mul]

theorem mul.succ_left (n m : Nat)
  shows mul(succ(n), m) = add(m, mul(n, m))
proof
  simp [mul]

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

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

theorem mul.left_factor_one (b : Set, a : Nat)
  requires hbNat : Nat(b)
  shows mul(a, b) = 1 → a = 1
proof
  induction a
  | zero =>
    intro h
    simp [mul] at h
  | succ(k) using ih =>
    intro h
    simp [mul] at h
    have productNat := mul.closed with hbNat, h_k
    have shape := add.eq_one with hbNat, productNat, h
    cases shape with hLeft | hRight
    . rcases hLeft with ⟨hbZero, hProductOne⟩
      exfalso
      rw hbZero at hProductOne
      have zero := mul.right_zero with h_k
      rw zero at hProductOne
      have impossible := Naturals.disjoint.zero.succ at 0
      apply impossible
      exact hProductOne
    . rcases hRight with ⟨hbOne, hProductZero⟩
      rw hbOne at hProductZero
      have unit := mul.right_unit with h_k
      rw unit at hProductZero
      rw hProductZero
      rfl

theorem mul.eq_zero (b : Set, a : Nat)
  requires hbNat : Nat(b)
  shows mul(a, b) = 0 → (a = 0 ∨ b = 0)
proof
  induction a
  | zero =>
    intro h
    left
    rfl
  | succ(k) using ih =>
    intro h
    right
    simp [mul] at h
    apply add.eq_zero_left at mul(k, b), b
    . settle with mul.closed

theorem mul.nonzero (a b : Nat)
  requires aNonzero : a ≠ 0
  requires bNonzero : b ≠ 0
  shows a * b ≠ 0
proof
  intro productZero
  have zeroFactor := mul.eq_zero with *, productZero
  cases zeroFactor with aZero | bZero
  . apply aNonzero
    exact aZero
  . apply bNonzero
    exact bZero

theorem mul.associative_reverse (y z : Nat, x : Nat)
  shows mul(x, mul(y, z)) = mul(mul(x, y), z)
proof
  simp [mul.associative]

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

-- The step law in the form a proof about n + 1 uses: (n + 1)! = (n + 1) · n!.
theorem factorial.succ (n : Nat)
  shows (n + 1)! = (n + 1) * n!
proof
  have one : n + 1 = succ(n) := add.right_one with *
  rw one
  simp [factorial]

theorem factorial.nonzero (n : Nat)
  shows n! ≠ 0
proof
  induction n
  | zero =>
    intro h
    simp [factorial] at h
  | k + 1 using ih =>
    intro h
    have step := factorial.succ with *
    rw step at h
    have zeroProduct := mul.eq_zero with h
    cases zeroProduct with hSucc | hFact
    . have one := add.right_one with *
      rw one at hSucc
      have impossible := Naturals.disjoint.zero.succ at k
      apply impossible
      simp
    . exact ih with hFact

lemma arithmetic.sample
  shows (17 + 25) * 3 = 126
proof
  compute

eval (17 + 25) * 3