feat: List.SatisfiesM_foldlM

Batteries/Data/List.lean

@@ -3,6 +3,7 @@ import Batteries.Data.List.Count
 import Batteries.Data.List.EraseIdx
 import Batteries.Data.List.Init.Lemmas
 import Batteries.Data.List.Lemmas
+import Batteries.Data.List.Monadic
 import Batteries.Data.List.OfFn
 import Batteries.Data.List.Pairwise
 import Batteries.Data.List.Perm

Batteries/Data/List/Monadic.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+import Batteries.Classes.SatisfiesM
+
+/-!
+# Results about monadic operations on `List`, in terms of `SatisfiesM`.
+
+-/
+
+namespace List
+
+theorem satisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (h₀ : motive b)
+    (h₁ : ∀ (b) (_ : motive b) (a : α) (_ : a ∈ l), SatisfiesM motive (f b a)) :
+    SatisfiesM motive (List.foldlM f b l) := by
+  have g b hb a am := Classical.indefiniteDescription _ (h₁ b hb a am)
+  clear h₁
+  induction l generalizing b with
+  | nil => exact SatisfiesM.pure h₀
+  | cons hd tl ih =>
+    simp only [foldlM_cons]
+    apply SatisfiesM.bind_pre
+    let ⟨q, qh⟩ := g b h₀ hd (mem_cons_self hd tl)
+    exact ⟨(fun ⟨b, bh⟩ => ⟨b, ih bh (fun b bh a am => g b bh a (mem_cons_of_mem hd am))⟩) <$> q,
+      by simpa using qh⟩
+
+theorem satisfiesM_foldrM [Monad m] [LawfulMonad m] {f : α → β → m β} (h₀ : motive b)
+    (h₁ : ∀ (a : α) (_ : a ∈ l) (b) (_ : motive b), SatisfiesM motive (f a b)) :
+    SatisfiesM motive (List.foldrM f b l) := by
+  induction l with
+  | nil => exact SatisfiesM.pure h₀
+  | cons hd tl ih =>
+    simp only [foldrM_cons]
+    apply SatisfiesM.bind_pre
+    let ⟨q, qh⟩ := ih (fun a am b hb => h₁ a (mem_cons_of_mem hd am) b hb)
+    exact ⟨(fun ⟨b, bh⟩ => ⟨b, h₁ hd (mem_cons_self hd tl) b bh⟩) <$> q,
+      by simpa using qh⟩
+
+end List