feat: interactions between List.foldX and List.filterX

src/Init/Data/List/Lemmas.lean

@@ -863,6 +863,22 @@ theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α
     (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
   induction l generalizing init <;> simp [*]
 
+theorem foldl_filterMap (f : α → Option β) (g : γ → β → γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldl g init = l.foldl (fun x y => match f y with | some b => g x b | none => x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldl_cons]
+    cases f a <;> simp [ih]
+
+theorem foldr_filterMap (f : α → Option β) (g : β → γ → γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldr g init = l.foldr (fun x y => match f x with | some b => g b y | none => y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldr_cons]
+    cases f a <;> simp [ih]
+
 theorem foldl_map' (g : α → β) (f : α → α → α) (f' : β → β → β) (a : α) (l : List α)
     (h : ∀ x y, f' (g x) (g y) = g (f x y)) :
     (l.map g).foldl f' (g a) = g (l.foldl f a) := by
@@ -1457,6 +1473,22 @@ theorem forall_mem_filter {l : List α} {p : α → Bool} {P : α → Prop} :
   | [] => rfl
   | a :: l => by by_cases hp : p a <;> by_cases hq : q a <;> simp [hp, hq, filter_filter _ l]
 
+theorem foldl_filter (p : α → Bool) (f : β → α → β) (l : List α) (init : β) :
+    (l.filter p).foldl f init = l.foldl (fun x y => if p y then f x y else x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldl_cons]
+    split <;> simp [ih]
+
+theorem foldr_filter (p : α → Bool) (f : α → β → β) (l : List α) (init : β) :
+    (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldr_cons]
+    split <;> simp [ih]
+
 theorem filter_map (f : β → α) (l : List β) : filter p (map f l) = map f (filter (p ∘ f) l) := by
   induction l with
   | nil => rfl

src/Init/Data/List/Monadic.lean

@@ -86,6 +86,42 @@ theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ 
     (init : α) : (l.map f).foldrM g init = l.foldrM (fun x y => g (f x) y) init := by
   induction l generalizing g init <;> simp [*]
 
+theorem foldlM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : γ → β → m γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldlM g init =
+      l.foldlM (fun x y => match f y with | some b => g x b | none => pure x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldlM_cons]
+    cases f a <;> simp [ih]
+
+theorem foldrM_filterMap [Monad m] [LawfulMonad m] (f : α → Option β) (g : β → γ → m γ) (l : List α) (init : γ) :
+    (l.filterMap f).foldrM g init =
+      l.foldrM (fun x y => match f x with | some b => g b y | none => pure y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filterMap_cons, foldrM_cons]
+    cases f a <;> simp [ih]
+
+theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : List α) (init : β) :
+    (l.filter p).foldlM g init =
+      l.foldlM (fun x y => if p y then g x y else pure x) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldlM_cons]
+    split <;> simp [ih]
+
+theorem foldrM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : α → β → m β) (l : List α) (init : β) :
+    (l.filter p).foldrM g init =
+      l.foldrM (fun x y => if p x then g x y else pure y) init := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons a l ih =>
+    simp only [filter_cons, foldrM_cons]
+    split <;> simp [ih]
+
 /-! ### forM -/
 
 -- We use `List.forM` as the simp normal form, rather that `ForM.forM`.