-- Core ring theory
-- 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.Core
import Group.Basic
import Defs

theorem IsSemiring.distributive (A add zero mul one : Set)
  requires h : IsSemiring(A, add, zero, mul, one)
  shows Distributive(A, add, mul)
proof
  simp [IsSemiring]

theorem IsRing.additive (A add zero neg mul one : Set)
  requires h : IsRing(A, add, zero, neg, mul, one)
  shows IsAbelianGroup(A, add, zero, neg)
proof
  simp [IsRing]

theorem IsRing.multiplicative (A add zero neg mul one : Set)
  requires h : IsRing(A, add, zero, neg, mul, one)
  shows IsMonoid(A, mul, one)
proof
  simp [IsRing]

theorem IsRing.distributive (A add zero neg mul one : Set)
  requires h : IsRing(A, add, zero, neg, mul, one)
  shows Distributive(A, add, mul)
proof
  simp [IsRing]

theorem IsRing.add_closed (A add zero neg mul one x y : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows call2(add, x, y) ∈ A
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have monoid := IsGroup.monoid with group
  exact IsMonoid.closed with monoid, xInA, yInA

theorem IsRing.neg_closed (A add zero neg mul one x : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  shows neg(x) ∈ A
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  exact IsGroup.inverse_closed with group, xInA

theorem IsRing.zero_in_carrier (A add zero neg mul one : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  shows zero ∈ A
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have monoid := IsGroup.monoid with group
  exact IsMonoid.unit_in_carrier with monoid

theorem IsRing.add_associative (A add zero neg mul one : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  shows Associative(A, add)
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have monoid := IsGroup.monoid with group
  exact IsMonoid.associative with monoid

theorem IsRing.add_left_identity (A add zero neg mul one x : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  shows call2(add, zero, x) = x
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have monoid := IsGroup.monoid with group
  exact IsMonoid.left_identity with monoid, xInA

theorem IsRing.add_right_identity (A add zero neg mul one x : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  shows call2(add, x, zero) = x
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have monoid := IsGroup.monoid with group
  exact IsMonoid.right_identity with monoid, xInA

theorem IsRing.add_inverse_left (A add zero neg mul one x : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  shows call2(add, neg(x), x) = zero
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  exact IsGroup.inverse_left with group, xInA

theorem IsRing.add_inverse_right (A add zero neg mul one x : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  shows call2(add, x, neg(x)) = zero
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  exact IsGroup.inverse_right with group, xInA

theorem IsRing.mul_closed (A add zero neg mul one x y : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows call2(mul, x, y) ∈ A
proof
  have multiplicative := IsRing.multiplicative with ring
  exact IsMonoid.closed with multiplicative, xInA, yInA

theorem IsRing.zero_mul (A add zero neg mul one x : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  shows call2(mul, zero, x) = zero
proof
  have zeroInA := IsRing.zero_in_carrier with ring
  have productInA := IsRing.mul_closed with ring, zeroInA, xInA
  have distributive := IsRing.distributive with ring
  obtain ⟨leftLaw, rightLaw⟩ := distributive with zero, zeroInA, zero, zeroInA, x, xInA
  have zeroPlusZero := IsRing.add_left_identity with ring, zeroInA
  rw zeroPlusZero at rightLaw
  have negProductInA := IsRing.neg_closed with ring, productInA
  have associative := IsRing.add_associative with ring
  have reassociate := Associative.law with associative, negProductInA, productInA, productInA
  have inverse := IsRing.add_inverse_left with ring, productInA
  have identity := IsRing.add_left_identity with ring, productInA
  cc

theorem IsRing.mul_zero (A add zero neg mul one x : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  shows call2(mul, x, zero) = zero
proof
  have zeroInA := IsRing.zero_in_carrier with ring
  have productInA := IsRing.mul_closed with ring, xInA, zeroInA
  have distributive := IsRing.distributive with ring
  obtain ⟨leftLaw, rightLaw⟩ := distributive with x, xInA, zero, zeroInA, zero, zeroInA
  have zeroPlusZero := IsRing.add_left_identity with ring, zeroInA
  rw zeroPlusZero at leftLaw
  have negProductInA := IsRing.neg_closed with ring, productInA
  have associative := IsRing.add_associative with ring
  have reassociate := Associative.law with associative, negProductInA, productInA, productInA
  have inverse := IsRing.add_inverse_left with ring, productInA
  have identity := IsRing.add_left_identity with ring, productInA
  cc

theorem IsRing.neg_mul (A add zero neg mul one x y : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows call2(mul, neg(x), y) = neg(call2(mul, x, y))
proof
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have monoid := IsGroup.monoid with group
  have negXInA := IsRing.neg_closed with ring, xInA
  have productInA := IsRing.mul_closed with ring, xInA, yInA
  have negProductInA := IsRing.neg_closed with ring, productInA
  have candidateInA := IsRing.mul_closed with ring, negXInA, yInA
  have distributive := IsRing.distributive with ring
  obtain ⟨leftLaw, rightLaw⟩ := distributive with neg(x), negXInA, x, xInA, y, yInA
  have inverseX := IsRing.add_inverse_left with ring, xInA
  have zeroProduct := IsRing.zero_mul with ring, yInA
  rw [inverseX, zeroProduct] at rightLaw
  have commutative := IsAbelianGroup.commutative with additive
  have candidateSwap := commutative with
    call2(mul, neg(x), y), candidateInA,
    call2(mul, x, y), productInA
  have candidateLeft : call2(add,
      call2(mul, neg(x), y), call2(mul, x, y)) = zero
    cc
  have candidateRight : call2(add,
      call2(mul, x, y), call2(mul, neg(x), y)) = zero
    cc
  have canonical : IsInverse(A, add, zero,
      call2(mul, x, y), neg(call2(mul, x, y)))
    unfold IsInverse
    refine ⟨productInA, negProductInA, _, _⟩
    . exact IsRing.add_inverse_left at
        A, add, zero, neg, mul, one, call2(mul, x, y) with ring, productInA
    . exact IsRing.add_inverse_right at
        A, add, zero, neg, mul, one, call2(mul, x, y) with ring, productInA
  have candidate : IsInverse(A, add, zero,
      call2(mul, x, y), call2(mul, neg(x), y))
    unfold IsInverse
    refine ⟨productInA, candidateInA, candidateLeft, candidateRight⟩
  have unique := IsInverse.unique with monoid, canonical, candidate
  cc

theorem CommSemiring.semiring (A add zero mul one : Set)
  requires h : CommSemiring(A, add, zero, mul, one)
  shows IsSemiring(A, add, zero, mul, one)
proof
  simp [CommSemiring]

theorem CommSemiring.commutative (A add zero mul one : Set)
  requires h : CommSemiring(A, add, zero, mul, one)
  shows Commutative(A, mul)
proof
  simp [CommSemiring]

theorem IsCommRing.ring (A add zero neg mul one : Set)
  requires h : IsCommRing(A, add, zero, neg, mul, one)
  shows IsRing(A, add, zero, neg, mul, one)
proof
  simp [IsCommRing]

theorem IsCommRing.commutative (A add zero neg mul one : Set)
  requires h : IsCommRing(A, add, zero, neg, mul, one)
  shows Commutative(A, mul)
proof
  simp [IsCommRing]

theorem IsCommRing.add_commutative (A add zero neg mul one : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  shows Commutative(A, add)
proof
  have ordinary := IsCommRing.ring with ring
  have additive := IsRing.additive with ordinary
  exact IsAbelianGroup.commutative with additive

-- Direct equational laws used by checked polynomial normalization.
theorem IsCommRing.add_comm (A add zero neg mul one x y : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows call2(add, x, y) = call2(add, y, x)
proof
  have comm := IsCommRing.add_commutative with ring
  exact comm with x, hx, y, hy

theorem IsCommRing.add_assoc (A add zero neg mul one x y z : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows call2(add, call2(add, x, y), z) = call2(add, x, call2(add, y, z))
proof
  have ordinary := IsCommRing.ring with ring
  have associative := IsRing.add_associative with ordinary
  exact Associative.law with associative, hx, hy, hz

theorem IsCommRing.add_swap (A add zero neg mul one x y z : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows call2(add, x, call2(add, y, z)) = call2(add, y, call2(add, x, z))
proof
  have xy := IsCommRing.add_comm with ring, hx, hy
  have lhs := IsCommRing.add_assoc with ring, hx, hy, hz
  have rhs := IsCommRing.add_assoc with ring, hy, hx, hz
  cc

theorem IsCommRing.neg_add (A add zero neg mul one x y : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows neg(call2(add, x, y)) = call2(add, neg(x), neg(y))
proof
  have ordinary := IsCommRing.ring with ring
  have group := IsRing.additive with ordinary
  exact IsAbelianGroup.inverse_op with group, hx, hy

theorem IsCommRing.neg_neg (A add zero neg mul one x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  shows neg(neg(x)) = x
proof
  have ordinary := IsCommRing.ring with ring
  have additive := IsRing.additive with ordinary
  have group := IsAbelianGroup.group with additive
  exact IsGroup.inverse_involutive with group, hx

theorem IsCommRing.neg_zero (A add zero neg mul one : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  shows neg(zero) = zero
proof
  have ordinary := IsCommRing.ring with ring
  have additive := IsRing.additive with ordinary
  have group := IsAbelianGroup.group with additive
  exact IsGroup.inverse_unit with group

theorem IsCommRing.mul_comm (A add zero neg mul one x y : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows call2(mul, x, y) = call2(mul, y, x)
proof
  have comm := IsCommRing.commutative with ring
  exact comm with x, hx, y, hy

theorem IsCommRing.mul_assoc (A add zero neg mul one x y z : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows call2(mul, call2(mul, x, y), z) = call2(mul, x, call2(mul, y, z))
proof
  have ordinary := IsCommRing.ring with ring
  have multiplicative := IsRing.multiplicative with ordinary
  have associative := IsMonoid.associative with multiplicative
  exact Associative.law with associative, hx, hy, hz

theorem IsCommRing.mul_swap (A add zero neg mul one x y z : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows call2(mul, x, call2(mul, y, z)) = call2(mul, y, call2(mul, x, z))
proof
  have xy := IsCommRing.mul_comm with ring, hx, hy
  have lhs := IsCommRing.mul_assoc with ring, hx, hy, hz
  have rhs := IsCommRing.mul_assoc with ring, hy, hx, hz
  cc

theorem IsCommRing.one_left (A add zero neg mul one x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  shows call2(mul, one, x) = x
proof
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  exact IsMonoid.left_identity with monoid, hx

theorem IsCommRing.one_right (A add zero neg mul one x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  shows call2(mul, x, one) = x
proof
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  exact IsMonoid.right_identity with monoid, hx

theorem IsCommRing.mul_add (A add zero neg mul one x y z : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows call2(mul, x, call2(add, y, z)) =
    call2(add, call2(mul, x, y), call2(mul, x, z))
proof
  have ordinary := IsCommRing.ring with ring
  have distributive := IsRing.distributive with ordinary
  obtain ⟨left, right⟩ := distributive with x, hx, y, hy, z, hz
  exact left

theorem IsCommRing.add_mul (A add zero neg mul one x y z : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  shows call2(mul, call2(add, x, y), z) =
    call2(add, call2(mul, x, z), call2(mul, y, z))
proof
  have ordinary := IsCommRing.ring with ring
  have distributive := IsRing.distributive with ordinary
  obtain ⟨left, right⟩ := distributive with x, hx, y, hy, z, hz
  exact right

theorem IsCommRing.mul_neg (A add zero neg mul one x y : Set)
  requires commRing : IsCommRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows call2(mul, x, neg(y)) = neg(call2(mul, x, y))
proof
  have ring := IsCommRing.ring with commRing
  have negYInA := IsRing.neg_closed with ring, yInA
  have commutative := IsCommRing.commutative with commRing
  have leftSwap := commutative with x, xInA, neg(y), negYInA
  have rightSwap := commutative with x, xInA, y, yInA
  have negated := IsRing.neg_mul with ring, yInA, xInA
  cc

theorem IsCommRing.neg_mul_neg (A add zero neg mul one x y : Set)
  requires commRing : IsCommRing(A, add, zero, neg, mul, one)
  requires xInA : x ∈ A
  requires yInA : y ∈ A
  shows call2(mul, neg(x), neg(y)) = call2(mul, x, y)
proof
  have ring := IsCommRing.ring with commRing
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have negYInA := IsRing.neg_closed with ring, yInA
  have outerNeg := IsRing.neg_mul with ring, xInA, negYInA
  have innerNeg := IsCommRing.mul_neg with commRing, xInA, yInA
  have productInA := IsRing.mul_closed with ring, xInA, yInA
  have involutive := IsGroup.inverse_involutive with group, productInA
  cc

theorem Nontrivial.distinct (A zero one : Set)
  requires h : Nontrivial(A, zero, one)
  shows zero ≠ one
proof
  simp [Nontrivial]

theorem IsIntegralDomain.comm_ring (A add zero neg mul one : Set)
  requires h : IsIntegralDomain(A, add, zero, neg, mul, one)
  shows IsCommRing(A, add, zero, neg, mul, one)
proof
  simp [IsIntegralDomain]

theorem IsIntegralDomain.nontrivial (A add zero neg mul one : Set)
  requires h : IsIntegralDomain(A, add, zero, neg, mul, one)
  shows Nontrivial(A, zero, one)
proof
  simp [IsIntegralDomain]

theorem IsIntegralDomain.no_zero_divisors (A add zero neg mul one : Set)
  requires h : IsIntegralDomain(A, add, zero, neg, mul, one)
  shows NoZeroDivisors(A, mul, zero)
proof
  simp [IsIntegralDomain]