-- Coordinatewise monomial divisibility and quotient monomials (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.Divisibility
import Monomial

predicate MonomialDivides (I m n : Set) := ∀ i ∈ I, m(i) ≤ n(i)

theorem MonomialDivides.reflexive (I m : Set)
  requires member : m ∈ monomials(I)
  shows MonomialDivides(I, m, m)
proof
  intros i hi
  have natural := monomials.exponent with *
  exact LessEqual.reflexive with *

theorem MonomialDivides.transitive (I m n p : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : n ∈ monomials(I)
  requires third : p ∈ monomials(I)
  requires left : MonomialDivides(I, m, n)
  requires right : MonomialDivides(I, n, p)
  shows MonomialDivides(I, m, p)
proof
  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 mn := left with i, hi
  have np := right with i, hi
  exact LessEqual.transitive with *

theorem MonomialDivides.antisymmetric (I m n : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : n ∈ monomials(I)
  requires left : MonomialDivides(I, m, n)
  requires right : MonomialDivides(I, n, m)
  shows m = n
proof
  apply monomials.ext with memberM, memberN
  intros i hi
  have mNat := monomials.exponent at I, m, i with *
  have nNat := monomials.exponent at I, n, i with *
  have mn := left with i, hi
  have nm := right with i, hi
  exact LessEqual.antisymmetric with *

theorem MonomialDivides.insert (I j m n : Set)
  requires previous : MonomialDivides(I, m, n)
  requires coordinate : m(j) ≤ n(j)
  shows MonomialDivides(insert(j, I), m, n)
proof
  intros i hi
  have alternatives := insert.membership.forward with hi
  cases alternatives with equal | old
  . rw equal
    exact coordinate
  . exact previous with i, old

defunique naturalDifference (a b : Nat) (k ∈ ℕ) := a + k = b
requires bounded : a ≤ b
proof
  obtain ⟨k, natural, equation⟩ := bounded
  have member := nat.omega.forward with natural
  refine ⟨k, member, equation⟩
uniqueness
  intros u hu memberM v hv memberN
  have equal : a + u = a + v by cc
  exact add.left_cancel with equal

theorem naturalDifference.natural (a b : Nat)
  requires bounded : a ≤ b
  shows Nat(naturalDifference(a, b))
proof
  have selected := naturalDifference.selected at a, b with *
  exact nat.omega.backward with selected.left

theorem naturalDifference.add (a b : Nat)
  requires bounded : a ≤ b
  shows a + naturalDifference(a, b) = b
proof
  have selected := naturalDifference.selected at a, b with *
  exact selected.right

defgraph monomialQuotient (I m n : Set) (i ∈ I) : ℕ := naturalDifference(m(i), n(i))
requires memberM : m ∈ monomials(I)
requires memberN : n ∈ monomials(I)
requires divides : MonomialDivides(I, m, n)
proof
  have mNat := monomials.exponent at I, m, i with *
  have nNat := monomials.exponent at I, n, i with *
  have bounded := divides with i, member
  have selected := naturalDifference.selected at m(i), n(i) with *
  exact selected.left

theorem monomialQuotient.equation (I m n i : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : n ∈ monomials(I)
  requires divides : MonomialDivides(I, m, n)
  requires index : i ∈ I
  shows m(i) + monomialQuotient(I, m, n)(i) = n(i)
proof
  have value := monomialQuotient.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 bounded := divides with i, index
  rw value
  exact naturalDifference.add with *

theorem monomialQuotient.support (I m n : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : n ∈ monomials(I)
  requires divides : MonomialDivides(I, m, n)
  shows functionSupport(monomialQuotient(I, m, n), I, 0) ⊆ functionSupport(n, I, 0)
proof
  have function := monomialQuotient.function at I, m, n with *
  intros i hi
  have data := functionSupport.membership.forward with hi
  have mNat := monomials.exponent at I, m, i with *
  have valueIn := FunctionBetween.apply_closed at monomialQuotient(I, m, n), I, ℕ, i with *
  have qNat := nat.omega.backward with valueIn
  have equation := monomialQuotient.equation at I, m, n, i with *
  have nonzero : n(i) ≠ 0
    intro zeroValue
    rw zeroValue at equation
    have zeros := add.eq_zero at monomialQuotient(I, m, n)(i), m(i) with *
    have both := zeros with equation
    exact data.right with both.right
  exact functionSupport.membership.backward with ⟨data.left, nonzero⟩

theorem monomialQuotient.member (I m n : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : n ∈ monomials(I)
  requires divides : MonomialDivides(I, m, n)
  shows monomialQuotient(I, m, n) ∈ monomials(I)
proof
  have map := monomials.map with memberN
  have finite := CoefficientMap.finite_support with map
  have support := monomialQuotient.support with *
  have finiteQ := Finite.subset with finite, support
  have function := monomialQuotient.function at I, m, n with *
  apply monomials.contains
  unfold CoefficientMap
  refine ⟨function, finiteQ⟩

theorem monomialQuotient.product (I m n : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : n ∈ monomials(I)
  requires divides : MonomialDivides(I, m, n)
  shows monomialProduct(I, m, monomialQuotient(I, m, n)) = n
proof
  have quotient := monomialQuotient.member with *
  have product := monomialProduct.member at I, m, monomialQuotient(I, m, n) with *
  apply monomials.ext with product, memberN
  intros i hi
  have value := monomialProduct.value at I, m, monomialQuotient(I, m, n), i with *
  rw value
  exact monomialQuotient.equation with *

theorem MonomialDivides.product (I m q : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : q ∈ monomials(I)
  shows MonomialDivides(I, m, monomialProduct(I, m, q))
proof
  intros i hi
  have mNat := monomials.exponent at I, m, i with *
  have qNat := monomials.exponent at I, q, i with *
  have value := monomialProduct.value at I, m, q, i with *
  rw value
  exact LessEqual.add_right with *

theorem MonomialDivides.iff_factor (I m n : Set)
  requires memberM : m ∈ monomials(I)
  requires memberN : n ∈ monomials(I)
  shows MonomialDivides(I, m, n) ↔ ∃ q ∈ monomials(I), monomialProduct(I, m, q) = n
proof
  constructor
  . intro divides
    have quotient := monomialQuotient.member with *
    have product := monomialQuotient.product with *
    refine ⟨monomialQuotient(I, m, n), quotient, product⟩
  . intro factored
    obtain ⟨q, member, equation⟩ := factored
    have divides := MonomialDivides.product at I, m, q with *
    rwa equation at divides