English
A variant of foldr induction: given q, p, base and membership-preserving assumptions, foldr f x s satisfies p.
Русский
Вариант индукции по foldr: при данных q, p, базовом и условиях сохранения принадлежности, выполняется p (foldr f x s).
LaTeX
$$$$ \\text{foldr_induction'}\\,(f, x, q, p, s, hpqf, px, q_s) : p(\\operatorname{foldr} f x s) $$$$
Lean4
theorem foldr_induction' (f : α → β → β) [LeftCommutative f] (x : β) (q : α → Prop) (p : β → Prop) (s : Multiset α)
(hpqf : ∀ a b, q a → p b → p (f a b)) (px : p x) (q_s : ∀ a ∈ s, q a) : p (foldr f x s) := by
induction s using Multiset.induction with
| empty => simpa
| cons a s ihs =>
simp only [forall_mem_cons, foldr_cons] at q_s ⊢
exact hpqf _ _ q_s.1 (ihs q_s.2)
