English
Let f be a left-commutative binary operation on a type α. For any x ∈ α and any predicate p on α, and any finite multiset s of α, if p holds for x and for every element of s, and p is preserved under f in the sense that p a and p b imply p (f a b), then p (foldr f x s).
Русский
Пусть f — бинарная операция над типом α, слева коммутирующая. Для любого элемента x из α и любого предиката p на α, и для любого конечного мультимножества s из α, если p выполняется для x и для каждого элемента из s, и если p сохраняется при объединении двух элементов через f (то есть p a и p b ⇒ p (f a b)), то выполняется p (foldr f x s).
LaTeX
$$$\\forall \\alpha\\ (f:\\\\alpha\\\\to\\\\alpha\\\\to\\\\alpha)\\ [\\\\text{LeftCommutative } f]\\ (x:\\\\alpha)\\ (p:\\\\alpha\\\\to \\\\mathrm{Prop})\\ (s:\\\\mathrm{Multiset}\\\\ \\alpha),\\;\\left(\\\\forall a\\\\ b,\\\\ p\\\\ a \\\\to\\\\ p\\\\ b \\\\to\\\\ p\\\\ (f\\\\ a\\\\ b)\\\\right) \\\\to p\\\\ x \\\\to \\\\left(\\\\forall a \\\\in s,\\\\ p\\\\ a\\\\right) \\\\to \\\\ p\\\\ (foldr\\\\ f\\\\ x\\\\ s).$$
Lean4
theorem foldr_induction (f : α → α → α) [LeftCommutative f] (x : α) (p : α → Prop) (s : Multiset α)
(p_f : ∀ a b, p a → p b → p (f a b)) (px : p x) (p_s : ∀ a ∈ s, p a) : p (foldr f x s) :=
foldr_induction' f x p p s p_f px p_s
