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 1/6] 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 34a0d27be..267579dd6 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 09d550b8b..74dea4913 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 000000000..6726cc17b
--- /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 000000000..71640b1e7
--- /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 a29e97470..168782d16 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 2/6] 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 6726cc17b..f8fd0ba36 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 168782d16..05cb6535d 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 3/6] 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 71640b1e7..389faaf17 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 4/6] 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 f8fd0ba36..90c79b4d8 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 5/6] 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 389faaf17..daa4cf621 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 6/6] 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 daa4cf621..95fd4d100 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 _ _