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 1/4] 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

From 731c7911031bde94f8229ed663843bfc15e8a653 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Tue, 12 Nov 2024 14:31:05 +1100
Subject: [PATCH 2/4] also foldrM

---
 Batteries/Data/List/Monadic.lean | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/Batteries/Data/List/Monadic.lean b/Batteries/Data/List/Monadic.lean
index 7fa5fdfdbc..055eccdb1b 100644
--- a/Batteries/Data/List/Monadic.lean
+++ b/Batteries/Data/List/Monadic.lean
@@ -22,8 +22,22 @@ theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (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)
+    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
+  have g a am b hb := Classical.indefiniteDescription _ (h₁ a am b hb)
+  clear h₁
+  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 => g a (mem_cons_of_mem hd am) b hb)
+    exact ⟨(fun ⟨b, bh⟩ => ⟨b, (g hd (mem_cons_self hd tl) b bh).existsOfSubtype⟩) <$> q,
+      by simpa using qh⟩
+
 end List

From 4acf5360327da8d94c0ee721b70705b17f329ce6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Tue, 12 Nov 2024 18:07:30 -0500
Subject: [PATCH 3/4] fix: naming convention

Co-authored-by: Eric Wieser <efw@google.com>
---
 Batteries/Data/List/Monadic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Batteries/Data/List/Monadic.lean b/Batteries/Data/List/Monadic.lean
index 055eccdb1b..789fdecd1e 100644
--- a/Batteries/Data/List/Monadic.lean
+++ b/Batteries/Data/List/Monadic.lean
@@ -12,7 +12,7 @@ import Batteries.Classes.SatisfiesM
 
 namespace List
 
-theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (h₀ : motive b)
+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)
@@ -26,7 +26,7 @@ theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (h
     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)
+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
   have g a am b hb := Classical.indefiniteDescription _ (h₁ a am b hb)

From d814fdaec9f920fd06c48417acef594f8b721957 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Tue, 12 Nov 2024 18:12:22 -0500
Subject: [PATCH 4/4] feat: avoid indefiniteDescription

Co-authored-by: Eric Wieser <efw@google.com>
---
 Batteries/Data/List/Monadic.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Batteries/Data/List/Monadic.lean b/Batteries/Data/List/Monadic.lean
index 789fdecd1e..00eb213755 100644
--- a/Batteries/Data/List/Monadic.lean
+++ b/Batteries/Data/List/Monadic.lean
@@ -29,15 +29,13 @@ theorem satisfiesM_foldlM [Monad m] [LawfulMonad m] {f : β → α → m β} (h
 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
-  have g a am b hb := Classical.indefiniteDescription _ (h₁ a am b hb)
-  clear h₁
   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 => g a (mem_cons_of_mem hd am) b hb)
-    exact ⟨(fun ⟨b, bh⟩ => ⟨b, (g hd (mem_cons_self hd tl) b bh).existsOfSubtype⟩) <$> q,
+    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