From 3ac9bbb3d87f6a8ccb3fce6378329e4b3e81c6d7 Mon Sep 17 00:00:00 2001
From: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Date: Wed, 17 Dec 2025 10:36:44 +0100
Subject: [PATCH] feat: MPL specs for loops over iterators (#11693)

This PR makes it possible to verify loops over iterators. It provides
MPL spec lemmas about `for` loops over pure iterators. It also provides
spec lemmas that rewrite loops over `mapM`, `filterMapM` or `filterM`
iterator combinators into loops over their base iterator.
---
 src/Init/Control/Lawful/Basic.lean            |   8 +-
 src/Init/Data/Iterators/Basic.lean            |   6 +-
 .../Iterators/Lemmas/Combinators/FlatMap.lean |   4 +-
 .../Lemmas/Combinators/Monadic/FilterMap.lean | 229 +++++++++++++++---
 .../Data/Iterators/Lemmas/Consumers/Loop.lean |   6 +-
 .../Lemmas/Consumers/Monadic/Loop.lean        |  65 +++++
 .../Data/Iterators/Lemmas/Producers/List.lean |   6 +-
 .../Lemmas/Producers/Monadic/List.lean        |   6 +-
 .../Iterators/Lemmas/Producers/Array.lean     |  12 +-
 .../Lemmas/Producers/Monadic/Array.lean       |  14 +-
 .../Lemmas/Producers/Monadic/List.lean        |   3 +-
 src/Std/Do/PostCond.lean                      |   2 +-
 src/Std/Do/SPred/DerivedLaws.lean             |   1 +
 src/Std/Do/SPred/Laws.lean                    |   2 +-
 src/Std/Do/Triple/SpecLemmas.lean             |  75 ++++++
 tests/lean/run/doLogicTests.lean              |  68 +++++-
 16 files changed, 436 insertions(+), 71 deletions(-)

diff --git a/src/Init/Control/Lawful/Basic.lean b/src/Init/Control/Lawful/Basic.lean
index c6d252c6a5..1b5d0421bb 100644
--- a/src/Init/Control/Lawful/Basic.lean
+++ b/src/Init/Control/Lawful/Basic.lean
@@ -248,10 +248,10 @@ namespace Id
 instance : LawfulMonad Id := by
   refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl
 
-@[simp] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
-@[simp] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
-@[simp] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
-@[simp] theorem pure_run (a : Id α) : pure a.run = a := rfl
+@[simp, grind =] theorem run_map (x : Id α) (f : α → β) : (f <$> x).run = f x.run := rfl
+@[simp, grind =] theorem run_bind (x : Id α) (f : α → Id β) : (x >>= f).run = (f x.run).run := rfl
+@[simp, grind =] theorem run_pure (a : α) : (pure a : Id α).run = a := rfl
+@[simp, grind =] theorem pure_run (a : Id α) : pure a.run = a := rfl
 @[simp] theorem run_seqRight (x y : Id α) : (x *> y).run = y.run := rfl
 @[simp] theorem run_seqLeft (x y : Id α) : (x <* y).run = x.run := rfl
 @[simp] theorem run_seq (f : Id (α → β)) (x : Id α) : (f <*> x).run = f.run x.run := rfl
diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index 84992a580d..372d97a68d 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -310,7 +310,7 @@ def PlausibleIterStep (IsPlausibleStep : IterStep α β → Prop) := Subtype IsP
 /--
 Match pattern for the `yield` case. See also `IterStep.yield`.
 -/
-@[match_pattern, simp, expose]
+@[match_pattern, simp, spec, expose]
 def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (out : β) (h : IsPlausibleStep (.yield it' out)) :
     PlausibleIterStep IsPlausibleStep :=
@@ -319,7 +319,7 @@ def PlausibleIterStep.yield {IsPlausibleStep : IterStep α β → Prop}
 /--
 Match pattern for the `skip` case. See also `IterStep.skip`.
 -/
-@[match_pattern, simp, expose]
+@[match_pattern, simp, grind =, expose]
 def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
     (it' : α) (h : IsPlausibleStep (.skip it')) : PlausibleIterStep IsPlausibleStep :=
   ⟨.skip it', h⟩
@@ -327,7 +327,7 @@ def PlausibleIterStep.skip {IsPlausibleStep : IterStep α β → Prop}
 /--
 Match pattern for the `done` case. See also `IterStep.done`.
 -/
-@[match_pattern, simp, expose]
+@[match_pattern, simp, grind =, expose]
 def PlausibleIterStep.done {IsPlausibleStep : IterStep α β → Prop}
     (h : IsPlausibleStep .done) : PlausibleIterStep IsPlausibleStep :=
   ⟨.done, h⟩
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
index 9a37520203..a66367635e 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/FlatMap.lean
@@ -247,7 +247,7 @@ public theorem Iter.toList_flatMapAfter {α α₂ β γ : Type w} [Iterator α I
       | some it₂ => it₂.toList ++
           (it₁.map fun b => (f b).toList).toList.flatten := by
   simp only [flatMapAfter, Iter.toList, toIterM_toIter, IterM.toList_flatMapAfter]
-  cases it₂ <;> simp [map]
+  cases it₂ <;> simp [map, IterM.toList_map_eq_toList_mapM, - IterM.toList_map]
 
 public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id] [IteratorCollect α Id Id] [IteratorCollect α₂ Id Id]
@@ -258,7 +258,7 @@ public theorem Iter.toArray_flatMapAfter {α α₂ β γ : Type w} [Iterator α
       | some it₂ => it₂.toArray ++
           (it₁.map fun b => (f b).toArray).toArray.flatten := by
   simp only [flatMapAfter, Iter.toArray, toIterM_toIter, IterM.toArray_flatMapAfter]
-  cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM]
+  cases it₂ <;> simp [map, IterM.toArray_map_eq_toArray_mapM, - IterM.toArray_map]
 
 public theorem Iter.toList_flatMap {α α₂ β γ : Type w} [Iterator α Id β] [Iterator α₂ Id γ]
     [Finite α Id] [Finite α₂ Id]
diff --git a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
index 3671f7b737..bc4c23ece3 100644
--- a/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean
@@ -1262,6 +1262,7 @@ theorem IterM.toArray_filterMapWithPostcondition {α β γ : Type w} {m : Type w
     (it.filterMapWithPostcondition f).toArray = it.toArray.run.filterMapM (fun x => (f x).run) := by
   simp [← toArray_toList]
 
+@[simp]
 theorem IterM.toArray_mapWithPostcondition {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m] [Iterator α Id β] [IteratorCollect α Id m]
     [LawfulIteratorCollect α Id m] [Finite α Id]
@@ -1280,6 +1281,7 @@ theorem IterM.toArray_filterMapM {α β γ : Type w} {m : Type w → Type w'}
     (it.filterMapM f).toArray = it.toArray.run.filterMapM f := by
   simp [← toArray_toList]
 
+@[simp]
 theorem IterM.toArray_mapM {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m]
     [Iterator α Id β] [IteratorCollect α Id m]
@@ -1289,6 +1291,7 @@ theorem IterM.toArray_mapM {α β γ : Type w} {m : Type w → Type w'}
     (it.mapM f).toArray = it.toArray.run.mapM f := by
   simp [← toArray_toList]
 
+@[simp]
 theorem IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'}
     [Monad m] [LawfulMonad m]
     [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m]
@@ -1296,12 +1299,14 @@ theorem IterM.toArray_filterMap {α β γ : Type w} {m : Type w → Type w'}
     (it.filterMap f).toArray = (fun x => x.filterMap f) <$> it.toArray := by
   simp [← toArray_toList]
 
+@[simp]
 theorem IterM.toArray_map {α β γ : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
     [Iterator α m β] [IteratorCollect α m m] [LawfulIteratorCollect α m m] [Finite α m] {f : β → γ}
     (it : IterM (α := α) m β) :
     (it.map f).toArray = (fun x => x.map f) <$> it.toArray := by
   simp [← toArray_toList]
 
+@[simp]
 theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
     {β : Type w} [Iterator α m β] [Finite α m] [IteratorCollect α m m] [LawfulIteratorCollect α m m]
     {f : β → Bool} {it : IterM (α := α) m β} :
@@ -1310,8 +1315,173 @@ theorem IterM.toArray_filter {α : Type w} {m : Type w → Type w'} [Monad m] [L
 
 end ToArray
 
+section ForIn
+
+@[spec]
+theorem IterM.forIn_filterMapWithPostcondition
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → PostconditionT n (Option β₂)} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    forIn (it.filterMapWithPostcondition f) init g = forIn it init (fun out acc => do
+        match ← (f out).run with
+        | some c => g c acc
+        | none => return .yield acc) := by
+  letI : MonadLift n o := ⟨monadLift⟩
+  simp only [PostconditionT.run_eq_map]
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
+  rw [IterM.forIn_eq_match_step, IterM.forIn_eq_match_step, IterM.step_filterMapWithPostcondition]
+  simp only [liftM_bind, bind_assoc]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp only [liftM_bind, bind_assoc, liftM_map, bind_map_left]
+    apply bind_congr; intro fx
+    match fx with
+    | ⟨none, _⟩ =>
+      simp [liftM_pure, pure_bind, Shrink.inflate_deflate, ihy ‹_›]
+    | ⟨some _, _⟩ =>
+      simp only [liftM_pure, pure_bind, Shrink.inflate_deflate]
+      apply bind_congr; intro gx
+      split <;> simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+@[spec]
+theorem IterM.forIn_filterMapM
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → n (Option β₂)} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    forIn (it.filterMapM f) init g = forIn it init (fun out acc => do
+        match ← f out with
+        | some c => g c acc
+        | none => return .yield acc) := by
+  rw [filterMapM, forIn_filterMapWithPostcondition]
+  simp [PostconditionT.run_attachLift]
+
+theorem IterM.forIn_filterMap
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    {it : IterM (α := α) m β} {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} :
+    forIn (it.filterMap f) init g = forIn it init (fun out acc => do
+        match f out with
+        | some c => g c acc
+        | none => return .yield acc) := by
+  rw [filterMap, forIn_filterMapWithPostcondition]
+  simp [PostconditionT.run_eq_map]
+
+@[spec]
+theorem IterM.forIn_mapWithPostcondition
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → PostconditionT n β₂} {init : γ}
+    {g : β₂ → γ → o (ForInStep γ)} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    forIn (it.mapWithPostcondition f) init g =
+      forIn it init (fun out acc => do g (← (f out).run) acc) := by
+  rw [mapWithPostcondition, InternalCombinators.map, ← InternalCombinators.filterMap,
+    ← filterMapWithPostcondition, forIn_filterMapWithPostcondition]
+  simp [PostconditionT.run_eq_map]
+
+@[spec]
+theorem IterM.forIn_mapM
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    forIn (it.mapM f) init g = forIn it init (fun out acc => do g (← f out) acc) := by
+  rw [mapM, forIn_mapWithPostcondition]
+  simp [PostconditionT.run_attachLift]
+
+theorem IterM.forIn_map
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    {it : IterM (α := α) m β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)} :
+    forIn (it.map f) init g = forIn it init (fun out acc => do g (f out) acc) := by
+  rw [map, forIn_mapWithPostcondition]
+  simp [PostconditionT.run_eq_map]
+
+@[spec]
+theorem IterM.forIn_filterWithPostcondition
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → PostconditionT n (ULift Bool)} {init : γ}
+    {g : β → γ → o (ForInStep γ)} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    forIn (it.filterWithPostcondition f) init g =
+      forIn it init (fun out acc => do if (← (f out).run).down then g out acc else return .yield acc) := by
+  rw [filterWithPostcondition, forIn_filterMapWithPostcondition]
+  congr 1; ext out acc
+  simp only [PostconditionT.map_eq_pure_bind, PostconditionT.run_eq_map,
+    PostconditionT.operation_bind, Function.comp_apply, PostconditionT.operation_pure, map_pure,
+    bind_pure_comp, liftM_map, bind_map_left]
+  apply bind_congr; intro fx
+  cases fx.val.down <;> simp
+
+@[spec]
+theorem IterM.forIn_filterM
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n] [Monad o] [LawfulMonad o]
+    [MonadAttach n] [WeaklyLawfulMonadAttach n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT n o]
+    [Iterator α m β] [Finite α m]
+    [IteratorLoop α m o] [LawfulIteratorLoop α m o]
+    {it : IterM (α := α) m β} {f : β → n (ULift Bool)} {init : γ} {g : β → γ → o (ForInStep γ)} :
+    haveI : MonadLift n o := ⟨monadLift⟩
+    forIn (it.filterM f) init g = forIn it init (fun out acc => do if (← f out).down then g out acc else return .yield acc) := by
+  rw [filterM, ← filterWithPostcondition, forIn_filterWithPostcondition]
+  simp [PostconditionT.run_attachLift]
+
+theorem IterM.forIn_filter
+    [Monad m] [LawfulMonad m] [Monad n] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n]
+    [Iterator α m β] [Finite α m] [IteratorLoop α m n] [LawfulIteratorLoop α m n]
+    {it : IterM (α := α) m β} {f : β → Bool} {init : γ} {g : β → γ → n (ForInStep γ)} :
+    forIn (it.filter f) init g = forIn it init (fun out acc => do if f out then g out acc else return .yield acc) := by
+  rw [filter, forIn_filterMap]
+  congr 1; ext out acc
+  cases f out <;> simp
+
+end ForIn
+
 section Fold
 
+@[spec]
+theorem IterM.foldM_filterMapWithPostcondition {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+    (it.filterMapWithPostcondition f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do
+          let some c ← (f b).run | pure d
+          g d c) := by
+  simp only [foldM_eq_forIn, forIn_filterMapWithPostcondition]
+  congr 1; ext out acc
+  simp only [map_bind]
+  apply bind_congr; intro fx
+  split <;> simp
+
+@[spec]
 theorem IterM.foldM_filterMapM {α β γ δ : Type w}
     {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
     [Iterator α m β] [Finite α m]
@@ -1327,18 +1497,23 @@ theorem IterM.foldM_filterMapM {α β γ δ : Type w}
       it.foldM (init := init) (fun d b => do
           let some c ← f b | pure d
           g d c) := by
-  letI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
-  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
-  rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMapM, liftM_bind, bind_assoc]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp only [PlausibleIterStep.skip, PlausibleIterStep.yield, liftM_bind, bind_assoc]
-    conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (x := f _), liftM_map, bind_map_left]
-    apply bind_congr; intro c?
-    split <;> simp [ihy ‹_›]
-  · simp [ihs ‹_›]
-  · simp
+  simp [filterMapM, foldM_filterMapWithPostcondition, PostconditionT.run_attachLift]
 
+@[spec]
+theorem IterM.foldM_mapWithPostcondition {α β γ δ : Type w}
+    {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
+    [Iterator α m β] [Finite α m]
+    [Monad m] [Monad n] [Monad o] [LawfulMonad m] [LawfulMonad n] [LawfulMonad o]
+    [IteratorLoop α m n] [IteratorLoop α m o]
+    [LawfulIteratorLoop α m n] [LawfulIteratorLoop α m o]
+    [MonadLiftT m n] [MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
+    {f : β → PostconditionT n γ} {g : δ → γ → o δ} {init : δ} {it : IterM (α := α) m β} :
+    haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
+    (it.mapWithPostcondition f).foldM (init := init) g =
+      it.foldM (init := init) (fun d b => do let c ← (f b).run; g d c) := by
+  simp [foldM_eq_forIn, forIn_mapWithPostcondition]
+
+@[spec]
 theorem IterM.foldM_mapM {α β γ δ : Type w}
     {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
     [Iterator α m β] [Finite α m]
@@ -1352,16 +1527,7 @@ theorem IterM.foldM_mapM {α β γ δ : Type w}
     haveI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
     (it.mapM f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do let c ← f b; g d c) := by
-  letI : MonadLift n o := ⟨MonadLiftT.monadLift⟩
-  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
-  rw [foldM_eq_match_step, foldM_eq_match_step, step_mapM, liftM_bind, bind_assoc]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp only [bind_pure_comp, liftM_map, bind_map_left, Shrink.inflate_deflate, bind_assoc]
-    conv => rhs; rw [← WeaklyLawfulMonadAttach.map_attach (x := f _)]
-    simp [ihy ‹_›]
-  · simp [ihs ‹_›]
-  · simp
+  simp [foldM_eq_forIn, forIn_mapM]
 
 theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
@@ -1373,14 +1539,9 @@ theorem IterM.foldM_filterMap {α β γ δ : Type w} {m : Type w → Type w'} {n
       it.foldM (init := init) (fun d b => do
           let some c := f b | pure d
           g d c) := by
-  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
-  rw [foldM_eq_match_step, foldM_eq_match_step, step_filterMap, liftM_bind, bind_assoc]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp only [PlausibleIterStep.skip, PlausibleIterStep.yield]
-    split <;> simp [ihy ‹_›, *]
-  · simp [ihs ‹_›]
-  · simp
+  simp only [foldM_eq_forIn, forIn_filterMap]
+  congr 1; ext out acc
+  split <;> simp [*]
 
 theorem IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m] [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
@@ -1390,14 +1551,9 @@ theorem IterM.foldM_map {α β γ δ : Type w} {m : Type w → Type w'} {n : Typ
     {f : β → γ} {g : δ → γ → n δ} {init : δ} {it : IterM (α := α) m β} :
     (it.map f).foldM (init := init) g =
       it.foldM (init := init) (fun d b => do g d (f b)) := by
-  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
-  rw [foldM_eq_match_step, foldM_eq_match_step, step_map, liftM_bind, bind_assoc]
-  apply bind_congr; intro step
-  cases step.inflate using PlausibleIterStep.casesOn
-  · simp [ihy ‹_›]
-  · simp [ihs ‹_›]
-  · simp
+  simp [foldM_eq_forIn, forIn_map]
 
+@[spec]
 theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m]
@@ -1412,6 +1568,7 @@ theorem IterM.fold_filterMapM {α β γ δ : Type w} {m : Type w → Type w'} {n
           return g d c) := by
   simp [fold_eq_foldM, foldM_filterMapM]
 
+@[spec]
 theorem IterM.fold_mapM {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''}
     [Iterator α m β] [Finite α m]
     [Monad m] [LawfulMonad m]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
index 002f66c9ec..d79061ffa3 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean
@@ -364,9 +364,9 @@ theorem Iter.foldlM_toList {α β : Type w} {γ : Type x} [Iterator α Id β] [F
     {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
     [LawfulIteratorLoop α Id m] [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
     {f : γ → β → m γ} {init : γ} {it : Iter (α := α) β} :
-    it.toList.foldlM (init := init) f = it.foldM (init := init) f := by
-  rw [Iter.foldM_eq_forIn, ← Iter.forIn_toList]
-  simp only [List.forIn_yield_eq_foldlM, id_map']
+    it.toList.foldlM (init := init) f = it.foldM (init := init) f:= by
+  rw [foldM_eq_forIn, ← Iter.forIn_toList]
+  simp
 
 theorem Iter.foldlM_toArray {α β : Type w} {γ : Type x} [Iterator α Id β] [Finite α Id]
     {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m]
diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
index 4a47195424..15a348ca56 100644
--- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
+++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean
@@ -218,6 +218,36 @@ theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite
   simp only [forIn]
   exact forIn'_eq_match_step
 
+theorem IterM.forIn_toList {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : IterM (α := α) Id β} {f : β → γ → m (ForInStep γ)} {init : γ} :
+    ForIn.forIn it.toList.run init f = ForIn.forIn it init f := by
+  rw [List.forIn_eq_foldlM]
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
+  rw [forIn_eq_match_step, IterM.toList_eq_match_step]
+  simp only [map_eq_pure_bind, Id.run_bind, liftM, monadLift, pure_bind]
+  cases it.step.run.inflate using PlausibleIterStep.casesOn
+  · rename_i it' out h
+    simp only [List.foldlM_cons, bind_pure_comp, map_bind, Id.run_map]
+    apply bind_congr
+    intro forInStep
+    cases forInStep
+    · induction it'.toList.run <;> simp [*]
+    · simp only [ForIn.forIn] at ihy
+      simp [ihy h]
+  · rename_i it' h
+    simp only [bind_pure_comp]
+    rw [ihs h]
+  · simp
+
+theorem IterM.forIn_toArray {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : IterM (α := α) Id β} {f : β → γ → m (ForInStep γ)} {init : γ} :
+    ForIn.forIn it.toArray.run init f = ForIn.forIn it init f := by
+  simp [← toArray_toList, forIn_toList]
+
 theorem IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β]
     [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n]
     [IteratorLoop α m n] [LawfulIteratorLoop α m n]
@@ -356,6 +386,41 @@ theorem IterM.toArray_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterato
   rw [← fold_hom]
   simp
 
+theorem IterM.foldlM_toList {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : IterM (α := α) Id β} {f : γ → β → m γ} {init : γ} :
+    it.toList.run.foldlM f init = it.foldM f init := by
+  simp [foldM_eq_forIn, ← forIn_toList]
+
+theorem IterM.foldlM_toArray {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α Id β]
+    [Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : IterM (α := α) Id β} {f : γ → β → m γ} {init : γ} :
+    it.toArray.run.foldlM f init = it.foldM f init := by
+  simp [← toArray_toList, foldlM_toList]
+
+theorem IterM.foldl_toList {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {it : IterM (α := α) m β} {f : γ → β → γ} {init : γ} :
+    (·.foldl f init) <$> it.toList = it.fold f init := by
+  induction it using IterM.inductSteps generalizing init with | step it ihy ihs
+  rw [toList_eq_match_step, fold_eq_match_step]
+  simp only [bind_pure_comp, map_bind]
+  apply bind_congr; intro step
+  cases step.inflate using PlausibleIterStep.casesOn
+  · simp [ihy ‹_›]
+  · simp [ihs ‹_›]
+  · simp
+
+theorem IterM.foldl_toArray {α β : Type w} [Monad m] [LawfulMonad m] [Iterator α m β]
+    [Finite α m] [IteratorLoop α m m] [LawfulIteratorLoop α m m]
+    [IteratorCollect α m m] [LawfulIteratorCollect α m m]
+    {it : IterM (α := α) m β} {f : γ → β → γ} {init : γ} :
+    (·.foldl f init) <$> it.toArray = it.fold f init := by
+  simp only [← toArray_toList, Functor.map_map, List.foldl_toArray, foldl_toList]
+
 theorem IterM.drain_eq_fold {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m]
     [Monad m] [IteratorLoop α m m] {it : IterM (α := α) m β} :
     it.drain = it.fold (init := PUnit.unit) (fun _ _ => .unit) :=
diff --git a/src/Init/Data/Iterators/Lemmas/Producers/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
index e8e94c87f4..e49423bbc8 100644
--- a/src/Init/Data/Iterators/Lemmas/Producers/List.lean
+++ b/src/Init/Data/Iterators/Lemmas/Producers/List.lean
@@ -34,17 +34,17 @@ theorem List.step_iter_cons {x : β} {xs : List β} :
   simp [List.iter, List.iterM, IterM.mk, IterM.toIter, Iter.step, Iter.toIterM, IterM.step,
     Iterator.step]
 
-@[simp]
+@[simp, grind =]
 theorem List.toArray_iter {l : List β} :
     l.iter.toArray = l.toArray := by
   simp [List.iter, List.toArray_iterM, Iter.toArray_eq_toArray_toIterM]
 
-@[simp]
+@[simp, grind =]
 theorem List.toList_iter {l : List β} :
     l.iter.toList = l := by
   simp [List.iter, List.toList_iterM]
 
-@[simp]
+@[simp, grind =]
 theorem List.toListRev_iter {l : List β} :
     l.iter.toListRev = l.reverse := by
   simp [List.iter, Iter.toListRev_eq_toListRev_toIterM, List.toListRev_iterM]
diff --git a/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean
index f57fc8078a..aeea79ba64 100644
--- a/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean
+++ b/src/Init/Data/Iterators/Lemmas/Producers/Monadic/List.lean
@@ -51,18 +51,18 @@ theorem Std.Iterators.Types.ListIterator.toArrayMapped_iterM [Monad n] [LawfulMo
     rw [IterM.DefaultConsumers.toArrayMapped_eq_match_step]
     simp [List.step_iterM_cons, List.mapM_cons, pure_bind, ih, LawfulMonadLiftFunction.lift_pure]
 
-@[simp]
+@[simp, grind =]
 theorem List.toArray_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).toArray = pure l.toArray := by
   simp only [IterM.toArray, ListIterator.toArrayMapped_iterM]
   rw [List.mapM_pure, map_pure, List.map_id']
 
-@[simp]
+@[simp, grind =]
 theorem List.toList_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).toList = pure l := by
   rw [← IterM.toList_toArray, List.toArray_iterM, map_pure, List.toList_toArray]
 
-@[simp]
+@[simp, grind =]
 theorem List.toListRev_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).toListRev = pure l.reverse := by
   simp [IterM.toListRev_eq, List.toList_iterM]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
index 00231a1f11..79d4f7f6b9 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Array.lean
@@ -58,34 +58,34 @@ theorem Array.step_iter {array : Array β} :
         .done (Nat.not_lt.mp h) := by
   simp only [Array.iter_eq_iterFromIdx, Array.step_iterFromIdx]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toList_iterFromIdx {array : Array β}
     {pos : Nat} :
     (array.iterFromIdx pos).toList = array.toList.drop pos := by
   simp [Iter.toList, Array.iterFromIdx_eq_toIter_iterFromIdxM, Iter.toIterM_toIter,
     Array.toList_iterFromIdxM]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toList_iter {array : Array β} :
     array.iter.toList = array.toList := by
   simp [Array.iter_eq_iterFromIdx, Array.toList_iterFromIdx]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toArray_iterFromIdx {array : Array β} {pos : Nat} :
     (array.iterFromIdx pos).toArray = array.extract pos := by
   simp [iterFromIdx_eq_toIter_iterFromIdxM, Iter.toArray]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toArray_toIter {array : Array β} :
     array.iter.toArray = array := by
   simp [Array.iter_eq_iterFromIdx]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toListRev_iterFromIdx {array : Array β} {pos : Nat} :
     (array.iterFromIdx pos).toListRev = (array.toList.drop pos).reverse := by
   simp [Iter.toListRev_eq, Array.toList_iterFromIdx]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toListRev_toIter {array : Array β} :
     array.iter.toListRev = array.toListRev := by
   simp [Array.iter_eq_iterFromIdx]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
index 5adaccf7eb..248f85bf49 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean
@@ -92,7 +92,7 @@ theorem Array.iterFromIdxM_equiv_iterM_drop_toList {α : Type w} {array : Array
   intro it
   match it with
   | Array.iterFromIdxM array _ pos =>
-    rw [ArrayIterator.stepAsHetT_iterFromIdxM, ListIterator.stepAsHetT_iterM]
+    rw [ArrayIterator.stepAsHetT_iterFromIdxM, Types.ListIterator.stepAsHetT_iterM]
     simp [Array.iterFromIdxM, IterM.mk]
     rw [show array = array.toList.toArray from Array.toArray_toList]
     generalize array.toList = l
@@ -122,35 +122,35 @@ theorem Array.iterM_equiv_iterM_toList {α : Type w} {array : Array α} {m : Typ
 
 end Equivalence
 
-@[simp]
+@[simp, grind =]
 theorem Array.toList_iterFromIdxM [LawfulMonad m] {array : Array β}
     {pos : Nat} :
     (array.iterFromIdxM m pos).toList = pure (array.toList.drop pos) := by
   simp [Array.iterFromIdxM_equiv_iterM_drop_toList.toList_eq]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toList_iterM [LawfulMonad m] {array : Array β} :
     (array.iterM m).toList = pure array.toList := by
   simp [Array.iterM_eq_iterFromIdxM, Array.toList_iterFromIdxM]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toArray_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} :
     (array.iterFromIdxM m pos).toArray = pure (array.extract pos) := by
   simp [← IterM.toArray_toList, Array.toList_iterFromIdxM]
   rw (occs := [2]) [← Array.toArray_toList (xs := array)]
   rw [← List.toArray_drop]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toArray_toIterM [LawfulMonad m] {array : Array β} :
     (array.iterM m).toArray = pure array := by
   simp [Array.iterM_eq_iterFromIdxM, Array.toArray_iterFromIdxM]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toListRev_iterFromIdxM [LawfulMonad m] {array : Array β} {pos : Nat} :
     (array.iterFromIdxM m pos).toListRev = pure (array.toList.drop pos).reverse := by
   simp [IterM.toListRev_eq, Array.toList_iterFromIdxM]
 
-@[simp]
+@[simp, grind =]
 theorem Array.toListRev_toIterM [LawfulMonad m] {array : Array β} :
     (array.iterM m).toListRev = pure array.toListRev := by
   simp [Array.iterM_eq_iterFromIdxM, Array.toListRev_iterFromIdxM]
diff --git a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
index 02e1e68ebb..6dbb8a7c0c 100644
--- a/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
+++ b/src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean
@@ -9,13 +9,14 @@ prelude
 public import Init.Data.Iterators.Lemmas.Producers.Monadic.List
 public import Std.Data.Iterators.Lemmas.Equivalence.Basic
 
+
 namespace Std
 open Std.Internal Std.Iterators Std.Iterators.Types
 
 variable {m : Type w → Type w'} {n : Type w → Type w''} [Monad m] {β : Type w}
 
 -- We don't want to pollute `List` with this rarely used lemma.
-public theorem ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
+public theorem Types.ListIterator.stepAsHetT_iterM [LawfulMonad m] {l : List β} :
     (l.iterM m).stepAsHetT = (match l with
       | [] => pure .done
       | x :: xs => pure (.yield (xs.iterM m) x)) := by
diff --git a/src/Std/Do/PostCond.lean b/src/Std/Do/PostCond.lean
index a318b58a4d..32913f175f 100644
--- a/src/Std/Do/PostCond.lean
+++ b/src/Std/Do/PostCond.lean
@@ -171,7 +171,7 @@ def ExceptConds.entails {ps : PostShape.{u}} (x y : ExceptConds ps) : Prop :=
 @[inherit_doc ExceptConds.entails]
 scoped infixr:25 " ⊢ₑ " => ExceptConds.entails
 
-@[refl, simp]
+@[refl, simp, grind ←]
 theorem ExceptConds.entails.refl {ps : PostShape} (x : ExceptConds ps) : x ⊢ₑ x := by
   induction ps <;> simp [entails, *]
 
diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean
index 8087693255..96662bf7e2 100644
--- a/src/Std/Do/SPred/DerivedLaws.lean
+++ b/src/Std/Do/SPred/DerivedLaws.lean
@@ -128,6 +128,7 @@ theorem pure_elim {φ : Prop} (h1 : Q ⊢ₛ ⌜φ⌝) (h2 : φ → Q ⊢ₛ R)
   and_self.mpr.trans <| imp_elim <| h1.trans <| pure_elim' fun h =>
     imp_intro' <| and_elim_l.trans (h2 h)
 
+@[grind ←]
 theorem pure_mono {φ₁ φ₂ : Prop} (h : φ₁ → φ₂) : ⌜φ₁⌝ ⊢ₛ (⌜φ₂⌝ : SPred σs) := pure_elim' <| pure_intro ∘ h
 theorem pure_congr {φ₁ φ₂ : Prop} (h : φ₁ ↔ φ₂) : ⌜φ₁⌝ ⊣⊢ₛ (⌜φ₂⌝ : SPred σs) := bientails.iff.mpr ⟨pure_mono h.1, pure_mono h.2⟩
 
diff --git a/src/Std/Do/SPred/Laws.lean b/src/Std/Do/SPred/Laws.lean
index 4ce244e7b8..04aae44bd0 100644
--- a/src/Std/Do/SPred/Laws.lean
+++ b/src/Std/Do/SPred/Laws.lean
@@ -29,7 +29,7 @@ variable {σs : List (Type u)}
 
 /-! # Entailment -/
 
-@[refl, simp]
+@[refl, simp, grind ←]
 theorem entails.refl (P : SPred σs) : P ⊢ₛ P := by
   induction σs with
   | nil => simp [entails]
diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean
index 42de98cf8f..51c5e9f137 100644
--- a/src/Std/Do/Triple/SpecLemmas.lean
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@@ -1163,6 +1163,81 @@ theorem Spec.forIn_slice {m : Type w → Type x} {ps : PostShape}
   simp only [← Slice.forIn_toList]
   exact Spec.forIn_list inv step
 
+open Std.Iterators in
+@[spec]
+theorem Spec.forIn_iter {ps : PostShape} [Monad n] [WPMonad n ps]
+    {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {init : γ} {f : β → γ → n (ForInStep γ)}
+    {it : Iter (α := α) β}
+    (inv : Invariant it.toList γ ps)
+    (step : ∀ pref cur suff (h : it.toList = pref ++ cur :: suff) b,
+      Triple
+        (f cur b)
+        (inv.1 (⟨pref, cur::suff, h.symm⟩, b))
+        (fun r => match r with
+          | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+          | .done b' => inv.1 (⟨it.toList, [], by simp⟩, b'), inv.2)) :
+    Triple (forIn it init f) (inv.1 (⟨[], it.toList, rfl⟩, init)) (fun b => inv.1 (⟨it.toList, [], by simp⟩, b), inv.2) := by
+  simp only [← Iter.forIn_toList]
+  exact Spec.forIn_list inv step
+
+open Std.Iterators in
+@[spec]
+theorem Spec.forIn_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
+    {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {init : γ} {f : β → γ → n (ForInStep γ)}
+    {it : IterM (α := α) Id β}
+    (inv : Invariant it.toList.run γ ps)
+    (step : ∀ pref cur suff (h : it.toList.run = pref ++ cur :: suff) b,
+      Triple
+        (f cur b)
+        (inv.1 (⟨pref, cur::suff, h.symm⟩, b))
+        (fun r => match r with
+          | .yield b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b')
+          | .done b' => inv.1 (⟨it.toList.run, [], by simp⟩, b'), inv.2)) :
+    Triple (forIn it init f) (inv.1 (⟨[], it.toList.run, rfl⟩, init)) (fun b => inv.1 (⟨it.toList.run, [], by simp⟩, b), inv.2) := by
+  conv =>
+    congr
+    rw [← Iter.toIterM_toIter (it := it), ← Iter.forIn_eq_forIn_toIterM, ← Iter.forIn_toList,
+      IterM.toList_toIter]
+  exact Spec.forIn_list inv step
+
+open Std.Iterators in
+@[spec]
+theorem Spec.foldM_iter {ps : PostShape} [Monad n] [WPMonad n ps]
+    {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : Iter (α := α) β}
+    {init : γ} {f : γ → β → n γ}
+    (inv : Invariant it.toList γ ps)
+    (step : ∀ pref cur suff (h : it.toList = pref ++ cur :: suff) b,
+      Triple
+        (f b cur)
+        (inv.1 (⟨pref, cur::suff, h.symm⟩, b))
+        (fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)) :
+    Triple (it.foldM f init) (inv.1 (⟨[], it.toList, rfl⟩, init)) (fun b => inv.1 (⟨it.toList, [], by simp⟩, b), inv.2) := by
+  rw [← Iter.foldlM_toList]
+  exact Spec.foldlM_list inv step
+
+open Std.Iterators in
+@[spec]
+theorem Spec.foldM_iterM_id {ps : PostShape} [Monad n] [WPMonad n ps]
+    {α β γ} [Iterator α Id β] [Finite α Id] [IteratorLoop α Id n] [LawfulIteratorLoop α Id n]
+    [IteratorCollect α Id Id] [LawfulIteratorCollect α Id Id]
+    {it : IterM (α := α) Id β}
+    {init : γ} {f : γ → β → n γ}
+    (inv : Invariant it.toList.run γ ps)
+    (step : ∀ pref cur suff (h : it.toList.run = pref ++ cur :: suff) b,
+      Triple
+        (f b cur)
+        (inv.1 (⟨pref, cur::suff, h.symm⟩, b))
+        (fun b' => inv.1 (⟨pref ++ [cur], suff, by simp [h]⟩, b'), inv.2)) :
+    Triple (it.foldM f init) (inv.1 (⟨[], it.toList.run, rfl⟩, init)) (fun b => inv.1 (⟨it.toList.run, [], by simp⟩, b), inv.2) := by
+  rw [← IterM.foldlM_toList]
+  exact Spec.foldlM_list inv step
+
 @[spec]
 theorem Spec.forIn'_array {α β : Type u} {m : Type u → Type v} {ps : PostShape}
     [Monad m] [WPMonad m ps]
diff --git a/tests/lean/run/doLogicTests.lean b/tests/lean/run/doLogicTests.lean
index e9d8c1cc63..c1547ab1ed 100644
--- a/tests/lean/run/doLogicTests.lean
+++ b/tests/lean/run/doLogicTests.lean
@@ -6,6 +6,7 @@ Authors: Sebastian Graf
 
 import Std
 import Lean.Elab.Tactic.Do.VCGen
+import Lean
 
 open Std.Do
 
@@ -914,4 +915,69 @@ example  : (hp : ∀m, m = 42 → q → p) → (hinv : ∀ (inv : Nat → Prop),
   -- exact hp ?n ?prf2
   case prf2 => rfl
   case inv => exact fun _ => True
-  case prf1 => trivial
+  case prf1 => grind
+
+variable {m} [Monad m]
+open Std Std.Iterators
+
+theorem forIn_eq_sum (xs : Array Nat) {m ps} [Monad m] [WPMonad m ps] :
+    Triple (m := m) (do
+      let mut sum : Nat := 0
+      for n in xs.iter do
+        sum := sum + n
+      return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum⌝) := by
+  mvcgen
+  case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
+  · simp only [List.sum_append_nat, List.sum_cons, List.sum_nil, Nat.add_zero,
+    Nat.add_right_cancel_iff, SPred.entails.refl]
+  · simp only [List.sum_nil, SPred.entails.refl]
+  · simp only [Array.toList_iter, Array.sum_eq_sum_toList, SPred.entails.refl]
+  · simp only [ExceptConds.entails.refl]
+
+theorem forIn_map_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
+    [WPMonad m ps] :
+    Triple (m := m) (do
+      let mut sum : Nat := 0
+      for n in (xs.iterM Id).map (· + 1) do
+        sum := sum + n
+      return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
+  mvcgen
+  case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
+  all_goals (try grind)
+  apply SPred.pure_mono
+  simp only [IterM.toList_map, Array.toList_iterM, map_pure, Id.run_pure]
+  rw [← Array.sum_eq_sum_toList, ← Array.length_toList]
+  rename_i r
+  induction xs.toList generalizing r <;> grind
+
+theorem forIn_mapM_eq_sum_add_size (xs : Array Nat) {m ps} [Monad m] [MonadAttach m]
+    [LawfulMonad m] [WeaklyLawfulMonadAttach m] [WPMonad m ps] :
+    Triple (m := m) (do
+      let mut sum : Nat := 0
+      for n in (xs.iterM Id).mapM (pure (f := m) <| · + 1) do
+        sum := sum + n
+      return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
+  mvcgen
+  case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum + cur.prefix.length⌝
+  all_goals grind
+
+theorem forIn_filterMapM_eq_sum_add_size (xs : Array Nat) {m ps}
+    [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] [WPMonad m ps] :
+    Triple (m := m) (do
+      let mut sum : Nat := 0
+      for n in (xs.iterM Id).filterMapM (pure (f := m) <| some <| · + 1) do
+        sum := sum + n
+      return sum) ⌜True⌝ (⇓r => ⌜r = xs.sum + xs.size⌝) := by
+  mvcgen
+  case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum + cur.prefix.length⌝
+  all_goals (try grind)
+
+theorem foldM_eq_sum (xs : Array Nat) {m ps} [Monad m] [LawfulMonad m]
+    [WPMonad m ps] :
+    Triple (m := m)
+      (xs.iter.foldM (m := m) (init := 0) (pure <| · + ·))
+      ⌜True⌝
+      (⇓r => ⌜r = xs.sum⌝) := by
+  mvcgen
+  case inv1 => exact ⇓⟨cur, n⟩ => ⌜n = cur.prefix.sum⌝
+  all_goals (try grind)