List Utils

Small list-fold lemmas used throughout TorchLean proof files. They are generic, not NN-specific, so tensor, runtime-approximation, and RL proofs can share the same fold facts instead of carrying local copies.

theorem List.foldl_max_le_of_le {ι β : Type} [LinearOrder β] (l : List ι) (f : ι → β) {acc eps : β} (hacc : acc ≤ eps) (hf : ∀ i ∈ l, f i ≤ eps) : foldl (fun (a : β) (i : ι) => max a (f i)) acc l ≤ eps

foldl max upper bound helper.

If the initial accumulator and every f i are ≤ eps, then the folded maximum is also ≤ eps.

theorem List.le_foldl_max_init {ι β : Type} [LinearOrder β] (l : List ι) (f : ι → β) (acc : β) : acc ≤ foldl (fun (a : β) (i : ι) => max a (f i)) acc l

Lower bound helper for foldl max.

The folded maximum is always at least as large as the initial accumulator.

theorem List.le_foldl_max_of_mem {ι β : Type} [LinearOrder β] (l : List ι) (f : ι → β) {acc : β} {i : ι} (hi : i ∈ l) : f i ≤ foldl (fun (a : β) (j : ι) => max a (f j)) acc l

Membership helper for foldl max.

If i ∈ l, then f i is ≤ the folded maximum.

theorem List.foldl_max_eq_init_or_mem {ι β : Type} [LinearOrder β] (l : List ι) (f : ι → β) (acc : β) : foldl (fun (a : β) (i : ι) => max a (f i)) acc l = acc ∨ ∃ i ∈ l, foldl (fun (a : β) (j : ι) => max a (f j)) acc l = f i

A finite left fold of max returns either its initial accumulator or one of the values it visited. This complements the order bounds above with the attainment fact needed by stable softmax: the computed maximum is an actual input coordinate, so one max-shifted exponential is exactly exp 0 = 1.

theorem List.foldl_add_congr {α β : Type} [Add α] (l : List β) (f g : β → α) (a : α) (h : ∀ (x : β), f x = g x) : foldl (fun (s : α) (x : β) => s + f x) a l = foldl (fun (s : α) (x : β) => s + g x) a l

Pointwise congruence for left folds of the shape acc + f x.

Many tensor and autograd proofs use executable folds for sums; this lemma lets them rewrite the per-coordinate summand without re-proving a list induction locally.

theorem List.foldl_add_const_zero {α β : Type} [AddMonoid α] (l : List β) (a : α) : foldl (fun (s : α) (x : β) => s + 0) a l = a

Folding (+ 0) over a list leaves the accumulator unchanged.

theorem List.foldl_add_init {α β : Type} [AddMonoid β] (l : List α) (f : α → β) (acc : β) : foldl (fun (a : β) (x : α) => a + f x) acc l = acc + foldl (fun (a : β) (x : α) => a + f x) 0 l

Turn foldl (fun a x => a + f x) acc into acc + foldl (fun a x => a + f x) 0.

This is the standard "peel off the initial accumulator" lemma for left folds over +.

theorem List.add_foldl_add0 {α β : Type} [AddMonoid β] (l : List α) (f : α → β) (acc : β) : acc + foldl (fun (a : β) (x : α) => a + f x) 0 l = foldl (fun (a : β) (x : α) => a + f x) acc l

theorem List.foldl_add_distrib2 {α β : Type} [AddCommMonoid α] (l : List β) (g1 g2 : β → α) (a1 a2 : α) : foldl (fun (s : α) (x : β) => s + (g1 x + g2 x)) (a1 + a2) l = foldl (fun (s : α) (x : β) => s + g1 x) a1 l + foldl (fun (s : α) (x : β) => s + g2 x) a2 l

Distribute a fold of g1 x + g2 x into the sum of two folds.

This is the list-level form of “finite sum distributes over addition”.

theorem List.foldl_add_mul_right {α β : Type} [Semiring α] (l : List β) (g : β → α) (a k : α) : foldl (fun (acc : α) (x : β) => acc + g x * k) (a * k) l = foldl (fun (acc : α) (x : β) => acc + g x) a l * k

Pull multiplication by a fixed scalar through an additive left fold.

theorem List.foldl_cons_snd_length {α β : Type} (l : List β) (step : α → β → α) (accScalar : α) (accList : List α) : (foldl (fun (acc : α × List α) (x : β) => have y := step acc.1 x; (y, y :: acc.2)) (accScalar, accList) l).2.length = accList.length + l.length

Length of the second component when a left fold prepends exactly one output per input.

This captures the common "right-to-left scan implemented as reverse.foldl" proof pattern used by return/advantage computations: the first accumulator evolves by step, while the second accumulator records one new value with :: at every iteration.

theorem List.finRange_foldl_add_eq_finset_sum {β : Type} [AddCommMonoid β] {n : ℕ} (f : Fin n → β) : foldl (fun (s : β) (i : Fin n) => s + f i) 0 (finRange n) = Finset.univ.sum f

Rewrite the canonical List.finRange addition fold into a Finset.univ sum.

Specs use List.foldl because it computes well; proofs usually want Finset.sum so standard big-operator lemmas apply.

theorem List.finRange_foldl_add_acc {β : Type} [AddCommMonoid β] {n : ℕ} (f : Fin n → β) (acc : β) : foldl (fun (s : β) (i : Fin n) => s + f i) acc (finRange n) = acc + Finset.univ.sum f

Accumulator form of finRange_foldl_add_eq_finset_sum.

This avoids re-proving "peel off the initial accumulator, then rewrite the zero fold" in large finite-sum proofs.