From 2024bc58a538224e051ae741cdeadcc657bd8d6b Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 7 Apr 2026 14:52:47 -0400
Subject: [PATCH 01/10] feat(Data/PFunctor): add free monad of a polynomial
 functor

Port `PFunctor.FreeM` from VCV-io (ToMathlib/PFunctor/Free.lean).

This defines the free monad on a polynomial functor (`PFunctor`),
which extends the W-type construction with an extra `pure` constructor.

Main definitions:
- `PFunctor.FreeM`: inductive type with `pure` and `roll` constructors
- `FreeM.lift` / `FreeM.liftA`: lifting from the base functor
- `Monad` and `LawfulMonad` instances
- `FreeM.inductionOn` / `FreeM.construct`: elimination principles
- `FreeM.mapM`: canonical interpretation into any target monad

Made-with: Cursor
---
 Cslib.lean                                 |   1 +
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 226 +++++++++++++++++++++
 2 files changed, 227 insertions(+)
 create mode 100644 Cslib/Foundations/Data/PFunctor/FreeM.lean

diff --git a/Cslib.lean b/Cslib.lean
index 3e5977af2..494c95506 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -42,6 +42,7 @@ public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.FinFun
+public import Cslib.Foundations.Data.PFunctor.FreeM
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
new file mode 100644
index 000000000..8eefda8a9
--- /dev/null
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2026 Quang Dao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Quang Dao
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.PFunctor.Univariate.Basic
+
+/-!
+# Free Monad of a Polynomial Functor
+
+We define the free monad on a **polynomial functor** (`PFunctor`), and prove some basic properties.
+
+The free monad `PFunctor.FreeM P` extends the W-type construction with an extra `pure`
+constructor, yielding a monad that is free over the polynomial functor `P`.
+
+This construction is ported from the [VCV-io](https://github.com/Verified-zkEVM/VCV-io) library.
+
+## Main Definitions
+
+- `PFunctor.FreeM`: The free monad on a polynomial functor.
+- `PFunctor.FreeM.lift`: Lift an object of the base polynomial functor into the free monad.
+- `PFunctor.FreeM.liftA`: Lift a position of the base polynomial functor into the free monad.
+- `PFunctor.FreeM.mapM`: Canonical mapping of `FreeM P` into any other monad.
+- `PFunctor.FreeM.inductionOn`: Induction principle for `FreeM P`.
+- `PFunctor.FreeM.construct`: Dependent eliminator for `FreeM P`.
+-/
+
+@[expose] public section
+
+universe u v uA uB
+
+namespace PFunctor
+
+/-- The free monad on a polynomial functor.
+This extends the `W`-type construction with an extra `pure` constructor. -/
+inductive FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)
+  /-- A leaf node wrapping a pure value. -/
+  | pure {α} (a : α) : FreeM P α
+  /-- A node with shape `a : P.A` and subtrees given by the continuation
+  `cont : P.B a → FreeM P α`. -/
+  | roll {α} (a : P.A) (cont : P.B a → FreeM P α) : FreeM P α
+deriving Inhabited
+
+namespace FreeM
+
+variable {P : PFunctor.{uA, uB}} {α β γ : Type v}
+
+/-- Lift an object of the base polynomial functor into the free monad. -/
+@[always_inline, inline, reducible]
+def lift (x : P.Obj α) : FreeM P α := FreeM.roll x.1 (fun y ↦ FreeM.pure (x.2 y))
+
+/-- Lift a position of the base polynomial functor into the free monad. -/
+@[always_inline, inline, reducible]
+def liftA (a : P.A) : FreeM P (P.B a) := lift ⟨a, id⟩
+
+instance : MonadLift P (FreeM P) where
+  monadLift x := FreeM.lift x
+
+@[simp] lemma lift_ne_pure (x : P α) (y : α) :
+    (lift x : FreeM P α) ≠ PFunctor.FreeM.pure y := by simp [lift]
+
+@[simp] lemma pure_ne_lift (x : P α) (y : α) :
+    PFunctor.FreeM.pure y ≠ (lift x : FreeM P α) := by simp [lift]
+
+lemma monadLift_eq_lift (x : P.Obj α) : (x : FreeM P α) = FreeM.lift x := rfl
+
+/-- Bind operator on `FreeM P` used in the monad definition. -/
+@[always_inline, inline]
+protected def bind : FreeM P α → (α → FreeM P β) → FreeM P β
+  | FreeM.pure a, f => f a
+  | FreeM.roll a cont, f => FreeM.roll a (fun u ↦ FreeM.bind (cont u) f)
+
+@[simp]
+lemma bind_pure (a : α) (f : α → FreeM P β) :
+    FreeM.bind (FreeM.pure a) f = f a := rfl
+
+@[simp]
+lemma bind_roll (a : P.A) (cont : P.B a → FreeM P β) (f : β → FreeM P γ) :
+    FreeM.bind (FreeM.roll a cont) f = FreeM.roll a (fun u ↦ FreeM.bind (cont u) f) := rfl
+
+@[simp]
+lemma bind_lift (x : P.Obj α) (f : α → FreeM P β) :
+    FreeM.bind (FreeM.lift x) f = FreeM.roll x.1 (fun a ↦ f (x.2 a)) := rfl
+
+@[simp] lemma bind_eq_pure_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
+    FreeM.bind x f = FreeM.pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
+  cases x <;> simp
+
+@[simp] lemma pure_eq_bind_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
+    FreeM.pure b = FreeM.bind x f ↔ ∃ a, x = pure a ∧ pure b = f a := by
+  cases x <;> simp
+
+instance : Monad (FreeM P) where
+  pure := FreeM.pure
+  bind := FreeM.bind
+
+lemma monad_pure_def (a : α) : (pure a : FreeM P α) = FreeM.pure a := rfl
+
+lemma monad_bind_def (x : FreeM P α) (f : α → FreeM P β) :
+    x >>= f = FreeM.bind x f := rfl
+
+instance : LawfulMonad (FreeM P) :=
+  LawfulMonad.mk' (FreeM P)
+    (fun x ↦ by
+      induction x with
+      | pure _ => rfl
+      | roll a _ h => refine congr_arg (FreeM.roll a) (funext fun i ↦ h i))
+    (fun x f ↦ rfl)
+    (fun x f g ↦ by
+      induction x with
+      | pure _ => rfl
+      | roll a _ h => refine congr_arg (FreeM.roll a) (funext fun i ↦ h i))
+
+lemma pure_inj (a b : α) : FreeM.pure (P := P) a = FreeM.pure b ↔ a = b := by simp
+
+@[simp] lemma roll_inj (a a' : P.A)
+    (cont : P.B a → P.FreeM α) (cont' : P.B a' → P.FreeM α) :
+    FreeM.roll a cont = FreeM.roll a' cont' ↔ ∃ h : a = a', h ▸ cont = cont' := by
+  simp
+  by_cases ha : a = a'
+  · cases ha
+    simp
+  · simp [ha]
+
+/-- Proving a predicate `C` of `FreeM P α` requires two cases:
+* `pure a` for some `a : α`
+* `roll a cont h` for some `a : P.A`, `cont : P.B a → FreeM P α`, and `h : ∀ y, C (cont y)` -/
+@[elab_as_elim]
+protected def inductionOn {C : FreeM P α → Prop}
+    (pure : ∀ a, C (pure a))
+    (roll : (a : P.A) → (cont : P.B a → FreeM P α) → (∀ y, C (cont y)) →
+      C (FreeM.roll a cont)) :
+    (x : FreeM P α) → C x
+  | FreeM.pure a => pure a
+  | FreeM.roll a cont => roll a _ (fun u ↦ FreeM.inductionOn pure roll (cont u))
+
+section construct
+
+/-- Dependent eliminator for `FreeM P`. -/
+@[elab_as_elim]
+protected def construct {C : FreeM P α → Type*}
+    (pure : (a : α) → C (pure a))
+    (roll : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
+      C (FreeM.roll a cont)) :
+    (x : FreeM P α) → C x
+  | .pure a => pure a
+  | .roll a cont => roll a _ (fun u ↦ FreeM.construct pure roll (cont u))
+
+variable {C : FreeM P α → Type*} (h_pure : (a : α) → C (pure a))
+  (h_roll : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
+    C (FreeM.roll a cont))
+
+@[simp]
+lemma construct_pure (a : α) : FreeM.construct h_pure h_roll (pure a) = h_pure a := rfl
+
+@[simp]
+lemma construct_roll (a : P.A) (cont : P.B a → FreeM P α) :
+    (FreeM.construct h_pure h_roll (FreeM.roll a cont) : C (FreeM.roll a cont)) =
+      (h_roll a cont (fun u => FreeM.construct h_pure h_roll (cont u))) := rfl
+
+end construct
+
+section mapM
+
+variable {m : Type uB → Type v} {α : Type uB}
+
+/-- Canonical mapping of `FreeM P` into any other monad, given a map `s : (a : P.A) → m (P.B a)`.
+-/
+protected def mapM [Pure m] [Bind m] (s : (a : P.A) → m (P.B a)) : FreeM P α → m α
+  | .pure a => Pure.pure a
+  | .roll a cont => (s a) >>= (fun u ↦ (cont u).mapM s)
+
+variable [Monad m] (s : (a : P.A) → m (P.B a))
+
+@[simp]
+lemma mapM_pure' (a : α) : (FreeM.pure a : FreeM P α).mapM s = Pure.pure a := rfl
+
+@[simp]
+lemma mapM_roll (a : P.A) (cont : P.B a → FreeM P α) :
+    (FreeM.roll a cont).mapM s = s a >>= fun u => (cont u).mapM s := rfl
+
+@[simp] lemma mapM_pure (a : α) : (Pure.pure a : FreeM P α).mapM s = Pure.pure a := rfl
+
+variable [LawfulMonad m]
+
+@[simp]
+lemma mapM_bind {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
+    (FreeM.bind x f).mapM s = x.mapM s >>= fun u => (f u).mapM s := by
+  induction x using FreeM.inductionOn with
+  | pure _ => simp
+  | roll a cont h => simp [h]
+
+@[simp]
+lemma mapM_bind' {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
+    (x >>= f).mapM s = x.mapM s >>= fun u => (f u).mapM s :=
+  mapM_bind _ _ _
+
+@[simp]
+lemma mapM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
+    FreeM.mapM s (f <$> x) = f <$> FreeM.mapM s x := by
+  simp [← bind_pure_comp]
+
+@[simp]
+lemma mapM_seq {α β : Type uB}
+    (s : (a : P.A) → m (P.B a)) (x : FreeM P (α → β)) (y : FreeM P α) :
+    FreeM.mapM s (x <*> y) = (FreeM.mapM s x) <*> (FreeM.mapM s y) := by
+  simp [seq_eq_bind_map]
+
+@[simp]
+lemma mapM_lift (s : (a : P.A) → m (P.B a)) (x : P.Obj α) :
+    FreeM.mapM s (FreeM.lift x) = s x.1 >>= (fun u ↦ (pure (x.2 u)).mapM s) := by
+  simp [FreeM.mapM]
+
+@[simp]
+lemma mapM_liftA (s : (a : P.A) → m (P.B a)) (a : P.A) :
+    FreeM.mapM s (FreeM.liftA a) = s a := by simp [liftA]
+
+end mapM
+
+end FreeM
+
+end PFunctor

From fd3d994859aa990f0409f53edb15930a7a80f143 Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 7 Apr 2026 18:29:38 -0400
Subject: [PATCH 02/10] refactor(Data/PFunctor/FreeM): align with cslib
 conventions

- Make `pure` constructor protected, add explicit `Pure`/`Bind`/`Functor`/`LawfulFunctor` instances
- Add `map`, `id_map`, `comp_map` as explicit definitions before typeclass wiring
- Replace `monad_pure_def`/`monad_bind_def` with `@[simp] pure_eq_pure`/`bind_eq_bind`
- Rename lemmas to subject-first form: `pure_bind`, `bind_pure`, `roll_bind`, `lift_bind`
- Add `bind_pure` (right identity) and `bind_pure_comp` lemmas
- Remove `@[always_inline, inline, reducible]` attributes from `lift`, `liftA`, `bind`
- Rename `mapM` parameter `s` to `interp`
- Add `mapM_seqLeft`, `mapM_seqRight` lemmas
- Update `mapM_lift` statement to simplified form

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 161 ++++++++++++++-------
 1 file changed, 109 insertions(+), 52 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
index 8eefda8a9..0bbfb1040 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -17,7 +17,7 @@ We define the free monad on a **polynomial functor** (`PFunctor`), and prove som
 The free monad `PFunctor.FreeM P` extends the W-type construction with an extra `pure`
 constructor, yielding a monad that is free over the polynomial functor `P`.
 
-This construction is ported from the [VCV-io](https://github.com/Verified-zkEVM/VCV-io) library.
+This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io) library.
 
 ## Main Definitions
 
@@ -39,7 +39,7 @@ namespace PFunctor
 This extends the `W`-type construction with an extra `pure` constructor. -/
 inductive FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)
   /-- A leaf node wrapping a pure value. -/
-  | pure {α} (a : α) : FreeM P α
+  | protected pure {α} (a : α) : FreeM P α
   /-- A node with shape `a : P.A` and subtrees given by the continuation
   `cont : P.B a → FreeM P α`. -/
   | roll {α} (a : P.A) (cont : P.B a → FreeM P α) : FreeM P α
@@ -49,12 +49,15 @@ namespace FreeM
 
 variable {P : PFunctor.{uA, uB}} {α β γ : Type v}
 
+instance : Pure (FreeM P) where pure := .pure
+
+@[simp]
+theorem pure_eq_pure : (pure : α → FreeM P α) = FreeM.pure := rfl
+
 /-- Lift an object of the base polynomial functor into the free monad. -/
-@[always_inline, inline, reducible]
 def lift (x : P.Obj α) : FreeM P α := FreeM.roll x.1 (fun y ↦ FreeM.pure (x.2 y))
 
 /-- Lift a position of the base polynomial functor into the free monad. -/
-@[always_inline, inline, reducible]
 def liftA (a : P.A) : FreeM P (P.B a) := lift ⟨a, id⟩
 
 instance : MonadLift P (FreeM P) where
@@ -69,51 +72,90 @@ instance : MonadLift P (FreeM P) where
 lemma monadLift_eq_lift (x : P.Obj α) : (x : FreeM P α) = FreeM.lift x := rfl
 
 /-- Bind operator on `FreeM P` used in the monad definition. -/
-@[always_inline, inline]
 protected def bind : FreeM P α → (α → FreeM P β) → FreeM P β
   | FreeM.pure a, f => f a
   | FreeM.roll a cont, f => FreeM.roll a (fun u ↦ FreeM.bind (cont u) f)
 
+protected theorem bind_assoc (x : FreeM P α) (f : α → FreeM P β) (g : β → FreeM P γ) :
+    (x.bind f).bind g = x.bind (fun a => (f a).bind g) := by
+  induction x with
+  | pure a => rfl
+  | roll a cont ih =>
+    simp [FreeM.bind] at *
+    simp [ih]
+
+instance : Bind (FreeM P) where bind := .bind
+
+@[simp]
+theorem bind_eq_bind {α β : Type v} :
+    Bind.bind = (FreeM.bind : FreeM P α → _ → FreeM P β) := rfl
+
+/-- Map a function over a `FreeM` computation. -/
+@[simp]
+def map (f : α → β) : FreeM P α → FreeM P β
+  | .pure a => .pure (f a)
+  | .roll a cont => .roll a fun u => FreeM.map f (cont u)
+
+@[simp]
+theorem id_map : ∀ x : FreeM P α, map id x = x
+  | .pure a => rfl
+  | .roll a cont => by simp_all [map, id_map]
+
+theorem comp_map (h : β → γ) (g : α → β) :
+    ∀ x : FreeM P α, map (h ∘ g) x = map h (map g x)
+  | .pure a => rfl
+  | .roll a cont => by simp_all [map, comp_map]
+
+instance : Functor (FreeM P) where
+  map := .map
+
+@[simp]
+theorem map_eq_map {α β : Type v} :
+    Functor.map = FreeM.map (P := P) (α := α) (β := β) := rfl
+
+/-- `.pure a` followed by `bind` collapses immediately. -/
 @[simp]
-lemma bind_pure (a : α) (f : α → FreeM P β) :
-    FreeM.bind (FreeM.pure a) f = f a := rfl
+lemma pure_bind (a : α) (f : α → FreeM P β) :
+    (FreeM.pure a).bind f = f a := rfl
 
 @[simp]
-lemma bind_roll (a : P.A) (cont : P.B a → FreeM P β) (f : β → FreeM P γ) :
-    FreeM.bind (FreeM.roll a cont) f = FreeM.roll a (fun u ↦ FreeM.bind (cont u) f) := rfl
+lemma bind_pure : ∀ x : FreeM P α, x.bind (.pure) = x
+  | .pure a => rfl
+  | .roll a cont => by simp [FreeM.bind, bind_pure]
 
 @[simp]
-lemma bind_lift (x : P.Obj α) (f : α → FreeM P β) :
-    FreeM.bind (FreeM.lift x) f = FreeM.roll x.1 (fun a ↦ f (x.2 a)) := rfl
+lemma bind_pure_comp (f : α → β) : ∀ x : FreeM P α, x.bind (.pure ∘ f) = map f x
+  | .pure a => rfl
+  | .roll a cont => by simp only [FreeM.bind, map, bind_pure_comp]
+
+@[simp]
+lemma roll_bind (a : P.A) (cont : P.B a → FreeM P β) (f : β → FreeM P γ) :
+    (FreeM.roll a cont).bind f = FreeM.roll a (fun u ↦ (cont u).bind f) := rfl
+
+@[simp]
+lemma lift_bind (x : P.Obj α) (f : α → FreeM P β) :
+    (FreeM.lift x).bind f = FreeM.roll x.1 (fun a ↦ f (x.2 a)) := rfl
 
 @[simp] lemma bind_eq_pure_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
-    FreeM.bind x f = FreeM.pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
+    x.bind f = FreeM.pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
   cases x <;> simp
 
 @[simp] lemma pure_eq_bind_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
-    FreeM.pure b = FreeM.bind x f ↔ ∃ a, x = pure a ∧ pure b = f a := by
+    FreeM.pure b = x.bind f ↔ ∃ a, x = pure a ∧ pure b = f a := by
   cases x <;> simp
 
+instance : LawfulFunctor (FreeM P) where
+  map_const := rfl
+  id_map := id_map
+  comp_map _ _ := comp_map _ _
+
 instance : Monad (FreeM P) where
-  pure := FreeM.pure
-  bind := FreeM.bind
-
-lemma monad_pure_def (a : α) : (pure a : FreeM P α) = FreeM.pure a := rfl
-
-lemma monad_bind_def (x : FreeM P α) (f : α → FreeM P β) :
-    x >>= f = FreeM.bind x f := rfl
-
-instance : LawfulMonad (FreeM P) :=
-  LawfulMonad.mk' (FreeM P)
-    (fun x ↦ by
-      induction x with
-      | pure _ => rfl
-      | roll a _ h => refine congr_arg (FreeM.roll a) (funext fun i ↦ h i))
-    (fun x f ↦ rfl)
-    (fun x f g ↦ by
-      induction x with
-      | pure _ => rfl
-      | roll a _ h => refine congr_arg (FreeM.roll a) (funext fun i ↦ h i))
+
+instance : LawfulMonad (FreeM P) := LawfulMonad.mk'
+  (bind_pure_comp := bind_pure_comp)
+  (id_map := id_map)
+  (pure_bind := pure_bind)
+  (bind_assoc := FreeM.bind_assoc)
 
 lemma pure_inj (a b : α) : FreeM.pure (P := P) a = FreeM.pure b ↔ a = b := by simp
 
@@ -168,56 +210,71 @@ section mapM
 
 variable {m : Type uB → Type v} {α : Type uB}
 
-/-- Canonical mapping of `FreeM P` into any other monad, given a map `s : (a : P.A) → m (P.B a)`.
--/
-protected def mapM [Pure m] [Bind m] (s : (a : P.A) → m (P.B a)) : FreeM P α → m α
+/-- Canonical mapping of `FreeM P` into any other monad, given an interpretation
+`interp : (a : P.A) → m (P.B a)`. -/
+protected def mapM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : FreeM P α → m α
   | .pure a => Pure.pure a
-  | .roll a cont => (s a) >>= (fun u ↦ (cont u).mapM s)
+  | .roll a cont => (interp a) >>= (fun u ↦ (cont u).mapM interp)
 
-variable [Monad m] (s : (a : P.A) → m (P.B a))
+variable [Monad m] (interp : (a : P.A) → m (P.B a))
 
 @[simp]
-lemma mapM_pure' (a : α) : (FreeM.pure a : FreeM P α).mapM s = Pure.pure a := rfl
+lemma mapM_pure' (a : α) : (FreeM.pure a : FreeM P α).mapM interp = Pure.pure a := rfl
 
 @[simp]
 lemma mapM_roll (a : P.A) (cont : P.B a → FreeM P α) :
-    (FreeM.roll a cont).mapM s = s a >>= fun u => (cont u).mapM s := rfl
+    (FreeM.roll a cont).mapM interp = interp a >>= fun u => (cont u).mapM interp := rfl
 
-@[simp] lemma mapM_pure (a : α) : (Pure.pure a : FreeM P α).mapM s = Pure.pure a := rfl
+@[simp]
+lemma mapM_pure (a : α) : (Pure.pure a : FreeM P α).mapM interp = Pure.pure a := rfl
 
 variable [LawfulMonad m]
 
 @[simp]
 lemma mapM_bind {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
-    (FreeM.bind x f).mapM s = x.mapM s >>= fun u => (f u).mapM s := by
+    (x.bind f).mapM interp = x.mapM interp >>= fun u => (f u).mapM interp := by
   induction x using FreeM.inductionOn with
   | pure _ => simp
   | roll a cont h => simp [h]
 
 @[simp]
 lemma mapM_bind' {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
-    (x >>= f).mapM s = x.mapM s >>= fun u => (f u).mapM s :=
+    (x >>= f).mapM interp = x.mapM interp >>= fun u => (f u).mapM interp :=
   mapM_bind _ _ _
 
 @[simp]
 lemma mapM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
-    FreeM.mapM s (f <$> x) = f <$> FreeM.mapM s x := by
-  simp [← bind_pure_comp]
+    FreeM.mapM interp (map f x) = f <$> FreeM.mapM interp x := by
+  induction x using FreeM.inductionOn with
+  | pure _ => simp
+  | roll a cont h => simp [h]
 
 @[simp]
 lemma mapM_seq {α β : Type uB}
-    (s : (a : P.A) → m (P.B a)) (x : FreeM P (α → β)) (y : FreeM P α) :
-    FreeM.mapM s (x <*> y) = (FreeM.mapM s x) <*> (FreeM.mapM s y) := by
-  simp [seq_eq_bind_map]
+    (interp : (a : P.A) → m (P.B a)) (x : FreeM P (α → β)) (y : FreeM P α) :
+    FreeM.mapM interp (x <*> y) = (FreeM.mapM interp x) <*> (FreeM.mapM interp y) := by
+  simp only [seq_eq_bind_map, mapM_bind', map_eq_map, mapM_map]
+
+@[simp]
+lemma mapM_seqLeft {α β : Type uB}
+    (interp : (a : P.A) → m (P.B a)) (x : FreeM P α) (y : FreeM P β) :
+    FreeM.mapM interp (x <* y) = FreeM.mapM interp x <* FreeM.mapM interp y := by
+  simp only [seqLeft_eq_bind, mapM_bind', mapM_pure]
+
+@[simp]
+lemma mapM_seqRight {α β : Type uB}
+    (interp : (a : P.A) → m (P.B a)) (x : FreeM P α) (y : FreeM P β) :
+    FreeM.mapM interp (x *> y) = FreeM.mapM interp x *> FreeM.mapM interp y := by
+  simp only [seqRight_eq_bind, mapM_bind']
 
 @[simp]
-lemma mapM_lift (s : (a : P.A) → m (P.B a)) (x : P.Obj α) :
-    FreeM.mapM s (FreeM.lift x) = s x.1 >>= (fun u ↦ (pure (x.2 u)).mapM s) := by
-  simp [FreeM.mapM]
+lemma mapM_lift (interp : (a : P.A) → m (P.B a)) (x : P.Obj α) :
+    FreeM.mapM interp (FreeM.lift x) = x.2 <$> interp x.1 := by
+  simp [lift]
 
 @[simp]
-lemma mapM_liftA (s : (a : P.A) → m (P.B a)) (a : P.A) :
-    FreeM.mapM s (FreeM.liftA a) = s a := by simp [liftA]
+lemma mapM_liftA (interp : (a : P.A) → m (P.B a)) (a : P.A) :
+    FreeM.mapM interp (FreeM.liftA a) = interp a := by simp [liftA]
 
 end mapM
 

From ff3359e98e3989585d786b203c0cfe01027af578 Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 7 Apr 2026 22:55:22 -0400
Subject: [PATCH 03/10] refactor(Data/PFunctor/FreeM): rename `roll` to
 `liftBind`

Rename the `roll` constructor and all associated lemma/parameter names
to `liftBind`, matching the naming convention of `Cslib.FreeM`.

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 72 ++++++++++++----------
 1 file changed, 38 insertions(+), 34 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
index 0bbfb1040..66cb2d7e7 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -40,9 +40,8 @@ This extends the `W`-type construction with an extra `pure` constructor. -/
 inductive FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)
   /-- A leaf node wrapping a pure value. -/
   | protected pure {α} (a : α) : FreeM P α
-  /-- A node with shape `a : P.A` and subtrees given by the continuation
-  `cont : P.B a → FreeM P α`. -/
-  | roll {α} (a : P.A) (cont : P.B a → FreeM P α) : FreeM P α
+  /-- Invoke the operation `a : P.A` with continuation `cont : P.B a → FreeM P α`. -/
+  | liftBind {α} (a : P.A) (cont : P.B a → FreeM P α) : FreeM P α
 deriving Inhabited
 
 namespace FreeM
@@ -55,7 +54,7 @@ instance : Pure (FreeM P) where pure := .pure
 theorem pure_eq_pure : (pure : α → FreeM P α) = FreeM.pure := rfl
 
 /-- Lift an object of the base polynomial functor into the free monad. -/
-def lift (x : P.Obj α) : FreeM P α := FreeM.roll x.1 (fun y ↦ FreeM.pure (x.2 y))
+def lift (x : P.Obj α) : FreeM P α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y))
 
 /-- Lift a position of the base polynomial functor into the free monad. -/
 def liftA (a : P.A) : FreeM P (P.B a) := lift ⟨a, id⟩
@@ -74,13 +73,13 @@ lemma monadLift_eq_lift (x : P.Obj α) : (x : FreeM P α) = FreeM.lift x := rfl
 /-- Bind operator on `FreeM P` used in the monad definition. -/
 protected def bind : FreeM P α → (α → FreeM P β) → FreeM P β
   | FreeM.pure a, f => f a
-  | FreeM.roll a cont, f => FreeM.roll a (fun u ↦ FreeM.bind (cont u) f)
+  | FreeM.liftBind a cont, f => FreeM.liftBind a (fun u ↦ FreeM.bind (cont u) f)
 
 protected theorem bind_assoc (x : FreeM P α) (f : α → FreeM P β) (g : β → FreeM P γ) :
     (x.bind f).bind g = x.bind (fun a => (f a).bind g) := by
   induction x with
   | pure a => rfl
-  | roll a cont ih =>
+  | liftBind a cont ih =>
     simp [FreeM.bind] at *
     simp [ih]
 
@@ -94,17 +93,17 @@ theorem bind_eq_bind {α β : Type v} :
 @[simp]
 def map (f : α → β) : FreeM P α → FreeM P β
   | .pure a => .pure (f a)
-  | .roll a cont => .roll a fun u => FreeM.map f (cont u)
+  | .liftBind a cont => .liftBind a fun u => FreeM.map f (cont u)
 
 @[simp]
 theorem id_map : ∀ x : FreeM P α, map id x = x
   | .pure a => rfl
-  | .roll a cont => by simp_all [map, id_map]
+  | .liftBind a cont => by simp_all [map, id_map]
 
 theorem comp_map (h : β → γ) (g : α → β) :
     ∀ x : FreeM P α, map (h ∘ g) x = map h (map g x)
   | .pure a => rfl
-  | .roll a cont => by simp_all [map, comp_map]
+  | .liftBind a cont => by simp_all [map, comp_map]
 
 instance : Functor (FreeM P) where
   map := .map
@@ -121,20 +120,20 @@ lemma pure_bind (a : α) (f : α → FreeM P β) :
 @[simp]
 lemma bind_pure : ∀ x : FreeM P α, x.bind (.pure) = x
   | .pure a => rfl
-  | .roll a cont => by simp [FreeM.bind, bind_pure]
+  | .liftBind a cont => by simp [FreeM.bind, bind_pure]
 
 @[simp]
 lemma bind_pure_comp (f : α → β) : ∀ x : FreeM P α, x.bind (.pure ∘ f) = map f x
   | .pure a => rfl
-  | .roll a cont => by simp only [FreeM.bind, map, bind_pure_comp]
+  | .liftBind a cont => by simp only [FreeM.bind, map, bind_pure_comp]
 
 @[simp]
-lemma roll_bind (a : P.A) (cont : P.B a → FreeM P β) (f : β → FreeM P γ) :
-    (FreeM.roll a cont).bind f = FreeM.roll a (fun u ↦ (cont u).bind f) := rfl
+lemma liftBind_bind (a : P.A) (cont : P.B a → FreeM P β) (f : β → FreeM P γ) :
+    (FreeM.liftBind a cont).bind f = FreeM.liftBind a (fun u ↦ (cont u).bind f) := rfl
 
 @[simp]
 lemma lift_bind (x : P.Obj α) (f : α → FreeM P β) :
-    (FreeM.lift x).bind f = FreeM.roll x.1 (fun a ↦ f (x.2 a)) := rfl
+    (FreeM.lift x).bind f = FreeM.liftBind x.1 (fun a ↦ f (x.2 a)) := rfl
 
 @[simp] lemma bind_eq_pure_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
     x.bind f = FreeM.pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
@@ -159,9 +158,9 @@ instance : LawfulMonad (FreeM P) := LawfulMonad.mk'
 
 lemma pure_inj (a b : α) : FreeM.pure (P := P) a = FreeM.pure b ↔ a = b := by simp
 
-@[simp] lemma roll_inj (a a' : P.A)
+@[simp] lemma liftBind_inj (a a' : P.A)
     (cont : P.B a → P.FreeM α) (cont' : P.B a' → P.FreeM α) :
-    FreeM.roll a cont = FreeM.roll a' cont' ↔ ∃ h : a = a', h ▸ cont = cont' := by
+    FreeM.liftBind a cont = FreeM.liftBind a' cont' ↔ ∃ h : a = a', h ▸ cont = cont' := by
   simp
   by_cases ha : a = a'
   · cases ha
@@ -170,15 +169,17 @@ lemma pure_inj (a b : α) : FreeM.pure (P := P) a = FreeM.pure b ↔ a = b := by
 
 /-- Proving a predicate `C` of `FreeM P α` requires two cases:
 * `pure a` for some `a : α`
-* `roll a cont h` for some `a : P.A`, `cont : P.B a → FreeM P α`, and `h : ∀ y, C (cont y)` -/
+* `liftBind a cont h` for some `a : P.A`, `cont : P.B a → FreeM P α`,
+  and `h : ∀ y, C (cont y)` -/
 @[elab_as_elim]
 protected def inductionOn {C : FreeM P α → Prop}
     (pure : ∀ a, C (pure a))
-    (roll : (a : P.A) → (cont : P.B a → FreeM P α) → (∀ y, C (cont y)) →
-      C (FreeM.roll a cont)) :
+    (liftBind : (a : P.A) → (cont : P.B a → FreeM P α) → (∀ y, C (cont y)) →
+      C (FreeM.liftBind a cont)) :
     (x : FreeM P α) → C x
   | FreeM.pure a => pure a
-  | FreeM.roll a cont => roll a _ (fun u ↦ FreeM.inductionOn pure roll (cont u))
+  | FreeM.liftBind a cont =>
+    liftBind a _ (fun u ↦ FreeM.inductionOn pure liftBind (cont u))
 
 section construct
 
@@ -186,23 +187,26 @@ section construct
 @[elab_as_elim]
 protected def construct {C : FreeM P α → Type*}
     (pure : (a : α) → C (pure a))
-    (roll : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
-      C (FreeM.roll a cont)) :
+    (liftBind : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
+      C (FreeM.liftBind a cont)) :
     (x : FreeM P α) → C x
   | .pure a => pure a
-  | .roll a cont => roll a _ (fun u ↦ FreeM.construct pure roll (cont u))
+  | .liftBind a cont =>
+    liftBind a _ (fun u ↦ FreeM.construct pure liftBind (cont u))
 
 variable {C : FreeM P α → Type*} (h_pure : (a : α) → C (pure a))
-  (h_roll : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
-    C (FreeM.roll a cont))
+  (h_liftBind : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
+    C (FreeM.liftBind a cont))
 
 @[simp]
-lemma construct_pure (a : α) : FreeM.construct h_pure h_roll (pure a) = h_pure a := rfl
+lemma construct_pure (a : α) :
+    FreeM.construct h_pure h_liftBind (pure a) = h_pure a := rfl
 
 @[simp]
-lemma construct_roll (a : P.A) (cont : P.B a → FreeM P α) :
-    (FreeM.construct h_pure h_roll (FreeM.roll a cont) : C (FreeM.roll a cont)) =
-      (h_roll a cont (fun u => FreeM.construct h_pure h_roll (cont u))) := rfl
+lemma construct_liftBind (a : P.A) (cont : P.B a → FreeM P α) :
+    (FreeM.construct h_pure h_liftBind (FreeM.liftBind a cont) :
+      C (FreeM.liftBind a cont)) =
+      (h_liftBind a cont (fun u => FreeM.construct h_pure h_liftBind (cont u))) := rfl
 
 end construct
 
@@ -214,7 +218,7 @@ variable {m : Type uB → Type v} {α : Type uB}
 `interp : (a : P.A) → m (P.B a)`. -/
 protected def mapM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : FreeM P α → m α
   | .pure a => Pure.pure a
-  | .roll a cont => (interp a) >>= (fun u ↦ (cont u).mapM interp)
+  | .liftBind a cont => (interp a) >>= (fun u ↦ (cont u).mapM interp)
 
 variable [Monad m] (interp : (a : P.A) → m (P.B a))
 
@@ -222,8 +226,8 @@ variable [Monad m] (interp : (a : P.A) → m (P.B a))
 lemma mapM_pure' (a : α) : (FreeM.pure a : FreeM P α).mapM interp = Pure.pure a := rfl
 
 @[simp]
-lemma mapM_roll (a : P.A) (cont : P.B a → FreeM P α) :
-    (FreeM.roll a cont).mapM interp = interp a >>= fun u => (cont u).mapM interp := rfl
+lemma mapM_liftBind (a : P.A) (cont : P.B a → FreeM P α) :
+    (FreeM.liftBind a cont).mapM interp = interp a >>= fun u => (cont u).mapM interp := rfl
 
 @[simp]
 lemma mapM_pure (a : α) : (Pure.pure a : FreeM P α).mapM interp = Pure.pure a := rfl
@@ -235,7 +239,7 @@ lemma mapM_bind {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
     (x.bind f).mapM interp = x.mapM interp >>= fun u => (f u).mapM interp := by
   induction x using FreeM.inductionOn with
   | pure _ => simp
-  | roll a cont h => simp [h]
+  | liftBind a cont h => simp [h]
 
 @[simp]
 lemma mapM_bind' {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
@@ -247,7 +251,7 @@ lemma mapM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
     FreeM.mapM interp (map f x) = f <$> FreeM.mapM interp x := by
   induction x using FreeM.inductionOn with
   | pure _ => simp
-  | roll a cont h => simp [h]
+  | liftBind a cont h => simp [h]
 
 @[simp]
 lemma mapM_seq {α β : Type uB}

From 0ee7a8a7929e82da267238b2771774dbce16731f Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 7 Apr 2026 23:03:18 -0400
Subject: [PATCH 04/10] refactor(Data/PFunctor/FreeM): flip pure_eq_pure
 direction

Flip `pure_eq_pure` to normalize `FreeM.pure` to `pure` (typeclass),
matching the direction advocated in leanprover/cslib#417.

Adjust proofs of `bind_pure`, `bind_pure_comp`, `bind_eq_pure_iff`,
`pure_eq_bind_iff`, `pure_inj`, `mapM_bind`, and `mapM_map` to
account for the new simp normal form.

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 34 +++++++++++++---------
 1 file changed, 21 insertions(+), 13 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
index 66cb2d7e7..56f557442 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -51,7 +51,7 @@ variable {P : PFunctor.{uA, uB}} {α β γ : Type v}
 instance : Pure (FreeM P) where pure := .pure
 
 @[simp]
-theorem pure_eq_pure : (pure : α → FreeM P α) = FreeM.pure := rfl
+theorem pure_eq_pure : (FreeM.pure : α → FreeM P α) = pure := rfl
 
 /-- Lift an object of the base polynomial functor into the free monad. -/
 def lift (x : P.Obj α) : FreeM P α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y))
@@ -118,12 +118,13 @@ lemma pure_bind (a : α) (f : α → FreeM P β) :
     (FreeM.pure a).bind f = f a := rfl
 
 @[simp]
-lemma bind_pure : ∀ x : FreeM P α, x.bind (.pure) = x
+lemma bind_pure : ∀ x : FreeM P α, x.bind pure = x
   | .pure a => rfl
-  | .liftBind a cont => by simp [FreeM.bind, bind_pure]
+  | .liftBind a cont => by
+    simp only [FreeM.bind]; congr 1; funext u; exact bind_pure (cont u)
 
 @[simp]
-lemma bind_pure_comp (f : α → β) : ∀ x : FreeM P α, x.bind (.pure ∘ f) = map f x
+lemma bind_pure_comp (f : α → β) : ∀ x : FreeM P α, x.bind (pure ∘ f) = map f x
   | .pure a => rfl
   | .liftBind a cont => by simp only [FreeM.bind, map, bind_pure_comp]
 
@@ -136,12 +137,16 @@ lemma lift_bind (x : P.Obj α) (f : α → FreeM P β) :
     (FreeM.lift x).bind f = FreeM.liftBind x.1 (fun a ↦ f (x.2 a)) := rfl
 
 @[simp] lemma bind_eq_pure_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
-    x.bind f = FreeM.pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
-  cases x <;> simp
+    x.bind f = pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
+  cases x with
+  | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by rwa [FreeM.pure.inj h]⟩
+  | liftBind a cont => simp [FreeM.bind]
 
 @[simp] lemma pure_eq_bind_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
-    FreeM.pure b = x.bind f ↔ ∃ a, x = pure a ∧ pure b = f a := by
-  cases x <;> simp
+    pure b = x.bind f ↔ ∃ a, x = pure a ∧ pure b = f a := by
+  cases x with
+  | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by rwa [FreeM.pure.inj h]⟩
+  | liftBind a cont => simp [FreeM.bind]
 
 instance : LawfulFunctor (FreeM P) where
   map_const := rfl
@@ -156,7 +161,10 @@ instance : LawfulMonad (FreeM P) := LawfulMonad.mk'
   (pure_bind := pure_bind)
   (bind_assoc := FreeM.bind_assoc)
 
-lemma pure_inj (a b : α) : FreeM.pure (P := P) a = FreeM.pure b ↔ a = b := by simp
+lemma pure_inj (a b : α) : (pure a : FreeM P α) = pure b ↔ a = b := by
+  constructor
+  · exact FreeM.pure.inj
+  · rintro rfl; rfl
 
 @[simp] lemma liftBind_inj (a a' : P.A)
     (cont : P.B a → P.FreeM α) (cont' : P.B a' → P.FreeM α) :
@@ -237,8 +245,8 @@ variable [LawfulMonad m]
 @[simp]
 lemma mapM_bind {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
     (x.bind f).mapM interp = x.mapM interp >>= fun u => (f u).mapM interp := by
-  induction x using FreeM.inductionOn with
-  | pure _ => simp
+  induction x with
+  | pure _ => simp [FreeM.bind, FreeM.mapM]
   | liftBind a cont h => simp [h]
 
 @[simp]
@@ -249,8 +257,8 @@ lemma mapM_bind' {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
 @[simp]
 lemma mapM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
     FreeM.mapM interp (map f x) = f <$> FreeM.mapM interp x := by
-  induction x using FreeM.inductionOn with
-  | pure _ => simp
+  induction x with
+  | pure _ => simp [map, FreeM.mapM]
   | liftBind a cont h => simp [h]
 
 @[simp]

From 3b8adf2f7a064f263eea7f01e559d8127d7f68d1 Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 7 Apr 2026 23:05:12 -0400
Subject: [PATCH 05/10] docs(Data/PFunctor/FreeM): explain difference with
 Cslib.FreeM

Add a "Comparison with Cslib.FreeM" section to the module docstring,
showing both liftBind constructors side by side and explaining that
PFunctor.FreeM avoids the universe bump from the existential in
Cslib.FreeM when the effect signature is naturally polynomial.

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
index 56f557442..1ece08ee0 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -17,6 +17,27 @@ We define the free monad on a **polynomial functor** (`PFunctor`), and prove som
 The free monad `PFunctor.FreeM P` extends the W-type construction with an extra `pure`
 constructor, yielding a monad that is free over the polynomial functor `P`.
 
+## Comparison with `Cslib.FreeM`
+
+`Cslib.FreeM F` (in `Cslib.Foundations.Control.Monad.Free`) builds a free monad over an
+arbitrary type constructor `F : Type u → Type v`, using a single `liftBind` constructor that
+existentially quantifies the intermediate type:
+```
+| liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : FreeM F α
+```
+Here the intermediate type `ι` is hidden, so `F` need not be a `Functor`.
+
+`PFunctor.FreeM P` instead takes a polynomial functor `P : PFunctor`, where the shapes
+`P.A` and children `P.B a` are given explicitly.
+Its `liftBind` constructor carries the shape and continuation without existential quantification:
+```
+| liftBind (a : P.A) (cont : P.B a → FreeM P α) : FreeM P α
+```
+
+When the effect signature is naturally polynomial (a fixed set of operations, each with a
+known return type), `PFunctor.FreeM` gives stronger eliminators and avoids the universe
+bump that the existential in `Cslib.FreeM` introduces.
+
 This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io) library.
 
 ## Main Definitions

From 514081abf815ad0e7574cec8b745bbc4fe75559e Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 7 Apr 2026 23:37:38 -0400
Subject: [PATCH 06/10] refactor(Data/PFunctor/FreeM): remove inductionOn and
 construct

Both are redundant with the auto-generated FreeM.rec:
- construct is FreeM.rec restricted to Type* (strictly weaker)
- inductionOn is FreeM.rec restricted to Prop

Plain `induction x with | pure | liftBind` works out of the box.

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 45 ----------------------
 1 file changed, 45 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
index 1ece08ee0..c2bd33aab 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -46,8 +46,6 @@ This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io)
 - `PFunctor.FreeM.lift`: Lift an object of the base polynomial functor into the free monad.
 - `PFunctor.FreeM.liftA`: Lift a position of the base polynomial functor into the free monad.
 - `PFunctor.FreeM.mapM`: Canonical mapping of `FreeM P` into any other monad.
-- `PFunctor.FreeM.inductionOn`: Induction principle for `FreeM P`.
-- `PFunctor.FreeM.construct`: Dependent eliminator for `FreeM P`.
 -/
 
 @[expose] public section
@@ -196,49 +194,6 @@ lemma pure_inj (a b : α) : (pure a : FreeM P α) = pure b ↔ a = b := by
     simp
   · simp [ha]
 
-/-- Proving a predicate `C` of `FreeM P α` requires two cases:
-* `pure a` for some `a : α`
-* `liftBind a cont h` for some `a : P.A`, `cont : P.B a → FreeM P α`,
-  and `h : ∀ y, C (cont y)` -/
-@[elab_as_elim]
-protected def inductionOn {C : FreeM P α → Prop}
-    (pure : ∀ a, C (pure a))
-    (liftBind : (a : P.A) → (cont : P.B a → FreeM P α) → (∀ y, C (cont y)) →
-      C (FreeM.liftBind a cont)) :
-    (x : FreeM P α) → C x
-  | FreeM.pure a => pure a
-  | FreeM.liftBind a cont =>
-    liftBind a _ (fun u ↦ FreeM.inductionOn pure liftBind (cont u))
-
-section construct
-
-/-- Dependent eliminator for `FreeM P`. -/
-@[elab_as_elim]
-protected def construct {C : FreeM P α → Type*}
-    (pure : (a : α) → C (pure a))
-    (liftBind : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
-      C (FreeM.liftBind a cont)) :
-    (x : FreeM P α) → C x
-  | .pure a => pure a
-  | .liftBind a cont =>
-    liftBind a _ (fun u ↦ FreeM.construct pure liftBind (cont u))
-
-variable {C : FreeM P α → Type*} (h_pure : (a : α) → C (pure a))
-  (h_liftBind : (a : P.A) → (cont : P.B a → FreeM P α) → ((y : P.B a) → C (cont y)) →
-    C (FreeM.liftBind a cont))
-
-@[simp]
-lemma construct_pure (a : α) :
-    FreeM.construct h_pure h_liftBind (pure a) = h_pure a := rfl
-
-@[simp]
-lemma construct_liftBind (a : P.A) (cont : P.B a → FreeM P α) :
-    (FreeM.construct h_pure h_liftBind (FreeM.liftBind a cont) :
-      C (FreeM.liftBind a cont)) =
-      (h_liftBind a cont (fun u => FreeM.construct h_pure h_liftBind (cont u))) := rfl
-
-end construct
-
 section mapM
 
 variable {m : Type uB → Type v} {α : Type uB}

From 5ee07e212b0b869be9eaafc4a1c4d782c012c389 Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 7 Apr 2026 23:38:43 -0400
Subject: [PATCH 07/10] refactor(Data/PFunctor/FreeM): rename mapM to liftM

Match the naming convention of Cslib.FreeM.liftM for the canonical
interpreter from the free monad into a target monad.

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 66 +++++++++++-----------
 1 file changed, 33 insertions(+), 33 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
index c2bd33aab..cea4e7e52 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -45,7 +45,7 @@ This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io)
 - `PFunctor.FreeM`: The free monad on a polynomial functor.
 - `PFunctor.FreeM.lift`: Lift an object of the base polynomial functor into the free monad.
 - `PFunctor.FreeM.liftA`: Lift a position of the base polynomial functor into the free monad.
-- `PFunctor.FreeM.mapM`: Canonical mapping of `FreeM P` into any other monad.
+- `PFunctor.FreeM.liftM`: Interpret `FreeM P` into any other monad.
 -/
 
 @[expose] public section
@@ -194,77 +194,77 @@ lemma pure_inj (a b : α) : (pure a : FreeM P α) = pure b ↔ a = b := by
     simp
   · simp [ha]
 
-section mapM
+section liftM
 
 variable {m : Type uB → Type v} {α : Type uB}
 
-/-- Canonical mapping of `FreeM P` into any other monad, given an interpretation
-`interp : (a : P.A) → m (P.B a)`. -/
-protected def mapM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : FreeM P α → m α
+/-- Interpret a `FreeM P` computation into any monad `m` by providing an interpretation
+`interp : (a : P.A) → m (P.B a)` for each operation. -/
+protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : FreeM P α → m α
   | .pure a => Pure.pure a
-  | .liftBind a cont => (interp a) >>= (fun u ↦ (cont u).mapM interp)
+  | .liftBind a cont => (interp a) >>= (fun u ↦ (cont u).liftM interp)
 
 variable [Monad m] (interp : (a : P.A) → m (P.B a))
 
 @[simp]
-lemma mapM_pure' (a : α) : (FreeM.pure a : FreeM P α).mapM interp = Pure.pure a := rfl
+lemma liftM_pure' (a : α) : (FreeM.pure a : FreeM P α).liftM interp = Pure.pure a := rfl
 
 @[simp]
-lemma mapM_liftBind (a : P.A) (cont : P.B a → FreeM P α) :
-    (FreeM.liftBind a cont).mapM interp = interp a >>= fun u => (cont u).mapM interp := rfl
+lemma liftM_liftBind (a : P.A) (cont : P.B a → FreeM P α) :
+    (FreeM.liftBind a cont).liftM interp = interp a >>= fun u => (cont u).liftM interp := rfl
 
 @[simp]
-lemma mapM_pure (a : α) : (Pure.pure a : FreeM P α).mapM interp = Pure.pure a := rfl
+lemma liftM_pure (a : α) : (Pure.pure a : FreeM P α).liftM interp = Pure.pure a := rfl
 
 variable [LawfulMonad m]
 
 @[simp]
-lemma mapM_bind {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
-    (x.bind f).mapM interp = x.mapM interp >>= fun u => (f u).mapM interp := by
+lemma liftM_bind {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
+    (x.bind f).liftM interp = x.liftM interp >>= fun u => (f u).liftM interp := by
   induction x with
-  | pure _ => simp [FreeM.bind, FreeM.mapM]
+  | pure _ => simp [FreeM.bind, FreeM.liftM]
   | liftBind a cont h => simp [h]
 
 @[simp]
-lemma mapM_bind' {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
-    (x >>= f).mapM interp = x.mapM interp >>= fun u => (f u).mapM interp :=
-  mapM_bind _ _ _
+lemma liftM_bind' {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
+    (x >>= f).liftM interp = x.liftM interp >>= fun u => (f u).liftM interp :=
+  liftM_bind _ _ _
 
 @[simp]
-lemma mapM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
-    FreeM.mapM interp (map f x) = f <$> FreeM.mapM interp x := by
+lemma liftM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
+    FreeM.liftM interp (map f x) = f <$> FreeM.liftM interp x := by
   induction x with
-  | pure _ => simp [map, FreeM.mapM]
+  | pure _ => simp [map, FreeM.liftM]
   | liftBind a cont h => simp [h]
 
 @[simp]
-lemma mapM_seq {α β : Type uB}
+lemma liftM_seq {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : FreeM P (α → β)) (y : FreeM P α) :
-    FreeM.mapM interp (x <*> y) = (FreeM.mapM interp x) <*> (FreeM.mapM interp y) := by
-  simp only [seq_eq_bind_map, mapM_bind', map_eq_map, mapM_map]
+    FreeM.liftM interp (x <*> y) = (FreeM.liftM interp x) <*> (FreeM.liftM interp y) := by
+  simp only [seq_eq_bind_map, liftM_bind', map_eq_map, liftM_map]
 
 @[simp]
-lemma mapM_seqLeft {α β : Type uB}
+lemma liftM_seqLeft {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : FreeM P α) (y : FreeM P β) :
-    FreeM.mapM interp (x <* y) = FreeM.mapM interp x <* FreeM.mapM interp y := by
-  simp only [seqLeft_eq_bind, mapM_bind', mapM_pure]
+    FreeM.liftM interp (x <* y) = FreeM.liftM interp x <* FreeM.liftM interp y := by
+  simp only [seqLeft_eq_bind, liftM_bind', liftM_pure]
 
 @[simp]
-lemma mapM_seqRight {α β : Type uB}
+lemma liftM_seqRight {α β : Type uB}
     (interp : (a : P.A) → m (P.B a)) (x : FreeM P α) (y : FreeM P β) :
-    FreeM.mapM interp (x *> y) = FreeM.mapM interp x *> FreeM.mapM interp y := by
-  simp only [seqRight_eq_bind, mapM_bind']
+    FreeM.liftM interp (x *> y) = FreeM.liftM interp x *> FreeM.liftM interp y := by
+  simp only [seqRight_eq_bind, liftM_bind']
 
 @[simp]
-lemma mapM_lift (interp : (a : P.A) → m (P.B a)) (x : P.Obj α) :
-    FreeM.mapM interp (FreeM.lift x) = x.2 <$> interp x.1 := by
+lemma liftM_lift (interp : (a : P.A) → m (P.B a)) (x : P.Obj α) :
+    FreeM.liftM interp (FreeM.lift x) = x.2 <$> interp x.1 := by
   simp [lift]
 
 @[simp]
-lemma mapM_liftA (interp : (a : P.A) → m (P.B a)) (a : P.A) :
-    FreeM.mapM interp (FreeM.liftA a) = interp a := by simp [liftA]
+lemma liftM_liftA (interp : (a : P.A) → m (P.B a)) (a : P.A) :
+    FreeM.liftM interp (FreeM.liftA a) = interp a := by simp [liftA]
 
-end mapM
+end liftM
 
 end FreeM
 

From 23a1c29e1668933e9a026027b02f01d7fd75c325 Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Mon, 13 Apr 2026 09:01:50 -0600
Subject: [PATCH 08/10] docs(Data/PFunctor/FreeM): clarify comparison with
 Cslib.FreeM

Address review comments: replace ambiguous "hidden" and "single" wording.

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/FreeM.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/FreeM.lean
index cea4e7e52..263a3fa34 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/FreeM.lean
@@ -20,12 +20,13 @@ constructor, yielding a monad that is free over the polynomial functor `P`.
 ## Comparison with `Cslib.FreeM`
 
 `Cslib.FreeM F` (in `Cslib.Foundations.Control.Monad.Free`) builds a free monad over an
-arbitrary type constructor `F : Type u → Type v`, using a single `liftBind` constructor that
-existentially quantifies the intermediate type:
+arbitrary type constructor `F : Type u → Type v`.
+Its `liftBind` constructor existentially quantifies the intermediate type:
 ```
 | liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : FreeM F α
 ```
-Here the intermediate type `ι` is hidden, so `F` need not be a `Functor`.
+Because `ι` is an implicit (existentially bound) argument, the caller need not name it,
+so `F` need not be a `Functor`.
 
 `PFunctor.FreeM P` instead takes a polynomial functor `P : PFunctor`, where the shapes
 `P.A` and children `P.B a` are given explicitly.

From 45fe23e8b80ba3b97e7a988b92301fbea8ca10c9 Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 14 Apr 2026 17:20:59 -0600
Subject: [PATCH 09/10] refactor(Data/PFunctor/FreeM): address PR review
 comments

- Rename FreeM.lean to Free.lean
- Use P.FreeM dot notation throughout
- Use Type* instead of Type v in variable declaration
- Rework docstring comparison with Cslib.FreeM

Made-with: Cursor
---
 Cslib.lean                                    |  2 +-
 .../Data/PFunctor/{FreeM.lean => Free.lean}   | 88 +++++++++----------
 2 files changed, 44 insertions(+), 46 deletions(-)
 rename Cslib/Foundations/Data/PFunctor/{FreeM.lean => Free.lean} (71%)

diff --git a/Cslib.lean b/Cslib.lean
index 494c95506..76e8a7dc6 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -42,7 +42,7 @@ public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
 public import Cslib.Foundations.Data.FinFun
-public import Cslib.Foundations.Data.PFunctor.FreeM
+public import Cslib.Foundations.Data.PFunctor.Free
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
diff --git a/Cslib/Foundations/Data/PFunctor/FreeM.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
similarity index 71%
rename from Cslib/Foundations/Data/PFunctor/FreeM.lean
rename to Cslib/Foundations/Data/PFunctor/Free.lean
index 263a3fa34..50d20d591 100644
--- a/Cslib/Foundations/Data/PFunctor/FreeM.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -20,19 +20,17 @@ constructor, yielding a monad that is free over the polynomial functor `P`.
 ## Comparison with `Cslib.FreeM`
 
 `Cslib.FreeM F` (in `Cslib.Foundations.Control.Monad.Free`) builds a free monad over an
-arbitrary type constructor `F : Type u → Type v`.
+arbitrary type constructor `F : Type u → Type v`, which need not be functorial.
 Its `liftBind` constructor existentially quantifies the intermediate type:
 ```
 | liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : FreeM F α
 ```
-Because `ι` is an implicit (existentially bound) argument, the caller need not name it,
-so `F` need not be a `Functor`.
 
 `PFunctor.FreeM P` instead takes a polynomial functor `P : PFunctor`, where the shapes
 `P.A` and children `P.B a` are given explicitly.
 Its `liftBind` constructor carries the shape and continuation without existential quantification:
 ```
-| liftBind (a : P.A) (cont : P.B a → FreeM P α) : FreeM P α
+| liftBind (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α
 ```
 
 When the effect signature is naturally polynomial (a fixed set of operations, each with a
@@ -59,43 +57,43 @@ namespace PFunctor
 This extends the `W`-type construction with an extra `pure` constructor. -/
 inductive FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)
   /-- A leaf node wrapping a pure value. -/
-  | protected pure {α} (a : α) : FreeM P α
-  /-- Invoke the operation `a : P.A` with continuation `cont : P.B a → FreeM P α`. -/
-  | liftBind {α} (a : P.A) (cont : P.B a → FreeM P α) : FreeM P α
+  | protected pure {α} (a : α) : P.FreeM α
+  /-- Invoke the operation `a : P.A` with continuation `cont : P.B a → P.FreeM α`. -/
+  | liftBind {α} (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α
 deriving Inhabited
 
 namespace FreeM
 
-variable {P : PFunctor.{uA, uB}} {α β γ : Type v}
+variable {P : PFunctor.{uA, uB}} {α β γ : Type*}
 
-instance : Pure (FreeM P) where pure := .pure
+instance : Pure (P.FreeM) where pure := .pure
 
 @[simp]
-theorem pure_eq_pure : (FreeM.pure : α → FreeM P α) = pure := rfl
+theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl
 
 /-- Lift an object of the base polynomial functor into the free monad. -/
-def lift (x : P.Obj α) : FreeM P α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y))
+def lift (x : P.Obj α) : P.FreeM α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y))
 
 /-- Lift a position of the base polynomial functor into the free monad. -/
-def liftA (a : P.A) : FreeM P (P.B a) := lift ⟨a, id⟩
+def liftA (a : P.A) : P.FreeM (P.B a) := lift ⟨a, id⟩
 
-instance : MonadLift P (FreeM P) where
+instance : MonadLift P (P.FreeM) where
   monadLift x := FreeM.lift x
 
 @[simp] lemma lift_ne_pure (x : P α) (y : α) :
-    (lift x : FreeM P α) ≠ PFunctor.FreeM.pure y := by simp [lift]
+    (lift x : P.FreeM α) ≠ PFunctor.FreeM.pure y := by simp [lift]
 
 @[simp] lemma pure_ne_lift (x : P α) (y : α) :
-    PFunctor.FreeM.pure y ≠ (lift x : FreeM P α) := by simp [lift]
+    PFunctor.FreeM.pure y ≠ (lift x : P.FreeM α) := by simp [lift]
 
-lemma monadLift_eq_lift (x : P.Obj α) : (x : FreeM P α) = FreeM.lift x := rfl
+lemma monadLift_eq_lift (x : P.Obj α) : (x : P.FreeM α) = FreeM.lift x := rfl
 
 /-- Bind operator on `FreeM P` used in the monad definition. -/
-protected def bind : FreeM P α → (α → FreeM P β) → FreeM P β
+protected def bind : P.FreeM α → (α → P.FreeM β) → P.FreeM β
   | FreeM.pure a, f => f a
   | FreeM.liftBind a cont, f => FreeM.liftBind a (fun u ↦ FreeM.bind (cont u) f)
 
-protected theorem bind_assoc (x : FreeM P α) (f : α → FreeM P β) (g : β → FreeM P γ) :
+protected theorem bind_assoc (x : P.FreeM α) (f : α → P.FreeM β) (g : β → P.FreeM γ) :
     (x.bind f).bind g = x.bind (fun a => (f a).bind g) := by
   induction x with
   | pure a => rfl
@@ -103,29 +101,29 @@ protected theorem bind_assoc (x : FreeM P α) (f : α → FreeM P β) (g : β 
     simp [FreeM.bind] at *
     simp [ih]
 
-instance : Bind (FreeM P) where bind := .bind
+instance : Bind (P.FreeM) where bind := .bind
 
 @[simp]
 theorem bind_eq_bind {α β : Type v} :
-    Bind.bind = (FreeM.bind : FreeM P α → _ → FreeM P β) := rfl
+    Bind.bind = (FreeM.bind : P.FreeM α → _ → P.FreeM β) := rfl
 
 /-- Map a function over a `FreeM` computation. -/
 @[simp]
-def map (f : α → β) : FreeM P α → FreeM P β
+def map (f : α → β) : P.FreeM α → P.FreeM β
   | .pure a => .pure (f a)
   | .liftBind a cont => .liftBind a fun u => FreeM.map f (cont u)
 
 @[simp]
-theorem id_map : ∀ x : FreeM P α, map id x = x
+theorem id_map : ∀ x : P.FreeM α, map id x = x
   | .pure a => rfl
   | .liftBind a cont => by simp_all [map, id_map]
 
 theorem comp_map (h : β → γ) (g : α → β) :
-    ∀ x : FreeM P α, map (h ∘ g) x = map h (map g x)
+    ∀ x : P.FreeM α, map (h ∘ g) x = map h (map g x)
   | .pure a => rfl
   | .liftBind a cont => by simp_all [map, comp_map]
 
-instance : Functor (FreeM P) where
+instance : Functor (P.FreeM) where
   map := .map
 
 @[simp]
@@ -134,54 +132,54 @@ theorem map_eq_map {α β : Type v} :
 
 /-- `.pure a` followed by `bind` collapses immediately. -/
 @[simp]
-lemma pure_bind (a : α) (f : α → FreeM P β) :
+lemma pure_bind (a : α) (f : α → P.FreeM β) :
     (FreeM.pure a).bind f = f a := rfl
 
 @[simp]
-lemma bind_pure : ∀ x : FreeM P α, x.bind pure = x
+lemma bind_pure : ∀ x : P.FreeM α, x.bind pure = x
   | .pure a => rfl
   | .liftBind a cont => by
     simp only [FreeM.bind]; congr 1; funext u; exact bind_pure (cont u)
 
 @[simp]
-lemma bind_pure_comp (f : α → β) : ∀ x : FreeM P α, x.bind (pure ∘ f) = map f x
+lemma bind_pure_comp (f : α → β) : ∀ x : P.FreeM α, x.bind (pure ∘ f) = map f x
   | .pure a => rfl
   | .liftBind a cont => by simp only [FreeM.bind, map, bind_pure_comp]
 
 @[simp]
-lemma liftBind_bind (a : P.A) (cont : P.B a → FreeM P β) (f : β → FreeM P γ) :
+lemma liftBind_bind (a : P.A) (cont : P.B a → P.FreeM β) (f : β → P.FreeM γ) :
     (FreeM.liftBind a cont).bind f = FreeM.liftBind a (fun u ↦ (cont u).bind f) := rfl
 
 @[simp]
-lemma lift_bind (x : P.Obj α) (f : α → FreeM P β) :
+lemma lift_bind (x : P.Obj α) (f : α → P.FreeM β) :
     (FreeM.lift x).bind f = FreeM.liftBind x.1 (fun a ↦ f (x.2 a)) := rfl
 
-@[simp] lemma bind_eq_pure_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
+@[simp] lemma bind_eq_pure_iff (x : P.FreeM α) (f : α → P.FreeM β) (b : β) :
     x.bind f = pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by
   cases x with
   | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by rwa [FreeM.pure.inj h]⟩
   | liftBind a cont => simp [FreeM.bind]
 
-@[simp] lemma pure_eq_bind_iff (x : FreeM P α) (f : α → FreeM P β) (b : β) :
+@[simp] lemma pure_eq_bind_iff (x : P.FreeM α) (f : α → P.FreeM β) (b : β) :
     pure b = x.bind f ↔ ∃ a, x = pure a ∧ pure b = f a := by
   cases x with
   | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by rwa [FreeM.pure.inj h]⟩
   | liftBind a cont => simp [FreeM.bind]
 
-instance : LawfulFunctor (FreeM P) where
+instance : LawfulFunctor (P.FreeM) where
   map_const := rfl
   id_map := id_map
   comp_map _ _ := comp_map _ _
 
-instance : Monad (FreeM P) where
+instance : Monad (P.FreeM) where
 
-instance : LawfulMonad (FreeM P) := LawfulMonad.mk'
+instance : LawfulMonad (P.FreeM) := LawfulMonad.mk'
   (bind_pure_comp := bind_pure_comp)
   (id_map := id_map)
   (pure_bind := pure_bind)
   (bind_assoc := FreeM.bind_assoc)
 
-lemma pure_inj (a b : α) : (pure a : FreeM P α) = pure b ↔ a = b := by
+lemma pure_inj (a b : α) : (pure a : P.FreeM α) = pure b ↔ a = b := by
   constructor
   · exact FreeM.pure.inj
   · rintro rfl; rfl
@@ -201,38 +199,38 @@ variable {m : Type uB → Type v} {α : Type uB}
 
 /-- Interpret a `FreeM P` computation into any monad `m` by providing an interpretation
 `interp : (a : P.A) → m (P.B a)` for each operation. -/
-protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : FreeM P α → m α
+protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.FreeM α → m α
   | .pure a => Pure.pure a
   | .liftBind a cont => (interp a) >>= (fun u ↦ (cont u).liftM interp)
 
 variable [Monad m] (interp : (a : P.A) → m (P.B a))
 
 @[simp]
-lemma liftM_pure' (a : α) : (FreeM.pure a : FreeM P α).liftM interp = Pure.pure a := rfl
+lemma liftM_pure' (a : α) : (FreeM.pure a : P.FreeM α).liftM interp = Pure.pure a := rfl
 
 @[simp]
-lemma liftM_liftBind (a : P.A) (cont : P.B a → FreeM P α) :
+lemma liftM_liftBind (a : P.A) (cont : P.B a → P.FreeM α) :
     (FreeM.liftBind a cont).liftM interp = interp a >>= fun u => (cont u).liftM interp := rfl
 
 @[simp]
-lemma liftM_pure (a : α) : (Pure.pure a : FreeM P α).liftM interp = Pure.pure a := rfl
+lemma liftM_pure (a : α) : (Pure.pure a : P.FreeM α).liftM interp = Pure.pure a := rfl
 
 variable [LawfulMonad m]
 
 @[simp]
-lemma liftM_bind {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
+lemma liftM_bind {α β : Type uB} (x : P.FreeM α) (f : α → P.FreeM β) :
     (x.bind f).liftM interp = x.liftM interp >>= fun u => (f u).liftM interp := by
   induction x with
   | pure _ => simp [FreeM.bind, FreeM.liftM]
   | liftBind a cont h => simp [h]
 
 @[simp]
-lemma liftM_bind' {α β : Type uB} (x : FreeM P α) (f : α → FreeM P β) :
+lemma liftM_bind' {α β : Type uB} (x : P.FreeM α) (f : α → P.FreeM β) :
     (x >>= f).liftM interp = x.liftM interp >>= fun u => (f u).liftM interp :=
   liftM_bind _ _ _
 
 @[simp]
-lemma liftM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
+lemma liftM_map {α β : Type uB} (x : P.FreeM α) (f : α → β) :
     FreeM.liftM interp (map f x) = f <$> FreeM.liftM interp x := by
   induction x with
   | pure _ => simp [map, FreeM.liftM]
@@ -240,19 +238,19 @@ lemma liftM_map {α β : Type uB} (x : FreeM P α) (f : α → β) :
 
 @[simp]
 lemma liftM_seq {α β : Type uB}
-    (interp : (a : P.A) → m (P.B a)) (x : FreeM P (α → β)) (y : FreeM P α) :
+    (interp : (a : P.A) → m (P.B a)) (x : P.FreeM (α → β)) (y : P.FreeM α) :
     FreeM.liftM interp (x <*> y) = (FreeM.liftM interp x) <*> (FreeM.liftM interp y) := by
   simp only [seq_eq_bind_map, liftM_bind', map_eq_map, liftM_map]
 
 @[simp]
 lemma liftM_seqLeft {α β : Type uB}
-    (interp : (a : P.A) → m (P.B a)) (x : FreeM P α) (y : FreeM P β) :
+    (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) :
     FreeM.liftM interp (x <* y) = FreeM.liftM interp x <* FreeM.liftM interp y := by
   simp only [seqLeft_eq_bind, liftM_bind', liftM_pure]
 
 @[simp]
 lemma liftM_seqRight {α β : Type uB}
-    (interp : (a : P.A) → m (P.B a)) (x : FreeM P α) (y : FreeM P β) :
+    (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) (y : P.FreeM β) :
     FreeM.liftM interp (x *> y) = FreeM.liftM interp x *> FreeM.liftM interp y := by
   simp only [seqRight_eq_bind, liftM_bind']
 

From d38d3045661c5d5de5288d4d6ec91ba2adf0bd47 Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Tue, 14 Apr 2026 17:23:04 -0600
Subject: [PATCH 10/10] docs(Data/PFunctor/Free): clarify docstring terminology

Replace "existentially quantifies" / "existentially-bound" with
clearer phrasing per review feedback.

Made-with: Cursor
---
 Cslib/Foundations/Data/PFunctor/Free.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean
index 50d20d591..3e220d165 100644
--- a/Cslib/Foundations/Data/PFunctor/Free.lean
+++ b/Cslib/Foundations/Data/PFunctor/Free.lean
@@ -21,21 +21,21 @@ constructor, yielding a monad that is free over the polynomial functor `P`.
 
 `Cslib.FreeM F` (in `Cslib.Foundations.Control.Monad.Free`) builds a free monad over an
 arbitrary type constructor `F : Type u → Type v`, which need not be functorial.
-Its `liftBind` constructor existentially quantifies the intermediate type:
+Its `liftBind` constructor abstracts over the intermediate type `ι`:
 ```
 | liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : FreeM F α
 ```
 
 `PFunctor.FreeM P` instead takes a polynomial functor `P : PFunctor`, where the shapes
-`P.A` and children `P.B a` are given explicitly.
-Its `liftBind` constructor carries the shape and continuation without existential quantification:
+`P.A` and positions `P.B a` are given explicitly.
+Its `liftBind` constructor uses the shape and continuation directly:
 ```
 | liftBind (a : P.A) (cont : P.B a → P.FreeM α) : P.FreeM α
 ```
 
 When the effect signature is naturally polynomial (a fixed set of operations, each with a
 known return type), `PFunctor.FreeM` gives stronger eliminators and avoids the universe
-bump that the existential in `Cslib.FreeM` introduces.
+bump that the abstract `ι` in `Cslib.FreeM` introduces.
 
 This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io) library.