English
Let f be a right-commutative binary operation on α. For x ∈ β, a predicate q on α, a predicate p on β, and a multiset s of α, if for all a,b we have q a → p b → p (f b a), and p holds at x and for every a ∈ s, q a holds, then p (foldl f x s).
Русский
Пусть f — бинарная операция над типом α, правая коммутативна. Пусть x ∈ β, предикат q на α, предикат p на β и мультимножество s из α. Если для всех a,b выполняется q a → p b → p (f b a), и p выполняется в x, а для каждого a ∈ s выполняется q a, тогда p (foldl f x s).
LaTeX
$$$\\forall \\alpha\\ (f:\\\\beta\\\\to\\\\alpha\\\\to\\\\beta) [\\\\text{RightCommutative } f] (x:\\\\beta) (q:\\\\alpha\\\\to \\\\mathrm{Prop}) (p:\\\\beta\\\\to \\\\mathrm{Prop}) (s:\\\\mathrm{Multiset}\\\\ \\alpha),\\\\(\\\\forall a\\\\ b,\\\\ q\\\\ a \\\\to\\\\ p\\\\ b \\\\to\\\\ p\\\\ (f\\\\ b\\\\ a)) \\\\to p\\\\ x \\\\to (\\\\forall a \\\\in s,\\\\ q\\\\ a) \\\\to p\\\\ (foldl\\\\ f\\\\ x\\\\ s).$$
Lean4
theorem foldl_induction' (f : β → α → β) [RightCommutative f] (x : β) (q : α → Prop) (p : β → Prop) (s : Multiset α)
(hpqf : ∀ a b, q a → p b → p (f b a)) (px : p x) (q_s : ∀ a ∈ s, q a) : p (foldl f x s) :=
by
rw [foldl_swap]
exact foldr_induction' (fun x y => f y x) x q p s hpqf px q_s
