foldl1_eq_foldr1 — Mathlib

English

Assume f is associative. Then for any a,b and list l, foldl f a (l ++ [b]) = foldr f b (a :: l).

Русский

Предположим, что f ассоциативна. Тогда для любого a, b и списка l верно: foldl f a (l ++ [b]) = foldr f b (a :: l).

LaTeX

$$$$\forall a\, b\, l:\ List\ α,\ foldl f\, a\ (l \append [b]) = foldr f\, b\ (a :: l),$$ при условии [hassoc : Std.Associative f].$$

Lean4

theorem foldl1_eq_foldr1 [hassoc : Std.Associative f] : ∀ a b l, foldl f a (l ++ [b]) = foldr f b (a :: l)
  | _, _, nil => rfl
  | a, b, c :: l => by
    simp only [cons_append, foldl_cons, foldr_cons, foldl1_eq_foldr1 _ _ l]
    rw [hassoc.assoc]

Похожие утверждения