English
Given a function f: α → β → β and a multiset s, together with a proof that f is 'left-commutative' on all elements of s (i.e., swapping the arguments of successive applications yields the same result), there is a fold over s yielding an element of β: noncommFoldr(s, comm, b) = foldr of f over any linear extension of s.
Русский
Дано отображение f: α → β → β и мультимножество s вместе с доказательством того, что f удовлетворяет левому коммутативному свойству на всех элементах s; тогда существует свертка по s, которая даёт элемент β: noncommFoldr(s, comm, b) равен свертке по любому упорядочению s.
LaTeX
$$$\\mathrm{noncommFoldr}(s,\\,comm,\\,b) = s.{\\text{attach}}.\\mathrm{foldr}(f\\circ\\mathrm{Subtype.val}, b).$$$
Lean4
/-- Fold of a `s : Multiset α` with `f : α → β → β`, given a proof that `LeftCommutative f`
on all elements `x ∈ s`. -/
def noncommFoldr (s : Multiset α) (comm : {x | x ∈ s}.Pairwise fun x y => ∀ b, f x (f y b) = f y (f x b)) (b : β) : β :=
letI : LeftCommutative (α := { x // x ∈ s }) (f ∘ Subtype.val) :=
⟨fun ⟨_, hx⟩ ⟨_, hy⟩ =>
haveI : IsRefl α fun x y => ∀ b, f x (f y b) = f y (f x b) := ⟨fun _ _ => rfl⟩
comm.of_refl hx hy⟩
s.attach.foldr (f ∘ Subtype.val) b
