English
If f,g: α → β → α and a ∈ α and H: ∀ a ∈ l, ∀ b, f a b = g a b, then foldl f a l = foldl g a l.
Русский
Если f,g: α → β → α и a ∈ α, и H: ∀ a ∈ l, ∀ b, f a b = g a b, то foldl f a l = foldl g a l.
LaTeX
$$$\\\\forall {f,g:\\\\alpha \\\\to \\\\beta \\\\to \\\\alpha} {a:\\\\alpha} {l:\\\\text{List }\\\\beta}, \\\\bigl(\\\\forall (a:\\\\alpha) (b:\\\\beta),\\\\, b \\\\in l \\\\Rightarrow f a b = g a b\\\\bigr) \\\\Rightarrow \\\\operatorname{foldl} f a l = \\\\operatorname{foldl} g a l.$$$
Lean4
theorem foldl_ext (f g : α → β → α) (a : α) {l : List β} (H : ∀ a : α, ∀ b ∈ l, f a b = g a b) :
foldl f a l = foldl g a l := by
induction l generalizing a with
| nil => rfl
| cons hd tl ih =>
unfold foldl
rw [ih _ fun a b bin => H a b <| mem_cons_of_mem _ bin, H a hd mem_cons_self]
