English
Let f be a binary operation on α that is RightCommutative. For x ∈ α, a predicate p on α, a multiset s of α, and a function p_f establishing a closure under f, if p holds at x and on every element of s, then p holds at foldl f x s.
Русский
Пусть f — бинарная операция на α, которая является RightCommutative. Для x ∈ α и предиката p на α, мультимножества s из α, и функции p_f, устанавливающей замыкание по f, если p выполняется в x и на каждом элементе s, тогда p выполняется и на foldl f x s.
LaTeX
$$$\\forall \\alpha\\ (f:\\\\alpha\\\\to\\\\alpha\\\\to\\\\alpha) [\\\\text{RightCommutative } f] (x:\\\\alpha) (p:\\\\alpha\\\\to \\\\mathrm{Prop}) (s:\\\\mathrm{Multiset}\\\\ \\alpha), (\\\\forall a b,\\\\ p\\\\ a \\\\to\\\\ p\\\\ b \\\\to\\\\ p\\\\ (f\\\\ b\\\\ a)) \\\\to p\\\\ x \\\\to (\\\\forall a \\\\in s,\\\\ p\\\\ a) \\\\to p\\\\ (foldl\\\\ f\\\\ x\\\\ s).$$
Lean4
theorem foldl_induction (f : α → α → α) [RightCommutative f] (x : α) (p : α → Prop) (s : Multiset α)
(p_f : ∀ a b, p a → p b → p (f b a)) (px : p x) (p_s : ∀ a ∈ s, p a) : p (foldl f x s) :=
foldl_induction' f x p p s p_f px p_s
