From ab0840342523b217610b75692c9020e2930e1600 Mon Sep 17 00:00:00 2001
From: Shreyas <shreyasss94@gmail.com>
Date: Tue, 17 Mar 2026 18:09:16 +0100
Subject: [PATCH 1/4] add grind annotations and coe instance

---
 Cslib/Foundations/Control/Monad/Free.lean | 42 ++++++++---------------
 1 file changed, 14 insertions(+), 28 deletions(-)

diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 58b0b88ce..90d78b6da 100644
--- a/Cslib/Foundations/Control/Monad/Free.lean
+++ b/Cslib/Foundations/Control/Monad/Free.lean
@@ -96,7 +96,7 @@ variable {F : Type u → Type v} {ι : Type u} {α : Type w} {β : Type w'} {γ
 
 instance : Pure (FreeM F) where pure := .pure
 
-@[simp]
+@[simp, grind =]
 theorem pure_eq_pure : (pure : α → FreeM F α) = FreeM.pure := rfl
 
 /-- Bind operation for the `FreeM` monad. -/
@@ -115,7 +115,7 @@ protected theorem bind_assoc (x : FreeM F α) (f : α → FreeM F β) (g : β 
 
 instance : Bind (FreeM F) where bind := .bind
 
-@[simp]
+@[simp, grind =]
 theorem bind_eq_bind {α β : Type w} : Bind.bind = (FreeM.bind : FreeM F α → _ → FreeM F β) := rfl
 
 /-- Map a function over a `FreeM` monad. -/
@@ -154,14 +154,21 @@ lemma map_lift (f : ι → α) (op : F ι) :
     map f (lift op : FreeM F ι) = liftBind op (fun z => (.pure (f z) : FreeM F α)) := rfl
 
 /-- `.pure a` followed by `bind` collapses immediately. -/
-@[simp]
+@[simp, grind =]
 lemma pure_bind (a : α) (f : α → FreeM F β) : (.pure a : FreeM F α).bind f = f a := rfl
 
-@[simp]
+@[simp, grind =]
+lemma pure_bind' {α β} (a : α) (f : α → FreeM F β) : (.pure a : FreeM F α) >>= f = f a :=
+  pure_bind a f
+
+@[simp, grind =]
 lemma bind_pure : ∀ x : FreeM F α, x.bind (.pure) = x
   | .pure a => rfl
   | liftBind op k => by simp [FreeM.bind, bind_pure]
 
+@[simp, grind =]
+lemma bind_pure' : ∀ x : FreeM F α, x >>= .pure = x := bind_pure
+
 @[simp]
 lemma bind_pure_comp (f : α → β) : ∀ x : FreeM F α, x.bind (.pure ∘ f) = map f x
   | .pure a => rfl
@@ -216,36 +223,15 @@ lemma liftM_lift [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (op
 @[simp]
 lemma liftM_bind [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (f : α → FreeM F β) :
-    (x.bind f).liftM interp = (do let a ← x.liftM interp; (f a).liftM interp) := by
+    (x.bind f : FreeM F β).liftM interp = (do let a ← x.liftM interp; (f a).liftM interp) := by
   induction x generalizing f with
   | pure a => simp only [pure_bind, liftM_pure, LawfulMonad.pure_bind]
   | liftBind op cont ih =>
     rw [FreeM.bind, liftM_liftBind, liftM_liftBind, bind_assoc]
     simp_rw [ih]
 
-@[simp]
-lemma liftM_map [LawfulMonad m]
-    (interp : {ι : Type u} → F ι → m ι) (f : α → β) (x : FreeM F α) :
-    (x.map f).liftM interp = f <$> x.liftM interp := by
-  simp_rw [← bind_pure_comp, ← LawfulMonad.bind_pure_comp, liftM_bind, Function.comp, liftM_pure]
-
-@[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]
-
-@[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]
-
-@[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]
+instance {Q α} : CoeOut (Q α) (FreeM Q α) where
+  coe := FreeM.lift
 
 /--
 A predicate stating that `interp : FreeM F α → m α` is an interpreter for the effect

From 7b4ea3513aba850266d27df7455751661337ec61 Mon Sep 17 00:00:00 2001
From: Shreyas <shreyasss94@gmail.com>
Date: Tue, 17 Mar 2026 18:15:43 +0100
Subject: [PATCH 2/4] Readd lemmas

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

diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 90d78b6da..61303e7a5 100644
--- a/Cslib/Foundations/Control/Monad/Free.lean
+++ b/Cslib/Foundations/Control/Monad/Free.lean
@@ -230,6 +230,30 @@ lemma liftM_bind [LawfulMonad m]
     rw [FreeM.bind, liftM_liftBind, liftM_liftBind, bind_assoc]
     simp_rw [ih]
 
+@[simp]
+lemma liftM_map [LawfulMonad m]
+    (interp : {ι : Type u} → F ι → m ι) (f : α → β) (x : FreeM F α) :
+    (x.map f).liftM interp = f <$> x.liftM interp := by
+  simp_rw [← bind_pure_comp, ← LawfulMonad.bind_pure_comp, liftM_bind, Function.comp, liftM_pure]
+
+@[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]
+
+@[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]
+
+@[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]
+
 instance {Q α} : CoeOut (Q α) (FreeM Q α) where
   coe := FreeM.lift
 

From 32741cae1f3f734dd7a420480c20a86308a127c8 Mon Sep 17 00:00:00 2001
From: Shreyas <shreyasss94@gmail.com>
Date: Tue, 17 Mar 2026 18:16:52 +0100
Subject: [PATCH 3/4] Remove unnecessary type annotation

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

diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 61303e7a5..92ffa3aac 100644
--- a/Cslib/Foundations/Control/Monad/Free.lean
+++ b/Cslib/Foundations/Control/Monad/Free.lean
@@ -223,7 +223,7 @@ lemma liftM_lift [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (op
 @[simp]
 lemma liftM_bind [LawfulMonad m]
     (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (f : α → FreeM F β) :
-    (x.bind f : FreeM F β).liftM interp = (do let a ← x.liftM interp; (f a).liftM interp) := by
+    (x.bind f).liftM interp = (do let a ← x.liftM interp; (f a).liftM interp) := by
   induction x generalizing f with
   | pure a => simp only [pure_bind, liftM_pure, LawfulMonad.pure_bind]
   | liftBind op cont ih =>

From 7935144d50ed36e69ccf8a2bcc2f3844fc24a93f Mon Sep 17 00:00:00 2001
From: Shreyas <shreyasss94@gmail.com>
Date: Tue, 17 Mar 2026 19:03:21 +0100
Subject: [PATCH 4/4] remove Coe as advised

---
 Cslib/Foundations/Control/Monad/Free.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean
index 92ffa3aac..d8402ebce 100644
--- a/Cslib/Foundations/Control/Monad/Free.lean
+++ b/Cslib/Foundations/Control/Monad/Free.lean
@@ -254,9 +254,6 @@ lemma liftM_seqRight [LawfulMonad m]
     (x *> y).liftM interp = x.liftM interp *> y.liftM interp := by
   simp [seqRight_eq_bind]
 
-instance {Q α} : CoeOut (Q α) (FreeM Q α) where
-  coe := FreeM.lift
-
 /--
 A predicate stating that `interp : FreeM F α → m α` is an interpreter for the effect
 handler `handler : ∀ {α}, F α → m α`.