Skip to content

Commit c415fc2

Browse files
tannerduvetannerduve
committed
refactor(Free): move state/reader handlers to Effects.lean
1 parent 93c3d51 commit c415fc2

3 files changed

Lines changed: 75 additions & 72 deletions

File tree

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

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ Authors: Tanner Duve
77
module
88

99
public import Cslib.Foundations.Control.Monad.Free
10+
public import Cslib.Foundations.Control.Monad.Free.WP
1011
public import Mathlib.Control.Monad.Cont
1112

1213
/-!
@@ -39,10 +40,14 @@ Free monad, state monad, writer monad, continuation monad
3940

4041
@[expose] public section
4142

43+
set_option mvcgen.warning false
44+
4245
namespace Cslib
4346

4447
namespace FreeM
4548

49+
open Std.Do
50+
4651
universe u v w w' w''
4752

4853
/-! ### State Monad via `FreeM` -/
@@ -157,6 +162,32 @@ lemma run'_bind (x : FreeState σ α) (f : α → FreeState σ β) (s₀ : σ) :
157162

158163
end FreeState
159164

165+
/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/
166+
def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) :=
167+
LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op)
168+
169+
instance StateF.instHasHandler {σ : Type u} :
170+
HasHandler (StateF σ) (.arg σ .pure) where
171+
handler := StateF.handler
172+
173+
/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/
174+
theorem StateF.wp_FreeState_eq_wp_toStateM {σ α : Type u} (comp : FreeState σ α) :
175+
wp comp = wp (FreeState.toStateM comp) :=
176+
wpH_ofInterp_eq_wp_liftM (m := StateM σ)
177+
(fun _ op => FreeState.stateInterp op) comp
178+
179+
/-- Hoare spec for `get` on `FreeState`. -/
180+
@[spec]
181+
theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} :
182+
Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by
183+
mvcgen
184+
185+
/-- Hoare spec for `set` on `FreeState`. -/
186+
@[spec]
187+
theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} :
188+
Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by
189+
mvcgen
190+
160191
/-! ### Writer Monad via `FreeM` -/
161192

162193
/--
@@ -453,6 +484,26 @@ instance instMonadWithReaderOf : MonadWithReaderOf σ (FreeReader σ) where
453484

454485
end FreeReader
455486

487+
/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/
488+
def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) :=
489+
LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op)
490+
491+
instance ReaderF.instHasHandler {σ : Type u} :
492+
HasHandler (ReaderF σ) (.arg σ .pure) where
493+
handler := ReaderF.handler
494+
495+
/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/
496+
theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ α : Type u} (comp : FreeReader σ α) :
497+
wp comp = wp (FreeReader.toReaderM comp) :=
498+
wpH_ofInterp_eq_wp_liftM (m := ReaderM σ)
499+
(fun _ op => FreeReader.readInterp op) comp
500+
501+
/-- Hoare spec for `read` on `FreeReader`. -/
502+
@[spec]
503+
theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} :
504+
Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by
505+
mvcgen
506+
456507
end FreeM
457508

458509
end Cslib

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

Lines changed: 19 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@ Authors: Tanner Duve
77
module
88

99
public import Cslib.Foundations.Control.Monad.Free
10-
public import Cslib.Foundations.Control.Monad.Free.Effects
1110
public import Std.Do.PredTrans
1211
public import Std.Do.WP.Basic
1312
public import Std.Do.WP.Monad
@@ -18,9 +17,9 @@ public import Std.Do.Triple
1817
1918
Weakest-precondition interpretation of `FreeM F` programs through `Std.Do`'s
2019
predicate-transformer monad `PredTrans ps`. The universal property of `FreeM` lifts any
21-
effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H.run`,
22-
so weakest preconditions are compositional in `FreeM`'s monadic structure. An
23-
`[LHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple`
20+
effect handler `F ι → PredTrans ps ι` to a unique monad morphism `wpH H = liftM H`,
21+
so weakest preconditions are compositional in `FreeM`'s monadic structure. A
22+
`[HasHandler F ps]` instance plugs `FreeM F` into `Std.Do`'s `WP`/`WPMonad`/`Triple`
2423
infrastructure.
2524
2625
The WP's structural rules (`wpH_pure`, `wpH_bind`, …) are immediate from `liftM` being a monad
@@ -47,52 +46,51 @@ variable {F G : Type u → Type v} {ps : PostShape.{u}} {α β : Type u}
4746

4847
/-- A logical handler: an effect handler from `F` into the predicate-transformer monad
4948
`PredTrans ps`. -/
50-
structure LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) where
51-
/-- The assignment from operations to predicate transformers. -/
52-
run {ι : Type u} : F ι → PredTrans ps ι
49+
abbrev LHandler (F : Type u → Type v) (ps : PostShape.{u}) : Type (max (u + 1) v) :=
50+
∀ {ι : Type u}, F ι → PredTrans ps ι
5351

5452
namespace LHandler
5553

5654
/-- Sum of handlers; the counterpart of the paper's `H₁ ⊕ H₂`. -/
5755
def sum (H₁ : LHandler F ps) (H₂ : LHandler G ps) :
58-
LHandler (fun α => F α ⊕ G α) ps where
59-
run := Sum.elim H₁.run H₂.run
56+
LHandler (fun α => F α ⊕ G α) ps :=
57+
fun op => Sum.elim H₁ H₂ op
6058

61-
@[simp] theorem sum_run_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps)
59+
@[simp] theorem sum_inl (H₁ : LHandler F ps) (H₂ : LHandler G ps)
6260
{ι : Type u} (x : F ι) :
63-
(LHandler.sum H₁ H₂).run (Sum.inl x : F ι ⊕ G ι) = H₁.run x := rfl
61+
LHandler.sum H₁ H₂ (Sum.inl x : F ι ⊕ G ι) = H₁ x := rfl
6462

65-
@[simp] theorem sum_run_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps)
63+
@[simp] theorem sum_inr (H₁ : LHandler F ps) (H₂ : LHandler G ps)
6664
{ι : Type u} (y : G ι) :
67-
(LHandler.sum H₁ H₂).run (Sum.inr y : F ι ⊕ G ι) = H₂.run y := rfl
65+
LHandler.sum H₁ H₂ (Sum.inr y : F ι ⊕ G ι) = H₂ y := rfl
6866

6967
/-- Derive a logical handler from an effect handler into any `[WP m ps]` monad, by composing
7068
with `m`'s WP. -/
7169
def ofInterp {m : Type u → Type w} [WP m ps]
72-
(interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps where
73-
run {ι} op := wp (interp ι op)
70+
(interp : ∀ ι : Type u, F ι → m ι) : LHandler F ps :=
71+
fun {ι} op => wp (interp ι op)
7472

75-
@[simp] theorem ofInterp_run {m : Type u → Type w} [WP m ps]
73+
@[simp] theorem ofInterp_apply {m : Type u → Type w} [WP m ps]
7674
(interp : ∀ ι : Type u, F ι → m ι) {ι : Type u} (op : F ι) :
77-
(LHandler.ofInterp interp).run op = wp (interp ι op) := rfl
75+
LHandler.ofInterp interp op = wp (interp ι op) := rfl
7876

7977
end LHandler
8078

8179
/-- Weakest-precondition interpretation of a `FreeM F α` program against a logical handler `H`.
8280
Defined as `FreeM.liftM` instantiated at `PredTrans ps`, the unique monad morphism
8381
`FreeM F → PredTrans ps` extending `H` per the universal property of `FreeM`. -/
8482
def wpH (H : LHandler F ps) (x : FreeM F α) : PredTrans ps α :=
85-
x.liftM (fun {_} => H.run)
83+
x.liftM H
8684

8785
@[simp] theorem wpH_pure (H : LHandler F ps) (a : α) :
8886
wpH H (pure a : FreeM F α) = Pure.pure a := rfl
8987

9088
@[simp] theorem wpH_liftBind (H : LHandler F ps) {ι : Type u}
9189
(op : F ι) (k : ι → FreeM F α) :
92-
wpH H (lift op >>= k) = H.run op >>= fun x => wpH H (k x) := rfl
90+
wpH H (lift op >>= k) = H op >>= fun x => wpH H (k x) := rfl
9391

9492
@[simp] theorem wpH_lift (H : LHandler F ps) {ι : Type u} (op : F ι) :
95-
wpH H (lift op : FreeM F ι) = H.run op :=
93+
wpH H (lift op : FreeM F ι) = H op :=
9694
liftM_lift _ op
9795

9896
@[simp] theorem wpH_bind (H : LHandler F ps) (x : FreeM F α) (f : α → FreeM F β) :
@@ -115,7 +113,7 @@ theorem wpH_ofInterp_eq_wp_liftM
115113
`WP (FreeM F) ps` instance and any `Triple`/`mvcgen` reasoning over `FreeM F`. -/
116114
class HasHandler (F : Type u → Type v) (ps : outParam (PostShape.{u})) where
117115
/-- The default logical handler for `F`. -/
118-
handler : LHandler F ps
116+
handler {ι : Type u} : F ι → PredTrans ps ι
119117

120118
instance instWPFreeM [HasHandler F ps] : WP (FreeM F) ps where
121119
wp := wpH HasHandler.handler
@@ -124,52 +122,6 @@ instance instWPMonadFreeM [HasHandler F ps] : WPMonad (FreeM F) ps where
124122
wp_pure _ := rfl
125123
wp_bind x f := wpH_bind _ x f
126124

127-
/-- Logical handler for the state effect, induced by `Std.Do`'s `WP (StateM σ)`. -/
128-
def StateF.handler {σ : Type u} : LHandler (StateF σ) (.arg σ .pure) :=
129-
LHandler.ofInterp (m := StateM σ) (fun _ op => FreeState.stateInterp op)
130-
131-
instance StateF.instHasHandler {σ : Type u} :
132-
HasHandler (StateF σ) (.arg σ .pure) where
133-
handler := StateF.handler
134-
135-
/-- WP of a `FreeState` program matches WP of its `StateM` interpretation. -/
136-
theorem StateF.wp_FreeState_eq_wp_toStateM {σ : Type u} (comp : FreeState σ α) :
137-
wp comp = wp (FreeState.toStateM comp) :=
138-
wpH_ofInterp_eq_wp_liftM (m := StateM σ)
139-
(fun _ op => FreeState.stateInterp op) comp
140-
141-
/-- Hoare spec for `get` on `FreeState`. -/
142-
@[spec]
143-
theorem Spec.get_FreeState {σ : Type u} {Q : PostCond σ (.arg σ .pure)} :
144-
Triple (MonadStateOf.get : FreeState σ σ) (spred(fun s => Q.1 s s)) Q := by
145-
mvcgen
146-
147-
/-- Hoare spec for `set` on `FreeState`. -/
148-
@[spec]
149-
theorem Spec.set_FreeState {σ : Type u} (s : σ) {Q : PostCond PUnit (.arg σ .pure)} :
150-
Triple (MonadStateOf.set s : FreeState σ PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by
151-
mvcgen
152-
153-
/-- Logical handler for the reader effect, induced by `Std.Do`'s `WP (ReaderM σ)`. -/
154-
def ReaderF.handler {σ : Type u} : LHandler (ReaderF σ) (.arg σ .pure) :=
155-
LHandler.ofInterp (m := ReaderM σ) (fun _ op => FreeReader.readInterp op)
156-
157-
instance ReaderF.instHasHandler {σ : Type u} :
158-
HasHandler (ReaderF σ) (.arg σ .pure) where
159-
handler := ReaderF.handler
160-
161-
/-- WP of a `FreeReader` program matches WP of its `ReaderM` interpretation. -/
162-
theorem ReaderF.wp_FreeReader_eq_wp_toReaderM {σ : Type u} (comp : FreeReader σ α) :
163-
wp comp = wp (FreeReader.toReaderM comp) :=
164-
wpH_ofInterp_eq_wp_liftM (m := ReaderM σ)
165-
(fun _ op => FreeReader.readInterp op) comp
166-
167-
/-- Hoare spec for `read` on `FreeReader`. -/
168-
@[spec]
169-
theorem Spec.read_FreeReader {ρ : Type u} {Q : PostCond ρ (.arg ρ .pure)} :
170-
Triple (MonadReaderOf.read : FreeReader ρ ρ) (spred(fun r => Q.1 r r)) Q := by
171-
mvcgen
172-
173125
end FreeM
174126

175127
end Cslib

‎CslibTests/FreeMonadWP.lean‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Tanner Duve
55
-/
66

7-
import Cslib.Foundations.Control.Monad.Free.WP
7+
import Cslib.Foundations.Control.Monad.Free.Effects
88
import Std.Tactic.Do
99

1010
/-!
@@ -107,8 +107,8 @@ inductive FailF : Type → Type where
107107

108108
/-- Logical handler for `FailF`: `fail` has precondition `⌜False⌝`, so it is only provable in
109109
unreachable branches. -/
110-
def FailF.handler {ps : PostShape} : LHandler FailF ps where
111-
run {_} op := match op with
110+
def FailF.handler {ps : PostShape} : LHandler FailF ps :=
111+
fun op => match op with
112112
| .fail => PredTrans.const spred(⌜False⌝)
113113

114114
/-- A combined state + failure signature, sequencing `StateF Nat` with `FailF`. -/
@@ -186,8 +186,8 @@ inductive DemonicF : Type → Type 1 where
186186
/-- Logical handler for `DemonicF`: the predicate transformer for `choice α` is universal
187187
quantification over `α`. Conjunctivity of `∀` (i.e. `∀ a, P a ∧ Q a ⊣⊢ (∀ a, P a) ∧ (∀ a, Q a)`)
188188
is what makes this admissible in `PredTrans`. -/
189-
def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps where
190-
run {_} op := match op with
189+
def DemonicF.handler {ps : PostShape} : LHandler DemonicF ps :=
190+
fun op => match op with
191191
| .choice _ =>
192192
{ trans := fun Q => SPred.forall (fun a => Q.1 a)
193193
conjunctiveRaw := by

0 commit comments

Comments
 (0)