-- Removing zero summands from finite ring sums, without Choice.
-- 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.SumSupport
import SumExtension

section Rings
variable (A add zero neg mul one w : Set)
hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)
notation ring R := (A, add, zero, neg, mul, one)

theorem matchingRingRow.zero (f x : Set, n : Nat)
  requires vanishes : w(x) = zero
  shows matchingRingRow(A, zero, add, w, f, x, n) = zero
proof
  induction n
  | zero =>
    rw matchingRingRow
    rfl
  | succ(k) using ih =>
    have ordinary := IsCommRing.ring with ring
    have zeroIn := IsRing.zero_in_carrier with ordinary
    have value : w(x) ∈ A
      rwa vanishes
    have alternatives : f(k) = x ∨ f(k) ≠ x by tauto
    have entry : singleValue(A, zero, w(x), x, f(k)) = zero
      cases alternatives with same | different
      . have selected := singleValue.same at A, zero, w(x), x, f(k) with *
        cc
      . exact singleValue.other at A, zero, w(x), x, f(k) with *
    rw [matchingRingRow, ih, entry]
    ring

theorem matchingRingRow.covered_or_zero (f x : Set, n : Nat)
  requires value : w(x) ∈ A
  requires distinct : DistinctValues(f, n)
  requires covered : Occurs(f, n, x) ∨ w(x) = zero
  shows matchingRingRow(A, zero, add, w, f, x, n) = w(x)
proof
  cases covered with occurs | vanishes
  . have unique := matchingRingRow.unique at A, add, zero, neg, mul, one, w, f, x, n with *
    exact unique with distinct, occurs
  . have empty := matchingRingRow.zero at A, add, zero, neg, mul, one, w, f, x, n with *
    cc

theorem matchingRingTotal.support_sum (f g : Set, n m : Nat)
  requires distinct : DistinctValues(f, n)
  shows WeightedValues(w, g, A, m) → (∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = zero) →
    matchingRingTotal(A, zero, add, w, f, g, n, m) = indexedRingSum(w, g, add, zero, m)
proof
  induction m
  | zero =>
    intros values covered
    simp [matchingRingTotal, indexedRingSum]
  | succ(k) using ih =>
    intros values covered
    have prefix : ∀ j ∈ k, Occurs(f, n, g(j)) ∨ w(g(j)) = zero
      intros j before
      have included := membership.into_successor at j, k with *
      exact covered with j, included
    have last := covered with k, membership.self_successor at k with *
    have valuePrefix := WeightedValues.prefix at w, g, A, k with *
    have valueLast := WeightedValues.last at w, g, A, k with *
    have row := matchingRingRow.covered_or_zero at A, add, zero, neg, mul, one, w, f, g(k), n with *
    have previous := ih with valuePrefix, prefix
    rw [matchingRingTotal, indexedRingSum, previous, row]
    rfl

theorem indexedRingSum.same_nonzero_entries (f g : Set, n m : Nat)
  requires valuesF : WeightedValues(w, f, A, n)
  requires valuesG : WeightedValues(w, g, A, m)
  requires distinctF : DistinctValues(f, n)
  requires distinctG : DistinctValues(g, m)
  requires coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = zero
  requires coveredG : ∀ j ∈ m, Occurs(f, n, g(j)) ∨ w(g(j)) = zero
  shows indexedRingSum(w, f, add, zero, n) = indexedRingSum(w, g, add, zero, m)
proof
  have left := matchingRingTotal.support_sum at A, add, zero, neg, mul, one, w, g, f, m, n with *, valuesF, coveredF
  have right := matchingRingTotal.support_sum at A, add, zero, neg, mul, one, w, f, g, n, m with *, valuesG, coveredG
  have transpose := matchingRingTotal.transpose at A, add, zero, neg, mul, one, w, f, g, m, n with *
  rw [← left, ← right]
  symm
  exact transpose with valuesF

end Rings

theorem finiteRingSum.restrict (V S A add zero neg mul one w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weights : w : V → A
  requires subset : S ⊆ V
  requires vanishes : ∀ x ∈ V, ¬(x ∈ S) → w(x) = zero
  shows finiteRingSum(V, A, add, zero, neg, mul, one, w) =
    finiteRingSum(S, A, add, zero, neg, mul, one, restrict(w, S))
proof
  have finiteS := Finite.subset with finite, subset
  have closed : ∀ x ∈ S, w(x) ∈ A
    intros x hx
    have included := subset
    have member := included with x, hx
    exact FunctionBetween.apply_closed with *
  have restricted := restrict.function with *
  have selectedV := finiteRingSum.selected at V, A, add, zero, neg, mul, one, w with *
  have selectedS := finiteRingSum.selected at S, A, add, zero, neg, mul, one, restrict(w, S) with *
  obtain ⟨n, naturalN, f, enumerationF, equationV⟩ := selectedV.right
  obtain ⟨m, naturalM, g, enumerationG, equationS⟩ := selectedS.right
  have injF := Bijective.injective with enumerationF
  have injG := Bijective.injective with enumerationG
  have surjF := Bijective.surjective with enumerationF
  have surjG := Bijective.surjective with enumerationG
  have functionF := Injective.function with injF
  have functionG := Injective.function with injG
  have distinctF := Injective.distinct_values with injF
  have distinctG := Injective.distinct_values with injG
  have valuesF := WeightedValues.of_functions with weights, functionF
  have valuesG : WeightedValues(w, g, A, m)
    intros i hi
    have member := FunctionBetween.apply_closed with *
    exact closed with g(i), member
  have coveredF : ∀ i ∈ n, Occurs(g, m, f(i)) ∨ w(f(i)) = zero
    intros i hi
    have member := FunctionBetween.apply_closed with *
    have alternatives : f(i) ∈ S ∨ ¬(f(i) ∈ S) by tauto
    cases alternatives with inside | outside
    . left
      exact Surjective.occurs with *
    . right
      exact vanishes with f(i), member, outside
  have coveredG : ∀ i ∈ m, Occurs(f, n, g(i)) ∨ w(g(i)) = zero
    intros i hi
    have inS := FunctionBetween.apply_closed with *
    have included := subset
    have inV := included with g(i), inS
    left
    exact Surjective.occurs with *
  have same := indexedRingSum.same_nonzero_entries with valuesF, valuesG, distinctF, distinctG, coveredF, coveredG
  have pointwise : ∀ i ∈ m, w(g(i)) = restrict(w, S)(g(i))
    intros i hi
    have inS := FunctionBetween.apply_closed with *
    symm
    exact restrict.apply with *
  have congr := indexedRingSum.congr at w, restrict(w, S), g, g, add, zero, m with naturalM
  have equal := congr with pointwise
  cc

theorem finiteRingSum.reindex (D E A add zero neg mul one w v f : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : E → A
  requires bijective : BijectiveBetween(f, D, E)
  requires values : ∀ d ∈ D, w(d) = v(f(d))
  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = finiteRingSum(E, A, add, zero, neg, mul, one, v)
proof
  have selected := finiteRingSum.selected at D, A, add, zero, neg, mul, one, w with *
  obtain ⟨n, natural, g, enumeration, equation⟩ := selected.right
  have composed := compose.bijective at f, g, n, D, E with *
  have injF := Bijective.injective with bijective
  have injG := Bijective.injective with enumeration
  have functionF := Injective.function with injF
  have functionG := Injective.function with injG
  have equationV := finiteRingSum.enumeration at E, A, add, zero, neg, mul, one, v, compose(f, g, n, D, E), n with *
  have pointwise : ∀ i ∈ n, w(g(i)) = v(compose(f, g, n, D, E)(i))
    intros i hi
    have member := FunctionBetween.apply_closed at g, n, D, i with *
    have value := values with g(i), member
    have composite := compose.apply at f, g, n, D, E, i with *
    cc
  have congr := indexedRingSum.congr at w, v, g, compose(f, g, n, D, E), add, zero, n with natural
  have same := congr with pointwise
  cc

-- The smaller-domain weights may be represented by any agreeing graph.
theorem finiteRingSum.zero_extension (D S A add zero neg mul one w v : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : S → A
  requires subset : S ⊆ D
  requires agreement : ∀ s ∈ S, w(s) = v(s)
  requires vanishes : ∀ d ∈ D, ¬(d ∈ S) → w(d) = zero
  shows finiteRingSum(D, A, add, zero, neg, mul, one, w) = finiteRingSum(S, A, add, zero, neg, mul, one, v)
proof
  have closed : ∀ s ∈ S, w(s) ∈ A
    intros s hs
    have value := FunctionBetween.apply_closed with *
    have equal := agreement with s, hs
    rwa equal
  have restricted := restrict.function with *
  have same : restrict(w, S) = v
    apply FunctionBetween.ext with restricted, weightsV
    intros s hs
    have value := restrict.apply with *
    have equal := agreement with s, hs
    cc
  have sum := finiteRingSum.restrict with *
  rwa same at sum

theorem finiteRingSum.singleton (A add zero neg mul one w x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires weights : w : {x} → A
  shows finiteRingSum({x}, A, add, zero, neg, mul, one, w) = w(x)
proof
  have same : insert(x, ∅) = {x}
    ext y
    simp
  have empty := Finite.empty
  have fresh : ¬(x ∈ ∅) by exact set.empty at x
  have extended : w : insert(x, ∅) → A by rwa same
  have subset : ∅ ⊆ insert(x, ∅) by simp [Subset, set.empty]
  have closed : ∀ y ∈ ∅, w(y) ∈ A
    intros y hy
    exfalso
    exact set.empty with hy
  have restricted := restrict.function with *
  have emptySum := finiteRingSum.empty with *
  have inserted := finiteRingSum.insert with *
  have member : x ∈ {x} by simp [singleton.membership]
  have value := FunctionBetween.apply_closed with *
  rw same at inserted
  rw [inserted, emptySum]
  ring

theorem finiteRingSum.single (C A add zero neg mul one a c : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(C)
  requires coefficient : a ∈ A
  requires index : c ∈ C
  shows finiteRingSum(C, A, add, zero, neg, mul, one, coefficientSingle(C, A, zero, a, c)) = a
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have weights := coefficientSingle.function at C, A, zero, a, c with *
  have small := coefficientSingle.function at {c}, A, zero, a, c with *
  have singletonMember : c ∈ {c}
    settle with singleton.membership
  have subset : {c} ⊆ C
    settle with Subset, singleton.membership
  have agreement : ∀ x ∈ {c}, coefficientSingle(C, A, zero, a, c)(x) = coefficientSingle({c}, A, zero, a, c)(x)
    intros x hx
    have equal := singleton.membership.forward at x, c with hx
    have left := coefficientSingle.same at C, A, zero, a, c with *
    have right := coefficientSingle.same at {c}, A, zero, a, c with *
    cc
  have vanishes : ∀ x ∈ C, ¬(x ∈ {c}) → coefficientSingle(C, A, zero, a, c)(x) = zero
    intros x hx outside
    have different : x ≠ c
      settle with singleton.membership
    exact coefficientSingle.other at C, A, zero, a, c, x with *
  have reduced := finiteRingSum.zero_extension at C, {c}, A, add, zero, neg, mul, one, coefficientSingle(C, A, zero, a, c), coefficientSingle({c}, A, zero, a, c) with *
  have singleton := finiteRingSum.singleton at A, add, zero, neg, mul, one, coefficientSingle({c}, A, zero, a, c), c with *
  have value := coefficientSingle.same at {c}, A, zero, a, c with *
  cc

-- A fixed equality selector commutes with a finite sum.
theorem finiteRingSum.select (D A add zero neg mul one w v j i : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(D)
  requires weightsW : w : D → A
  requires weightsV : v : D → A
  requires values : ∀ d ∈ D, v(d) = singleValue(A, zero, w(d), j, i)
  shows finiteRingSum(D, A, add, zero, neg, mul, one, v) =
    singleValue(A, zero, finiteRingSum(D, A, add, zero, neg, mul, one, w), j, i)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroIn := IsRing.zero_in_carrier with ordinary
  have alternatives : i = j ∨ i ≠ j by tauto
  cases alternatives with same | different
  . have equal : v = w
      apply FunctionBetween.ext with weightsV, weightsW
      intros d hd
      have coefficient := FunctionBetween.apply_closed at w, D, A, d with *
      have selected := singleValue.same at A, zero, w(d), j, i with *
      have value := values with d, hd
      cc
    have selected := singleValue.same at A, zero, finiteRingSum(D, A, add, zero, neg, mul, one, w), j, i with *
    cc
  . have vanishes : ∀ d ∈ D, v(d) = zero
      intros d hd
      have coefficient := FunctionBetween.apply_closed at w, D, A, d with *
      have selected := singleValue.other at A, zero, w(d), j, i with *
      have value := values with d, hd
      cc
    have sum := finiteRingSum.zero at D, A, add, zero, neg, mul, one, v with *
    have selected := singleValue.other at A, zero, finiteRingSum(D, A, add, zero, neg, mul, one, w), j, i with *
    cc