From 2024bc58a538224e051ae741cdeadcc657bd8d6b Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Tue, 7 Apr 2026 14:52:47 -0400 Subject: [PATCH 01/14] 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 Date: Tue, 7 Apr 2026 18:29:38 -0400 Subject: [PATCH 02/14] 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 Date: Tue, 7 Apr 2026 22:55:22 -0400 Subject: [PATCH 03/14] 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 Date: Tue, 7 Apr 2026 23:03:18 -0400 Subject: [PATCH 04/14] 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 Date: Tue, 7 Apr 2026 23:05:12 -0400 Subject: [PATCH 05/14] 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 Date: Tue, 7 Apr 2026 23:37:38 -0400 Subject: [PATCH 06/14] 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 Date: Tue, 7 Apr 2026 23:38:43 -0400 Subject: [PATCH 07/14] 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 Date: Mon, 13 Apr 2026 09:01:50 -0600 Subject: [PATCH 08/14] 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 Date: Tue, 14 Apr 2026 17:20:59 -0600 Subject: [PATCH 09/14] 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 Date: Tue, 14 Apr 2026 17:23:04 -0600 Subject: [PATCH 10/14] 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. From 2e74c08121bf3f4e37ab7224d017c88893cb2071 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sat, 23 May 2026 21:12:27 +0700 Subject: [PATCH 11/14] fix(pfunctor): address free monad review Align PFunctor.FreeM with the existing FreeM constructor normal form, add the matching Interprets API, and document the relation from the general free monad file. Co-authored-by: Cursor --- Cslib/Foundations/Control/Monad/Free.lean | 2 + Cslib/Foundations/Data/PFunctor/Free.lean | 83 ++++++++++++++++------- 2 files changed, 59 insertions(+), 26 deletions(-) diff --git a/Cslib/Foundations/Control/Monad/Free.lean b/Cslib/Foundations/Control/Monad/Free.lean index 0fe080521..e0d362d11 100644 --- a/Cslib/Foundations/Control/Monad/Free.lean +++ b/Cslib/Foundations/Control/Monad/Free.lean @@ -39,6 +39,8 @@ This unique interpreter is `FreeM.liftM f` - `FreeM.liftM_unique`: Proof of the universal property For elimination and interpretation theory, see `Free/Fold.lean`. +For polynomial effect signatures with explicit operation shapes and positions, see +`Cslib.Foundations.Data.PFunctor.Free`. See the Haskell [freer-simple](https://hackage.haskell.org/package/freer-simple) library for the Haskell implementation that inspired this approach. diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index 3e220d165..89aa07b87 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -69,7 +69,7 @@ variable {P : PFunctor.{uA, uB}} {α β γ : Type*} instance : Pure (P.FreeM) where pure := .pure @[simp] -theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl +theorem pure_eq_pure : (pure : α → P.FreeM α) = FreeM.pure := rfl /-- Lift an object of the base polynomial functor into the free monad. -/ def lift (x : P.Obj α) : P.FreeM α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y)) @@ -80,10 +80,10 @@ def liftA (a : P.A) : P.FreeM (P.B a) := lift ⟨a, id⟩ instance : MonadLift P (P.FreeM) where monadLift x := FreeM.lift x -@[simp] lemma lift_ne_pure (x : P α) (y : α) : +@[simp] lemma lift_ne_pure (x : P.Obj α) (y : α) : (lift x : P.FreeM α) ≠ PFunctor.FreeM.pure y := by simp [lift] -@[simp] lemma pure_ne_lift (x : P α) (y : α) : +@[simp] lemma pure_ne_lift (x : P.Obj α) (y : α) : PFunctor.FreeM.pure y ≠ (lift x : P.FreeM α) := by simp [lift] lemma monadLift_eq_lift (x : P.Obj α) : (x : P.FreeM α) = FreeM.lift x := rfl @@ -133,16 +133,16 @@ theorem map_eq_map {α β : Type v} : /-- `.pure a` followed by `bind` collapses immediately. -/ @[simp] lemma pure_bind (a : α) (f : α → P.FreeM β) : - (FreeM.pure a).bind f = f a := rfl + (.pure a : P.FreeM α).bind f = f a := rfl @[simp] -lemma bind_pure : ∀ x : P.FreeM α, x.bind pure = x +lemma bind_pure : ∀ x : P.FreeM α, x.bind FreeM.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 : P.FreeM α, x.bind (pure ∘ f) = map f x +lemma bind_pure_comp (f : α → β) : ∀ x : P.FreeM α, x.bind (FreeM.pure ∘ f) = map f x | .pure a => rfl | .liftBind a cont => by simp only [FreeM.bind, map, bind_pure_comp] @@ -155,13 +155,13 @@ 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 : P.FreeM α) (f : α → P.FreeM β) (b : β) : - x.bind f = pure b ↔ ∃ a, x = pure a ∧ f a = pure b := by + 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 : P.FreeM α) (f : α → P.FreeM β) (b : β) : - pure b = x.bind f ↔ ∃ a, x = pure a ∧ pure b = f a := by + .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] @@ -179,19 +179,20 @@ instance : LawfulMonad (P.FreeM) := LawfulMonad.mk' (pure_bind := pure_bind) (bind_assoc := FreeM.bind_assoc) -lemma pure_inj (a b : α) : (pure a : P.FreeM α) = 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 -@[simp] lemma liftBind_inj (a a' : P.A) +lemma liftBind_inj (a a' : P.A) (cont : P.B a → P.FreeM α) (cont' : P.B a' → P.FreeM α) : FreeM.liftBind a cont = FreeM.liftBind a' cont' ↔ ∃ h : a = a', h ▸ cont = cont' := by - simp - by_cases ha : a = a' - · cases ha - simp - · simp [ha] + constructor + · intro h + obtain ⟨rfl, hcont⟩ := FreeM.liftBind.inj h + exact ⟨rfl, eq_of_heq hcont⟩ + · rintro ⟨rfl, rfl⟩ + rfl section liftM @@ -206,14 +207,49 @@ protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.Fre variable [Monad m] (interp : (a : P.A) → m (P.B a)) @[simp] -lemma liftM_pure' (a : α) : (FreeM.pure a : P.FreeM α).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 → 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 : P.FreeM α).liftM interp = Pure.pure a := rfl +/-- +A predicate stating that `eval : P.FreeM α → m α` is an interpreter for the polynomial +effect handler `handler : (a : P.A) → m (P.B a)`. + +This means that `eval` is a monad morphism from the free monad `P.FreeM` to the +monad `m`, and that it extends the interpretation of individual operations given by +`handler`. +-/ +structure Interprets (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α → m α) : Prop where + apply_pure (a : α) : eval (.pure a) = pure a + apply_liftBind (a : P.A) (cont : P.B a → P.FreeM α) : + eval (FreeM.liftBind a cont) = handler a >>= fun x => eval (cont x) + +theorem Interprets.eq {handler : (a : P.A) → m (P.B a)} {eval : P.FreeM α → m α} + (h : Interprets handler eval) : + eval = (·.liftM handler) := by + ext x + induction x with + | pure a => exact h.apply_pure a + | liftBind a cont ih => + rw [liftM_liftBind, h.apply_liftBind] + simp [ih] + +theorem Interprets.liftM (handler : (a : P.A) → m (P.B a)) : + Interprets handler (·.liftM handler : P.FreeM α → _) where + apply_pure _ := rfl + apply_liftBind _ _ := rfl + +/-- +The universal property of the free monad `P.FreeM`. + +That is, `liftM handler` is the unique interpreter that extends the effect handler `handler` to +interpret `P.FreeM` computations in a monad `m`. +-/ +theorem Interprets.iff (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α → m α) : + Interprets handler eval ↔ eval = (·.liftM handler) := + ⟨(·.eq), fun h => h ▸ Interprets.liftM _⟩ variable [LawfulMonad m] @@ -224,11 +260,6 @@ lemma liftM_bind {α β : Type uB} (x : P.FreeM α) (f : α → P.FreeM β) : | pure _ => simp [FreeM.bind, FreeM.liftM] | liftBind a cont h => simp [h] -@[simp] -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 : P.FreeM α) (f : α → β) : FreeM.liftM interp (map f x) = f <$> FreeM.liftM interp x := by @@ -240,19 +271,19 @@ lemma liftM_map {α β : Type uB} (x : P.FreeM α) (f : α → β) : lemma liftM_seq {α β : Type uB} (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 only [seq_eq_bind_map, bind_eq_bind, liftM_bind, map_eq_map, liftM_map] @[simp] lemma liftM_seqLeft {α β : Type uB} (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 only [seqLeft_eq_bind, bind_eq_bind, liftM_bind, pure_eq_pure, liftM_pure] @[simp] lemma liftM_seqRight {α β : Type uB} (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'] + simp only [seqRight_eq_bind, bind_eq_bind, liftM_bind] @[simp] lemma liftM_lift (interp : (a : P.A) → m (P.B a)) (x : P.Obj α) : From 9dfc0337056b9354e502c4883962d41fd6d3c3c2 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Sun, 24 May 2026 04:37:52 +0700 Subject: [PATCH 12/14] fix(pfunctor): restore pure simp direction Restore the FreeM.pure-to-pure simp normal form requested for alignment with PR #417, and keep the surrounding simp lemmas in that normal form. Co-authored-by: Cursor --- Cslib/Foundations/Data/PFunctor/Free.lean | 26 +++++++++++++---------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index 89aa07b87..36f292708 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -69,7 +69,10 @@ variable {P : PFunctor.{uA, uB}} {α β γ : Type*} instance : Pure (P.FreeM) where pure := .pure @[simp] -theorem pure_eq_pure : (pure : α → P.FreeM α) = FreeM.pure := rfl +theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl + +attribute [-simp] FreeM.pure.injEq FreeM.pure.sizeOf_spec +attribute [nolint simpNF] FreeM.pure.injEq FreeM.pure.sizeOf_spec /-- Lift an object of the base polynomial functor into the free monad. -/ def lift (x : P.Obj α) : P.FreeM α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y)) @@ -81,10 +84,10 @@ instance : MonadLift P (P.FreeM) where monadLift x := FreeM.lift x @[simp] lemma lift_ne_pure (x : P.Obj α) (y : α) : - (lift x : P.FreeM α) ≠ PFunctor.FreeM.pure y := by simp [lift] + (lift x : P.FreeM α) ≠ pure y := by simp [lift] @[simp] lemma pure_ne_lift (x : P.Obj α) (y : α) : - PFunctor.FreeM.pure y ≠ (lift x : P.FreeM α) := by simp [lift] + pure y ≠ (lift x : P.FreeM α) := by simp [lift] lemma monadLift_eq_lift (x : P.Obj α) : (x : P.FreeM α) = FreeM.lift x := rfl @@ -133,16 +136,16 @@ theorem map_eq_map {α β : Type v} : /-- `.pure a` followed by `bind` collapses immediately. -/ @[simp] lemma pure_bind (a : α) (f : α → P.FreeM β) : - (.pure a : P.FreeM α).bind f = f a := rfl + (pure a : P.FreeM α).bind f = f a := rfl @[simp] -lemma bind_pure : ∀ x : P.FreeM α, x.bind FreeM.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 : P.FreeM α, x.bind (FreeM.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] @@ -155,13 +158,13 @@ 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 : P.FreeM α) (f : α → P.FreeM β) (b : β) : - x.bind f = .pure b ↔ ∃ a, x = .pure a ∧ f a = .pure b := by + 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 : P.FreeM α) (f : α → P.FreeM β) (b : β) : - .pure b = x.bind f ↔ ∃ a, x = .pure a ∧ .pure b = f a := by + 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] @@ -179,7 +182,8 @@ instance : LawfulMonad (P.FreeM) := LawfulMonad.mk' (pure_bind := pure_bind) (bind_assoc := FreeM.bind_assoc) -lemma pure_inj (a b : α) : (.pure a : P.FreeM α) = .pure b ↔ a = b := by +@[simp] +lemma pure_inj (a b : α) : (pure a : P.FreeM α) = pure b ↔ a = b := by constructor · exact FreeM.pure.inj · rintro rfl; rfl @@ -207,7 +211,7 @@ protected def liftM [Pure m] [Bind m] (interp : (a : P.A) → m (P.B a)) : P.Fre variable [Monad m] (interp : (a : P.A) → m (P.B a)) @[simp] -lemma liftM_pure (a : α) : (FreeM.pure a : P.FreeM α).liftM interp = Pure.pure a := rfl +lemma liftM_pure (a : α) : (Pure.pure a : P.FreeM α).liftM interp = Pure.pure a := rfl @[simp] lemma liftM_liftBind (a : P.A) (cont : P.B a → P.FreeM α) : @@ -277,7 +281,7 @@ lemma liftM_seq {α β : Type uB} lemma liftM_seqLeft {α β : Type uB} (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, bind_eq_bind, liftM_bind, pure_eq_pure, liftM_pure] + simp only [seqLeft_eq_bind, bind_eq_bind, liftM_bind, liftM_pure] @[simp] lemma liftM_seqRight {α β : Type uB} From 15102623006d47314dc161459a418c2619acebcc Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 28 May 2026 12:17:39 +0700 Subject: [PATCH 13/14] fix(pfunctor): address FreeM review comments --- Cslib/Foundations/Data/PFunctor/Free.lean | 196 ++++++++++++++-------- 1 file changed, 127 insertions(+), 69 deletions(-) diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index 36f292708..01c5aa026 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -19,7 +19,7 @@ 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 +`Cslib.FreeM F` (in `Cslib/Foundations/Control/Monad/Free.lean`) builds a free monad over an arbitrary type constructor `F : Type u → Type v`, which need not be functorial. Its `liftBind` constructor abstracts over the intermediate type `ι`: ``` @@ -34,8 +34,10 @@ Its `liftBind` constructor uses the shape and continuation directly: ``` 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 abstract `ι` in `Cslib.FreeM` introduces. +known return type), `PFunctor.FreeM` avoids the universe bump that the abstract `ι` in +`Cslib.FreeM` introduces. Its eliminators also expose the shape `a : P.A` and the +fiber `P.B a` directly in the recursive case, rather than hiding them behind an +arbitrary intermediate type `ι`. This construction is ported from the [VCV-io](https://github.com/dtumad/VCV-io) library. @@ -53,6 +55,9 @@ universe u v uA uB namespace PFunctor +-- Disable generation of unneeded lemmas which the simpNF linter would complain about. +set_option genInjectivity false in +set_option genSizeOfSpec false in /-- 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) @@ -71,14 +76,11 @@ instance : Pure (P.FreeM) where pure := .pure @[simp] theorem pure_eq_pure : (FreeM.pure : α → P.FreeM α) = pure := rfl -attribute [-simp] FreeM.pure.injEq FreeM.pure.sizeOf_spec -attribute [nolint simpNF] FreeM.pure.injEq FreeM.pure.sizeOf_spec - /-- Lift an object of the base polynomial functor into the free monad. -/ 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) : P.FreeM (P.B a) := lift ⟨a, id⟩ +abbrev liftA (a : P.A) : P.FreeM (P.B a) := lift ⟨a, id⟩ instance : MonadLift P (P.FreeM) where monadLift x := FreeM.lift x @@ -91,47 +93,56 @@ instance : MonadLift P (P.FreeM) where lemma monadLift_eq_lift (x : P.Obj α) : (x : P.FreeM α) = FreeM.lift x := rfl -/-- Bind operator on `FreeM P` used in the monad definition. -/ +/-- Bind operation for the `FreeM` monad. + +The builtin `>>=` notation should be preferred when `α` and `β` are in the same universe. -/ 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 : 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 - | liftBind a cont ih => - simp [FreeM.bind] at * - simp [ih] - instance : Bind (P.FreeM) where bind := .bind +/-- Note that this lemma does not always apply, as it is universe-constrained by `Bind.bind`. -/ @[simp] theorem bind_eq_bind {α β : Type v} : - Bind.bind = (FreeM.bind : P.FreeM α → _ → P.FreeM β) := rfl + (FreeM.bind : P.FreeM α → _ → P.FreeM β) = Bind.bind := rfl -/-- Map a function over a `FreeM` computation. -/ -@[simp] +/-- Map a function over a `FreeM` computation. + +The builtin `<$>` notation should be preferred when `α` and `β` are in the same universe. -/ 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 : P.FreeM α, map id x = x - | .pure a => rfl - | .liftBind a cont => by simp_all [map, id_map] - -theorem comp_map (h : β → γ) (g : α → β) : - ∀ 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 (P.FreeM) where map := .map +/-- Note that this lemma does not always apply, as it is universe-constrained by `Functor.map`. -/ @[simp] theorem map_eq_map {α β : Type v} : - Functor.map = FreeM.map (P := P) (α := α) (β := β) := rfl + FreeM.map (P := P) (α := α) (β := β) = Functor.map := rfl + +@[simp] +lemma liftBind_eq (a : P.A) (cont : P.B a → P.FreeM α) : + FreeM.liftBind a cont = (FreeM.liftA a).bind cont := rfl + +set_option linter.unusedVariables false in +/-- An override for the default induction principle that is in simp-normal form. + +Note that when `α` and `P.B a` are in the same universe, this simplifies slightly further. -/ +@[induction_eliminator] +protected theorem induction {motive : P.FreeM α → Prop} + (pure : ∀ a, motive (pure a)) + (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (ih : ∀ i, motive (cont i)), + motive ((FreeM.liftA a).bind cont)) : ∀ x, motive x + | .pure a => pure a + | liftBind a cont => lift_bind a cont fun u => FreeM.induction pure lift_bind (cont u) + +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 + | lift_bind a cont ih => simp [← liftBind_eq, FreeM.bind, ih] at * /-- `.pure a` followed by `bind` collapses immediately. -/ @[simp] @@ -160,22 +171,57 @@ lemma lift_bind (x : P.Obj α) (f : α → P.FreeM β) : @[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] + | pure a => + constructor + · intro h + exact ⟨a, rfl, h⟩ + · rintro ⟨_, h, hf⟩ + cases h + exact hf + | liftBind a cont => + constructor + · intro h + cases h + · rintro ⟨_, h, _⟩ + cases h @[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 (P.FreeM) where - map_const := rfl - id_map := id_map - comp_map _ _ := comp_map _ _ + | pure a => + constructor + · intro h + exact ⟨a, rfl, h⟩ + · rintro ⟨_, h, hf⟩ + cases h + exact hf + | liftBind a cont => + constructor + · intro h + cases h + · rintro ⟨_, h, _⟩ + cases h instance : Monad (P.FreeM) where +@[simp] +theorem id_map : ∀ x : P.FreeM α, map id x = x + | .pure a => rfl + | .liftBind a cont => by + simp only [map] + congr 1 + funext u + exact id_map (cont u) + +theorem comp_map (h : β → γ) (g : α → β) : + ∀ x : P.FreeM α, map (h ∘ g) x = map h (map g x) + | .pure a => rfl + | .liftBind a cont => by + simp only [map] + congr 1 + funext u + exact comp_map h g (cont u) + instance : LawfulMonad (P.FreeM) := LawfulMonad.mk' (bind_pure_comp := bind_pure_comp) (id_map := id_map) @@ -185,7 +231,9 @@ instance : LawfulMonad (P.FreeM) := LawfulMonad.mk' @[simp] lemma pure_inj (a b : α) : (pure a : P.FreeM α) = pure b ↔ a = b := by constructor - · exact FreeM.pure.inj + · intro h + cases h + rfl · rintro rfl; rfl lemma liftBind_inj (a a' : P.A) @@ -193,8 +241,8 @@ lemma liftBind_inj (a a' : P.A) FreeM.liftBind a cont = FreeM.liftBind a' cont' ↔ ∃ h : a = a', h ▸ cont = cont' := by constructor · intro h - obtain ⟨rfl, hcont⟩ := FreeM.liftBind.inj h - exact ⟨rfl, eq_of_heq hcont⟩ + cases h + exact ⟨rfl, rfl⟩ · rintro ⟨rfl, rfl⟩ rfl @@ -205,8 +253,8 @@ 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)) : P.FreeM α → m α - | .pure a => Pure.pure a - | .liftBind a cont => (interp a) >>= (fun u ↦ (cont u).liftM interp) + | .pure a => pure a + | .liftBind a cont => interp a >>= fun u ↦ (cont u).liftM interp variable [Monad m] (interp : (a : P.A) → m (P.B a)) @@ -214,8 +262,10 @@ variable [Monad m] (interp : (a : P.A) → m (P.B a)) lemma liftM_pure (a : α) : (Pure.pure a : P.FreeM α).liftM interp = Pure.pure a := rfl @[simp] -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 +lemma liftM_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) : + ((FreeM.liftA a).bind cont).liftM interp = + (do let u ← interp a; (cont u).liftM interp) := by + rfl /-- A predicate stating that `eval : P.FreeM α → m α` is an interpreter for the polynomial @@ -227,8 +277,8 @@ monad `m`, and that it extends the interpretation of individual operations given -/ structure Interprets (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α → m α) : Prop where apply_pure (a : α) : eval (.pure a) = pure a - apply_liftBind (a : P.A) (cont : P.B a → P.FreeM α) : - eval (FreeM.liftBind a cont) = handler a >>= fun x => eval (cont x) + apply_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) : + eval ((FreeM.liftA a).bind cont) = handler a >>= fun x => eval (cont x) theorem Interprets.eq {handler : (a : P.A) → m (P.B a)} {eval : P.FreeM α → m α} (h : Interprets handler eval) : @@ -236,14 +286,14 @@ theorem Interprets.eq {handler : (a : P.A) → m (P.B a)} {eval : P.FreeM α → ext x induction x with | pure a => exact h.apply_pure a - | liftBind a cont ih => - rw [liftM_liftBind, h.apply_liftBind] - simp [ih] + | lift_bind a cont ih => + rw [h.apply_lift_bind, liftM_lift_bind] + simp only [ih] theorem Interprets.liftM (handler : (a : P.A) → m (P.B a)) : Interprets handler (·.liftM handler : P.FreeM α → _) where apply_pure _ := rfl - apply_liftBind _ _ := rfl + apply_lift_bind _ _ := rfl /-- The universal property of the free monad `P.FreeM`. @@ -259,44 +309,52 @@ variable [LawfulMonad m] @[simp] 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 + (x >>= f).liftM interp = (do let u ← x.liftM interp; (f u).liftM interp) := by induction x with - | pure _ => simp [FreeM.bind, FreeM.liftM] - | liftBind a cont h => simp [h] + | pure _ => simp only [liftM_pure, LawfulMonad.pure_bind] + | lift_bind a cont h => + change (((FreeM.liftA a).bind cont).bind f).liftM interp = + (((FreeM.liftA a).bind cont).liftM interp >>= fun u => (f u).liftM interp) + rw [FreeM.bind_assoc, liftM_lift_bind, liftM_lift_bind] + simp only [bind_eq_bind, h, LawfulMonad.bind_assoc] @[simp] -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] - | liftBind a cont h => simp [h] +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] @[simp] lemma liftM_seq {α β : Type uB} (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, bind_eq_bind, liftM_bind, map_eq_map, liftM_map] + (x <*> y).liftM interp = x.liftM interp <*> y.liftM interp := by + simp [seq_eq_bind_map] @[simp] lemma liftM_seqLeft {α β : Type uB} (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, bind_eq_bind, liftM_bind, liftM_pure] + (x <* y).liftM interp = x.liftM interp <* y.liftM interp := by + simp [seqLeft_eq_bind] @[simp] lemma liftM_seqRight {α β : Type uB} (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, bind_eq_bind, liftM_bind] + (x *> y).liftM interp = x.liftM interp *> y.liftM interp := by + simp [seqRight_eq_bind] @[simp] 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] + (FreeM.lift x).liftM interp = x.2 <$> interp x.1 := by + change ((FreeM.liftA x.1).bind fun y ↦ pure (x.2 y)).liftM interp = x.2 <$> interp x.1 + rw [liftM_lift_bind] + simpa only [Function.comp_apply] using + (LawfulMonad.bind_pure_comp (f := x.2) (x := interp x.1)) @[simp] 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] + (FreeM.liftA a).liftM interp = interp a := by + change (FreeM.lift (⟨a, id⟩ : P.Obj (P.B a))).liftM interp = interp a + rw [liftM_lift] + simp end liftM From f57b943c817d299b2cc7a616203dc8e79a9bce44 Mon Sep 17 00:00:00 2001 From: Quang Dao Date: Thu, 28 May 2026 15:52:59 +0700 Subject: [PATCH 14/14] fix(pfunctor): address final FreeM review --- Cslib/Foundations/Data/PFunctor/Free.lean | 91 ++++++++++------------- 1 file changed, 41 insertions(+), 50 deletions(-) diff --git a/Cslib/Foundations/Data/PFunctor/Free.lean b/Cslib/Foundations/Data/PFunctor/Free.lean index 01c5aa026..bea56e608 100644 --- a/Cslib/Foundations/Data/PFunctor/Free.lean +++ b/Cslib/Foundations/Data/PFunctor/Free.lean @@ -35,17 +35,15 @@ Its `liftBind` constructor uses the shape and continuation directly: When the effect signature is naturally polynomial (a fixed set of operations, each with a known return type), `PFunctor.FreeM` avoids the universe bump that the abstract `ι` in -`Cslib.FreeM` introduces. Its eliminators also expose the shape `a : P.A` and the -fiber `P.B a` directly in the recursive case, rather than hiding them behind an -arbitrary intermediate type `ι`. +`Cslib.FreeM` introduces, and records operations using the explicit shape/fiber data of `P`. This construction is ported from the [VCV-io](https://github.com/dtumad/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.lift`: Lift a shape of the base polynomial functor into the free monad. +- `PFunctor.FreeM.liftObj`: Lift an object of the base polynomial functor into the free monad. - `PFunctor.FreeM.liftM`: Interpret `FreeM P` into any other monad. -/ @@ -59,7 +57,7 @@ namespace PFunctor set_option genInjectivity false in set_option genSizeOfSpec false in /-- The free monad on a polynomial functor. -This extends the `W`-type construction with an extra `pure` constructor. -/ +This extends `WType` 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 : α) : P.FreeM α @@ -76,22 +74,28 @@ instance : Pure (P.FreeM) where pure := .pure @[simp] 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 α) : P.FreeM α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y)) +/-- Lift a shape of the base polynomial functor into the free monad. -/ +def lift (a : P.A) : P.FreeM (P.B a) := FreeM.liftBind a pure -/-- Lift a position of the base polynomial functor into the free monad. -/ -abbrev liftA (a : P.A) : P.FreeM (P.B a) := lift ⟨a, id⟩ +/-- Lift an object of the base polynomial functor into the free monad. -/ +def liftObj (x : P.Obj α) : P.FreeM α := FreeM.liftBind x.1 (fun y ↦ FreeM.pure (x.2 y)) instance : MonadLift P (P.FreeM) where - monadLift x := FreeM.lift x + monadLift x := FreeM.liftObj x + +@[simp] lemma lift_ne_pure (a : P.A) (y : P.B a) : + (lift a : P.FreeM (P.B a)) ≠ pure y := by simp [lift] + +@[simp] lemma pure_ne_lift (a : P.A) (y : P.B a) : + pure y ≠ (lift a : P.FreeM (P.B a)) := by simp [lift] -@[simp] lemma lift_ne_pure (x : P.Obj α) (y : α) : - (lift x : P.FreeM α) ≠ pure y := by simp [lift] +@[simp] lemma liftObj_ne_pure (x : P.Obj α) (y : α) : + (liftObj x : P.FreeM α) ≠ pure y := by simp [liftObj] -@[simp] lemma pure_ne_lift (x : P.Obj α) (y : α) : - pure y ≠ (lift x : P.FreeM α) := by simp [lift] +@[simp] lemma pure_ne_liftObj (x : P.Obj α) (y : α) : + pure y ≠ (liftObj x : P.FreeM α) := by simp [liftObj] -lemma monadLift_eq_lift (x : P.Obj α) : (x : P.FreeM α) = FreeM.lift x := rfl +lemma monadLift_eq_liftObj (x : P.Obj α) : (x : P.FreeM α) = FreeM.liftObj x := rfl /-- Bind operation for the `FreeM` monad. @@ -124,7 +128,7 @@ theorem map_eq_map {α β : Type v} : @[simp] lemma liftBind_eq (a : P.A) (cont : P.B a → P.FreeM α) : - FreeM.liftBind a cont = (FreeM.liftA a).bind cont := rfl + FreeM.liftBind a cont = (FreeM.lift a).bind cont := rfl set_option linter.unusedVariables false in /-- An override for the default induction principle that is in simp-normal form. @@ -134,7 +138,7 @@ Note that when `α` and `P.B a` are in the same universe, this simplifies slight protected theorem induction {motive : P.FreeM α → Prop} (pure : ∀ a, motive (pure a)) (lift_bind : ∀ (a : P.A) (cont : P.B a → P.FreeM α) (ih : ∀ i, motive (cont i)), - motive ((FreeM.liftA a).bind cont)) : ∀ x, motive x + motive ((FreeM.lift a).bind cont)) : ∀ x, motive x | .pure a => pure a | liftBind a cont => lift_bind a cont fun u => FreeM.induction pure lift_bind (cont u) @@ -165,19 +169,13 @@ 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 : α → P.FreeM β) : - (FreeM.lift x).bind f = FreeM.liftBind x.1 (fun a ↦ f (x.2 a)) := rfl +lemma liftObj_bind (x : P.Obj α) (f : α → P.FreeM β) : + (FreeM.liftObj x).bind f = FreeM.liftBind x.1 (fun a ↦ f (x.2 a)) := rfl @[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 => - constructor - · intro h - exact ⟨a, rfl, h⟩ - · rintro ⟨_, h, hf⟩ - cases h - exact hf + | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by cases h; exact hf⟩ | liftBind a cont => constructor · intro h @@ -188,13 +186,7 @@ lemma lift_bind (x : P.Obj α) (f : α → P.FreeM β) : @[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 => - constructor - · intro h - exact ⟨a, rfl, h⟩ - · rintro ⟨_, h, hf⟩ - cases h - exact hf + | pure a => exact ⟨fun h => ⟨a, rfl, h⟩, fun ⟨_, h, hf⟩ => by cases h; exact hf⟩ | liftBind a cont => constructor · intro h @@ -263,7 +255,7 @@ lemma liftM_pure (a : α) : (Pure.pure a : P.FreeM α).liftM interp = Pure.pure @[simp] lemma liftM_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) : - ((FreeM.liftA a).bind cont).liftM interp = + ((FreeM.lift a).bind cont).liftM interp = (do let u ← interp a; (cont u).liftM interp) := by rfl @@ -278,7 +270,7 @@ monad `m`, and that it extends the interpretation of individual operations given structure Interprets (handler : (a : P.A) → m (P.B a)) (eval : P.FreeM α → m α) : Prop where apply_pure (a : α) : eval (.pure a) = pure a apply_lift_bind (a : P.A) (cont : P.B a → P.FreeM α) : - eval ((FreeM.liftA a).bind cont) = handler a >>= fun x => eval (cont x) + eval ((FreeM.lift a).bind cont) = handler a >>= fun x => eval (cont x) theorem Interprets.eq {handler : (a : P.A) → m (P.B a)} {eval : P.FreeM α → m α} (h : Interprets handler eval) : @@ -313,10 +305,12 @@ lemma liftM_bind {α β : Type uB} (x : P.FreeM α) (f : α → P.FreeM β) : induction x with | pure _ => simp only [liftM_pure, LawfulMonad.pure_bind] | lift_bind a cont h => - change (((FreeM.liftA a).bind cont).bind f).liftM interp = - (((FreeM.liftA a).bind cont).liftM interp >>= fun u => (f u).liftM interp) + simp_rw [← bind_eq_bind] rw [FreeM.bind_assoc, liftM_lift_bind, liftM_lift_bind] - simp only [bind_eq_bind, h, LawfulMonad.bind_assoc] + rw [LawfulMonad.bind_assoc] + congr + funext u + exact h u @[simp] lemma liftM_map {α β : Type uB} (f : α → β) (x : P.FreeM α) : @@ -342,19 +336,16 @@ lemma liftM_seqRight {α β : Type uB} simp [seqRight_eq_bind] @[simp] -lemma liftM_lift (interp : (a : P.A) → m (P.B a)) (x : P.Obj α) : - (FreeM.lift x).liftM interp = x.2 <$> interp x.1 := by - change ((FreeM.liftA x.1).bind fun y ↦ pure (x.2 y)).liftM interp = x.2 <$> interp x.1 - rw [liftM_lift_bind] - simpa only [Function.comp_apply] using - (LawfulMonad.bind_pure_comp (f := x.2) (x := interp x.1)) +lemma liftM_lift (interp : (a : P.A) → m (P.B a)) (a : P.A) : + (FreeM.lift a).liftM interp = interp a := by + simp_rw [lift, FreeM.liftM, _root_.bind_pure] @[simp] -lemma liftM_liftA (interp : (a : P.A) → m (P.B a)) (a : P.A) : - (FreeM.liftA a).liftM interp = interp a := by - change (FreeM.lift (⟨a, id⟩ : P.Obj (P.B a))).liftM interp = interp a - rw [liftM_lift] - simp +lemma liftM_liftObj (interp : (a : P.A) → m (P.B a)) (x : P.Obj α) : + (FreeM.liftObj x).liftM interp = x.2 <$> interp x.1 := by + rw [liftObj, liftBind_eq, liftM_lift_bind] + simpa only [Function.comp_apply] using + (LawfulMonad.bind_pure_comp (f := x.2) (x := interp x.1)) end liftM