English
For an associative binary operation ⋆ on α, for any list l and elements a1,a2 ∈ α, we have op: if we map each element x of l to x ⋆ a1 and then apply ⋆ with a2, this equals a1 ⋆ (foldr (⋆) a2 l). Precisely: (map (λ x, x ⋆ a1) l) ⋆ a2 = a1 ⋆ foldr (λ x y, x ⋆ y) a2 l.
Русский
Для бинарной операции ⋆ на множестве α, если отображать элементы списка l в виде x ⋆ a1, а затем применять ⋆ с a2, то получить можно как a1 ⋆ (foldr (⋆) a2 l). Формально: map (λ x, x ⋆ a1) l ⋆ a2 = a1 ⋆ foldr (λ x y, x ⋆ y) a2 l.
LaTeX
$$$$ (\operatorname{map}(\lambda x. x \;\ast\; a_1)\, l) \;\ast\; a_2
= a_1 \ast \operatorname{foldr}(\lambda x y. x \ast y)\; a_2\; l $$$$
Lean4
theorem foldl_eq_of_comm_of_assoc [hcomm : Std.Commutative f] [hassoc : Std.Associative f] :
∀ a b l, foldl f a (b :: l) = f b (foldl f a l)
| a, b, nil => hcomm.comm a b
| a, b, c :: l => by
simp only [foldl_cons]
have : RightCommutative f := inferInstance
rw [← foldl_eq_of_comm_of_assoc .., this.right_comm, foldl_cons]
