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_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.