English
Let l be a list of indices ι, f: α → β → γ, op₁, op₂, op₃ be indexwise operations with a compatibility h: ∀ a b i, f (op₁ a i) (op₂ b i) = op₃ (f a b) i. Then foldl op₃ (f a b) l = f (foldl op₁ a l) (foldl op₂ b l).
Русский
Пусть l — список индексов ι, f: α → β → γ, оперaции op₁, op₂, op₃ индексно совместимы через h: ∀ a b i, f (op₁ a i) (op₂ b i) = op₃ (f a b) i. Тогда foldl op₃ (f a b) l = f (foldl op₁ a l) (foldl op₂ b l).
LaTeX
$$$$\forall l:\ List\ ι,\ f:\alpha\to\beta\to\gamma,\ op_1:\alpha\to ι\to\alpha,\ op_2:\beta\to ι\to\beta,\ op_3:\gamma\to ι\to\gamma,\ a:\alpha,\ b:\beta,\ (\forall a\ b\ i,\ f (op_1\ a\ i) (op_2\ b\ i) = op_3\ (f\ a\ b)\ i) \implies
\quad \operatorname{foldl} op_3 (f a b) l = f (\operatorname{foldl} op_1 a l) (\operatorname{foldl} op_2 b l).$$$$
Lean4
theorem foldl_hom₂ (l : List ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β) (op₃ : γ → ι → γ) (a : α) (b : β)
(h : ∀ a b i, f (op₁ a i) (op₂ b i) = op₃ (f a b) i) : foldl op₃ (f a b) l = f (foldl op₁ a l) (foldl op₂ b l) :=
Eq.symm <| by
revert a b
induction l <;> intros <;> [rfl; simp only [*, foldl]]
