-- Natural numbers inside a ring: ringNat(add, zero, one, n) is the n-fold sum
-- of one. Scoped ring numerals above 1 elaborate to it, and the ring tactic
-- adds and multiplies such coefficients through the laws proved here.
-- 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.Algebra.Ring.Numeral
import Core
import Nat.Core

def ringNat (plus z u : Set, n : Nat) → Set
  | plus, z, u, zero => z
  | plus, z, u, succ(k) => plus(ringNat(plus, z, u, k), u)

theorem ringNat.zero (add zero one : Set)
  shows ringNat(add, zero, one, 0) = zero
proof
  simp [ringNat]

theorem ringNat.succ (add zero one : Set, n : Nat)
  shows ringNat(add, zero, one, succ(n)) =
    call2(add, ringNat(add, zero, one, n), one)
proof
  simp [ringNat]

theorem IsRing.numeral_closed (A add zero neg mul one : Set, n : Nat)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  shows ringNat(add, zero, one, n) ∈ A
proof
  induction n
  | zero =>
    rw ringNat.zero
    exact IsRing.zero_in_carrier with ring
  | succ(k) using ih =>
    have monoid := IsRing.multiplicative with ring
    have oneInA := IsMonoid.unit_in_carrier with monoid
    rw ringNat.succ
    exact IsRing.add_closed with ring, ih, oneInA

theorem IsRing.numeral_one (A add zero neg mul one : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  shows ringNat(add, zero, one, 1) = one
proof
  have monoid := IsRing.multiplicative with ring
  have oneInA := IsMonoid.unit_in_carrier with monoid
  simp [ringNat]
  exact IsRing.add_left_identity with ring, oneInA

theorem IsCommRing.numeral_add (A add zero neg mul one : Set, m n : Nat)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  shows ringNat(add, zero, one, m + n) =
    call2(add, ringNat(add, zero, one, m), ringNat(add, zero, one, n))
proof
  induction n
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m
      with ordinary
    rw [add.right_unit, ringNat.zero]
    have rightIdentity := IsRing.add_right_identity with ordinary, mInA
    rw rightIdentity
    rfl
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m
      with ordinary
    have kInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, k
      with ordinary
    have monoid := IsRing.multiplicative with ordinary
    have oneInA := IsMonoid.unit_in_carrier with monoid
    rw [add.succ_right, ringNat.succ, ringNat.succ, ih]
    have reassociate := IsCommRing.add_assoc with ring, mInA, kInA, oneInA
    rw reassociate
    rfl

theorem IsCommRing.numeral_mul (A add zero neg mul one : Set, m n : Nat)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  shows ringNat(add, zero, one, m * n) =
    call2(mul, ringNat(add, zero, one, m), ringNat(add, zero, one, n))
proof
  induction n
  | zero =>
    have ordinary := IsCommRing.ring with ring
    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m
      with ordinary
    rw [mul.right_zero, ringNat.zero]
    have annihilate := IsRing.mul_zero with ordinary, mInA
    rw annihilate
    rfl
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have mInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, m
      with ordinary
    have kInA := IsRing.numeral_closed at A, add, zero, neg, mul, one, k
      with ordinary
    have monoid := IsRing.multiplicative with ordinary
    have oneInA := IsMonoid.unit_in_carrier with monoid
    have productInA := IsRing.mul_closed with ordinary, mInA, kInA
    rw [mul.succ_right, ringNat.succ]
    have split := IsCommRing.numeral_add at A, add, zero, neg, mul, one, m,
      m * k
      with ring
    rw [split, ih]
    have distribute := IsCommRing.mul_add with ring, mInA, kInA, oneInA
    have unit := IsCommRing.one_right with ring, mInA
    have commute := IsCommRing.add_comm with ring, mInA, productInA
    rw [distribute, unit, commute]
    rfl