1.6. Fold and compatibility lemmas🔗

Nearly every library above this one reduces a list with a single operation: xs.foldl (fun acc x => acc + f x) z for a coefficient convolution or a finite sum, and its multiplicative twin for a product. A Mathlib-free library cannot reach for Finset.sum, and the core lemmas about associative folds require Std.Associative and Std.LawfulIdentity instances that a bare Lean.Grind.Semiring does not carry. HexBasic.Fold supplies those instances file-locally and states the algebra the libraries actually use, so the same rearrangement is proved once rather than in each consumer.

The two most-used shapes pull the running accumulator out of a fold and factor a scalar through one.

theorem

List.foldl_add_eq_add_foldl.{u, v} {α : Type v} {R : Type u}
  [Lean.Grind.Semiring R] (xs : List α) (f : α → R) (z : R) :
  List.foldl (fun acc x => acc + f x) z xs =
    z + List.foldl (fun acc x => acc + f x) 0 xs
List.foldl_add_eq_add_foldl.{u, v}
  {α : Type v} {R : Type u}
  [Lean.Grind.Semiring R] (xs : List α)
  (f : α → R) (z : R) :
  List.foldl (fun acc x => acc + f x) z
      xs =
    z +
      List.foldl (fun acc 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.

theorem

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

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

Reordering and reassociation matter because a sum indexed by an ordered map's keys has no canonical order, and because coefficient convolutions are naturally written as nested sums.

theorem

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

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

theorem

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

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

Bounds on Nat folds carry the degree and size arguments that termination and size reasoning need.

theorem

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

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

namespace HexBasicFolds

-- The fold shape the lemmas above talk about.
def sum2 (z : Int) (xs : List Int) : Int :=
  xs.foldl (fun a i => a + 2 * i) z

-- The sum itself.
#guard sum2 0 [1, 2, 3] = 12
-- Reordering the list does not change it.
#guard sum2 0 [3, 1, 2] = 12
-- A nonzero start shifts it by exactly that much.
#guard sum2 5 [1, 2, 3] = 17

end HexBasicFolds

HexBasic carries the handful of duplicate-freeness and lexicographic-comparison list lemmas that the canonical-form libraries share.