-- Inserting fresh indices into canonical finite sums (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.Ring.SumExtension
import FiniteSetSum

theorem finiteRingSum.empty (A add zero neg mul one w : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires weights : w : ∅ → A
  shows finiteRingSum(∅, A, add, zero, neg, mul, one, w) = zero
proof
  have finite := Finite.empty
  have values : ∀ x ∈ ∅, w(x) = zero
    intros x impossible
    exfalso
    exact set.empty with impossible
  exact finiteRingSum.zero with ring, finite, weights, values

theorem finiteRingSum.insert (V A add zero neg mul one w a : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weights : w : insert(a, V) → A
  requires fresh : ¬(a ∈ V)
  shows finiteRingSum(insert(a, V), A, add, zero, neg, mul, one, w) =
    call2(add, finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V)), w(a))
proof
  have subset : V ⊆ insert(a, V)
    intros x hx
    exact insert.contains with hx
  have closed : ∀ x ∈ V, w(x) ∈ A
    intros x hx
    have member := insert.contains at x, a, V with hx
    exact FunctionBetween.apply_closed at w, insert(a, V), A, x with *
  have restricted := restrict.function at w, insert(a, V), A, V, A with *
  have selected := finiteRingSum.selected at V, A, add, zero, neg, mul, one, restrict(w, V) with *
  obtain ⟨n, natural, f, enumeration, equation⟩ := selected.right
  have injective := Bijective.injective with enumeration
  have function := Injective.function with injective
  have nFresh := membership.irreflexive at n
  have extended := adjoinMap.bijective with enumeration, nFresh, fresh
  have successor := natural.successor_as_insert with natural
  rw ← successor at extended
  have extendedInjective := Bijective.injective with extended
  have extendedFunction := Injective.function with extendedInjective
  have extendedSum := finiteRingSum.enumeration at insert(a, V), A, add, zero, neg, mul, one, w, adjoinMap(f, n, a), succ(n) with *
  have oldValues : ∀ i ∈ n, w(adjoinMap(f, n, a)(i)) = restrict(w, V)(f(i))
    intros i hi
    have oldMember := FunctionBetween.apply_closed at f, n, V, i with *
    have oldEdge := FunctionBetween.relates_apply at f, n, V, i with *
    have edge := adjoinMap.relates_old at f, n, a, i, f(i) with oldEdge
    have next := membership.into_successor at i, n with *
    have value := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), i, f(i) with *
    have restrictedValue := restrict.apply at w, insert(a, V), A, V, A, f(i) with *
    cc
  have congr := indexedRingSum.congr at w, restrict(w, V), adjoinMap(f, n, a), f, add, zero, n with natural
  have prefix := congr with oldValues
  have newIndex := membership.self_successor with natural
  have newEdge := adjoinMap.relates_new at f, n, a
  have newValue := FunctionBetween.apply_value at adjoinMap(f, n, a), succ(n), insert(a, V), n, a with *
  rw [extendedSum, indexedRingSum, prefix, newValue, equation]
  rfl

theorem finiteRingSum.insert_zero (V A add zero neg mul one w a : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires finite : Finite(V)
  requires weights : w : insert(a, V) → A
  requires fresh : ¬(a ∈ V)
  requires vanishes : w(a) = zero
  shows finiteRingSum(insert(a, V), A, add, zero, neg, mul, one, w) =
    finiteRingSum(V, A, add, zero, neg, mul, one, restrict(w, V))
proof
  have inserted := finiteRingSum.insert with *
  have subset : V ⊆ insert(a, V)
    intros x hx
    exact insert.contains with hx
  have closed : ∀ x ∈ V, w(x) ∈ A
    intros x hx
    have member := insert.contains at x, a, V with hx
    exact FunctionBetween.apply_closed with *
  have restricted := restrict.function with *
  have sumIn := finiteRingSum.closed with *
  rw [inserted, vanishes]
  ring