From 2798f88401932b82587dc3328b957a026e3a3eab Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 2 Sep 2026 18:58:57 +0000
Subject: [PATCH 01/24] feat: add a predicate for monad morphisms

We show that various list operations are monad morphisms, and that FreeM.liftM is.
---
 Cslib.lean                                    |   2 +
 Cslib/Foundations/Control/Monad/Free.lean     |  32 +-
 .../Foundations/Control/Monad/IsMonadHom.lean | 302 ++++++++++++++++++
 .../Control/Monad/IsMonadHom/List.lean        | 148 +++++++++
 Cslib/Foundations/Data/PFunctor/Free.lean     |  31 +-
 5 files changed, 499 insertions(+), 16 deletions(-)
 create mode 100644 Cslib/Foundations/Control/Monad/IsMonadHom.lean
 create mode 100644 Cslib/Foundations/Control/Monad/IsMonadHom/List.lean

diff --git a/Cslib.lean b/Cslib.lean
index 34a0d27bef..267579dd69 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -69,6 +69,8 @@ public import Cslib.Foundations.Combinatorics.InfiniteGraphRamsey
 public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
+public import Cslib.Foundations.Control.Monad.IsMonadHom
+public import Cslib.Foundations.Control.Monad.IsMonadHom.List
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 09d550b8bc..74dea4913c 100644
--- a/Cslib/Foundations/Control/Monad/Free.lean
+++ b/Cslib/Foundations/Control/Monad/Free.lean
@@ -7,6 +7,7 @@ Authors: Tanner Duve, Eric Wieser
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
 /-!
 # Free Monad
@@ -243,29 +244,44 @@ lemma liftM_bind [LawfulMonad m]
   | pure a => simp only [liftM_pure, LawfulMonad.pure_bind]
   | lift_bind op cont ih => simp [← ih]
 
+/-- A morphism of monads moves inside `FreeM.liftM`. -/
+theorem _root_.Cslib.IsMonadHom.map_freeMLiftM [Monad n]
+    {f : ∀ {α}, m α → n α} (hf : IsMonadHom m n f)
+    (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) :
+    f (x.liftM interp) = x.liftM (fun op => f (interp op)) := by
+  induction x with
+  | pure a => exact hf.map_pure a
+  | lift_bind op cont ih =>
+    simp only [bind_eq_bind, liftM_lift_bind, hf.map_bind, ih]
+
+/-- `FreeM.liftM interp` is a morphism of monads. -/
+theorem isMonadHom_liftM [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) :
+    IsMonadHom (FreeM F) m (FreeM.liftM interp) :=
+  IsMonadHom.mk' (liftM_pure interp) (liftM_bind interp)
+
 @[simp]
 lemma liftM_map [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (f : α → β) (x : FreeM F α) :
-    (f <$> x).liftM interp = f <$> x.liftM interp := by
-  simp_rw [← LawfulMonad.bind_pure_comp, liftM_bind, liftM_pure]
+    (f <$> x).liftM interp = f <$> x.liftM interp :=
+  isMonadHom_liftM interp |>.map_map _ _
 
 @[simp]
 lemma liftM_seq [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F (α → β)) (y : FreeM F α) :
-    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp := by
-  simp [seq_eq_bind_map]
+    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seq _ _
 
 @[simp]
 lemma liftM_seqLeft [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (y : FreeM F β) :
-    (x <* y).liftM interp = x.liftM interp <* y.liftM interp := by
-  simp [seqLeft_eq_bind]
+    (x <* y).liftM interp = x.liftM interp <* y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqLeft _ _
 
 @[simp]
 lemma liftM_seqRight [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (y : FreeM F β) :
-    (x *> y).liftM interp = x.liftM interp *> y.liftM interp := by
-  simp [seqRight_eq_bind]
+    (x *> y).liftM interp = x.liftM interp *> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqRight _ _
 
 /--
 A predicate stating that `interp : FreeM F α → m α` is an interpreter for the effect
diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom.lean b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
new file mode 100644
index 0000000000..6726cc17ba
--- /dev/null
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
@@ -0,0 +1,302 @@
+/-
+Copyright (c) 2026 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+module
+
+public import Cslib.Init
+public import Mathlib.Logic.Function.Defs
+
+/-!
+# (unbundled) morphisms of monads
+
+This file defines predicates on functions `f : ∀ {α}, m α → n α` that preserve functor, applicative,
+monadic, and alternative structure (`IsFunctorHom`, `IsApplicativeHom`, `IsMonadHom`,
+`IsAlternativeHom`, `IsAlternativeMonadHom`).
+
+Rather than assuming lawfulness, they explicitly require compatibility with every operator
+defined by the corresponding typeclasses, with helper constructors that dismiss the derived
+operators when the structures are lawful.
+-/
+
+public section
+
+namespace Cslib
+
+/-! ### Functor Homomorphisms -/
+
+/--
+A function `f` is a morphism of functors if it preserves `<$>` and `Functor.mapConst`.
+-/
+structure IsFunctorHom (m n) [Functor m] [Functor n] (f : ∀ {α}, m α → n α) : Prop where
+  map_map {α β} (g : α → β) (x : m α) : f (g <$> x) = g <$> f x
+  map_mapConst {α β} (a : α) (x : m β) : f (Functor.mapConst a x) = Functor.mapConst a (f x)
+
+namespace IsFunctorHom
+variable {m n p : Type _ → Type _} [Functor m] [Functor n] [Functor p]
+
+attribute [grind .] map_map map_mapConst
+
+private theorem map_mapConst_of_map_map
+    [LawfulFunctor m] [LawfulFunctor n] (f : ∀ {α}, m α → n α)
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x) :
+    ∀ {α β} (a : α) (x : m β), f (Functor.mapConst a x) = Functor.mapConst a (f x) := by
+  intros α β a x
+  simp [LawfulFunctor.map_const, map_map]
+
+/-- Construct an `IsFunctorHom` for lawful functors from `map_map`. -/
+theorem mk' [LawfulFunctor m] [LawfulFunctor n] {f : ∀ {α}, m α → n α}
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x) :
+    IsFunctorHom m n f where
+  map_map := map_map
+  map_mapConst := map_mapConst_of_map_map f map_map
+
+variable (m) in
+protected theorem id : IsFunctorHom m m id where
+  map_map _ _ := rfl
+  map_mapConst _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsFunctorHom n p f) (hg : IsFunctorHom m n g) :
+    IsFunctorHom m p (Function.dcomp f g) where
+  map_map _ _ := by simp [Function.dcomp, hf.map_map, hg.map_map]
+  map_mapConst _ _ := by simp [Function.dcomp, hf.map_mapConst, hg.map_mapConst]
+
+end IsFunctorHom
+
+
+/-! ### Applicative Homomorphisms -/
+
+/--
+A function `f` is a morphism of applicatives if it preserves `pure`, `<$>`, `<*>`, `<*`, and `*>`.
+-/
+structure IsApplicativeHom (m n) [Applicative m] [Applicative n] (f : ∀ {α}, m α → n α) : Prop
+    extends IsFunctorHom m n f where
+  map_pure {α} (a : α) : f (pure a) = pure a
+  map_seq {α β} (x : m (α → β)) (y : Unit → m α) :
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)
+  map_seqLeft {α β} (x : m α) (y : Unit → m β) :
+      f (SeqLeft.seqLeft x y) = SeqLeft.seqLeft (f x) (f <| y ·)
+  map_seqRight {α β} (x : m α) (y : Unit → m β) :
+      f (SeqRight.seqRight x y) = SeqRight.seqRight (f x) (f <| y ·)
+
+
+namespace IsApplicativeHom
+variable {m n p : Type _ → Type _} [Applicative m] [Applicative n] [Applicative p]
+
+attribute [grind .] map_pure map_seq map_seqLeft map_seqRight
+attribute [grind →] toIsFunctorHom
+
+private theorem map_map_of_map_pure_map_seq
+    [LawfulApplicative m] [LawfulApplicative n] (f : ∀ {α}, m α → n α)
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x := by
+  intros α β g x
+  rw [← pure_seq, ← pure_seq]
+  change f (Seq.seq (pure g) (fun _ => x)) = Seq.seq (pure g) (fun _ => f x)
+  rw [map_seq, map_pure]
+
+private theorem map_seqLeft_of_map_seq_map_map
+    [LawfulApplicative m] [LawfulApplicative n] (f : ∀ {α}, m α → n α)
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    ∀ {α β} (x : m α) (y : Unit → m β),
+      f (SeqLeft.seqLeft x y) = SeqLeft.seqLeft (f x) (f <| y ·) := by
+  intros α β x y
+  let y' := y (); have hy : y = fun _ => y' := rfl; clear_value y'; subst y
+  simp [seqLeft_eq, map_seq, map_map]
+
+private theorem map_seqRight_of_map_seq_map_map
+    [LawfulApplicative m] [LawfulApplicative n] (f : ∀ {α}, m α → n α)
+    (map_map : ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    ∀ {α β} (x : m α) (y : Unit → m β),
+      f (SeqRight.seqRight x y) = SeqRight.seqRight (f x) (f <| y ·) := by
+  intros α β x y
+  let y' := y (); have hy : y = fun _ => y' := rfl; clear_value y'; subst y
+  simp [seqRight_eq, map_seq, map_map]
+
+/-- Construct an `IsApplicativeHom` for lawful applicatives from `map_pure` and `map_seq`. -/
+theorem mk' [LawfulApplicative m] [LawfulApplicative n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·)) :
+    IsApplicativeHom m n f where
+  map_pure
+  toIsFunctorHom := .mk' (map_map_of_map_pure_map_seq f map_pure map_seq)
+  map_seq
+  map_seqLeft := map_seqLeft_of_map_seq_map_map f
+    (map_map_of_map_pure_map_seq f map_pure map_seq) map_seq
+  map_seqRight := map_seqRight_of_map_seq_map_map f
+    (map_map_of_map_pure_map_seq f map_pure map_seq) map_seq
+
+variable (m) in
+protected theorem id : IsApplicativeHom m m id where
+  map_pure _ := rfl
+  toIsFunctorHom := IsFunctorHom.id m
+  map_seq _ _ := rfl
+  map_seqLeft _ _ := rfl
+  map_seqRight _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsApplicativeHom n p f) (hg : IsApplicativeHom m n g) :
+    IsApplicativeHom m p (Function.dcomp f g) where
+  map_pure _ := by simp [Function.dcomp, hf.map_pure, hg.map_pure]
+  toIsFunctorHom := hf.toIsFunctorHom.comp hg.toIsFunctorHom
+  map_seq _ _ := by simp [Function.dcomp, hf.map_seq, hg.map_seq]
+  map_seqLeft _ _ := by simp [Function.dcomp, hf.map_seqLeft, hg.map_seqLeft]
+  map_seqRight _ _ := by simp [Function.dcomp, hf.map_seqRight, hg.map_seqRight]
+
+end IsApplicativeHom
+
+
+/-! ### Monad Homomorphisms -/
+
+/--
+A function `f` is a morphism of monads if it preserves `pure`, `>>=`, `<$>`, `<*>`, `<*`, and `*>`.
+-/
+structure IsMonadHom (m n) [Monad m] [Monad n] (f : ∀ {α}, m α → n α) : Prop
+    extends IsApplicativeHom m n f where
+  map_bind {α β} (x : m α) (y : α → m β) : f (x >>= y) = f x >>= (f <| y ·)
+
+namespace IsMonadHom
+variable {m n p : Type _ → Type _} [Monad m] [Monad n] [Monad p]
+
+attribute [grind .] map_bind
+attribute [grind →] toIsApplicativeHom
+
+private theorem map_map_of_map_pure_map_bind
+    [LawfulMonad m] [LawfulMonad n] (f : ∀ {α}, m α → n α)
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·)) :
+    ∀ {α β} (g : α → β) (x : m α), f (g <$> x) = g <$> f x := by
+  intros α β g x
+  simp [← bind_pure_comp, map_bind, map_pure]
+
+private theorem map_seq_of_map_pure_map_bind
+    [LawfulMonad m] [LawfulMonad n] (f : ∀ {α}, m α → n α)
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·)) :
+    ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·) := by
+  intros α β x y
+  let y' := y (); have hy : y = fun _ => y' := rfl; clear_value y'; subst y
+  simp [seq_eq_bind_map, map_map_of_map_pure_map_bind f map_pure, map_bind]
+
+/-- Construct an `IsMonadHom` for lawful monads from `map_pure` and `map_bind`. -/
+theorem mk' [LawfulMonad m] [LawfulMonad n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·)) :
+    IsMonadHom m n f where
+  map_bind
+  toIsApplicativeHom := .mk' map_pure (map_seq_of_map_pure_map_bind f map_pure map_bind)
+
+variable (m) in
+protected theorem id : IsMonadHom m m id where
+  toIsApplicativeHom := IsApplicativeHom.id m
+  map_bind _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsMonadHom n p f) (hg : IsMonadHom m n g) :
+    IsMonadHom m p (Function.dcomp f g) where
+  toIsApplicativeHom := hf.toIsApplicativeHom.comp hg.toIsApplicativeHom
+  map_bind _ _ := by simp [Function.dcomp, hf.map_bind, hg.map_bind]
+
+end IsMonadHom
+
+/-! ### Alternative Homomorphisms -/
+
+/--
+A function `f` is a morphism of alternatives if it preserves `pure`, `<$>`, `<*>`, `<*`, `*>`,
+`failure`, and `orElse`.
+-/
+structure IsAlternativeHom (m n) [Alternative m] [Alternative n] (f : ∀ {α}, m α → n α) : Prop
+    extends IsApplicativeHom m n f where
+  map_failure {α} : f (Alternative.failure : m α) = Alternative.failure
+  map_orElse {α} (x : m α) (y : Unit → m α) :
+    f (HOrElse.hOrElse x y) = HOrElse.hOrElse (f x) (f <| y ·)
+
+namespace IsAlternativeHom
+variable {m n p : Type _ → Type _} [Alternative m] [Alternative n] [Alternative p]
+
+attribute [grind .] map_failure map_orElse
+attribute [grind →] toIsApplicativeHom
+
+/-- Construct an `IsAlternativeHom` for lawful applicatives from `map_pure`, `map_seq`,
+`map_failure`, and `map_orElse`. -/
+theorem mk' [LawfulApplicative m] [LawfulApplicative n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_seq : ∀ {α β} (x : m (α → β)) (y : Unit → m α),
+      f (Seq.seq x y) = Seq.seq (f x) (f <| y ·))
+    (map_failure : ∀ {α}, f (Alternative.failure : m α) = Alternative.failure)
+    (map_orElse : ∀ {α} (x : m α) (y : Unit → m α),
+      f (HOrElse.hOrElse x y) = HOrElse.hOrElse (f x) (f <| y ·)) :
+    IsAlternativeHom m n f where
+  toIsApplicativeHom := .mk' map_pure map_seq
+  map_failure
+  map_orElse
+
+variable (m) in
+protected theorem id : IsAlternativeHom m m id where
+  toIsApplicativeHom := IsApplicativeHom.id m
+  map_failure := rfl
+  map_orElse _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsAlternativeHom n p f) (hg : IsAlternativeHom m n g) :
+    IsAlternativeHom m p (Function.dcomp f g) where
+  toIsApplicativeHom := hf.toIsApplicativeHom.comp hg.toIsApplicativeHom
+  map_failure := by simp [Function.dcomp, hf.map_failure, hg.map_failure]
+  map_orElse _ _ := by simp [Function.dcomp, hf.map_orElse, hg.map_orElse]
+
+end IsAlternativeHom
+
+/-! ### Alternative Monad Homomorphisms -/
+
+/--
+A function `f` is a morphism of alternative monads if it preserves monadic and alternative
+structure.
+-/
+structure IsAlternativeMonadHom (m n) [AlternativeMonad m] [AlternativeMonad n]
+    (f : ∀ {α}, m α → n α) : Prop
+    extends IsMonadHom m n f, IsAlternativeHom m n f
+
+namespace IsAlternativeMonadHom
+variable {m n p : Type _ → Type _} [AlternativeMonad m] [AlternativeMonad n] [AlternativeMonad p]
+
+attribute [grind →] toIsMonadHom toIsAlternativeHom
+
+/-- Construct an `IsAlternativeMonadHom` for lawful monads from `map_pure`, `map_bind`,
+`map_failure`, and `map_orElse`. -/
+theorem mk' [LawfulMonad m] [LawfulMonad n] {f : ∀ {α}, m α → n α}
+    (map_pure : ∀ {α} (a : α), f (pure a) = pure a)
+    (map_bind : ∀ {α β} (x : m α) (y : α → m β), f (x >>= y) = f x >>= (f <| y ·))
+    (map_failure : ∀ {α}, f (Alternative.failure : m α) = Alternative.failure)
+    (map_orElse : ∀ {α} (x : m α) (y : Unit → m α),
+      f (HOrElse.hOrElse x y) = HOrElse.hOrElse (f x) (f <| y ·)) :
+    IsAlternativeMonadHom m n f where
+  toIsMonadHom := .mk' map_pure map_bind
+  map_failure
+  map_orElse
+
+variable (m) in
+protected theorem id : IsAlternativeMonadHom m m id where
+  toIsMonadHom := IsMonadHom.id m
+  map_failure := rfl
+  map_orElse _ _ := rfl
+
+protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
+    (hf : IsAlternativeMonadHom n p f) (hg : IsAlternativeMonadHom m n g) :
+    IsAlternativeMonadHom m p (Function.dcomp f g) where
+  toIsMonadHom := hf.toIsMonadHom.comp hg.toIsMonadHom
+  map_failure := by simp [Function.dcomp, hf.map_failure, hg.map_failure]
+  map_orElse _ _ := by simp [Function.dcomp, hf.map_orElse, hg.map_orElse]
+
+end IsAlternativeMonadHom
+
+end Cslib
diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
new file mode 100644
index 0000000000..71640b1e78
--- /dev/null
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2026 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
+public import Mathlib.Data.List.Monad
+import all Init.Data.List.Control
+
+/-!
+# List operations and monad morphisms
+
+This file proves that monadic operations on lists commute with monad homomorphisms
+(and applicative homomorphisms), and that `List.reverse` is a monad homomorphism on `List`.
+-/
+
+namespace Cslib
+
+universe u v w
+variable {m n : Type u → Type v}
+
+/-! ### Preservation of list operations under applicative homomorphisms -/
+
+namespace IsApplicativeHom
+variable [Applicative m] [Applicative n]
+
+@[grind .]
+theorem map_listMapA {F : ∀ {α}, m α → n α} (hf : IsApplicativeHom m n F)
+    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapA f) = l.mapA (F ∘ f) := by
+  induction l with grind [List.mapA]
+
+@[grind .]
+theorem map_listForA {F : ∀ {α}, m α → n α} (hf : IsApplicativeHom m n F)
+    {α : Type w} (l : List α) (f : α → m PUnit) :
+    F (l.forA f) = l.forA (F ∘ f) := by
+  induction l with grind [List.forA]
+
+end IsApplicativeHom
+
+/-! ### Preservation of list operations under monad homomorphisms -/
+
+namespace IsMonadHom
+variable [Monad m] [Monad n]
+
+@[grind .]
+theorem map_listMapM'
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapM' f) = l.mapM' (F ∘ f) := by
+  induction l with grind [List.mapM']
+
+@[grind .]
+theorem map_listMapM [LawfulMonad m] [LawfulMonad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.mapM f) = l.mapM (F ∘ f) := by
+  induction l with grind
+
+@[grind .]
+theorem map_listForM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} (l : List α) (f : α → m PUnit) :
+    F (l.forM f) = l.forM (F ∘ f) := by
+  induction l with grind [List.forM]
+
+@[grind .]
+theorem map_listFoldlM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {s : Type u} {α : Type w} (f : s → α → m s) (init : s) (l : List α) :
+    F (l.foldlM f init) = l.foldlM (fun s a => F (f s a)) init := by
+  induction l generalizing init with grind [List.foldlM]
+
+@[grind .]
+theorem map_listFoldrM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) :
+    F (l.foldrM f init) = l.foldrM (fun a s => F (f a s)) init := by
+  simp only [List.foldrM]
+  exact hf.map_listFoldlM (fun s a => f a s) init l.reverse
+
+@[grind .]
+theorem map_listFindSomeM?
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} {β : Type u} (f : α → m (Option β)) (l : List α) :
+    F (l.findSomeM? f) = l.findSomeM? (F ∘ f) := by
+  induction l with grind
+
+@[grind .]
+theorem map_listFindM? {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type} (p : α → m Bool) (l : List α) :
+    F (l.findM? p) = l.findM? (F ∘ p) := by
+  induction l with grind [List.findM?]
+
+@[grind .]
+theorem map_listAnyM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} (p : α → m Bool) (l : List α) :
+    F (l.anyM p) = l.anyM (F ∘ p) := by
+  induction l with grind [List.anyM]
+
+@[grind .]
+theorem map_listAllM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type w} (p : α → m Bool) (l : List α) :
+    F (l.allM p) = l.allM (F ∘ p) := by
+  induction l with grind [List.allM]
+
+@[grind .]
+theorem map_listFilterAuxM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type} (p : α → m Bool) (l acc : List α) :
+    F (List.filterAuxM p l acc) = List.filterAuxM (F ∘ p) l acc := by
+  induction l generalizing acc with grind [List.filterAuxM]
+
+@[grind .]
+theorem map_listFilterM {m n : Type → Type v} [Monad m] [Monad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type} (p : α → m Bool) (l : List α) :
+    F (l.filterM p) = l.filterM (F ∘ p) := by
+  grind [List.filterM]
+
+end IsMonadHom
+
+/-! ### Preservation of list operations under alternative homomorphisms -/
+
+namespace IsAlternativeHom
+variable [Alternative m] [Alternative n]
+
+@[grind .]
+theorem map_listFirstM {F : ∀ {α}, m α → n α} (hf : IsAlternativeHom m n F)
+    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    F (l.firstM f) = l.firstM (F ∘ f) := by
+  induction l with grind [List.firstM]
+
+end IsAlternativeHom
+
+/-! ### Monad homomorphisms on `List` -/
+
+protected theorem List.isMonadHom_reverse : IsMonadHom List List List.reverse :=
+  .mk' (fun _ => rfl) (fun _ _ => List.reverse_flatMap)
+
+/-- The only applicative morphism on lists are the identity and reversal. -/
+proof_wanted isApplicative_list_iff (f : ∀ {α}, List α → List α) :
+    IsApplicativeHom List List f ↔ @f = (@id <| List ·) ∨ @f = @List.reverse
+
+end Cslib
diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
index a29e974704..168782d16f 100644
--- a/Cslib/Foundations/Data/PFunctor/Free.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -7,6 +7,7 @@ Authors: Quang Dao
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 public import Mathlib.Data.PFunctor.Univariate.Basic
 
 /-!
@@ -321,6 +322,16 @@ theorem Interprets.iff (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α 
     Interprets handler eval ↔ eval = (·.liftM handler) :=
   ⟨(·.eq), fun h => h ▸ Interprets.liftM _⟩
 
+/-- A morphism of monads moves inside `FreeM.liftM`. -/
+theorem _root_.Cslib.IsMonadHom.map_pfunctorFreeMLiftM [Monad n]
+    {f : ∀ {α}, m α → n α} (hf : Cslib.IsMonadHom m n f) (interp : (a : P.A) → m (P.B a))
+    (x : P.FreeM α) :
+    f (x.liftM interp) = x.liftM (fun op => f (interp op)) := by
+  induction x with
+  | pure a => exact hf.map_pure a
+  | lift_bind op cont ih =>
+    simp only [bind_eq_bind, liftM_lift_bind, hf.map_bind, ih]
+
 variable [LawfulMonad m]
 
 @[simp]
@@ -336,28 +347,32 @@ lemma liftM_bind {α β : Type uB} (x : P.FreeM α) (f : α → P.FreeM β) :
     funext u
     exact h u
 
+/-- `FreeM.liftM interp` is a morphism of monads. -/
+theorem isMonadHom_liftM : Cslib.IsMonadHom P.FreeM m (FreeM.liftM interp) :=
+  .mk' (liftM_pure interp) (liftM_bind interp)
+
 @[simp]
 lemma liftM_map {α β : Type uB} (f : α → β) (x : P.FreeM α) :
-    (f <$> x).liftM interp = f <$> x.liftM interp := by
-  simp_rw [← LawfulMonad.bind_pure_comp, liftM_bind, liftM_pure]
+    (f <$> x).liftM interp = f <$> x.liftM interp :=
+  isMonadHom_liftM interp |>.map_map _ _
 
 @[simp]
 lemma liftM_seq {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : P.FreeM (α → β)) (y : P.FreeM α) :
-    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp := by
-  simp [seq_eq_bind_map]
+    (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seq _ _
 
 @[simp]
 lemma liftM_seqLeft {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) :
-    (x <* y).liftM interp = x.liftM interp <* y.liftM interp := by
-  simp [seqLeft_eq_bind]
+    (x <* y).liftM interp = x.liftM interp <* y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqLeft _ _
 
 @[simp]
 lemma liftM_seqRight {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) :
-    (x *> y).liftM interp = x.liftM interp *> y.liftM interp := by
-  simp [seqRight_eq_bind]
+    (x *> y).liftM interp = x.liftM interp *> y.liftM interp :=
+  isMonadHom_liftM interp |>.map_seqRight _ _
 
 @[simp]
 lemma liftM_lift (interp : (a : P.A) → m (P.B a)) (a : P.A) :

From 050995dce72df44d7737f126950770047219a5b7 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 2 Sep 2026 20:49:45 +0000
Subject: [PATCH 02/24] drop dcomp

---
 .../Foundations/Control/Monad/IsMonadHom.lean | 33 ++++++++++---------
 Cslib/Foundations/Data/PFunctor/Free.lean     |  2 +-
 2 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom.lean b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
index 6726cc17ba..f8fd0ba36b 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
@@ -7,6 +7,7 @@ module
 
 public import Cslib.Init
 public import Mathlib.Logic.Function.Defs
+public import Batteries.Control.AlternativeMonad
 
 /-!
 # (unbundled) morphisms of monads
@@ -59,9 +60,9 @@ protected theorem id : IsFunctorHom m m id where
 
 protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
     (hf : IsFunctorHom n p f) (hg : IsFunctorHom m n g) :
-    IsFunctorHom m p (Function.dcomp f g) where
-  map_map _ _ := by simp [Function.dcomp, hf.map_map, hg.map_map]
-  map_mapConst _ _ := by simp [Function.dcomp, hf.map_mapConst, hg.map_mapConst]
+    IsFunctorHom m p (f ∘ g) where
+  map_map _ _ := by simp [hf.map_map, hg.map_map]
+  map_mapConst _ _ := by simp [hf.map_mapConst, hg.map_mapConst]
 
 end IsFunctorHom
 
@@ -145,12 +146,12 @@ protected theorem id : IsApplicativeHom m m id where
 
 protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
     (hf : IsApplicativeHom n p f) (hg : IsApplicativeHom m n g) :
-    IsApplicativeHom m p (Function.dcomp f g) where
-  map_pure _ := by simp [Function.dcomp, hf.map_pure, hg.map_pure]
+    IsApplicativeHom m p (f ∘ g) where
+  map_pure _ := by simp [hf.map_pure, hg.map_pure]
   toIsFunctorHom := hf.toIsFunctorHom.comp hg.toIsFunctorHom
-  map_seq _ _ := by simp [Function.dcomp, hf.map_seq, hg.map_seq]
-  map_seqLeft _ _ := by simp [Function.dcomp, hf.map_seqLeft, hg.map_seqLeft]
-  map_seqRight _ _ := by simp [Function.dcomp, hf.map_seqRight, hg.map_seqRight]
+  map_seq _ _ := by simp [hf.map_seq, hg.map_seq]
+  map_seqLeft _ _ := by simp [hf.map_seqLeft, hg.map_seqLeft]
+  map_seqRight _ _ := by simp [hf.map_seqRight, hg.map_seqRight]
 
 end IsApplicativeHom
 
@@ -203,9 +204,9 @@ protected theorem id : IsMonadHom m m id where
 
 protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
     (hf : IsMonadHom n p f) (hg : IsMonadHom m n g) :
-    IsMonadHom m p (Function.dcomp f g) where
+    IsMonadHom m p (f ∘ g) where
   toIsApplicativeHom := hf.toIsApplicativeHom.comp hg.toIsApplicativeHom
-  map_bind _ _ := by simp [Function.dcomp, hf.map_bind, hg.map_bind]
+  map_bind _ _ := by simp [hf.map_bind, hg.map_bind]
 
 end IsMonadHom
 
@@ -249,10 +250,10 @@ protected theorem id : IsAlternativeHom m m id where
 
 protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
     (hf : IsAlternativeHom n p f) (hg : IsAlternativeHom m n g) :
-    IsAlternativeHom m p (Function.dcomp f g) where
+    IsAlternativeHom m p (f ∘ g) where
   toIsApplicativeHom := hf.toIsApplicativeHom.comp hg.toIsApplicativeHom
-  map_failure := by simp [Function.dcomp, hf.map_failure, hg.map_failure]
-  map_orElse _ _ := by simp [Function.dcomp, hf.map_orElse, hg.map_orElse]
+  map_failure := by simp [hf.map_failure, hg.map_failure]
+  map_orElse _ _ := by simp [hf.map_orElse, hg.map_orElse]
 
 end IsAlternativeHom
 
@@ -292,10 +293,10 @@ protected theorem id : IsAlternativeMonadHom m m id where
 
 protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n α}
     (hf : IsAlternativeMonadHom n p f) (hg : IsAlternativeMonadHom m n g) :
-    IsAlternativeMonadHom m p (Function.dcomp f g) where
+    IsAlternativeMonadHom m p (f ∘ g) where
   toIsMonadHom := hf.toIsMonadHom.comp hg.toIsMonadHom
-  map_failure := by simp [Function.dcomp, hf.map_failure, hg.map_failure]
-  map_orElse _ _ := by simp [Function.dcomp, hf.map_orElse, hg.map_orElse]
+  map_failure := by simp [hf.map_failure, hg.map_failure]
+  map_orElse _ _ := by simp [hf.map_orElse, hg.map_orElse]
 
 end IsAlternativeMonadHom
 
diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
index 168782d16f..05cb6535d0 100644
--- a/Cslib/Foundations/Data/PFunctor/Free.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -352,7 +352,7 @@ theorem isMonadHom_liftM : Cslib.IsMonadHom P.FreeM m (FreeM.liftM interp) :=
   .mk' (liftM_pure interp) (liftM_bind interp)
 
 @[simp]
-lemma liftM_map {α β : Type uB} (f : α → β) (x : P.FreeM α) :
+lemma liftM_map {α β : Type uB} (f : α → β) (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) :
     (f <$> x).liftM interp = f <$> x.liftM interp :=
   isMonadHom_liftM interp |>.map_map _ _
 

From f9eec96a7f86c9944556204bd884f36df8d6efb6 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 2 Sep 2026 20:50:41 +0000
Subject: [PATCH 03/24] section

---
 Cslib/Foundations/Control/Monad/IsMonadHom/List.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
index 71640b1e78..389faaf177 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -17,6 +17,8 @@ This file proves that monadic operations on lists commute with monad homomorphis
 (and applicative homomorphisms), and that `List.reverse` is a monad homomorphism on `List`.
 -/
 
+public section
+
 namespace Cslib
 
 universe u v w

From a522805f5ff03fc4d2fbee1a01bf7b3f97566143 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 2 Sep 2026 21:26:06 +0000
Subject: [PATCH 04/24] wp

---
 Cslib/Foundations/Control/Monad/IsMonadHom.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom.lean b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
index f8fd0ba36b..90c79b4d86 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
@@ -8,6 +8,7 @@ module
 public import Cslib.Init
 public import Mathlib.Logic.Function.Defs
 public import Batteries.Control.AlternativeMonad
+public import Std.Do.WP.Monad
 
 /-!
 # (unbundled) morphisms of monads
@@ -300,4 +301,8 @@ protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n 
 
 end IsAlternativeMonadHom
 
+open Std.Do WPMonad in
+theorem wp_isMonadHom [Monad m] [WPMonad m ps] : IsMonadHom m (PredTrans ps) WP.wp :=
+  .mk' wp_pure wp_bind
+
 end Cslib

From 87da9b3e614456c5aad4320148f4ac87dbf1f77c Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 2 Sep 2026 22:22:39 +0000
Subject: [PATCH 05/24] Close the proof_wanted

---
 .../Control/Monad/IsMonadHom/List.lean        | 67 +++++++++++++++++--
 1 file changed, 63 insertions(+), 4 deletions(-)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
index 389faaf177..daa4cf6211 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -8,7 +8,9 @@ module
 public import Cslib.Init
 public import Cslib.Foundations.Control.Monad.IsMonadHom
 public import Mathlib.Data.List.Monad
+
 import all Init.Data.List.Control
+import Mathlib.Data.List.Basic
 
 /-!
 # List operations and monad morphisms
@@ -138,13 +140,70 @@ theorem map_listFirstM {F : ∀ {α}, m α → n α} (hf : IsAlternativeHom m n
 
 end IsAlternativeHom
 
-/-! ### Monad homomorphisms on `List` -/
+/-! ### Monad homomorphisms on the `List` monad -/
+
+@[grind .]
+theorem IsApplicativeHom.map_listSingleton
+    {F : ∀ {α}, List α → List α} (hf : IsApplicativeHom List List F) {α} (a : α) :
+    F ([a] : List α) = [a] := hf.map_pure _
+
+@[grind .]
+theorem IsMonadHom.map_listFlatMap
+    {F : ∀ {α}, List α → List α} (hf : IsMonadHom List List F) {α β} (l : List α) (g : α → List β) :
+    F (l.flatMap g) = (F l).flatMap (F <| g ·) := hf.map_bind _ _
+
+@[grind .]
+theorem IsFunctorHom.map_listNil {F : ∀ {α}, List α → List α} (hf : IsFunctorHom List List F) {α} :
+    F ([] : List α) = [] := by
+  simpa [Subsingleton.elim (F ([] : List PEmpty)) []]
+    using (hf.map_map PEmpty.elim []).symm
 
 protected theorem List.isMonadHom_reverse : IsMonadHom List List List.reverse :=
   .mk' (fun _ => rfl) (fun _ _ => List.reverse_flatMap)
 
-/-- The only applicative morphism on lists are the identity and reversal. -/
-proof_wanted isApplicative_list_iff (f : ∀ {α}, List α → List α) :
-    IsApplicativeHom List List f ↔ @f = (@id <| List ·) ∨ @f = @List.reverse
+section uniqueness
+
+/-- A property holds on all lists if it holds on the nil list, the singleton list,
+and concatenations thereof. -/
+private theorem List.nil_singleton_append_induction {motive : List α → Prop}
+    (nil : motive []) (singleton : ∀ a, motive [a])
+    (append : ∀ xs ys, motive xs → motive ys → motive (xs ++ ys)) :
+    ∀ l, motive l
+  | [] => nil
+  | x :: xs => append [x] xs (singleton x) (nil_singleton_append_induction nil singleton append xs)
+
+/-- Universe-generic type with two elements. This is used only internally in a proof, and keeps
+things more concise than `ULift Bool`. -/
+private inductive Two : Type u | a | b
+
+private theorem eq_ab_or_ba : ∀ (l : List Two),
+    l.flatMap (fun | .a => [.a] | .b => []) = [Two.a] →
+    l.flatMap (fun | .a => [] | .b => [.b]) = [Two.b] →
+    l = [Two.a, Two.b] ∨ l = [Two.b, Two.a]
+  | [.a, .b], _, _ => .inl rfl
+  | [.b, .a], _, _ => .inr rfl
+
+/-- The only monad morphisms on lists are the identity and reversal. -/
+theorem isMonadHom_list_iff (f : ∀ {α : Type u}, List α → List α) :
+    IsMonadHom List List @f ↔ @f = (@id <| List ·) ∨ @f = @List.reverse := by
+  refine ⟨fun h => ?_, ?_⟩
+  · have h_append {α} (xs ys : List α) :
+        f (xs ++ ys) = (f [Two.a, Two.b]).flatMap (fun | .a => f xs | .b => f ys) := by
+      have : xs ++ ys = [Two.a, Two.b].flatMap (fun | .a => xs | .b => ys) := by
+        simp
+      rw [this, h.map_listFlatMap]
+      congr 1; funext x; cases x <;> rfl
+    refine (eq_ab_or_ba (f [Two.a, Two.b]) ?_ ?_).imp (fun hL => ?_) (fun hL => ?_)
+    · simpa [h.map_listNil, h.map_listSingleton] using (h_append [Two.a] []).symm
+    · simpa [h.map_listNil, h.map_listSingleton] using (h_append [] [Two.b]).symm
+    · funext α l
+      induction l using List.nil_singleton_append_induction with grind
+    · funext α l
+      induction l using List.nil_singleton_append_induction with grind
+  · rintro (rfl | rfl)
+    · exact .id _
+    · exact List.isMonadHom_reverse
+
+end uniqueness
 
 end Cslib

From 75b9bd2fc9363f03ae6799bb270fadfd30f81813 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 2 Sep 2026 22:28:26 +0000
Subject: [PATCH 06/24] remove grind

---
 Cslib/Foundations/Control/Monad/IsMonadHom/List.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
index daa4cf6211..95fd4d1002 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -147,7 +147,6 @@ theorem IsApplicativeHom.map_listSingleton
     {F : ∀ {α}, List α → List α} (hf : IsApplicativeHom List List F) {α} (a : α) :
     F ([a] : List α) = [a] := hf.map_pure _
 
-@[grind .]
 theorem IsMonadHom.map_listFlatMap
     {F : ∀ {α}, List α → List α} (hf : IsMonadHom List List F) {α β} (l : List α) (g : α → List β) :
     F (l.flatMap g) = (F l).flatMap (F <| g ·) := hf.map_bind _ _

From 9b8ed4e2cc1df855656871a1770f42d6dd0760bb Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 3 Sep 2026 23:33:06 +0000
Subject: [PATCH 07/24] feat: add monad-polymorphic sorts

These can be used to:
* replace the specialized timeM version
* implement sorts that log as they sort
* specialize to FreeM or PFunctor.FreeM
---
 Cslib.lean                                    |  2 +
 .../Algorithms/Lean/MergeSort/MergeSort.lean  |  2 +
 Cslib/Algorithms/Lean/Sort/Insertion.lean     | 54 +++++++++++++
 Cslib/Algorithms/Lean/Sort/Merge.lean         | 77 +++++++++++++++++++
 4 files changed, 135 insertions(+)
 create mode 100644 Cslib/Algorithms/Lean/Sort/Insertion.lean
 create mode 100644 Cslib/Algorithms/Lean/Sort/Merge.lean

diff --git a/Cslib.lean b/Cslib.lean
index 34a0d27bef..afe8bc375d 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -2,6 +2,8 @@ module  -- shake: keep-all --deprecated_module: ignore
 
 public import Cslib.Algorithms.CCS.VendingMachine
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
+public import Cslib.Algorithms.Lean.Sort.Insertion
+public import Cslib.Algorithms.Lean.Sort.Merge
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor
 public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index bb9f9c8f1f..cee7d5c0b6 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -33,6 +33,7 @@ namespace Cslib.Algorithms.Lean.TimeM
 
 variable {α : Type} [LinearOrder α]
 
+-- TODO: replace this with `List.mergeM`
 /-- Merges two lists into a single list, counting comparisons as time cost.
 Returns a `TimeM ℕ (List α)` where the time represents the number of comparisons performed. -/
 def merge :  List α → List α → TimeM ℕ (List α)
@@ -47,6 +48,7 @@ def merge :  List α → List α → TimeM ℕ (List α)
       let rest ← merge (x::xs') ys'
       return (y :: rest)
 
+-- TODO: replace this with `List.mergeSortM`
 /-- Sorts a list using the merge sort algorithm, counting comparisons as time cost.
 Returns a `TimeM ℕ (List α)` where the time represents the total number of comparisons. -/
 def mergeSort (xs : List α) : TimeM ℕ (List α) :=  do
diff --git a/Cslib/Algorithms/Lean/Sort/Insertion.lean b/Cslib/Algorithms/Lean/Sort/Insertion.lean
new file mode 100644
index 0000000000..5e5d61d437
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Sort/Insertion.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad, Eric Wieser
+-/
+module
+public import Mathlib.Data.List.Sort
+
+/-!
+# A Monadic version of the builtin `List.insertionSort`
+
+This can be instantiated with `Id` to recover the original, or with `TimeM` or `FreeM` for
+algorithmic analysis.
+-/
+
+public section
+
+namespace List
+
+variable {m} [Monad m] (r : α → α → m Bool)
+
+/-- A monadic version of `List.orderedInsert`. -/
+def orderedInsertM (a : α) : List α → m (List α)
+  | [] => return [a]
+  | b :: l => do if ← r a b then return a :: b :: l else return b :: (← orderedInsertM a l)
+
+@[simp]
+theorem orderedInsertM_pure [LawfulMonad m] (r : α → α → Bool) (a : α) (xs : List α) :
+    orderedInsertM (fun x y => (pure (r x y) : m Bool)) a xs =
+      pure (orderedInsert (r · ·) a xs) := by
+  fun_induction orderedInsertM with grind [orderedInsertM]
+
+@[simp]
+theorem idRun_orderedInsertM (r : α → α → Id Bool) (a : α) (xs : List α) :
+    Id.run (orderedInsertM r a xs) = orderedInsert (fun x y => Id.run <| r x y) a xs :=
+  orderedInsertM_pure _ _ _
+
+/-- A monadic version of `List.insertionSort`. -/
+@[simp]
+def insertionSortM : List α → m (List α)
+  | [] => return []
+  | b :: l => do orderedInsertM r b (← insertionSortM l)
+
+@[simp]
+theorem insertionSortM_pure [LawfulMonad m] (xs : List α) (r : α → α → Bool) :
+    insertionSortM (fun x y => (pure (r x y) : m Bool)) xs = pure (insertionSort (r · ·) xs) := by
+  fun_induction insertionSortM with simp_all
+
+@[simp]
+theorem idRun_insertionSortM (xs : List α) (r : α → α → Id Bool) :
+    Id.run (insertionSortM r xs) = insertionSort (fun x y => Id.run <| r x y) xs :=
+  insertionSortM_pure _ _
+
+end List
diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
new file mode 100644
index 0000000000..9dfc994720
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Eric Wieser
+-/
+module
+import all Init.Data.List.Sort.Basic
+
+/-!
+# A Monadic version of the builtin `List.mergeSort`
+
+This can be instantiated with `Id` to recover the original, or with `TimeM` or `FreeM` for
+algorithmic analysis.
+-/
+
+public section
+
+namespace List
+
+variable {m} [Monad m]
+
+/-- A monadic version of `List.merge` -/
+def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
+  match xs, ys with
+  | [], ys => return ys
+  | xs, [] => return xs
+  | x :: xs, y :: ys =>
+    if ← le x y then
+      return x :: (← mergeM xs (y :: ys) le)
+    else
+      return y :: (← mergeM (x :: xs) ys le)
+
+@[simp] theorem nil_mergeM (ys : List α) (le : α → α → m Bool) : mergeM [] ys le = pure ys := by
+  simp [mergeM]
+@[simp] theorem mergeM_right (xs : List α) (le : α → α → m Bool) : mergeM xs [] le = pure xs := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih => simp [mergeM]
+
+@[simp]
+theorem mergeM_pure [LawfulMonad m] (xs ys : List α) (le : α → α → Bool) :
+    mergeM xs ys (fun x y => (pure (le x y) : m Bool)) = pure (merge xs ys le) := by
+  fun_induction mergeM with grind [merge]
+
+@[simp]
+theorem idRun_mergeM (xs ys : List α) (le : α → α → Id Bool) :
+    Id.run (mergeM xs ys le) = merge xs ys (fun x y => Id.run <| le x y) :=
+  mergeM_pure _ _ _
+
+set_option linter.unusedVariables false in
+/-- A monadic version of `List.mergeSortM` -/
+def mergeSortM : ∀ (xs : List α) (le : α → α → m Bool), m (List α)
+  | [], _ => return []
+  | [a], _ => return [a]
+  | a :: b :: xs, le => do
+    let lr := MergeSort.Internal.splitInTwo ⟨a :: b :: xs, rfl⟩
+    have := by simpa using lr.2.2
+    have := by simpa using lr.1.2
+    mergeM (← mergeSortM lr.1 le) (← mergeSortM lr.2 le) le
+termination_by xs => xs.length
+
+@[simp]
+theorem mergeSortM_pure [LawfulMonad m] (xs : List α) (le : α → α → Bool) :
+    mergeSortM xs (fun x y => (pure (le x y) : m Bool)) = pure (mergeSort xs le) := by
+  fun_induction mergeSort with
+  | case1 | case2 => simp [mergeSortM]
+  | case3  a b xs le lr _ _ ih1 ih2 =>
+    simp only [mergeSortM]
+    rw [ih1, ih2]
+    simp
+
+@[simp]
+theorem idRun_mergeSortM (xs : List α) (le : α → α → Id Bool) :
+    Id.run (mergeSortM xs le) = mergeSort xs (fun x y => Id.run <| le x y) :=
+  mergeSortM_pure _ _
+
+end List

From e4b031eb6a9f69a2f5f4ceb4a08a09b10af0eba3 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 3 Sep 2026 23:41:07 +0000
Subject: [PATCH 08/24] drop merge

---
 .../Algorithms/Lean/MergeSort/MergeSort.lean  | 25 ++++++++-----------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index cee7d5c0b6..c2be5d897f 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -7,6 +7,8 @@ Authors: Sorrachai Yingchareonthawornhcai
 module
 
 public import Cslib.Algorithms.Lean.TimeM
+public import Cslib.Algorithms.Lean.Sort.Merge
+import all Cslib.Algorithms.Lean.Sort.Merge
 public import Mathlib.Data.Nat.Cast.Order.Ring
 public import Mathlib.Order.Lattice.Nat
 public import Mathlib.Data.Nat.Log
@@ -33,20 +35,10 @@ namespace Cslib.Algorithms.Lean.TimeM
 
 variable {α : Type} [LinearOrder α]
 
--- TODO: replace this with `List.mergeM`
 /-- Merges two lists into a single list, counting comparisons as time cost.
 Returns a `TimeM ℕ (List α)` where the time represents the number of comparisons performed. -/
-def merge :  List α → List α → TimeM ℕ (List α)
-  | [], ys => return ys
-  | xs, [] => return xs
-  | x::xs', y::ys' => do
-    ✓ let c := (x ≤ y : Bool)
-    if c then
-      let rest ← merge xs' (y::ys')
-      return (x :: rest)
-    else
-      let rest ← merge (x::xs') ys'
-      return (y :: rest)
+def merge (xs ys : List α) : TimeM ℕ (List α) :=
+  List.mergeM xs ys fun x y => do ✓ return x ≤ y
 
 -- TODO: replace this with `List.mergeSortM`
 /-- Sorts a list using the merge sort algorithm, counting comparisons as time cost.
@@ -68,7 +60,8 @@ open List
 /-- Our merge computes the one already in mathlib. -/
 @[simp, grind =]
 theorem ret_merge (xs ys : List α) : ⟪merge xs ys⟫ = xs.merge ys := by
-  fun_induction merge with grind [nil_merge, merge_right, cons_merge_cons]
+  unfold merge
+  fun_induction mergeM with grind [nil_merge, merge_right, cons_merge_cons]
 
 /-- A list is sorted if it satisfies the `Pairwise (· ≤ ·)` predicate. -/
 abbrev IsSorted (l : List α) : Prop := List.Pairwise (· ≤ ·) l
@@ -95,7 +88,8 @@ theorem mergeSort_sorted (xs : List α) : IsSorted ⟪mergeSort xs⟫ := by
   | case2 _ _ _ _ _ ih2 ih1 => exact sorted_merge ih2 ih1
 
 lemma merge_perm (l₁ l₂ : List α) : ⟪merge l₁ l₂⟫ ~ l₁ ++ l₂ := by
-  fun_induction merge with grind [List.merge_perm_append]
+  unfold merge
+  fun_induction mergeM with grind [List.merge_perm_append]
 
 theorem mergeSort_perm (xs : List α) : ⟪mergeSort xs⟫ ~ xs := by
   fun_induction mergeSort xs with
@@ -181,7 +175,8 @@ theorem merge_ret_length_eq_sum (xs ys : List α) :
   · grind [List.length_merge]
 
 @[simp] theorem merge_time (xs ys : List α) : (merge xs ys).time ≤ xs.length + ys.length := by
-  fun_induction merge with
+  unfold merge
+  fun_induction List.mergeM with
   | case3 =>
     grind
   | _ => simp

From 5576d8ba9fe828227c56cfaf286f41d386f83661 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 3 Sep 2026 23:47:46 +0000
Subject: [PATCH 09/24] imports

---
 Cslib/Algorithms/Lean/Sort/Insertion.lean | 3 +++
 Cslib/Algorithms/Lean/Sort/Merge.lean     | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/Cslib/Algorithms/Lean/Sort/Insertion.lean b/Cslib/Algorithms/Lean/Sort/Insertion.lean
index 5e5d61d437..095f56ef91 100644
--- a/Cslib/Algorithms/Lean/Sort/Insertion.lean
+++ b/Cslib/Algorithms/Lean/Sort/Insertion.lean
@@ -4,8 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Eric Wieser
 -/
 module
+
 public import Mathlib.Data.List.Sort
 
+import Cslib.Init
+
 /-!
 # A Monadic version of the builtin `List.insertionSort`
 
diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
index 9dfc994720..b8d6ad0def 100644
--- a/Cslib/Algorithms/Lean/Sort/Merge.lean
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -4,8 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Eric Wieser
 -/
 module
+
 import all Init.Data.List.Sort.Basic
 
+import Cslib.Init
+
 /-!
 # A Monadic version of the builtin `List.mergeSort`
 

From fd34ff171b114eaee11884ac24d47f8711bebcc8 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Fri, 4 Sep 2026 01:47:37 +0000
Subject: [PATCH 10/24] Address the TODO

---
 .../Algorithms/Lean/MergeSort/MergeSort.lean  | 71 ++++++++++---------
 1 file changed, 36 insertions(+), 35 deletions(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index c2be5d897f..31b07274b9 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -33,25 +33,37 @@ set_option autoImplicit false
 
 namespace Cslib.Algorithms.Lean.TimeM
 
-variable {α : Type} [LinearOrder α]
+variable {α : Type}
+
+open List in
+/-- `TimeM.ret` passes through `List.mergeM` into the comparator. -/
+@[simp, grind =]
+theorem ret_mergeM {T} [AddMonoid T] (xs ys : List α) (le : α → α → TimeM T Bool) :
+    ⟪List.mergeM xs ys le⟫ = List.merge xs ys (fun x y => ⟪le x y⟫) := by
+  fun_induction merge with grind [mergeM, nil_merge, merge_right, cons_merge_cons]
+
+open List in
+/-- `TimeM.ret` passes through `List.mergeSortM` into the comparator. -/
+@[simp]
+theorem ret_mergeSortM {T} [AddMonoid T] (xs : List α) (le : α → α → TimeM T Bool) :
+    ⟪List.mergeSortM xs le⟫ = List.mergeSort xs (fun x y => ⟪le x y⟫) := by
+  fun_induction List.mergeSortM with
+  | case1 | case2 => simp
+  | case3 a b xs le _ _ _ iha ihb =>
+    simp only [ret_bind, ret_mergeM, mergeSort]
+    rw [iha, ihb]
+
+variable [LinearOrder α]
 
 /-- Merges two lists into a single list, counting comparisons as time cost.
 Returns a `TimeM ℕ (List α)` where the time represents the number of comparisons performed. -/
-def merge (xs ys : List α) : TimeM ℕ (List α) :=
+abbrev merge (xs ys : List α) : TimeM ℕ (List α) :=
   List.mergeM xs ys fun x y => do ✓ return x ≤ y
 
--- TODO: replace this with `List.mergeSortM`
 /-- Sorts a list using the merge sort algorithm, counting comparisons as time cost.
 Returns a `TimeM ℕ (List α)` where the time represents the total number of comparisons. -/
-def mergeSort (xs : List α) : TimeM ℕ (List α) :=  do
-  if xs.length < 2 then return xs
-  else
-    let half  := xs.length / 2
-    let left  := xs.take half
-    let right := xs.drop half
-    let sortedLeft  ← mergeSort left
-    let sortedRight ← mergeSort right
-    merge sortedLeft sortedRight
+abbrev mergeSort (xs : List α) : TimeM ℕ (List α) :=
+  List.mergeSortM xs fun x y => do ✓ return x ≤ y
 
 section Correctness
 
@@ -82,25 +94,16 @@ theorem sorted_merge {l1 l2 : List α} (hxs : IsSorted l1) (hys : IsSorted l2) :
   grind [hxs.merge hys]
 
 theorem mergeSort_sorted (xs : List α) : IsSorted ⟪mergeSort xs⟫ := by
-  fun_induction mergeSort xs with
-  | case1 x =>
-    rcases x with _ | ⟨a, _ | ⟨b, rest⟩⟩ <;> grind
-  | case2 _ _ _ _ _ ih2 ih1 => exact sorted_merge ih2 ih1
+  unfold mergeSort
+  simp only [bind_pure_comp, ret_mergeSortM, ret_map]
+  convert List.pairwise_mergeSort ?_ ?_ ?_ <;> grind
 
 lemma merge_perm (l₁ l₂ : List α) : ⟪merge l₁ l₂⟫ ~ l₁ ++ l₂ := by
   unfold merge
   fun_induction mergeM with grind [List.merge_perm_append]
 
 theorem mergeSort_perm (xs : List α) : ⟪mergeSort xs⟫ ~ xs := by
-  fun_induction mergeSort xs with
-  | case1 => simp
-  | case2 x _ _ left right ih2 ih1 =>
-    simp only [ret_bind]
-    calc
-      ⟪merge ⟪mergeSort left⟫ ⟪mergeSort right⟫⟫  ~
-      ⟪mergeSort left⟫ ++ ⟪mergeSort right⟫  := by apply merge_perm
-      _ ~ left++right := Perm.append ih2 ih1
-      _ ~ x := by simp only [take_append_drop, Perm.refl, left, right]
+  simpa using List.mergeSort_perm _ _
 
 /-- MergeSort is functionally correct. -/
 theorem mergeSort_correct (xs : List α) : IsSorted ⟪mergeSort xs⟫ ∧ ⟪mergeSort xs⟫ ~ xs :=
@@ -170,23 +173,21 @@ theorem merge_ret_length_eq_sum (xs ys : List α) :
 
 @[simp] theorem mergeSort_same_length (xs : List α) :
     ⟪mergeSort xs⟫.length = xs.length := by
-  fun_induction mergeSort
-  · simp
-  · grind [List.length_merge]
+  simp
 
 @[simp] theorem merge_time (xs ys : List α) : (merge xs ys).time ≤ xs.length + ys.length := by
   unfold merge
-  fun_induction List.mergeM with
-  | case3 =>
-    grind
-  | _ => simp
+  fun_induction List.mergeM with grind
 
 theorem mergeSort_time_le (xs : List α) :
     (mergeSort xs).time ≤ timeMergeSortRec xs.length := by
-  fun_induction mergeSort with
-  | case1 =>
+  unfold mergeSort
+  generalize hle' : (fun x y : α => _) = le'
+  fun_induction List.mergeSortM with
+  | case1 | case2 =>
     grind
-  | case2 _ _ _ _ _ ih2 ih1 =>
+  | case3 _ _ _ _ _ ih2 ih1 =>
+    subst hle'
     simp only [time_bind]
     grw [merge_time]
     simp only [mergeSort_same_length]

From 715b668c4d66ca350267e3d08c98a3f9bcc471db Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 6 Sep 2026 09:21:22 +0100
Subject: [PATCH 11/24] Fix lint

---
 Cslib/Algorithms/Lean/MergeSort/MergeSort.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index 31b07274b9..41a17bd4b7 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -171,7 +171,7 @@ theorem merge_ret_length_eq_sum (xs ys : List α) :
     ⟪merge xs ys⟫.length = xs.length + ys.length := by
   simp
 
-@[simp] theorem mergeSort_same_length (xs : List α) :
+theorem mergeSort_same_length (xs : List α) :
     ⟪mergeSort xs⟫.length = xs.length := by
   simp
 

From ba1178b7b7c68c48fd4ab4c95adc453871a62af4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 6 Sep 2026 11:46:21 +0100
Subject: [PATCH 12/24] lint fix

---
 Cslib/Algorithms/Lean/MergeSort/MergeSort.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index 41a17bd4b7..bade9d406f 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -70,10 +70,8 @@ section Correctness
 open List
 
 /-- Our merge computes the one already in mathlib. -/
-@[simp, grind =]
 theorem ret_merge (xs ys : List α) : ⟪merge xs ys⟫ = xs.merge ys := by
-  unfold merge
-  fun_induction mergeM with grind [nil_merge, merge_right, cons_merge_cons]
+  simp
 
 /-- A list is sorted if it satisfies the `Pairwise (· ≤ ·)` predicate. -/
 abbrev IsSorted (l : List α) : Prop := List.Pairwise (· ≤ ·) l

From e0136118d537a31c35824df9916967522e0618c4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sun, 6 Sep 2026 13:51:18 +0100
Subject: [PATCH 13/24] Update Cslib/Algorithms/Lean/Sort/Merge.lean

Co-authored-by: Fabrizio Montesi <fm@fabriziomontesi.com>
---
 Cslib/Algorithms/Lean/Sort/Merge.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
index b8d6ad0def..d7265326f5 100644
--- a/Cslib/Algorithms/Lean/Sort/Merge.lean
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -51,7 +51,7 @@ theorem idRun_mergeM (xs ys : List α) (le : α → α → Id Bool) :
   mergeM_pure _ _ _
 
 set_option linter.unusedVariables false in
-/-- A monadic version of `List.mergeSortM` -/
+/-- A monadic version of `List.mergeSort` -/
 def mergeSortM : ∀ (xs : List α) (le : α → α → m Bool), m (List α)
   | [], _ => return []
   | [a], _ => return [a]

From 8e0c1a9972f6285b5f73aff77bdba849aa963a98 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 9 Sep 2026 08:37:30 +0000
Subject: [PATCH 14/24] review comments

---
 Cslib/Algorithms/Lean/MergeSort/MergeSort.lean | 13 ++++---------
 Cslib/Algorithms/Lean/Sort/Merge.lean          | 18 ++++++++----------
 2 files changed, 12 insertions(+), 19 deletions(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index 31b07274b9..793b4955dd 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -49,7 +49,7 @@ theorem ret_mergeSortM {T} [AddMonoid T] (xs : List α) (le : α → α → Time
     ⟪List.mergeSortM xs le⟫ = List.mergeSort xs (fun x y => ⟪le x y⟫) := by
   fun_induction List.mergeSortM with
   | case1 | case2 => simp
-  | case3 a b xs le _ _ _ iha ihb =>
+  | case3 a b xs le iha ihb =>
     simp only [ret_bind, ret_mergeM, mergeSort]
     rw [iha, ihb]
 
@@ -94,13 +94,10 @@ theorem sorted_merge {l1 l2 : List α} (hxs : IsSorted l1) (hys : IsSorted l2) :
   grind [hxs.merge hys]
 
 theorem mergeSort_sorted (xs : List α) : IsSorted ⟪mergeSort xs⟫ := by
-  unfold mergeSort
-  simp only [bind_pure_comp, ret_mergeSortM, ret_map]
-  convert List.pairwise_mergeSort ?_ ?_ ?_ <;> grind
+  simpa using List.pairwise_mergeSort' _ xs
 
 lemma merge_perm (l₁ l₂ : List α) : ⟪merge l₁ l₂⟫ ~ l₁ ++ l₂ := by
-  unfold merge
-  fun_induction mergeM with grind [List.merge_perm_append]
+  simpa using List.merge_perm_append _
 
 theorem mergeSort_perm (xs : List α) : ⟪mergeSort xs⟫ ~ xs := by
   simpa using List.mergeSort_perm _ _
@@ -182,12 +179,10 @@ theorem merge_ret_length_eq_sum (xs ys : List α) :
 theorem mergeSort_time_le (xs : List α) :
     (mergeSort xs).time ≤ timeMergeSortRec xs.length := by
   unfold mergeSort
-  generalize hle' : (fun x y : α => _) = le'
   fun_induction List.mergeSortM with
   | case1 | case2 =>
     grind
-  | case3 _ _ _ _ _ ih2 ih1 =>
-    subst hle'
+  | case3 _ _ _ _ ih2 ih1 =>
     simp only [time_bind]
     grw [merge_time]
     simp only [mergeSort_same_length]
diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
index b8d6ad0def..7f01c5df60 100644
--- a/Cslib/Algorithms/Lean/Sort/Merge.lean
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -40,7 +40,7 @@ def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
   | nil => simp
   | cons x xs ih => simp [mergeM]
 
-@[simp]
+@[simp↓]
 theorem mergeM_pure [LawfulMonad m] (xs ys : List α) (le : α → α → Bool) :
     mergeM xs ys (fun x y => (pure (le x y) : m Bool)) = pure (merge xs ys le) := by
   fun_induction mergeM with grind [merge]
@@ -50,19 +50,17 @@ theorem idRun_mergeM (xs ys : List α) (le : α → α → Id Bool) :
     Id.run (mergeM xs ys le) = merge xs ys (fun x y => Id.run <| le x y) :=
   mergeM_pure _ _ _
 
-set_option linter.unusedVariables false in
 /-- A monadic version of `List.mergeSortM` -/
-def mergeSortM : ∀ (xs : List α) (le : α → α → m Bool), m (List α)
-  | [], _ => return []
-  | [a], _ => return [a]
-  | a :: b :: xs, le => do
+def mergeSortM (xs : List α) (le : α → α → m Bool) : m (List α) :=
+  match xs with
+  | [] => return []
+  | [a] => return [a]
+  | a :: b :: xs => do
     let lr := MergeSort.Internal.splitInTwo ⟨a :: b :: xs, rfl⟩
-    have := by simpa using lr.2.2
-    have := by simpa using lr.1.2
     mergeM (← mergeSortM lr.1 le) (← mergeSortM lr.2 le) le
-termination_by xs => xs.length
+termination_by xs.length
 
-@[simp]
+@[simp↓]
 theorem mergeSortM_pure [LawfulMonad m] (xs : List α) (le : α → α → Bool) :
     mergeSortM xs (fun x y => (pure (le x y) : m Bool)) = pure (mergeSort xs le) := by
   fun_induction mergeSort with

From ff566e06d807e97cd01c16af97d31ef07900dc3d Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Wed, 9 Sep 2026 09:43:12 +0100
Subject: [PATCH 15/24] Update Cslib/Algorithms/Lean/Sort/Insertion.lean

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
---
 Cslib/Algorithms/Lean/Sort/Insertion.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Sort/Insertion.lean b/Cslib/Algorithms/Lean/Sort/Insertion.lean
index 095f56ef91..c666d6c1e8 100644
--- a/Cslib/Algorithms/Lean/Sort/Insertion.lean
+++ b/Cslib/Algorithms/Lean/Sort/Insertion.lean
@@ -10,7 +10,7 @@ public import Mathlib.Data.List.Sort
 import Cslib.Init
 
 /-!
-# A Monadic version of the builtin `List.insertionSort`
+# A Monadic version of Mathlib's `List.insertionSort`
 
 This can be instantiated with `Id` to recover the original, or with `TimeM` or `FreeM` for
 algorithmic analysis.

From bd9edd2f7dfce45e8f1558b0de657acd10e7dbd0 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 9 Sep 2026 08:52:14 +0000
Subject: [PATCH 16/24] generalize universes

---
 .../Control/Monad/IsMonadHom/List.lean        | 28 +++++++++----------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
index 95fd4d1002..0d26693d18 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -23,8 +23,8 @@ public section
 
 namespace Cslib
 
-universe u v w
-variable {m n : Type u → Type v}
+universe u um un v
+variable {m : Type u → Type um} {n : Type u → Type un}
 
 /-! ### Preservation of list operations under applicative homomorphisms -/
 
@@ -33,13 +33,13 @@ variable [Applicative m] [Applicative n]
 
 @[grind .]
 theorem map_listMapA {F : ∀ {α}, m α → n α} (hf : IsApplicativeHom m n F)
-    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
     F (l.mapA f) = l.mapA (F ∘ f) := by
   induction l with grind [List.mapA]
 
 @[grind .]
 theorem map_listForA {F : ∀ {α}, m α → n α} (hf : IsApplicativeHom m n F)
-    {α : Type w} (l : List α) (f : α → m PUnit) :
+    {α : Type v} (l : List α) (f : α → m PUnit) :
     F (l.forA f) = l.forA (F ∘ f) := by
   induction l with grind [List.forA]
 
@@ -53,32 +53,32 @@ variable [Monad m] [Monad n]
 @[grind .]
 theorem map_listMapM'
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
     F (l.mapM' f) = l.mapM' (F ∘ f) := by
   induction l with grind [List.mapM']
 
 @[grind .]
 theorem map_listMapM [LawfulMonad m] [LawfulMonad n]
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
     F (l.mapM f) = l.mapM (F ∘ f) := by
   induction l with grind
 
 @[grind .]
 theorem map_listForM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {α : Type w} (l : List α) (f : α → m PUnit) :
+    {α : Type v} (l : List α) (f : α → m PUnit) :
     F (l.forM f) = l.forM (F ∘ f) := by
   induction l with grind [List.forM]
 
 @[grind .]
 theorem map_listFoldlM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {s : Type u} {α : Type w} (f : s → α → m s) (init : s) (l : List α) :
+    {s : Type u} {α : Type v} (f : s → α → m s) (init : s) (l : List α) :
     F (l.foldlM f init) = l.foldlM (fun s a => F (f s a)) init := by
   induction l generalizing init with grind [List.foldlM]
 
 @[grind .]
 theorem map_listFoldrM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) :
+    {s : Type u} {α : Type v} (f : α → s → m s) (init : s) (l : List α) :
     F (l.foldrM f init) = l.foldrM (fun a s => F (f a s)) init := by
   simp only [List.foldrM]
   exact hf.map_listFoldlM (fun s a => f a s) init l.reverse
@@ -86,7 +86,7 @@ theorem map_listFoldrM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
 @[grind .]
 theorem map_listFindSomeM?
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {α : Type w} {β : Type u} (f : α → m (Option β)) (l : List α) :
+    {α : Type v} {β : Type u} (f : α → m (Option β)) (l : List α) :
     F (l.findSomeM? f) = l.findSomeM? (F ∘ f) := by
   induction l with grind
 
@@ -100,14 +100,14 @@ theorem map_listFindM? {m n : Type → Type v} [Monad m] [Monad n]
 @[grind .]
 theorem map_listAnyM {m n : Type → Type v} [Monad m] [Monad n]
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {α : Type w} (p : α → m Bool) (l : List α) :
+    {α : Type v} (p : α → m Bool) (l : List α) :
     F (l.anyM p) = l.anyM (F ∘ p) := by
   induction l with grind [List.anyM]
 
 @[grind .]
 theorem map_listAllM {m n : Type → Type v} [Monad m] [Monad n]
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
-    {α : Type w} (p : α → m Bool) (l : List α) :
+    {α : Type v} (p : α → m Bool) (l : List α) :
     F (l.allM p) = l.allM (F ∘ p) := by
   induction l with grind [List.allM]
 
@@ -134,7 +134,7 @@ variable [Alternative m] [Alternative n]
 
 @[grind .]
 theorem map_listFirstM {F : ∀ {α}, m α → n α} (hf : IsAlternativeHom m n F)
-    {α : Type w} {β : Type u} (f : α → m β) (l : List α) :
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
     F (l.firstM f) = l.firstM (F ∘ f) := by
   induction l with grind [List.firstM]
 
@@ -164,7 +164,7 @@ section uniqueness
 
 /-- A property holds on all lists if it holds on the nil list, the singleton list,
 and concatenations thereof. -/
-private theorem List.nil_singleton_append_induction {motive : List α → Prop}
+private theorem List.nil_singleton_append_induction {α : Type*} {motive : List α → Prop}
     (nil : motive []) (singleton : ∀ a, motive [a])
     (append : ∀ xs ys, motive xs → motive ys → motive (xs ++ ys)) :
     ∀ l, motive l

From b69ee6bf3633cc6ebe0c3f2377244653a2a830d6 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 9 Sep 2026 08:59:47 +0000
Subject: [PATCH 17/24] more review comments

---
 Cslib/Foundations/Control/Monad/IsMonadHom.lean    | 14 ++++++++++++--
 .../Foundations/Control/Monad/IsMonadHom/List.lean | 11 ++++++++++-
 2 files changed, 22 insertions(+), 3 deletions(-)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom.lean b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
index 90c79b4d86..a515d1a408 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 module
 
 public import Cslib.Init
-public import Mathlib.Logic.Function.Defs
+
 public import Batteries.Control.AlternativeMonad
 public import Std.Do.WP.Monad
 
@@ -209,6 +209,16 @@ protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n 
   toIsApplicativeHom := hf.toIsApplicativeHom.comp hg.toIsApplicativeHom
   map_bind _ _ := by simp [hf.map_bind, hg.map_bind]
 
+protected theorem monadLift [LawfulMonad m] [LawfulMonad n]
+    [MonadLift m n] [LawfulMonadLift m n] :
+    IsMonadHom m n MonadLift.monadLift :=
+  .mk' LawfulMonadLift.monadLift_pure LawfulMonadLift.monadLift_bind
+
+protected theorem monadLiftT [LawfulMonad m] [LawfulMonad n]
+    [MonadLiftT m n] [LawfulMonadLiftT m n] :
+    IsMonadHom m n monadLift :=
+  .mk' LawfulMonadLiftT.monadLift_pure LawfulMonadLiftT.monadLift_bind
+
 end IsMonadHom
 
 /-! ### Alternative Homomorphisms -/
@@ -302,7 +312,7 @@ protected theorem comp {f : ∀ {α}, n α → p α} {g : ∀ {α}, m α → n 
 end IsAlternativeMonadHom
 
 open Std.Do WPMonad in
-theorem wp_isMonadHom [Monad m] [WPMonad m ps] : IsMonadHom m (PredTrans ps) WP.wp :=
+theorem IsMonadHom.wp [Monad m] [WPMonad m ps] : IsMonadHom m (PredTrans ps) WP.wp :=
   .mk' wp_pure wp_bind
 
 end Cslib
diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
index 0d26693d18..a7efbde8f9 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -57,12 +57,21 @@ theorem map_listMapM'
     F (l.mapM' f) = l.mapM' (F ∘ f) := by
   induction l with grind [List.mapM']
 
+@[grind .]
+theorem map_listMapMLoop [LawfulMonad m] [LawfulMonad n]
+    {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
+    {α : Type v} {β : Type u} (f : α → m β) (l : List α) (acc : List β) :
+    F (List.mapM.loop f l acc) = List.mapM.loop (F ∘ f) l acc := by
+  induction l generalizing acc with
+  | nil => exact hf.map_pure _
+  | cons a l ih => simp only [List.mapM.loop, hf.map_bind, ih, Function.comp_def]
+
 @[grind .]
 theorem map_listMapM [LawfulMonad m] [LawfulMonad n]
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
     {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
     F (l.mapM f) = l.mapM (F ∘ f) := by
-  induction l with grind
+  grind [List.mapM]
 
 @[grind .]
 theorem map_listForM {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)

From 445d6bde609bd797125f88ad2c6f5368ce25e6b1 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Wed, 9 Sep 2026 09:02:55 +0000
Subject: [PATCH 18/24] drop lawful

---
 Cslib/Foundations/Control/Monad/IsMonadHom/List.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
index a7efbde8f9..7bd945023e 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -58,7 +58,7 @@ theorem map_listMapM'
   induction l with grind [List.mapM']
 
 @[grind .]
-theorem map_listMapMLoop [LawfulMonad m] [LawfulMonad n]
+theorem map_listMapMLoop
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
     {α : Type v} {β : Type u} (f : α → m β) (l : List α) (acc : List β) :
     F (List.mapM.loop f l acc) = List.mapM.loop (F ∘ f) l acc := by
@@ -67,7 +67,7 @@ theorem map_listMapMLoop [LawfulMonad m] [LawfulMonad n]
   | cons a l ih => simp only [List.mapM.loop, hf.map_bind, ih, Function.comp_def]
 
 @[grind .]
-theorem map_listMapM [LawfulMonad m] [LawfulMonad n]
+theorem map_listMapM
     {F : ∀ {α}, m α → n α} (hf : IsMonadHom m n F)
     {α : Type v} {β : Type u} (f : α → m β) (l : List α) :
     F (l.mapM f) = l.mapM (F ∘ f) := by

From 9025e649dac9bf2b52764c79f07436a9f9083e8d Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 10 Sep 2026 09:34:09 +0000
Subject: [PATCH 19/24] fix namespace

---
 Cslib/Foundations/Control/Monad/IsMonadHom/List.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
index 7bd945023e..44e3cc6583 100644
--- a/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
+++ b/Cslib/Foundations/Control/Monad/IsMonadHom/List.lean
@@ -166,7 +166,7 @@ theorem IsFunctorHom.map_listNil {F : ∀ {α}, List α → List α} (hf : IsFun
   simpa [Subsingleton.elim (F ([] : List PEmpty)) []]
     using (hf.map_map PEmpty.elim []).symm
 
-protected theorem List.isMonadHom_reverse : IsMonadHom List List List.reverse :=
+protected theorem _root_.List.isMonadHom_reverse : IsMonadHom List List List.reverse :=
   .mk' (fun _ => rfl) (fun _ _ => List.reverse_flatMap)
 
 section uniqueness

From 1a1e3275faece7d9d2b06abeda6fcb3103d64228 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 10 Sep 2026 09:44:09 +0000
Subject: [PATCH 20/24] add simp lemmas

---
 Cslib/Algorithms/Lean/Sort/Insertion.lean | 14 +++++++++++++-
 Cslib/Algorithms/Lean/Sort/Merge.lean     | 17 +++++++++++++++--
 2 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Sort/Insertion.lean b/Cslib/Algorithms/Lean/Sort/Insertion.lean
index c666d6c1e8..8c571cf86a 100644
--- a/Cslib/Algorithms/Lean/Sort/Insertion.lean
+++ b/Cslib/Algorithms/Lean/Sort/Insertion.lean
@@ -27,6 +27,13 @@ def orderedInsertM (a : α) : List α → m (List α)
   | [] => return [a]
   | b :: l => do if ← r a b then return a :: b :: l else return b :: (← orderedInsertM a l)
 
+@[simp] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := by
+  rfl
+@[simp] theorem orderedInsertM_cons (a b : α) (l : List α) :
+    orderedInsertM r a (b :: l) = do
+      if ← r a b then return a :: b :: l else return b :: (← orderedInsertM r a l) := by
+  rfl
+
 @[simp]
 theorem orderedInsertM_pure [LawfulMonad m] (r : α → α → Bool) (a : α) (xs : List α) :
     orderedInsertM (fun x y => (pure (r x y) : m Bool)) a xs =
@@ -39,11 +46,16 @@ theorem idRun_orderedInsertM (r : α → α → Id Bool) (a : α) (xs : List α)
   orderedInsertM_pure _ _ _
 
 /-- A monadic version of `List.insertionSort`. -/
-@[simp]
 def insertionSortM : List α → m (List α)
   | [] => return []
   | b :: l => do orderedInsertM r b (← insertionSortM l)
 
+@[simp] theorem insertionSortM_nil : insertionSortM r [] = pure [] := by
+  rfl
+@[simp] theorem insertionSortM_cons (b : α) (l : List α) :
+    insertionSortM r (b :: l) = (do orderedInsertM r b (← insertionSortM r l)) := by
+  rfl
+
 @[simp]
 theorem insertionSortM_pure [LawfulMonad m] (xs : List α) (r : α → α → Bool) :
     insertionSortM (fun x y => (pure (r x y) : m Bool)) xs = pure (insertionSort (r · ·) xs) := by
diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
index 7f01c5df60..a1f4c68d72 100644
--- a/Cslib/Algorithms/Lean/Sort/Merge.lean
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -39,6 +39,13 @@ def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
   induction xs with
   | nil => simp
   | cons x xs ih => simp [mergeM]
+@[simp] theorem cons_mergeM_cons (x y : α) (xs ys : List α) (le : α → α → m Bool) :
+    mergeM (x :: xs) (y :: ys) le = do
+      if ← le x y then
+        return x :: (← mergeM xs (y :: ys) le)
+      else
+        return y :: (← mergeM (x :: xs) ys le) := by
+  simp [mergeM]
 
 @[simp↓]
 theorem mergeM_pure [LawfulMonad m] (xs ys : List α) (le : α → α → Bool) :
@@ -60,12 +67,18 @@ def mergeSortM (xs : List α) (le : α → α → m Bool) : m (List α) :=
     mergeM (← mergeSortM lr.1 le) (← mergeSortM lr.2 le) le
 termination_by xs.length
 
+@[simp] theorem mergeSortM_nil (le : α → α → m Bool) : mergeSortM [] le = pure [] := by
+  simp [mergeSortM]
+@[simp] theorem mergeSortM_singleton (a : α) (le : α → α → m Bool) :
+    mergeSortM [a] le = pure [a] := by
+  simp [mergeSortM]
+
 @[simp↓]
 theorem mergeSortM_pure [LawfulMonad m] (xs : List α) (le : α → α → Bool) :
     mergeSortM xs (fun x y => (pure (le x y) : m Bool)) = pure (mergeSort xs le) := by
   fun_induction mergeSort with
-  | case1 | case2 => simp [mergeSortM]
-  | case3  a b xs le lr _ _ ih1 ih2 =>
+  | case1 | case2 => simp
+  | case3 a b xs le lr _ _ ih1 ih2 =>
     simp only [mergeSortM]
     rw [ih1, ih2]
     simp

From fff58b10940b6219aad0a535ae2a2b3d899dca89 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 10 Sep 2026 10:18:46 +0000
Subject: [PATCH 21/24] add IsMonadHom uses

---
 Cslib/Algorithms/Lean/Sort/Merge.lean | 29 +++++++++++++++++++++++----
 1 file changed, 25 insertions(+), 4 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
index a1f4c68d72..ecbe700d25 100644
--- a/Cslib/Algorithms/Lean/Sort/Merge.lean
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -5,8 +5,9 @@ Authors: Kim Morrison, Eric Wieser
 -/
 module
 
-import all Init.Data.List.Sort.Basic
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
+import all Init.Data.List.Sort.Basic
 import Cslib.Init
 
 /-!
@@ -18,9 +19,11 @@ algorithmic analysis.
 
 public section
 
+open Cslib (IsMonadHom)
+
 namespace List
 
-variable {m} [Monad m]
+variable {m n} [Monad m] [Monad n]
 
 /-- A monadic version of `List.merge` -/
 def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
@@ -33,9 +36,11 @@ def mergeM (xs ys : List α) (le : α → α → m Bool) : m (List α) := do
     else
       return y :: (← mergeM (x :: xs) ys le)
 
-@[simp] theorem nil_mergeM (ys : List α) (le : α → α → m Bool) : mergeM [] ys le = pure ys := by
+@[simp, grind =]
+theorem nil_mergeM (ys : List α) (le : α → α → m Bool) : mergeM [] ys le = pure ys := by
   simp [mergeM]
-@[simp] theorem mergeM_right (xs : List α) (le : α → α → m Bool) : mergeM xs [] le = pure xs := by
+@[simp, grind =]
+theorem mergeM_right (xs : List α) (le : α → α → m Bool) : mergeM xs [] le = pure xs := by
   induction xs with
   | nil => simp
   | cons x xs ih => simp [mergeM]
@@ -57,6 +62,14 @@ theorem idRun_mergeM (xs ys : List α) (le : α → α → Id Bool) :
     Id.run (mergeM xs ys le) = merge xs ys (fun x y => Id.run <| le x y) :=
   mergeM_pure _ _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listMergeM (f : {β : Type} → m β → n β)
+    (hf : IsMonadHom m n f) (xs ys : List α) (le : α → α → m Bool) :
+    f (mergeM xs ys le) = mergeM xs ys (fun x y => f (le x y)) := by
+  fun_induction mergeM xs ys le with
+  | case1 | case2 => grind
+  | case3 x xs y ys ihx ihy => simp [hf.map_bind, hf.map_pure, apply_ite f, ihx, ihy]
+
 /-- A monadic version of `List.mergeSortM` -/
 def mergeSortM (xs : List α) (le : α → α → m Bool) : m (List α) :=
   match xs with
@@ -88,4 +101,12 @@ theorem idRun_mergeSortM (xs : List α) (le : α → α → Id Bool) :
     Id.run (mergeSortM xs le) = mergeSort xs (fun x y => Id.run <| le x y) :=
   mergeSortM_pure _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listMergeSortM (f : {β : Type} → m β → n β)
+    (hf : IsMonadHom m n f) (xs : List α) (le : α → α → m Bool) :
+    f (mergeSortM xs le) = mergeSortM xs (fun x y => f (le x y)) := by
+  fun_induction mergeSortM xs le with
+  | case1 | case2 => simp [hf.map_pure]
+  | case3 a b xs le ih1 ih2 => simp only [mergeSortM, hf.map_bind, ih1, ih2, hf.map_listMergeM, le]
+
 end List

From 0002400b2deba033ed8ca31c556d037f49426257 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 10 Sep 2026 10:31:09 +0000
Subject: [PATCH 22/24] ret is a monad hom

---
 Cslib/Algorithms/Lean/MergeSort/MergeSort.lean |  8 ++------
 Cslib/Algorithms/Lean/Sort/Merge.lean          |  4 ++--
 Cslib/Algorithms/Lean/TimeM.lean               | 12 ++++++++++++
 3 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
index 44a703f0bc..2a1384cdc4 100644
--- a/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
+++ b/Cslib/Algorithms/Lean/MergeSort/MergeSort.lean
@@ -40,18 +40,14 @@ open List in
 @[simp, grind =]
 theorem ret_mergeM {T} [AddMonoid T] (xs ys : List α) (le : α → α → TimeM T Bool) :
     ⟪List.mergeM xs ys le⟫ = List.merge xs ys (fun x y => ⟪le x y⟫) := by
-  fun_induction merge with grind [mergeM, nil_merge, merge_right, cons_merge_cons]
+  simpa using Id.ext_iff.1 <| isMonadHom_pure_ret.map_listMergeM xs ys le
 
 open List in
 /-- `TimeM.ret` passes through `List.mergeSortM` into the comparator. -/
 @[simp]
 theorem ret_mergeSortM {T} [AddMonoid T] (xs : List α) (le : α → α → TimeM T Bool) :
     ⟪List.mergeSortM xs le⟫ = List.mergeSort xs (fun x y => ⟪le x y⟫) := by
-  fun_induction List.mergeSortM with
-  | case1 | case2 => simp
-  | case3 a b xs le iha ihb =>
-    simp only [ret_bind, ret_mergeM, mergeSort]
-    rw [iha, ihb]
+  simpa using Id.ext_iff.1 <| isMonadHom_pure_ret.map_listMergeSortM xs le
 
 variable [LinearOrder α]
 
diff --git a/Cslib/Algorithms/Lean/Sort/Merge.lean b/Cslib/Algorithms/Lean/Sort/Merge.lean
index ecbe700d25..e64c6523b4 100644
--- a/Cslib/Algorithms/Lean/Sort/Merge.lean
+++ b/Cslib/Algorithms/Lean/Sort/Merge.lean
@@ -63,7 +63,7 @@ theorem idRun_mergeM (xs ys : List α) (le : α → α → Id Bool) :
   mergeM_pure _ _ _
 
 @[grind .]
-theorem _root_.Cslib.IsMonadHom.map_listMergeM (f : {β : Type} → m β → n β)
+theorem _root_.Cslib.IsMonadHom.map_listMergeM {f : {β : Type} → m β → n β}
     (hf : IsMonadHom m n f) (xs ys : List α) (le : α → α → m Bool) :
     f (mergeM xs ys le) = mergeM xs ys (fun x y => f (le x y)) := by
   fun_induction mergeM xs ys le with
@@ -102,7 +102,7 @@ theorem idRun_mergeSortM (xs : List α) (le : α → α → Id Bool) :
   mergeSortM_pure _ _
 
 @[grind .]
-theorem _root_.Cslib.IsMonadHom.map_listMergeSortM (f : {β : Type} → m β → n β)
+theorem _root_.Cslib.IsMonadHom.map_listMergeSortM {f : {β : Type} → m β → n β}
     (hf : IsMonadHom m n f) (xs : List α) (le : α → α → m Bool) :
     f (mergeSortM xs le) = mergeSortM xs (fun x y => f (le x y)) := by
   fun_induction mergeSortM xs le with
diff --git a/Cslib/Algorithms/Lean/TimeM.lean b/Cslib/Algorithms/Lean/TimeM.lean
index 389d6945b0..1cf75a4af4 100644
--- a/Cslib/Algorithms/Lean/TimeM.lean
+++ b/Cslib/Algorithms/Lean/TimeM.lean
@@ -7,6 +7,7 @@ Authors: Sorrachai Yingchareonthawornhcai, Eric Wieser
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 public import Mathlib.Algebra.Group.Defs
 
 /-!
@@ -97,6 +98,8 @@ instance [AddZero T] : Monad (TimeM T) where
 @[simp, grind =] theorem ret_bind {α β} [Add T] (m : TimeM T α) (f : α → TimeM T β) :
     (m >>= f).ret = (f m.ret).ret := rfl
 @[simp, grind =] theorem ret_map {α β} (f : α → β) (x : TimeM T α) : (f <$> x).ret = f x.ret := rfl
+@[simp, grind =] theorem ret_mapConst {α β} (a : α) (x : TimeM T β) :
+    (Functor.mapConst a x).ret = a := rfl
 @[simp] theorem ret_seqRight {α} (x : TimeM T α) (y : Unit → TimeM T β) [Add T] :
     (SeqRight.seqRight x y).ret = (y ()).ret := rfl
 @[simp] theorem ret_seqLeft {α} [Add T] (x : TimeM T α) (y : Unit → TimeM T β) :
@@ -104,6 +107,15 @@ instance [AddZero T] : Monad (TimeM T) where
 @[simp] theorem ret_seq {α β} [Add T] (f : TimeM T (α → β)) (x : Unit → TimeM T α) :
     (Seq.seq f x).ret = f.ret (x ()).ret := rfl
 
+theorem isMonadHom_pure_ret [AddZero T] : Cslib.IsMonadHom (TimeM T) Id (fun x => pure x.ret) where
+  map_map _ _ := Id.ext <| ret_map _ _
+  map_mapConst _ __ := Id.ext <| ret_mapConst _ _
+  map_pure _ := Id.ext <| ret_pure _
+  map_seq _ _ := Id.ext <| ret_seq _ _
+  map_seqLeft _ _ := Id.ext <| ret_seqLeft _ _
+  map_seqRight _ _ := Id.ext <| ret_seqRight _ _
+  map_bind _ _ := Id.ext <| ret_bind _ _
+
 @[simp, grind =] theorem time_bind {α β} [Add T] (m : TimeM T α) (f : α → TimeM T β) :
     (m >>= f).time = m.time + (f m.ret).time := rfl
 @[simp, grind =] theorem time_pure {α} [Zero T] (a : α) : (pure a : TimeM T α).time = 0 := rfl

From 94497e1eb47a44eafdb793feee3af6e71d195881 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 10 Sep 2026 10:49:31 +0000
Subject: [PATCH 23/24] and insertionSort

---
 Cslib/Algorithms/Lean/Sort/Insertion.lean | 21 ++++++++++++++++++---
 1 file changed, 18 insertions(+), 3 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Sort/Insertion.lean b/Cslib/Algorithms/Lean/Sort/Insertion.lean
index 8c571cf86a..99f181437c 100644
--- a/Cslib/Algorithms/Lean/Sort/Insertion.lean
+++ b/Cslib/Algorithms/Lean/Sort/Insertion.lean
@@ -6,6 +6,7 @@ Authors: Jeremy Avigad, Eric Wieser
 module
 
 public import Mathlib.Data.List.Sort
+public import Cslib.Foundations.Control.Monad.IsMonadHom
 
 import Cslib.Init
 
@@ -18,18 +19,20 @@ algorithmic analysis.
 
 public section
 
+open Cslib (IsMonadHom)
+
 namespace List
 
-variable {m} [Monad m] (r : α → α → m Bool)
+variable {m n} [Monad m] [Monad n] (r : α → α → m Bool)
 
 /-- A monadic version of `List.orderedInsert`. -/
 def orderedInsertM (a : α) : List α → m (List α)
   | [] => return [a]
   | b :: l => do if ← r a b then return a :: b :: l else return b :: (← orderedInsertM a l)
 
-@[simp] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := by
+@[simp, grind =] theorem orderedInsertM_nil (a : α) : orderedInsertM r a [] = pure [a] := by
   rfl
-@[simp] theorem orderedInsertM_cons (a b : α) (l : List α) :
+@[simp, grind =] theorem orderedInsertM_cons (a b : α) (l : List α) :
     orderedInsertM r a (b :: l) = do
       if ← r a b then return a :: b :: l else return b :: (← orderedInsertM r a l) := by
   rfl
@@ -45,6 +48,12 @@ theorem idRun_orderedInsertM (r : α → α → Id Bool) (a : α) (xs : List α)
     Id.run (orderedInsertM r a xs) = orderedInsert (fun x y => Id.run <| r x y) a xs :=
   orderedInsertM_pure _ _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_orderedInsertM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (r : α → α → m Bool) (a : α) (xs : List α) :
+    f (orderedInsertM r a xs) = orderedInsertM (fun x y => f (r x y)) a xs := by
+  fun_induction orderedInsertM r a xs with grind
+
 /-- A monadic version of `List.insertionSort`. -/
 def insertionSortM : List α → m (List α)
   | [] => return []
@@ -66,4 +75,10 @@ theorem idRun_insertionSortM (xs : List α) (r : α → α → Id Bool) :
     Id.run (insertionSortM r xs) = insertionSort (fun x y => Id.run <| r x y) xs :=
   insertionSortM_pure _ _
 
+@[grind .]
+theorem _root_.Cslib.IsMonadHom.map_listinsertionSortM {f : {β : Type} → m β → n β}
+    (hf : IsMonadHom m n f) (r : α → α → m Bool) (xs : List α) :
+    f (insertionSortM r xs) = insertionSortM (fun x y => f (r x y)) xs := by
+  fun_induction insertionSortM r xs with simp [hf.map_pure, hf.map_bind, hf.map_orderedInsertM, *]
+
 end List

From 386d4af1aebed08452a4eee49cb409e1cbbb84f5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <efw@google.com>
Date: Thu, 10 Sep 2026 10:49:56 +0000
Subject: [PATCH 24/24] fix name

---
 Cslib/Algorithms/Lean/Sort/Insertion.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Algorithms/Lean/Sort/Insertion.lean b/Cslib/Algorithms/Lean/Sort/Insertion.lean
index 99f181437c..33a0e9ce3b 100644
--- a/Cslib/Algorithms/Lean/Sort/Insertion.lean
+++ b/Cslib/Algorithms/Lean/Sort/Insertion.lean
@@ -76,7 +76,7 @@ theorem idRun_insertionSortM (xs : List α) (r : α → α → Id Bool) :
   insertionSortM_pure _ _
 
 @[grind .]
-theorem _root_.Cslib.IsMonadHom.map_listinsertionSortM {f : {β : Type} → m β → n β}
+theorem _root_.Cslib.IsMonadHom.map_listInsertionSortM {f : {β : Type} → m β → n β}
     (hf : IsMonadHom m n f) (r : α → α → m Bool) (xs : List α) :
     f (insertionSortM r xs) = insertionSortM (fun x y => f (r x y)) xs := by
   fun_induction insertionSortM r xs with simp [hf.map_pure, hf.map_bind, hf.map_orderedInsertM, *]