A partial fold simulating a total one #
When every successful step of a partial step function f maps, under a projection π, to the
step of a total function g, every successful foldlM f maps to the foldl g from the projected
start. [UPSTREAM] candidate for Init/Data/List/Monadic.lean.
Main results #
List.foldl_eq_of_foldlM_eq_some: a successful partial fold projects to the total fold.List.map_foldlM: a partial fold whose steps commute with a projection maps to the projected partial fold.
theorem
List.foldl_eq_of_foldlM_eq_some
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : β → α → Option β}
{g : γ → α → γ}
{π : β → γ}
(hf : ∀ (b : β) (a : α) (b' : β), f b a = some b' → π b' = g (π b) a)
{l : List α}
{b b' : β}
:
foldlM f b l = some b' → π b' = foldl g (π b) l
A successful fold of a partial step function whose successful steps project to those of g
projects to the fold of g.
theorem
List.map_foldlM
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{π : β → γ}
{f : β → α → Option β}
{g : γ → α → Option γ}
(hf : ∀ (b : β) (a : α), Option.map π (f b a) = g (π b) a)
(l : List α)
(b : β)
:
Option.map π (foldlM f b l) = foldlM g (π b) l
A partial fold whose steps commute with π maps under π to the partial fold of the
projected steps.