List fold invariants and selection

Main results

• List.foldl_take_invariant: an index-dependent invariant holds after every prefix of a fold.
• 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.

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