General List.foldl algebra shared across the Mathlib-free hex libraries.

The computational libraries repeatedly fold an accumulator with a single operation, xs.foldl (fun acc x => acc + f x) z or its multiplicative twin. Lean core already proves the underlying facts — List.foldl_assoc, List.sum_eq_foldl, List.foldl_map — but those need Std.Associative / Std.LawfulIdentity instances on the carrier, which a bare Lean.Grind.Semiring does not carry. This module supplies those four instances file-locally (just enough to prove the lemmas below) and then states the fold-algebra the libraries actually use.

The lemmas live in the List namespace and follow the standard-library naming: name the operation, not the use site (foldl_add_*, foldl_mul_*), mirror List.foldl_assoc/List.foldl_map, and keep foldl_add_eq_add_foldl symmetric with foldl_mul_eq_mul_foldl. The one exception is foldl_const_step: core/Mathlib already use List.foldl_const for the unrelated iterate lemma, so reusing that name here would collide in the Mathlib bridge layers (which import both this module and Mathlib). These are candidates to migrate up to lean4; the Grind Std instances in particular belong with the Grind algebra hierarchy.

The Std.Associative / Std.LawfulIdentity instances that List.foldl_assoc and friends need are kept file-local: they are used only to prove the lemmas below, which state their conclusions over Lean.Grind.Ring / CommRing without exposing the instances. Keeping them local avoids adding a second global Std.Associative resolution path for every Grind.Semiring (e.g. Nat/Int in the Mathlib bridge layers, where Mathlib already supplies its own). Promote / upstream them separately if a consumer ever needs them.

theorem List.instAssociativeHAdd_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.Associative fun (x1 x2 : R) => x1 + x2

Addition in a Grind.Semiring is an associative operation.

theorem List.instAssociativeHMul_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.Associative fun (x1 x2 : R) => x1 * x2

Multiplication in a Grind.Semiring is an associative operation.

theorem List.instLawfulIdentityHAddOfNat_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.LawfulIdentity (fun (x1 x2 : R) => x1 + x2) 0

0 is a two-sided identity for addition in a Grind.Semiring.

theorem List.instLawfulIdentityHMulOfNat_hexBasic {R : Type u} [Lean.Grind.Semiring R] : Std.LawfulIdentity (fun (x1 x2 : R) => x1 * x2) 1

1 is a two-sided identity for multiplication in a Grind.Semiring.

Congruence

theorem List.foldl_congr {α : Type v} {β : Type w} (xs : List α) (f g : β → α → β) (z : β) (h : ∀ (acc : β) (x : α), x ∈ xs → f acc x = g acc x) : foldl f z xs = foldl g z xs

Two folds over xs agree when their step functions agree pointwise on the elements of xs (for every accumulator). The fully general fold congruence.

theorem List.foldl_add_congr {α : Type v} {R : Type u} [Add R] (xs : List α) (f g : α → R) (z : R) (h : ∀ (x : α), x ∈ xs → f x = g x) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = foldl (fun (acc : R) (x : α) => acc + g x) z xs

Congruence for an additive fold-sum under its summand f.

theorem List.foldl_mul_congr {α : Type v} {R : Type u} [Mul R] (xs : List α) (f g : α → R) (z : R) (h : ∀ (x : α), x ∈ xs → f x = g x) : foldl (fun (acc : R) (x : α) => acc * f x) z xs = foldl (fun (acc : R) (x : α) => acc * g x) z xs

Congruence for a multiplicative fold-product under its factor f.

theorem List.foldl_mul_eq_mul_foldl {α : Type v} {M : Type u} [Mul M] [One M] [Std.Associative fun (x1 x2 : M) => x1 * x2] [Std.LawfulIdentity (fun (x1 x2 : M) => x1 * x2) 1] (xs : List α) (f : α → M) (z : M) : foldl (fun (acc : M) (x : α) => acc * f x) z xs = z * foldl (fun (acc : M) (x : α) => acc * f x) 1 xs

Pull the running accumulator out of a multiplicative fold-product, taking the product from a 1 start. Stated for any associative multiplication with a two-sided unit, so it applies to monoids that are not Grind rings (e.g. the executable polynomial types).

Constant step

theorem List.foldl_const_step {α : Type v} {β : Type w} (xs : List α) (z : β) : foldl (fun (acc : β) (x : α) => acc) z xs = z

Folding with a step that discards the element and returns the accumulator unchanged yields the initial accumulator. (Core's List.foldl_const is the unrelated iterate lemma, hence the name.)

Permutation invariance

theorem List.foldl_add_perm {α : Type v} {R : Type u} [Lean.Grind.Ring R] (f : α → R) {xs ys : List α} (h : xs.Perm ys) (z : R) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = foldl (fun (acc : R) (x : α) => acc + f x) z ys

An additive fold-sum is invariant under permuting the list.

theorem List.foldl_mul_perm {α : Type v} {R : Type u} [Lean.Grind.CommRing R] (f : α → R) {xs ys : List α} (h : xs.Perm ys) (z : R) : foldl (fun (acc : R) (x : α) => acc * f x) z xs = foldl (fun (acc : R) (x : α) => acc * f x) z ys

A multiplicative fold-product is invariant under permuting the list.

Accumulator extraction

theorem List.foldl_add_eq_add_foldl {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f : α → R) (z : R) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = z + foldl (fun (acc : R) (x : α) => acc + f x) 0 xs

Pull the running accumulator out of an additive fold-sum, taking the sum from a 0 start. The additive twin of foldl_mul_eq_mul_foldl.

All-zero collapse

theorem List.foldl_add_eq_self {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f : α → R) (z : R) (h : ∀ (x : α), x ∈ xs → f x = 0) : foldl (fun (acc : R) (x : α) => acc + f x) z xs = z

An additive fold-sum whose every summand vanishes on xs returns the initial accumulator.

theorem List.foldl_add_zero {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (z : R) : foldl (fun (acc : R) (x : α) => acc + 0) z xs = z

An additive fold-sum whose body adds a literal 0 returns the initial accumulator.

Scalar factoring

theorem List.foldl_add_mul_left {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (c : R) (f : α → R) (z : R) : foldl (fun (acc : R) (x : α) => acc + c * f x) (c * z) xs = c * foldl (fun (acc : R) (x : α) => acc + f x) z xs

Factor a left scalar out of an additive fold-sum.

theorem List.foldl_add_mul_left_zero {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (c : R) (f : α → R) : foldl (fun (acc : R) (x : α) => acc + c * f x) 0 xs = c * foldl (fun (acc : R) (x : α) => acc + f x) 0 xs

Factor a left scalar out of an additive fold-sum started from 0.

theorem List.foldl_add_mul_right {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f : α → R) (c z : R) : foldl (fun (acc : R) (x : α) => acc + f x) z xs * c = foldl (fun (acc : R) (x : α) => acc + f x * c) (z * c) xs

Factor a right scalar out of an additive fold-sum (right distributivity, no commutativity needed).

Negation and subtraction

theorem List.foldl_add_neg {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f : α → R) (z : R) : foldl (fun (acc : R) (x : α) => acc + -f x) (-z) xs = -foldl (fun (acc : R) (x : α) => acc + f x) z xs

Negation distributes through an additive fold-sum.

Additivity

theorem List.foldl_add_add_start {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f g : α → R) (a b : R) : foldl (fun (acc : R) (x : α) => acc + (f x + g x)) (a + b) xs = foldl (fun (acc : R) (x : α) => acc + f x) a xs + foldl (fun (acc : R) (x : α) => acc + g x) b xs

An additive fold-sum of a pointwise sum splits into two folds, distributing the starting accumulator.

theorem List.foldl_add_add_of_acc {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f g : α → R) (acc accF accG : R) (h : acc = accF + accG) : foldl (fun (acc : R) (x : α) => acc + (f x + g x)) acc xs = foldl (fun (acc : R) (x : α) => acc + f x) accF xs + foldl (fun (acc : R) (x : α) => acc + g x) accG xs

An additive fold-sum of a pointwise sum splits into two folds, given a splitting of the starting accumulator.

theorem List.foldl_add_add {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f g : α → R) : foldl (fun (acc : R) (x : α) => acc + (f x + g x)) 0 xs = foldl (fun (acc : R) (x : α) => acc + f x) 0 xs + foldl (fun (acc : R) (x : α) => acc + g x) 0 xs

An additive fold-sum of a pointwise sum from 0 splits into the sum of the two separate folds from 0.

theorem List.foldl_add_sub {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f g : α → R) (a b : R) : foldl (fun (acc : R) (x : α) => acc + (f x - g x)) (a - b) xs = foldl (fun (acc : R) (x : α) => acc + f x) a xs - foldl (fun (acc : R) (x : α) => acc + g x) b xs

An additive fold-sum of a pointwise difference splits into the difference of the two fold-sums, distributing the starting accumulator.

theorem List.foldl_add_sub_zero {α : Type v} {R : Type u} [Lean.Grind.Ring R] (xs : List α) (f g : α → R) : foldl (fun (acc : R) (x : α) => acc + (f x - g x)) 0 xs = foldl (fun (acc : R) (x : α) => acc + f x) 0 xs - foldl (fun (acc : R) (x : α) => acc + g x) 0 xs

An additive fold-sum of a pointwise difference from 0 splits into the difference of the two fold-sums from 0.

Fubini

theorem List.foldl_add_comm {α : Type v} {R : Type u} [Lean.Grind.Ring R] {γ : Type w} (xs : List α) (ys : List γ) (f : α → γ → R) : foldl (fun (acc : R) (x : α) => acc + foldl (fun (acc' : R) (y : γ) => acc' + f x y) 0 ys) 0 xs = foldl (fun (acc : R) (y : γ) => acc + foldl (fun (acc' : R) (x : α) => acc' + f x y) 0 xs) 0 ys

Sum-swap (Fubini) for nested additive fold-sums.

theorem List.foldl_add_mul_right_zero {α : Type v} {R : Type u} [Lean.Grind.CommRing R] (xs : List α) (f : α → R) (c : R) : foldl (fun (acc : R) (x : α) => acc + f x * c) 0 xs = foldl (fun (acc : R) (x : α) => acc + f x) 0 xs * c

Factor a right scalar out of an additive fold-sum started from 0.

flatMap

theorem List.foldl_add_flatMap {α : Type v} {R : Type u} [Add R] {γ : Type w} (xs : List α) (f : α → List γ) (g : γ → R) (z : R) : foldl (fun (acc : R) (x : γ) => acc + g x) z (flatMap f xs) = foldl (fun (acc : R) (x : α) => foldl (fun (acc : R) (y : γ) => acc + g y) acc (f x)) z xs

An additive fold-sum over xs.flatMap f equals the fold over xs whose body folds each sublist f x into the accumulator.

Indicator pickout

theorem List.foldl_add_single {α : Type v} {R : Type u} [Lean.Grind.CommRing R] [DecidableEq α] (xs : List α) (z : R) (q : α) (f : α → R) (hmem : q ∈ xs) (hnodup : xs.Nodup) : foldl (fun (acc : R) (x : α) => acc + if x = q then f x else 0) z xs = z + f q

An additive fold-sum over a Nodup list whose summand is supported at a single matching element collects exactly that summand.

Monotone bounds (Nat)

theorem List.le_foldl_add_self {α : Type v} (xs : List α) (g : α → Nat) (init : Nat) : init ≤ foldl (fun (acc : Nat) (x : α) => acc + g x) init xs

An additive fold-sum over Nat is at least its starting accumulator.

theorem List.le_foldl_add_of_mem {α : Type v} (xs : List α) (g : α → Nat) {x : α} {init : Nat} (hx : x ∈ xs) : g x ≤ foldl (fun (acc : Nat) (y : α) => acc + g y) init xs

Every summand is bounded by an additive fold-sum over Nat that contains it.

theorem List.le_foldl_max_self {α : Type v} (xs : List α) (g : α → Nat) (init : Nat) : init ≤ foldl (fun (acc : Nat) (x : α) => max acc (g x)) init xs

A Nat fold-max is at least its starting accumulator.

theorem List.le_foldl_max_of_mem {α : Type v} (xs : List α) (g : α → Nat) {x : α} {init : Nat} (hx : x ∈ xs) : g x ≤ foldl (fun (acc : Nat) (y : α) => max acc (g y)) init xs

Every element's value is bounded by a Nat fold-max that contains it.