-- Actual polynomial operation graphs and their commutative-ring structure (ZF).
-- 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.Polynomial.Ring
import Associativity

defunique polynomialPairAdd (I A add zero neg mul one t : Set) (s ∈ polynomials(I, A, zero)) :=
  ∃ p ∈ polynomials(I, A, zero), ∃ q ∈ polynomials(I, A, zero), t = (p, q) ∧ s = coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires pair : t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)
proof
  obtain ⟨bound, p, hp, q, hq, shape⟩ := product.membership.forward at
    polynomials(I, A, zero), polynomials(I, A, zero), t with pair
  have member := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  refine ⟨coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), member, p, hp, q, hq, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨p, hp, q, hq, shapeU, valueU⟩ := first
  obtain ⟨r, hr, s, hs, shapeV, valueV⟩ := second
  have equal : (p, q) = (r, s)
    cc
  have coordinates := orderedPair.injective at p, q, r, s with equal
  cc

defgraph polynomialAdd (I A add zero neg mul one : Set) (t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)) : polynomials(I, A, zero) := polynomialPairAdd(I, A, add, zero, neg, mul, one, t)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
proof
  have selected := polynomialPairAdd.selected at I, A, add, zero, neg, mul, one, t with *
  exact selected.left

notation scoped polynomialAdd(I, R) => polynomialAdd(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem polynomialAdd.apply (I A add zero neg mul one p q : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows (polynomialAdd(I, A, add, zero, neg, mul, one))(p, q) = coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q)
proof
  have pair := product.pair at p, q, polynomials(I, A, zero), polynomials(I, A, zero) with *
  have selected := polynomialPairAdd.selected at I, A, add, zero, neg, mul, one, (p, q) with *
  obtain ⟨r, hr, s, hs, shape, output⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := polynomialAdd.value at I, A, add, zero, neg, mul, one, (p, q) with *
  unfold call2
  cc

defunique polynomialPairMul (I A add zero neg mul one t : Set) (s ∈ polynomials(I, A, zero)) :=
  ∃ p ∈ polynomials(I, A, zero), ∃ q ∈ polynomials(I, A, zero), t = (p, q) ∧ s = polynomialProduct(I, A, add, zero, neg, mul, one, p, q)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
requires pair : t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)
proof
  obtain ⟨bound, p, hp, q, hq, shape⟩ := product.membership.forward with pair
  have member := polynomialProduct.member with hp, hq
  refine ⟨polynomialProduct(I, A, add, zero, neg, mul, one, p, q), member, p, hp, q, hq, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨p, hp, q, hq, shapeU, valueU⟩ := first
  obtain ⟨r, hr, s, hs, shapeV, valueV⟩ := second
  have equal : (p, q) = (r, s) by cc
  have coordinates := orderedPair.injective with equal
  cc

defgraph polynomialMul (I A add zero neg mul one : Set) (t ∈ polynomials(I, A, zero) × polynomials(I, A, zero)) : polynomials(I, A, zero) := polynomialPairMul(I, A, add, zero, neg, mul, one, t)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
proof
  have selected := polynomialPairMul.selected at I, A, add, zero, neg, mul, one, t with *
  exact selected.left

notation scoped polynomialMul(I, R) => polynomialMul(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem polynomialMul.apply (I A add zero neg mul one p q : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows (polynomialMul(I, A, add, zero, neg, mul, one))(p, q) = polynomialProduct(I, A, add, zero, neg, mul, one, p, q)
proof
  have pair := product.pair at p, q, polynomials(I, A, zero), polynomials(I, A, zero) with *
  have selected := polynomialPairMul.selected at I, A, add, zero, neg, mul, one, (p, q) with *
  obtain ⟨r, hr, s, hs, shape, output⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := polynomialMul.value at I, A, add, zero, neg, mul, one, (p, q) with *
  unfold call2
  cc

defgraph polynomialNeg (I A add zero neg mul one : Set) (p ∈ polynomials(I, A, zero)) : polynomials(I, A, zero) := coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)
requires ring : IsCommRing(A, add, zero, neg, mul, one)
proof
  exact polynomials.neg with *

notation scoped polynomialNeg(I, R) => polynomialNeg(I, R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem polynomialNeg.apply (I A add zero neg mul one p : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires member : p ∈ polynomials(I, A, zero)
  shows (polynomialNeg(I, A, add, zero, neg, mul, one))(p) = coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p)
proof
  exact polynomialNeg.value at I, A, add, zero, neg, mul, one, p with *

section Rings
variable (I A add zero neg mul one : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
notation ring P := (polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one))

theorem polynomials.add_commutative (p q : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows p + q = q + p
proof
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *
  have member1 := polynomials.add at I, A, add, zero, neg, mul, one, q, p with *
  have value1 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, q, p with *
  have law := coefficientAdd.commutative at monomials(I), A, add, zero, neg, mul, one, p, q with *
  cc

theorem polynomials.add_associative (p q r : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows (p + q) + r = p + (q + r)
proof
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have functionR := polynomials.function with memberR
  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *
  have member1 := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *
  have value1 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, q, r with *
  have member2 := polynomials.add at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *
  have value2 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *
  have member3 := polynomials.add at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *
  have value3 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *
  have law := coefficientAdd.associative at monomials(I), A, add, zero, neg, mul, one, p, q, r with *
  cc

theorem polynomials.add_zero (p : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  shows p + 0 = p
proof
  have functionP := polynomials.function with memberP
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero) with *
  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, constantFunction(monomials(I), A, zero) with *
  have law := coefficientAdd.zero with *
  cc

theorem polynomials.add_inverse (p : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  shows p + (-p) = 0
proof
  have functionP := polynomials.function with memberP
  have negative := polynomials.neg with *
  have negValue := polynomialNeg.apply at I, A, add, zero, neg, mul, one, p with *
  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *
  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p) with *
  have law := coefficientAdd.inverse with *
  cc

theorem polynomials.mul_commutative (p q : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  shows p * q = q * p
proof
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have member0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have value0 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *
  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, p with *
  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, p with *
  have law := polynomialProduct.commutative at I, A, add, zero, neg, mul, one, p, q with *
  cc

theorem polynomials.mul_associative (p q r : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows (p * q) * r = p * (q * r)
proof
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have functionR := polynomials.function with memberR
  have member0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have value0 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *
  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *
  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, r with *
  have member2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r with *
  have value2 := polynomialMul.apply at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), r with *
  have member3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *
  have value3 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *
  have law := polynomialProduct.associative at I, A, add, zero, neg, mul, one, p, q, r with *
  cc

theorem polynomials.mul_one (p : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  shows p * 1 = p
proof
  have functionP := polynomials.function with memberP
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have unitPolynomial := polynomialConstant.member at I, A, zero, one with *
  have member0 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one) with *
  have value0 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, polynomialConstant(I, A, zero, one) with *
  have law := polynomialProduct.one_right at I, A, add, zero, neg, mul, one, p with *
  cc

theorem polynomials.distribute_right (p q r : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows p * (q + r) = p * q + p * r
proof
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have functionR := polynomials.function with memberR
  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, q, r with *
  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, q, r with *
  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *
  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, q, r) with *
  have member2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, q with *
  have value2 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, q with *
  have member3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *
  have value3 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, r with *
  have member4 := polynomials.add at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *
  have value4 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, q), polynomialProduct(I, A, add, zero, neg, mul, one, p, r) with *
  have law := polynomialProduct.add_right at I, A, add, zero, neg, mul, one, p, q, r with *
  cc

theorem polynomials.distribute_left (p q r : Set)
  requires memberP : p ∈ polynomials(I, A, zero)
  requires memberQ : q ∈ polynomials(I, A, zero)
  requires memberR : r ∈ polynomials(I, A, zero)
  shows (p + q) * r = p * r + q * r
proof
  have functionP := polynomials.function with memberP
  have functionQ := polynomials.function with memberQ
  have functionR := polynomials.function with memberR
  have member0 := polynomials.add at I, A, add, zero, neg, mul, one, p, q with *
  have value0 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, p, q with *
  have member1 := polynomialProduct.member at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *
  have value1 := polynomialMul.apply at I, A, add, zero, neg, mul, one, coefficientAdd(monomials(I), A, add, zero, neg, mul, one, p, q), r with *
  have member2 := polynomialProduct.member at I, A, add, zero, neg, mul, one, p, r with *
  have value2 := polynomialMul.apply at I, A, add, zero, neg, mul, one, p, r with *
  have member3 := polynomialProduct.member at I, A, add, zero, neg, mul, one, q, r with *
  have value3 := polynomialMul.apply at I, A, add, zero, neg, mul, one, q, r with *
  have member4 := polynomials.add at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *
  have value4 := polynomialAdd.apply at I, A, add, zero, neg, mul, one, polynomialProduct(I, A, add, zero, neg, mul, one, p, r), polynomialProduct(I, A, add, zero, neg, mul, one, q, r) with *
  have law := polynomialProduct.add_left at I, A, add, zero, neg, mul, one, p, q, r with *
  cc

instance polynomials.comm_ring
  shows IsCommRing(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one))
proof
  have addition := polynomialAdd.function at I, A, add, zero, neg, mul, one with *
  have multiplication := polynomialMul.function at I, A, add, zero, neg, mul, one with *
  have negation := polynomialNeg.function at I, A, add, zero, neg, mul, one with *
  have zeroPolynomial := polynomials.zero at I, A, add, zero, neg, mul, one with *
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have multiplicative := IsRing.multiplicative with ordinary
  have oneIn := IsMonoid.unit_in_carrier with multiplicative
  have unitPolynomial := polynomialConstant.member at I, A, zero, one with *
  have addAssoc : Associative(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one))
    intros p hp q hq r hr
    exact polynomials.add_associative with *
  have addComm : Commutative(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one))
    intros p hp q hq
    exact polynomials.add_commutative with *
  have addIdentity : Identity(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero))
    constructor
    . exact zeroPolynomial
    . intros p hp
      have right := polynomials.add_zero with hp
      have comm := polynomials.add_commutative at I, A, add, zero, neg, mul, one, constantFunction(monomials(I), A, zero), p with *
      constructor
      . cc
      . exact right
  have inverses : Inverse(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one))
    constructor
    . exact negation
    . intros p hp
      have negative := polynomials.neg with hp
      have value := polynomialNeg.apply with hp
      have right := polynomials.add_inverse with hp
      have comm := polynomials.add_commutative at I, A, add, zero, neg, mul, one, coefficientNeg(monomials(I), A, add, zero, neg, mul, one, p), p with *
      constructor
      . cc
      . exact right
  have mulAssoc : Associative(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one))
    intros p hp q hq r hr
    exact polynomials.mul_associative with *
  have mulComm : Commutative(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one))
    intros p hp q hq
    exact polynomials.mul_commutative with *
  have mulIdentity : Identity(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one))
    constructor
    . exact unitPolynomial
    . intros p hp
      have right := polynomials.mul_one with hp
      have comm := polynomials.mul_commutative at I, A, add, zero, neg, mul, one, polynomialConstant(I, A, zero, one), p with *
      constructor
      . cc
      . exact right
  have distributive : Distributive(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), polynomialMul(I, A, add, zero, neg, mul, one))
    intros p hp q hq r hr
    constructor
    . exact polynomials.distribute_right with *
    . exact polynomials.distribute_left with *
  have additive : IsAbelianGroup(polynomials(I, A, zero), polynomialAdd(I, A, add, zero, neg, mul, one), constantFunction(monomials(I), A, zero), polynomialNeg(I, A, add, zero, neg, mul, one))
    unfold IsAbelianGroup
    refine ⟨_, addComm⟩
    unfold IsGroup
    refine ⟨_, inverses⟩
    unfold IsMonoid
    refine ⟨_, addIdentity⟩
    unfold IsSemigroup
    refine ⟨_, addAssoc⟩
    exact addition
  have multiplicativePolynomial : IsMonoid(polynomials(I, A, zero), polynomialMul(I, A, add, zero, neg, mul, one), polynomialConstant(I, A, zero, one))
    unfold IsMonoid
    refine ⟨_, mulIdentity⟩
    unfold IsSemigroup
    refine ⟨_, mulAssoc⟩
    exact multiplication
  constructor
  . unfold IsRing
    refine ⟨additive, multiplicativePolynomial, distributive⟩
  . exact mulComm

end Rings