[Merged by Bors] - feat: Bird–Wadler duality theorems

Mathlib.lean

@@ -3766,6 +3766,7 @@ public import Mathlib.Data.Int.SuccPred
 public import Mathlib.Data.Int.WithZero
 public import Mathlib.Data.List.AList
 public import Mathlib.Data.List.Basic
+public import Mathlib.Data.List.BirdWadler
 public import Mathlib.Data.List.Chain
 public import Mathlib.Data.List.ChainOfFn
 public import Mathlib.Data.List.Count

Mathlib/Data/List/Basic.lean

@@ -860,88 +860,6 @@ lemma append_cons_inj_of_notMem {x₁ x₂ z₁ z₂ : List α} {a₁ a₂ : α}
   · rintro ⟨rfl, rfl, rfl⟩
     rfl
 
-section FoldlEqFoldr
-
--- foldl and foldr coincide when f is commutative and associative
-variable {f : α → α → α}
-
-theorem foldl1_eq_foldr1 [hassoc : Std.Associative f] :
-    ∀ a b l, foldl f a (l ++ [b]) = foldr f b (a :: l)
-  | _, _, nil => rfl
-  | a, b, c :: l => by
-    simp only [cons_append, foldl_cons, foldr_cons, foldl1_eq_foldr1 _ _ l]
-    rw [hassoc.assoc]
-
-theorem foldl_eq_of_comm_of_assoc [hcomm : Std.Commutative f] [hassoc : Std.Associative f] :
-    ∀ a b l, foldl f a (b :: l) = f b (foldl f a l)
-  | a, b, nil => hcomm.comm a b
-  | a, b, c :: l => by
-    simp only [foldl_cons]
-    have : RightCommutative f := inferInstance
-    rw [← foldl_eq_of_comm_of_assoc .., this.right_comm, foldl_cons]
-
-theorem foldl_eq_foldr [Std.Commutative f] [Std.Associative f] :
-    ∀ a l, foldl f a l = foldr f a l
-  | _, nil => rfl
-  | a, b :: l => by
-    simp only [foldr_cons, foldl_eq_of_comm_of_assoc]
-    rw [foldl_eq_foldr a l]
-
-end FoldlEqFoldr
-
-section FoldlEqFoldr'
-
-variable {f : α → β → α}
-variable (hf : ∀ a b c, f (f a b) c = f (f a c) b)
-
-include hf
-
-theorem foldl_eq_of_comm' : ∀ a b l, foldl f a (b :: l) = f (foldl f a l) b
-  | _, _, [] => rfl
-  | a, b, c :: l => by rw [foldl, foldl, foldl, ← foldl_eq_of_comm' .., foldl, hf]
-
-theorem foldl_eq_foldr' : ∀ a l, foldl f a l = foldr (flip f) a l
-  | _, [] => rfl
-  | a, b :: l => by rw [foldl_eq_of_comm' hf, foldr, foldl_eq_foldr' ..]; rfl
-
-end FoldlEqFoldr'
-
-section FoldlEqFoldr'
-
-variable {f : α → β → β}
-
-theorem foldr_eq_of_comm' (hf : ∀ a b c, f a (f b c) = f b (f a c)) :
-    ∀ a b l, foldr f a (b :: l) = foldr f (f b a) l
-  | _, _, [] => rfl
-  | a, b, c :: l => by rw [foldr, foldr, foldr, hf, ← foldr_eq_of_comm' hf ..]; rfl
-
-end FoldlEqFoldr'
-
-section
-
-variable {op : α → α → α} [ha : Std.Associative op]
-
-/-- Notation for `op a b`. -/
-local notation a " ⋆ " b => op a b
-
--- Setting `priority := high` means that Lean will prefer this notation to the identical one
--- for `Seq.seq`
-/-- Notation for `foldl op a l`. -/
-local notation (priority := high) l " <*> " a => foldl op a l
-
-theorem foldl_op_eq_op_foldr_assoc :
-    ∀ {l : List α} {a₁ a₂}, ((l <*> a₁) ⋆ a₂) = a₁ ⋆ l.foldr (· ⋆ ·) a₂
-  | [], _, _ => rfl
-  | a :: l, a₁, a₂ => by
-    simp only [foldl_cons, foldr_cons, foldl_assoc, ha.assoc]; rw [foldl_op_eq_op_foldr_assoc]
-
-variable [hc : Std.Commutative op]
-
-theorem foldl_assoc_comm_cons {l : List α} {a₁ a₂} : ((a₁ :: l) <*> a₂) = a₁ ⋆ l <*> a₂ := by
-  rw [foldl_cons, hc.comm, foldl_assoc]
-
-end
-
 /-! ### foldlM, foldrM, mapM -/
 
 section FoldlMFoldrM

Mathlib/Data/List/BirdWadler.lean

@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2026 Jeremy Tan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Tan
+-/
+module
+
+public import Batteries.Tactic.Alias
+public import Mathlib.Logic.OpClass
+
+/-!
+# Bird–Wadler duality of list folds
+
+In their 1988 book _Introduction to Functional Programming_ [birdwadler],
+Richard Bird and Philip Wadler stated three duality theorems between `foldl` and `foldr`.
+Denoting the combining function as `f : α → β → β`, the theorems are:
+
+1. If `α = β` and `f` is commutative and associative, `l.foldl = l.foldr`
+2. If `f` is left-commutative, `l.foldl = l.foldr`
+3. `l.reverse.foldl = l.foldr` and `l.reverse.foldr = l.foldl`
+
+However, formalising these theorems in Lean (or Haskell or Scheme but not Rocq) presents a problem:
+`f`'s type in `foldl` is `β → α → β`. The history behind this difference is explored in an
+appendix to a paper by Olivier Danvy [danvy] about transforming functional programs
+between direct and continuation-passing styles. That paper uses a version of `foldl` whose `f` has
+type `α → β → β`, which not only removes the need for `flip` in the duality theorems' statements
+but also allows slightly generalising the first theorem to
+
+1. If `α = β`, `f` is associative and `a` commutes with all `x : α`, `l.foldl f a = l.foldr f a`
+
+This file defines the modified version of `foldl` as `foldf`, using it to state the duality theorems
+in their simplest and most general forms. Versions of the second theorem using `foldl` and `flip`
+are derived as corollaries.
+
+## Main declarations
+
+* `List.foldf`: `List.foldl` with a type signature matching `List.foldr`.
+* `List.foldl_eq_foldr_of_commute`, `List.foldl_eq_foldr`: first duality theorem.
+* `List.foldf_eq_foldr`: second duality theorem.
+* `List.foldf_reverse_eq_foldr`, `List.foldr_reverse_eq_foldf`: third duality theorem.
+-/
+
+@[expose] public section
+
+universe u v
+
+namespace List
+
+variable {α : Type u} {β : Type v} {l : List α} {f : α → β → β} {v : β → α → β} {a : α} {b : β}
+
+/--
+Folds a function over a list from the left, accumulating a value starting with `init`.
+The accumulated value is combined with the each element of the list in order, using `f`.
+
+This function differs from `List.foldl` in that its type signature matches `List.foldr`:
+`f` has type `α → β → β` instead of `β → α → β`.
+
+Examples:
+ * `[a, b, c].foldf f init = f c (f b (f a init))`
+ * `[1, 2, 3].foldf (toString · ++ ·) "" = "321"`
+ * `[1, 2, 3].foldf (s!"({·} {·})") "!" = "(3 (2 (1 !)))"`
+-/
+def foldf (f : α → β → β) (init : β) : List α → β
+  | []     => init
+  | a :: l => foldf f (f a init) l
+
+@[simp, grind =] theorem foldf_nil : [].foldf f b = b := rfl
+@[simp, grind =] theorem foldf_cons : (a :: l).foldf f b = l.foldf f (f a b) := rfl
+
+@[simp]
+theorem foldl_flip_eq_foldf : l.foldl (flip f) b = l.foldf f b := by
+  induction l generalizing b <;> simp [flip, *]
+
+@[simp]
+theorem foldf_flip_eq_foldl : l.foldf (flip v) b = l.foldl v b := by
+  induction l generalizing b <;> simp [flip, *]
+
+@[simp]
+theorem foldf_cons_eq_append {f : α → β} {l' : List β} :
+    l.foldf (f · :: ·) l' = (l.map f).reverse ++ l' := by
+  induction l generalizing l' <;> simp [*]
+
+@[simp, grind =]
+theorem foldf_cons_eq_append' {l' : List α} : l.foldf cons l' = l.reverse ++ l' := by
+  induction l generalizing l' <;> simp [*]
+
+theorem foldf_cons_nil : l.foldf cons [] = l.reverse := by simp
+
+@[simp, grind _=_]
+theorem foldf_append {l' : List α} : (l ++ l').foldf f b = l'.foldf f (l.foldf f b) := by
+  induction l generalizing b <;> simp [*]
+
+theorem foldl_permute [hv : RightCommutative v] : l.foldl v (v b a) = v (l.foldl v b) a := by
+  induction l generalizing a b <;> simp [*, hv.right_comm]
+
+theorem foldf_permute [hf : LeftCommutative f] : l.foldf f (f a b) = f a (l.foldf f b) := by
+  induction l generalizing b <;> simp [*, hf.left_comm]
+
+theorem foldr_permute [hf : LeftCommutative f] : l.foldr f (f a b) = f a (l.foldr f b) := by
+  induction l <;> simp [*, hf.left_comm]
+
+/-- First Bird–Wadler duality theorem. -/
+theorem foldl_eq_foldr_of_commute {f : α → α → α} [Std.Associative f] (ha : ∀ x, f a x = f x a) :
+    l.foldl f a = l.foldr f a := by
+  induction l <;> simp [*, foldl_assoc]
+
+/-- First Bird–Wadler duality theorem for commutative functions. -/
+theorem foldl_eq_foldr {f : α → α → α} [hf : Std.Commutative f] [Std.Associative f] :
+    l.foldl f a = l.foldr f a :=
+  foldl_eq_foldr_of_commute (hf.comm a)
+
+/-- Second Bird–Wadler duality theorem. -/
+theorem foldf_eq_foldr [LeftCommutative f] : l.foldf f b = l.foldr f b := by
+  induction l <;> simp [*, foldf_permute]
+
+theorem foldl_flip_eq_foldr [LeftCommutative f] : l.foldl (flip f) b = l.foldr f b := by
+  rw [foldl_flip_eq_foldf, foldf_eq_foldr]
+
+theorem foldr_flip_eq_foldl [RightCommutative v] : l.foldr (flip v) b = l.foldl v b := by
+  unfold flip
+  rw [← foldf_eq_foldr, ← foldf_flip_eq_foldl]
+  rfl
+
+/-- Third Bird–Wadler duality theorem.
+Corresponds to `foldl_reverse` and `foldr_eq_foldl_reverse` in the standard library. -/
+theorem foldf_reverse_eq_foldr : l.reverse.foldf f b = l.foldr f b := by
+  induction l <;> simp [*]
+
+/-- Third Bird–Wadler duality theorem.
+Corresponds to `foldr_reverse` and `foldl_eq_foldr_reverse` in the standard library. -/
+theorem foldr_reverse_eq_foldf : l.reverse.foldr f b = l.foldf f b := by
+  induction l generalizing b <;> simp [*]
+
+@[deprecated (since := "2026-02-24")] alias foldl_eq_of_comm' := foldl_permute
+@[deprecated (since := "2026-02-24")] alias foldr_eq_of_comm' := foldr_permute
+@[deprecated (since := "2026-02-24")] alias foldl_eq_foldr' := foldr_flip_eq_foldl
+
+theorem foldl1_eq_foldr1 {f : α → α → α} [ha : Std.Associative f] {a b : α} :
+    f (l.foldl f a) b = f a (l.foldr f b) := by
+  induction l generalizing a <;> simp [*, ha.assoc]
+
+@[deprecated (since := "2026-02-24")] alias foldl_eq_of_comm_of_assoc := foldl_permute
+@[deprecated (since := "2026-02-24")] alias foldl_op_eq_op_foldr_assoc := foldl1_eq_foldr1
+@[deprecated (since := "2026-02-24")] alias foldl_assoc_comm_cons := foldl_permute
+
+end List

docs/references.bib

@@ -454,6 +454,15 @@ @Book{            billingsley1999
   url           = {https://doi.org/10.1002/9780470316962}
 }
 
+@Book{            birdwadler,
+  author        = {Richard Bird and Philip Wadler},
+  year          = {1988},
+  title         = {Introduction to Functional Programming},
+  publisher     = {Prentice Hall},
+  address       = {New York},
+  isbn          = {978-0-13-484189-2}
+}
+
 @Article{         birkhoff1937,
   author        = {Birkhoff, Garrett},
   title         = {Rings of sets},
@@ -1443,6 +1452,17 @@ @Article{         crans2017
   url           = {https://doi.org/10.1007/s40062-016-0164-9}
 }
 
+@Article{         danvy,
+  author        = "Olivier Danvy",
+  title         = "Folding Left and Right Matters: Direct Style,
+                  Accumulators, and Continuations",
+  journal       = "Journal of Functional Programming",
+  year          = 2023,
+  volume        = 33,
+  number        = "e2",
+  doi           = "10.1017/S0956796822000156"
+}
+
 @Book{            dauben_1990,
   place         = {Princeton, NJ},
   title         = {Georg Cantor: His Mathematics and Philosophy of the