English
If f is left-commutative, then folding f over two permutation-related lists yields equal results for any accumulator.
Русский
Если f левая коммутативна, то перестановочно эквивалентные списки дают одинаковый результат при foldr.
LaTeX
$$$\\text{Forall } b, \\ \\operatorname{foldr} f\\; b\\; l_1 = \\operatorname{foldr} f\\; b\\; l_2$ for $l_1 \\sim l_2$ given left-commutativity$$
Lean4
theorem foldr_eq {f : α → β → β} {l₁ l₂ : List α} [lcomm : LeftCommutative f] (p : l₁ ~ l₂) :
∀ b, foldr f b l₁ = foldr f b l₂ := by
intro b
induction p using Perm.recOnSwap' generalizing b with
| nil => rfl
| cons _ _ r => simp [r b]
| swap' _ _ _ r => simp only [foldr_cons]; rw [lcomm.left_comm, r b]
| trans _ _ r₁ r₂ => exact Eq.trans (r₁ b) (r₂ b)
