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