-- Finite sums over arbitrary set-sized rings and their ideals (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.FiniteSum
import GeneratedIdeal
import Core.List

def ringSum {C : Set} (add z0 : Set) (xs : List(C)) → Set
  | add, z0, List.nil => z0
  | add, z0, List.cons(x, tail) => call2(add, x, ringSum(add, z0, tail))
  descends xs

def ringImageSum {C : Set} (f plus z : Set) (xs : List(C)) → Set
  | f, plus, z, List.nil => z
  | f, plus, z, List.cons(x, tail) => plus(f(x), ringImageSum(f, plus, z, tail))
  descends xs

def ringScale {C : Set} (mul a : Set) (xs : List(C)) → Set
  | mul, a, List.nil => []
  | mul, a, List.cons(x, tail) => call2(mul, a, x) :: ringScale(mul, a, tail)
  descends xs

theorem ringScale.closed (C mul a : Set) (xs : List(C))
  requires closed : ∀ x ∈ C, call2(mul, a, x) ∈ C
  shows List(C, ringScale{C}(mul, a, xs))
proof
  induction xs
  | List.nil =>
    rw ringScale
    typecheck
  | List.cons(x, tail) using ih =>
    have member := closed with x
    rw ringScale
    typecheck

theorem ringSum.nil (C add zero : Set)
  shows ringSum{C}(add, zero, []) = zero
proof
  unfold ringSum
  rfl

theorem ringSum.cons (C add zero x : Set) (xs : List(C))
  requires member : x ∈ C
  shows ringSum{C}(add, zero, x :: xs) = call2(add, x, ringSum{C}(add, zero, xs))
proof
  unfold ringSum
  rfl

theorem IsIdeal.sum_mem (A add zero neg mul I C : Set) (xs : List(C))
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires included : C ⊆ I
  shows ringSum{C}(add, zero, xs) ∈ I
proof
  induction xs
  | List.nil =>
    rw ringSum
    exact IsIdeal.zero_closed with ideal
  | List.cons(x, tail) using ih =>
    have member := included with x, assumption
    have sum := IsIdeal.add_closed with ideal, member, ih
    rwa ringSum

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

theorem ringSum.closed (xs : List(C))
  shows ringSum{C}(add, zero, xs) ∈ A
proof
  induction xs
  | List.nil =>
    have ordinary := IsCommRing.ring with ring
    rw ringSum
    exact IsRing.zero_in_carrier with ordinary
  | List.cons(x, tail) using ih =>
    have ordinary := IsCommRing.ring with ring
    have member := bounded with x, assumption
    have sum := IsRing.add_closed with ordinary, member, ih
    rwa ringSum

theorem ringSum.append (ys xs : List(C))
  shows ringSum{C}(add, zero, ListOps.append{C}(ys, xs)) =
    ringSum{C}(add, zero, xs) + ringSum{C}(add, zero, ys)
proof
  induction xs
  | List.nil =>
    have sumY := ringSum.closed at A, add, zero, neg, mul, one, C, ys with *
    simp [ListOps.append, ringSum]
    ring
  | List.cons(x, tail) using ih =>
    have sumY := ringSum.closed at A, add, zero, neg, mul, one, C, ys with *
    have sumTail := ringSum.closed at A, add, zero, neg, mul, one, C, tail with *
    have member := bounded with x, assumption
    simp [ListOps.append, ringSum, ih]
    ring

theorem ringSum.scale (a : Set) (xs : List(C))
  requires ha : a ∈ A
  requires closed : ∀ x ∈ C, a * x ∈ C
  shows ringSum{C}(add, zero, ringScale{C}(mul, a, xs)) = a * ringSum{C}(add, zero, xs)
proof
  induction xs
  | List.nil =>
    rw [ringScale, ringSum]
    ring
  | List.cons(x, tail) using ih =>
    have sumTail := ringSum.closed at A, add, zero, neg, mul, one, C, tail with *
    have scaledHead := closed with x
    have member := bounded with x, assumption
    rw [ringScale, ringSum, ringSum, ih]
    ring

section Maps
variable (f B plus z minus times unit : Set)
hypothesis target : IsCommRing(B, plus, z, minus, times, unit)
hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)
notation ring S := (B, plus, z, minus, times, unit)

theorem IsRingHom.sum (xs : List(C))
  shows f(ringSum{C}(add, zero, xs)) = ringImageSum{C}(f, plus, z, xs)
proof
  induction xs
  | List.nil =>
    rw [ringSum, ringImageSum]
    exact IsRingHom.zero with hom
  | List.cons(x, tail) using ih =>
    have sumTail := ringSum.closed at A, add, zero, neg, mul, one, C, tail with *
    have member := bounded with x, assumption
    have mapped := IsRingHom.add with hom, member, sumTail
    rw [ringSum, ringImageSum, mapped, ih]
    rfl

end Maps
end Rings