From 0d3360bf078021565785074855e523c42c9d145b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 11 Nov 2024 13:11:24 +1100
Subject: [PATCH] feat: List.SatisfiesM_foldlM

---
 Batteries/Data/List.lean         |  1 +
 Batteries/Data/List/Monadic.lean | 29 +++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 Batteries/Data/List/Monadic.lean

diff --git a/Batteries/Data/List.lean b/Batteries/Data/List.lean
index f93f90a6c2..3429039dc9 100644
--- a/Batteries/Data/List.lean
+++ b/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
diff --git a/Batteries/Data/List/Monadic.lean b/Batteries/Data/List/Monadic.lean
new file mode 100644
index 0000000000..7fa5fdfdbc
--- /dev/null
+++ b/Batteries/Data/List/Monadic.lean
@@ -0,0 +1,29 @@
+/-
+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 (List.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⟩
+
+end List