-- Monomials as finitely supported natural-valued exponent maps (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.Monomial
import CoefficientSingle

def monomials (I : Set) : Set := coefficientMaps(I, ℕ, 0)
def monomialOne (I : Set) : Set := constantFunction(I, ℕ, 0)
def monomialVariable (I j : Set) : Set := coefficientSingle(I, ℕ, 0, 1, j)

theorem monomials.map (I m : Set)
  requires member : m ∈ monomials(I)
  shows CoefficientMap(m, I, ℕ, 0)
proof
  unfold monomials at member
  have data := coefficientMaps.membership.forward with member
  exact data.right

theorem monomials.contains (I m : Set)
  requires map : CoefficientMap(m, I, ℕ, 0)
  shows m ∈ monomials(I)
proof
  unfold monomials
  exact coefficientMaps.contains with map

theorem monomials.function (I m : Set)
  requires member : m ∈ monomials(I)
  shows m : I → ℕ
proof
  have map := monomials.map with member
  exact CoefficientMap.function with map

theorem monomials.exponent (I m i : Set)
  requires member : m ∈ monomials(I)
  requires index : i ∈ I
  shows Nat(m(i))
proof
  have function := monomials.function with member
  have value := FunctionBetween.apply_closed with function, index
  exact nat.omega.backward with value

theorem monomials.ext (I m n : Set)
  requires left : m ∈ monomials(I)
  requires right : n ∈ monomials(I)
  requires exponents : ∀ i ∈ I, m(i) = n(i)
  shows m = n
proof
  have functionM := monomials.function with left
  have functionN := monomials.function with right
  exact FunctionBetween.ext with functionM, functionN, exponents

theorem monomialOne.value (I i : Set)
  requires index : i ∈ I
  shows monomialOne(I)(i) = 0
proof
  have zeroIn := nat.omega.forward with Naturals.constructor.zero
  unfold monomialOne
  exact constantFunction.apply with *

theorem monomialOne.member (I : Set)
  shows monomialOne(I) ∈ monomials(I)
proof
  have zeroIn := nat.omega.forward with Naturals.constructor.zero
  have function : monomialOne(I) : I → ℕ
    unfold monomialOne
    exact constantFunction.function with *
  have support : functionSupport(monomialOne(I), I, 0) = ∅
    ext i
    constructor
    . intro member
      have data := functionSupport.membership.forward with member
      have value := monomialOne.value with data.left
      have contradiction := data.right with value
      tauto
    . intro member
      simp
  apply monomials.contains
  unfold CoefficientMap
  refine ⟨function, ?_⟩
  rw support
  exact Finite.empty

theorem monomialVariable.member (I j : Set)
  shows monomialVariable(I, j) ∈ monomials(I)
proof
  have zeroIn := nat.omega.forward with Naturals.constructor.zero
  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero
  have oneIn := nat.omega.forward with oneNat
  have map := CoefficientMap.single at I, ℕ, 0, 1, j with *
  apply monomials.contains
  unfold monomialVariable
  exact map

theorem monomialVariable.same (I j : Set)
  requires index : j ∈ I
  shows monomialVariable(I, j)(j) = 1
proof
  have zeroIn := nat.omega.forward with Naturals.constructor.zero
  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero
  have oneIn := nat.omega.forward with oneNat
  unfold monomialVariable
  exact coefficientSingle.same with *

theorem monomialVariable.other (I j i : Set)
  requires index : i ∈ I
  requires different : i ≠ j
  shows monomialVariable(I, j)(i) = 0
proof
  have zeroIn := nat.omega.forward with Naturals.constructor.zero
  have oneNat := Naturals.constructor.succ with Naturals.constructor.zero
  have oneIn := nat.omega.forward with oneNat
  unfold monomialVariable
  exact coefficientSingle.other with *

defgraph monomialProduct (I m n : Set) (i ∈ I) : ℕ := m(i) + n(i)
requires left : m ∈ monomials(I)
requires right : n ∈ monomials(I)
proof
  have mNat := monomials.exponent at I, m, i with *
  have nNat := monomials.exponent at I, n, i with *
  have sumNat : Nat(m(i) + n(i)) by typecheck
  exact nat.omega.forward with sumNat

theorem monomialProduct.support (I m n : Set)
  requires left : m ∈ monomials(I)
  requires right : n ∈ monomials(I)
  shows functionSupport(monomialProduct(I, m, n), I, 0) = functionSupport(m, I, 0) ∪ functionSupport(n, I, 0)
proof
  ext i
  constructor
  . intro member
    have data := functionSupport.membership.forward with member
    have value := monomialProduct.value at I, m, n, i with *
    have mNat := monomials.exponent at I, m, i with *
    have nNat := monomials.exponent at I, n, i with *
    have zeroSum : m(i) = 0 → n(i) = 0 → m(i) + n(i) = 0
      intros mZero nZero
      rw [mZero, nZero]
      compute
    have nonzeroSum : m(i) + n(i) ≠ 0
      intro equal
      have impossible : monomialProduct(I, m, n)(i) = 0 by cc
      exact data.right with impossible
    have memM := functionSupport.membership at m, I, 0, i
    have memN := functionSupport.membership at n, I, 0, i
    apply union2.membership.backward
    tauto
  . intro member
    have alternatives := union2.membership.forward with member
    have memM := functionSupport.membership at m, I, 0, i
    have memN := functionSupport.membership at n, I, 0, i
    have index : i ∈ I by tauto
    have mNat := monomials.exponent at I, m, i with *
    have nNat := monomials.exponent at I, n, i with *
    have value := monomialProduct.value at I, m, n, i with *
    have bothZero := add.eq_zero at n(i), m(i) with *
    have nonzero : monomialProduct(I, m, n)(i) ≠ 0
      intro equal
      have sumZero : m(i) + n(i) = 0 by cc
      have zeros := bothZero with sumZero
      tauto
    exact functionSupport.membership.backward with ⟨index, nonzero⟩

theorem monomialProduct.member (I m n : Set)
  requires left : m ∈ monomials(I)
  requires right : n ∈ monomials(I)
  shows monomialProduct(I, m, n) ∈ monomials(I)
proof
  have mapM := monomials.map with left
  have mapN := monomials.map with right
  have finiteM := CoefficientMap.finite_support with mapM
  have finiteN := CoefficientMap.finite_support with mapN
  have finite := Finite.union with finiteM, finiteN
  have support := monomialProduct.support with left, right
  have function := monomialProduct.function at I, m, n with *
  apply monomials.contains
  unfold CoefficientMap
  refine ⟨function, ?_⟩
  rwa support

theorem monomialProduct.commutative (I m n : Set)
  requires left : m ∈ monomials(I)
  requires right : n ∈ monomials(I)
  shows monomialProduct(I, m, n) = monomialProduct(I, n, m)
proof
  have productM := monomialProduct.member at I, m, n with *
  have productN := monomialProduct.member at I, n, m with *
  apply monomials.ext with productM, productN
  intros i hi
  have mNat := monomials.exponent at I, m, i with *
  have nNat := monomials.exponent at I, n, i with *
  have leftValue := monomialProduct.value at I, m, n, i with *
  have rightValue := monomialProduct.value at I, n, m, i with *
  rw [leftValue, rightValue]
  exact add.commutative with *

theorem monomialProduct.associative (I m n p : Set)
  requires first : m ∈ monomials(I)
  requires second : n ∈ monomials(I)
  requires third : p ∈ monomials(I)
  shows monomialProduct(I, monomialProduct(I, m, n), p) = monomialProduct(I, m, monomialProduct(I, n, p))
proof
  have mn := monomialProduct.member at I, m, n with *
  have np := monomialProduct.member at I, n, p with *
  have left := monomialProduct.member at I, monomialProduct(I, m, n), p with *
  have right := monomialProduct.member at I, m, monomialProduct(I, n, p) with *
  apply monomials.ext with left, right
  intros i hi
  have mNat := monomials.exponent at I, m, i with *
  have nNat := monomials.exponent at I, n, i with *
  have pNat := monomials.exponent at I, p, i with *
  have mnValue := monomialProduct.value at I, m, n, i with *
  have npValue := monomialProduct.value at I, n, p, i with *
  have leftValue := monomialProduct.value at I, monomialProduct(I, m, n), p, i with *
  have rightValue := monomialProduct.value at I, m, monomialProduct(I, n, p), i with *
  rw [leftValue, rightValue, mnValue, npValue]
  exact add.associative with *

theorem monomialProduct.one (I m : Set)
  requires member : m ∈ monomials(I)
  shows monomialProduct(I, m, monomialOne(I)) = m
proof
  have unit := monomialOne.member at I
  have product := monomialProduct.member at I, m, monomialOne(I) with *
  apply monomials.ext with product, member
  intros i hi
  have mNat := monomials.exponent at I, m, i with *
  have value := monomialProduct.value at I, m, monomialOne(I), i with *
  have unitValue := monomialOne.value at I, i with *
  rw [value, unitValue]
  exact add.right_unit at m(i) with *

theorem monomialProduct.cancel (I m n p : Set)
  requires first : m ∈ monomials(I)
  requires second : n ∈ monomials(I)
  requires third : p ∈ monomials(I)
  requires equal : monomialProduct(I, m, n) = monomialProduct(I, m, p)
  shows n = p
proof
  apply monomials.ext with second, third
  intros i hi
  have mNat := monomials.exponent at I, m, i with *
  have nNat := monomials.exponent at I, n, i with *
  have pNat := monomials.exponent at I, p, i with *
  have leftValue := monomialProduct.value at I, m, n, i with *
  have rightValue := monomialProduct.value at I, m, p, i with *
  have sums : m(i) + n(i) = m(i) + p(i) by cc
  exact add.left_cancel with mNat, sums

defunique monomialPairProduct (I p : Set) (result ∈ monomials(I)) :=
  ∃ m ∈ monomials(I), ∃ n ∈ monomials(I), p = (m, n) ∧ result = monomialProduct(I, m, n)
requires pair : p ∈ monomials(I) × monomials(I)
proof
  obtain ⟨bound, m, hm, n, hn, shape⟩ := product.membership.forward with pair
  have member := monomialProduct.member with hm, hn
  refine ⟨monomialProduct(I, m, n), member, m, hm, n, hn, shape, rfl⟩
uniqueness
  intros u hu first v hv second
  obtain ⟨m, hm, n, hn, shapeU, valueU⟩ := first
  obtain ⟨q, hq, r, hr, shapeV, valueV⟩ := second
  have pairs : (m, n) = (q, r) by cc
  have coordinates := orderedPair.injective with pairs
  cc

defgraph monomialMul (I : Set) (p ∈ monomials(I) × monomials(I)) : monomials(I) := monomialPairProduct(I, p)
proof
  have selected := monomialPairProduct.selected with member
  exact selected.left

theorem monomialMul.apply (I m n : Set)
  requires left : m ∈ monomials(I)
  requires right : n ∈ monomials(I)
  shows (monomialMul(I))(m, n) = monomialProduct(I, m, n)
proof
  have pair := product.pair at m, n, monomials(I), monomials(I) with *
  have selected := monomialPairProduct.selected with pair
  obtain ⟨q, hq, r, hr, shape, output⟩ := selected.right
  have coordinates := orderedPair.injective with shape
  have value := monomialMul.value with pair
  unfold call2
  cc

theorem monomials.comm_monoid (I : Set)
  shows IsCommMonoid(monomials(I), monomialMul(I), monomialOne(I))
proof
  have operation := monomialMul.function at I
  have unit := monomialOne.member at I
  have associative : Associative(monomials(I), monomialMul(I))
    intros m hm n hn p hp
    have mn := monomialProduct.member with hm, hn
    have np := monomialProduct.member with hn, hp
    have leftInner := monomialMul.apply with hm, hn
    have rightInner := monomialMul.apply with hn, hp
    rw [leftInner, rightInner]
    have leftOuter := monomialMul.apply at I, monomialProduct(I, m, n), p with *
    have rightOuter := monomialMul.apply at I, m, monomialProduct(I, n, p) with *
    rw [leftOuter, rightOuter]
    exact monomialProduct.associative with *
  have identity : Identity(monomials(I), monomialMul(I), monomialOne(I))
    unfold Identity
    refine ⟨unit, ?_⟩
    intros m hm
    have leftValue := monomialMul.apply at I, monomialOne(I), m with *
    have rightValue := monomialMul.apply at I, m, monomialOne(I) with *
    have comm := monomialProduct.commutative at I, monomialOne(I), m with *
    have identity := monomialProduct.one with hm
    constructor
    . cc
    . cc
  have commutative : Commutative(monomials(I), monomialMul(I))
    intros m hm n hn
    have leftValue := monomialMul.apply with hm, hn
    have rightValue := monomialMul.apply with hn, hm
    have comm := monomialProduct.commutative with hm, hn
    cc
  unfold IsCommMonoid
  refine ⟨?_, commutative⟩
  unfold IsMonoid
  refine ⟨?_, identity⟩
  unfold IsSemigroup
  refine ⟨?_, associative⟩
  exact operation

theorem monomialVariable.injective (I j k : Set)
  requires first : j ∈ I
  requires second : k ∈ I
  requires equal : monomialVariable(I, j) = monomialVariable(I, k)
  shows j = k
proof
  have alternatives : j = k ∨ j ≠ k by tauto
  cases alternatives with same | different
  . exact same
  . have valueJ := monomialVariable.same with first
    have valueK := monomialVariable.other with first, different
    have impossible : 0 = 1 by cc
    exfalso
    exact Naturals.disjoint.zero.succ at 0 with impossible