refactor(FreeWP): inline handler wrappers, rename HasHandler to FreeM.WP

Address review feedback:
- inline `wpH`, the `LHandler` abbrev/namespace, and `LHandler.ofInterp`;
  handlers are now plain `F ι → PredTrans ps ι` functions
- rename the `HasHandler` class to `FreeM.WP`
- restate the adequacy lemma directly on `liftM` as `liftM_wp_eq_wp_liftM`

Author: tannerduve

Cslib/Foundations/Control/Monad/Free/Effects.lean

@@ -163,17 +163,18 @@ lemma run'_bind (x : FreeState σ α) (f : α → FreeState σ β) (s₀ : σ) :
 end FreeState
 
 /-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/
-def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) :=
-  LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op)
+def StateF.handler {σ : Type u} :
+    {ι : Type u} → StateF σ ι → PredTrans (.arg σ .pure) ι :=
+  fun {ι} op => wp (FreeState.stateInterp (σ := σ) (α := ι) op)
 
-instance StateF.instHasHandler {σ : Type u} :
-    HasHandler (StateF σ) (.arg σ .pure) where
+instance StateF.instWP {σ : Type u} :
+    FreeM.WP (StateF σ) (.arg σ .pure) where
   handler := StateF.handler
 
 /-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/
 theorem StateF.wp_FreeState_eq_wp_toStateM {σ α : Type u} (comp : FreeState σ α) :
     wp comp = wp (FreeState.toStateM comp) :=
-  wpH_ofInterp_eq_wp_liftM (m := StateM σ)
+  liftM_wp_eq_wp_liftM (m := StateM σ)
     (fun _ op => FreeState.stateInterp op) comp
 
 /-- Hoare spec for `get` on `FreeState`. -/
@@ -485,17 +486,18 @@ instance instMonadWithReaderOf : MonadWithReaderOf σ (FreeReader σ) where
 end FreeReader
 
 /-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/
-def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) :=
-  LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op)
+def ReaderF.handler {σ : Type u} :
+    {ι : Type u} → ReaderF σ ι → PredTrans (.arg σ .pure) ι :=
+  fun {ι} op => wp (FreeReader.readInterp (σ := σ) (α := ι) op)
 
-instance ReaderF.instHasHandler {σ : Type u} :
-    HasHandler (ReaderF σ) (.arg σ .pure) where
+instance ReaderF.instWP {σ : Type u} :
+    FreeM.WP (ReaderF σ) (.arg σ .pure) where
   handler := ReaderF.handler
 
 /-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/
 theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ α : Type u} (comp : FreeReader σ α) :
     wp comp = wp (FreeReader.toReaderM comp) :=
-  wpH_ofInterp_eq_wp_liftM (m := ReaderM σ)
+  liftM_wp_eq_wp_liftM (m := ReaderM σ)
     (fun _ op => FreeReader.readInterp op) comp
 
 /-- Hoare spec for `read` on `FreeReader`. -/

Cslib/Foundations/Control/Monad/Free/WP.lean

@@ -17,13 +17,13 @@ public import Std.Do.Triple
 
 Weakest-precondition interpretation of `FreeM F` programs through `Std.Do`'s
 predicate-transformer monad `PredTrans ps`. The universal property of `FreeM` lifts any
-effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H`,
+effect handler `F ι → PredTrans ps ι` to a unique monad morphism `liftM H`,
 so weakest preconditions are compositional in `FreeM`'s monadic structure. A
-`[HasHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple`
+`[FreeM.WP F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple`
 infrastructure.
 
-The WP's structural rules (`wpH_pure`, `wpH_bind`, …) are immediate from `liftM` being a monad
-morphism; the adequacy theorem `wpH_ofInterp_eq_wp_liftM` — that WP-via-handler agrees with
+The WP's structural rules are immediate from `liftM` being a monad morphism; the
+adequacy theorem `liftM_wp_eq_wp_liftM` — that WP-via-handler agrees with
 `Std.Do`'s WP of the `liftM` interpretation — is the same statement of uniqueness.
 
 The design follows [Vistrup, Sammler, Jung. *Program Logics à la Carte.* POPL 2025], adapted
@@ -42,85 +42,33 @@ namespace FreeM
 
 universe u v w
 
-variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u}
+variable {F : Type u → Type v} {ps : PostShape.{u}} {α β : Type u}
 
-/-- A logical handler: an effect handler from `F` into the predicate-transformer monad
-`PredTrans ps`. -/
-abbrev LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) :=
-  ∀ {ι : Type u}, F ι → PredTrans ps ι
-
-namespace LHandler
-
-/-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/
-def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) :
-    LHandler (fun α => F α ⊕ G α) ps :=
-  fun op => Sum.elim H₁ H₂ op
-
-@[simp] theorem sum_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps)
-    {ι : Type u} (x : F ι) :
-    LHandler.sum H₁ H₂ (Sum.inl x : F ι ⊕ G ι) = H₁ x := rfl
-
-@[simp] theorem sum_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps)
-    {ι : Type u} (y : G ι) :
-    LHandler.sum H₁ H₂ (Sum.inr y : F ι ⊕ G ι) = H₂ y := rfl
-
-/-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing
-with `m`'s WP. -/
-def ofInterp {m : Type u → Type w} [WP m ps]
-    (interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps :=
-  fun {ι} op => wp (interp ι op)
-
-@[simp] theorem ofInterp_apply {m : Type u → Type w} [WP m ps]
-    (interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) :
-    LHandler.ofInterp interp op = wp (interp ι op) := rfl
-
-end LHandler
-
-/-- Weakest-precondition interpretation of a `FreeM F α` program against a logical handler `H`.
-Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism
-`FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/
-def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α :=
-  x.liftM H
-
-@[simp] theorem wpH_pure (H : LHandler F ps) (a : α) :
-    wpH H (pure a : FreeM F α) = Pure.pure a := rfl
-
-@[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u}
-    (op : F ι) (k : ι → FreeM F α) :
-    wpH H (lift op >>= k) = H op >>= fun x => wpH H (k x) := rfl
-
-@[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) :
-    wpH H (lift op : FreeM F ι) = H op :=
-  liftM_lift _ op
-
-@[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) :
-    wpH H (x >>= f) = wpH H x >>= fun a => wpH H (f a) :=
-  liftM_bind _ x f
-
-/-- Adequacy theorem: WP via `FreeM` against an `ofInterp`-derived handler agrees with
+/-- Adequacy theorem: WP via `FreeM` against a WP-derived handler agrees with
 `Std.Do`'s WP of the `liftM` interpretation. Equivalently, two monad morphisms
 `FreeM F → PredTrans ps` extending the same handler are equal. -/
-theorem wpH_ofInterp_eq_wp_liftM
-    {m : Type u → Type w} [Monad m] [LawfulMonad m] [WPMonad m ps]
+theorem liftM_wp_eq_wp_liftM
+    {m : Type u → Type w} [Monad m] [WPMonad m ps]
     (interp : ∀ ι : Type u, F ι → m ι) (x : FreeM F α) :
-    wpH (LHandler.ofInterp interp) x = wp (x.liftM (fun {_} => interp _)) := by
+    x.liftM (fun {ι} op => wp (interp ι op)) =
+      wp (x.liftM (fun {_} => interp _)) := by
   induction x with
-  | pure a => simp [wpH, FreeM.liftM, WPMonad.wp_pure]
+  | pure a => simp [WPMonad.wp_pure]
   | lift_bind op k ih =>
     simp [WPMonad.wp_bind, ih]
 
 /-- Records a default logical handler for `F` at shape `ps`, enabling the global
 `WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/
-class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where
+class WP (F : Type u → Type v) (ps : outParam (PostShape.{u})) where
   /-- The default logical handler for `F`. -/
   handler {ι : Type u} : F ι → PredTrans ps ι
 
-instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where
-  wp := wpH HasHandler.handler
+instance instStdDoWP [WP F ps] : Std.Do.WP (FreeM F) ps where
+  wp x := x.liftM WP.handler
 
-instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where
+instance instWPMonadFreeM [WP F ps] : WPMonad (FreeM F) ps where
   wp_pure _ := rfl
-  wp_bind x f := wpH_bind _ x f
+  wp_bind x f := liftM_bind _ x f
 
 end FreeM
 

CslibTests/FreeMonadWP.lean

@@ -19,10 +19,10 @@ namespace CslibTests.FreeMonadWP
 
 open Cslib Cslib.FreeM Std.Do
 
-example : WP (FreeState Nat) (.arg Nat .pure) := inferInstance
+example : Std.Do.WP (FreeState Nat) (.arg Nat .pure) := inferInstance
 example : WPMonad (FreeState Nat) (.arg Nat .pure) := inferInstance
-example : WP (FreeReader Nat) (.arg Nat .pure) := inferInstance
-example : HasHandler (StateF Nat) (.arg Nat .pure) := inferInstance
+example : Std.Do.WP (FreeReader Nat) (.arg Nat .pure) := inferInstance
+example : FreeM.WP (StateF Nat) (.arg Nat .pure) := inferInstance
 
 /-- Increment the natural-number state by 1. -/
 def incr : FreeState Nat Unit := do
@@ -61,10 +61,10 @@ def interp : ∀ ι : Type, CounterF ι → StateM Nat ι
 
 /-- Logical handler for `CounterF` induced by `interp` and `Std.Do`'s `WP (StateM Nat)`
 instance. -/
-def handler : LHandler CounterF (.arg Nat .pure) :=
-  LHandler.ofInterp CounterF.interp
+def handler : {ι : Type} → CounterF ι → PredTrans (.arg Nat .pure) ι :=
+  fun {ι} op => wp (CounterF.interp ι op)
 
-instance : HasHandler CounterF (.arg Nat .pure) where
+instance : FreeM.WP CounterF (.arg Nat .pure) where
   handler := CounterF.handler
 
 /-- Interpret counter programs as `StateM Nat` programs. -/
@@ -74,7 +74,7 @@ abbrev toStateM {α : Type} (comp : FreeCounter α) : StateM Nat α :=
 /-- Adequacy theorem specialized to `CounterF`. -/
 theorem wp_FreeCounter_eq_wp_toStateM {α : Type} (comp : FreeCounter α) :
     wp comp = wp (CounterF.toStateM comp) :=
-  wpH_ofInterp_eq_wp_liftM (m := StateM Nat) CounterF.interp comp
+  liftM_wp_eq_wp_liftM (m := StateM Nat) CounterF.interp comp
 
 end CounterF
 
@@ -107,7 +107,7 @@ inductive FailF : Type → Type where
 
 /-- Logical handler for `FailF`: `fail` has precondition `⌜False⌝`, so it is only provable in
 unreachable branches. -/
-def FailF.handler {ps : PostShape} : LHandler FailF ps :=
+def FailF.handler {ps : PostShape} : {ι : Type} → FailF ι → PredTrans ps ι :=
   fun op => match op with
     | .fail => PredTrans.const spred(⌜False⌝)
 
@@ -116,8 +116,8 @@ abbrev StateFail := fun α => StateF Nat α ⊕ FailF α
 
 /-- Handler for the combined signature: the sum of the component handlers — the paper's
 `H₁ ⊕ H₂` composition. -/
-instance : HasHandler StateFail (.arg Nat .pure) where
-  handler := StateF.handler.sum FailF.handler
+instance : FreeM.WP StateFail (.arg Nat .pure) where
+  handler := fun op => Sum.elim StateF.handler FailF.handler op
 
 /-- Smart constructor for state-read in the combined signature. -/
 abbrev sfGet : FreeM StateFail Nat := lift (Sum.inl StateF.get)
@@ -186,7 +186,7 @@ inductive DemonicF : Type → Type 1 where
 /-- Logical handler for `DemonicF`: the predicate transformer for `choice α` is universal
 quantification over `α`. Conjunctivity of `∀` (i.e. `∀ a, P a ∧ Q a ⊣⊢ (∀ a, P a) ∧ (∀ a, Q a)`)
 is what makes this admissible in `PredTrans`. -/
-def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps :=
+def DemonicF.handler {ps : PostShape} : {ι : Type} → DemonicF ι → PredTrans ps ι :=
   fun op => match op with
     | .choice _ =>
       { trans := fun Q => SPred.forall (fun a => Q.1 a)
@@ -207,7 +207,7 @@ def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps :=
             · exact SPred.and_elim_l.trans (SPred.forall_elim a)
             · exact SPred.and_elim_r.trans (SPred.forall_elim a) }
 
-instance : HasHandler DemonicF .pure where
+instance : FreeM.WP DemonicF .pure where
   handler := DemonicF.handler
 
 /-- Smart constructor for demonic choice over `α`. -/