List fold invariants and selection

Main results

• List.foldl_take_invariant: an index-dependent invariant holds after every prefix of a fold.
• List.foldl_keep_fst: folding a step that keeps the first component of a pair preserves that component and folds over the second.
• List.foldr_ite_eq_of_mem: a chain of equality tests selects the branch of a contained tag, regardless of duplicates or fallback. Used by finite-control certificates.
• List.foldl_or_eq, List.foldl_min_add_eq: folding a disjunction is List.any, and folding a sum capped at cap caps the sum.

References

Adapts the selection identity from Computability/Probabilistic/Finite.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem List.foldl_take_invariant {α : Type u_1} {β : Type u_2} (l : List α) (step : β → α → β) (init : β) (P : ℕ → β → Prop) (hbase : P 0 init) (hstep : ∀ (i : ℕ) (hi : i < l.length) (state : β), P i state → P (i + 1) (step state l[i])) (i : ℕ) : i ≤ l.length → P i (foldl step init (take i l))

An invariant depending on the number of consumed elements holds after every bounded prefix fold if it holds initially and is preserved by the next list element. Unlike List.foldlRecOn, preservation may depend on the position. This is a semantic rule with no resource assumptions.

theorem List.foldl_keep_fst {ι : Type u_1} {π : Type u_2} {α : Type u_3} (step : π → α → ι → α) (par : π) (xs : List ι) (init : α) : foldl (fun (pa : π × α) (i : ι) => (pa.fst, step pa.fst pa.snd i)) (par, init) xs = (par, foldl (step par) init xs)

Folding a step that keeps the first component of a pair preserves that component and folds over the second.

theorem List.foldr_ite_eq_of_mem {Tag : Type u_1} {Value : Type u_2} [DecidableEq Tag] (tags : List Tag) (tag : Tag) (branch : Tag → Value) (fallback : Value) (h : tag ∈ tags) : foldr (fun (candidate : Tag) (rest : Value) => if tag = candidate then branch candidate else rest) fallback tags = branch tag

A chain of equality tests selects a contained tag, regardless of duplicates or fallback.

theorem List.foldl_or_eq {α : Type u_1} (f : α → Bool) (b : Bool) (l : List α) : foldl (fun (acc : Bool) (x : α) => acc || f x) b l = (b || l.any f)

Folding a disjunction over a list adds whether some element satisfies the test.

theorem List.foldl_min_add_eq {α : Type u_1} (cap : ℕ) (f : α → ℕ) {b : ℕ} (hb : b ≤ cap) (l : List α) : foldl (fun (acc : ℕ) (x : α) => min cap (acc + f x)) b l = min cap (b + (map f l).sum)

Folding a sum capped at cap over a list, from a value at most cap, caps the whole sum.

@[simp]

theorem foldl_and_eq_and_all {α : Type u_1} (p : α → Bool) (xs : List α) (init : Bool) : List.foldl (fun (ok : Bool) (x : α) => ok && p x) init xs = (init && xs.all p)