-- Integer-valued sums over finite sets: the canonical commutative ring sum
-- of ℤ over a finite index set, with closure, the singleton sum,
-- congruence, vanishing, restriction to a support, reindexing along a
-- bijection, and scaling by an integer
-- 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.Combinatorics.IntegerSum
import Int
import Algebra.Ring.WeightedRegrouping
import Cardinal

-- The sum of an integer-valued weight over a finite set, as the canonical
-- commutative ring sum of the integers.
def integerSetSum (V w : Set) : Set :=
  finiteRingSum(V, ℤ, integerAdd, integerZero, integerNeg, integerMul,
    integerOne, restrict(w, V))

theorem integerSetSum.integer (V Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℤ
  requires subset : V ⊆ Ω
  shows Integer(integerSetSum(V, w))
proof
  have ring := integers.comm_ring
  have restricted := restrict.domain_function with weights, subset
  have closed := finiteRingSum.closed with ring, finite, restricted
  unfold integerSetSum
  exact closed

theorem integerSetSum.singleton (Ω w a : Set)
  requires weights : w : Ω → ℤ
  requires member : a ∈ Ω
  shows integerSetSum({a}, w) = w(a)
proof
  have ring := integers.comm_ring
  have subset : {a} ⊆ Ω by simp
  have self : a ∈ {a} by simp
  have restricted := restrict.domain_function with weights, subset
  have sum := finiteRingSum.singleton with ring, restricted
  have value := restrict.domain_apply with weights, subset, self
  unfold integerSetSum
  cc

theorem integerSetSum.congr (V Ω w v : Set)
  requires weightsW : w : Ω → ℤ
  requires weightsV : v : Ω → ℤ
  requires subset : V ⊆ Ω
  requires values : ∀ x ∈ V, w(x) = v(x)
  shows integerSetSum(V, w) = integerSetSum(V, v)
proof
  have restrictedW := restrict.domain_function with weightsW, subset
  have restrictedV := restrict.domain_function with weightsV, subset
  have same : ∀ x ∈ V, restrict(w, V)(x) = restrict(v, V)(x)
    intros x hx
    have left := restrict.domain_apply with weightsW, subset, hx
    have right := restrict.domain_apply with weightsV, subset, hx
    have equal := values with x, hx
    cc
  have equal := FunctionBetween.ext with restrictedW, restrictedV, same
  unfold integerSetSum
  cc

theorem integerSetSum.zero (V Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℤ
  requires subset : V ⊆ Ω
  requires values : ∀ x ∈ V, w(x) = integerZero
  shows integerSetSum(V, w) = integerZero
proof
  have ring := integers.comm_ring
  have restricted := restrict.domain_function with weights, subset
  have vanishing : ∀ x ∈ V, restrict(w, V)(x) = integerZero
    intros x hx
    have value := restrict.domain_apply with weights, subset, hx
    have zero := values with x, hx
    cc
  have sum := finiteRingSum.zero with ring, finite, restricted, vanishing
  unfold integerSetSum
  cc

-- A sum shrinks to any subset outside of which its weight vanishes.
theorem integerSetSum.support (V S Ω w : Set)
  requires finite : Finite(V)
  requires weights : w : Ω → ℤ
  requires subset : V ⊆ Ω
  requires inner : S ⊆ V
  requires vanishes : ∀ x ∈ V, ¬(x ∈ S) → w(x) = integerZero
  shows integerSetSum(V, w) = integerSetSum(S, w)
proof
  have ring := integers.comm_ring
  have restricted := restrict.domain_function with weights, subset
  have vanishing : ∀ x ∈ V, ¬(x ∈ S) → restrict(w, V)(x) = integerZero
    intros x hx outside
    have value := restrict.domain_apply with weights, subset, hx
    have zero := vanishes with x, hx, outside
    cc
  have sum := finiteRingSum.restrict at V, S, ℤ, integerAdd, integerZero,
    integerNeg, integerMul, integerOne, restrict(w, V) with ring, finite,
      restricted, inner, vanishing
  have nested := restrict.nested at w, S, V with inner
  unfold integerSetSum
  cc

-- A bijection between index sets carrying one weight to the other
-- identifies the two sums.
theorem integerSetSum.reindex (D E ΩD ΩE w v f : Set)
  requires finite : Finite(D)
  requires weightsW : w : ΩD → ℤ
  requires weightsV : v : ΩE → ℤ
  requires subsetD : D ⊆ ΩD
  requires subsetE : E ⊆ ΩE
  requires bijective : BijectiveBetween(f, D, E)
  requires values : ∀ d ∈ D, w(d) = v(f(d))
  shows integerSetSum(D, w) = integerSetSum(E, v)
proof
  have ring := integers.comm_ring
  have restrictedW := restrict.domain_function with weightsW, subsetD
  have restrictedV := restrict.domain_function with weightsV, subsetE
  have injective := Bijective.injective with bijective
  have function := Injective.function with injective
  have agree : ∀ d ∈ D, restrict(w, D)(d) = restrict(v, E)(f(d))
    intros d hd
    have image := FunctionBetween.apply_closed with function, hd
    have left := restrict.domain_apply with weightsW, subsetD, hd
    have right := restrict.domain_apply with weightsV, subsetE, image
    have equal := values with d, hd
    cc
  have sum := finiteRingSum.reindex with ring, finite, restrictedW,
    restrictedV, bijective, agree
  unfold integerSetSum
  cc

theorem integerSetSum.scale (V Ω w v : Set) (a : Integer)
  requires finite : Finite(V)
  requires weightsW : w : Ω → ℤ
  requires weightsV : v : Ω → ℤ
  requires subset : V ⊆ Ω
  requires values : ∀ x ∈ V, v(x) = integerMulValue(a, w(x))
  shows integerSetSum(V, v) = integerMulValue(a, integerSetSum(V, w))
proof
  have ring := integers.comm_ring
  have scalar : a ∈ ℤ by simp [Integer]
  have restrictedW := restrict.domain_function with weightsW, subset
  have restrictedV := restrict.domain_function with weightsV, subset
  have entries : ∀ x ∈ V, restrict(v, V)(x) =
      call2(integerMul, a, restrict(w, V)(x))
    intros x hx
    have left := restrict.domain_apply with weightsV, subset, hx
    have right := restrict.domain_apply with weightsW, subset, hx
    have inDomain := subset with x, hx
    have valueW := FunctionBetween.apply_closed with weightsW, inDomain
    have equal := values with x, hx
    have bridge := integerMulValue.notation at a, w(x) with *
    cc
  have sum := finiteRingSum.scale_eq with ring, finite, restrictedW,
    restrictedV, scalar, entries
  have total := integerSetSum.integer with finite, weightsW, subset
  have bridge := integerMulValue.notation at a, integerSetSum(V, w) with *
  unfold integerSetSum at bridge
  unfold integerSetSum
  cc