# Monad morphisms and weakest precondition interpretations #

A `WP m ps` is a `WPMonad m ps` if the interpretation `WP.wp` is also a monad morphism, that is, it preserves `pure` and `bind`.

source
class Std.Do.WPMonad (m : Type u → Type v) (ps : outParam PostShape) [Monad m] extends LawfulMonad m, Std.Do.WP m ps :
Type (max (u + 1) v)

A `WP` that is also a monad morphism, preserving `pure` and `bind`. (They all are.)

- map_const {α β : Type u} : Functor.mapConst = Functor.map ∘ Function.const β
- id_map {α : Type u} (x : m α) : id <$> x = x
- comp_map {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
- seqLeft_eq {α β : Type u} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
- seqRight_eq {α β : Type u} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
- pure_seq {α β : Type u} (g : α → β) (x : m α) : pure g <*> x = g <$> x
- map_pure {α β : Type u} (g : α → β) (x : α) : g <$> pure x = pure (g x)
- seq_pure {α β : Type u} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
- seq_assoc {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
- bind_pure_comp {α β : Type u} (f : α → β) (x : m α) : (do let a ← x pure (f a)) = f <$> x
- bind_map {α β : Type u} (f : m (α → β)) (x : m α) : (do let x_1 ← f x_1 <$> x) = f <*> x
- pure_bind {α β : Type u} (x : α) (f : α → m β) : pure x >>= f = f x
- bind_assoc {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ) : x >>= f >>= g = x >>= fun (x : α) => f x >>= g
- wp {α : Type u} (x : m α) : PredTrans ps α
- wp_pure {α : Type u} (a : α) : wp (pure a) = pure a

  `WP.wp` preserves `pure`.

- wp_bind {α β : Type u} (x : m α) (f : α → m β) : (wp do let a ← x f a) = do let a ← wp x wp (f a)

  `WP.wp` preserves `bind`.

Instances

source
theorem Std.Do.WPMonad.wp_map {m : Type u → Type v} {ps : PostShape} {α β : Type u} [Monad m] [WPMonad m ps] (f : α → β) (x : m α) :
wp (f <$> x) = f <$> wp x

`WP.wp` preserves `map`.

source
theorem Std.Do.WPMonad.wp_seq {m : Type u → Type v} {ps : PostShape} {α β : Type u} [Monad m] [WPMonad m ps] (f : m (α → β)) (x : m α) :
wp (f <*> x) = wp f <*> wp x

`WP.wp` preserves `seq`.

source
instance Std.Do.Id.instWPMonad :
WPMonad Id PostShape.pure
Equations

- Std.Do.Id.instWPMonad = { toLawfulMonad := Id.instLawfulMonad, toWP := Std.Do.Id.instWP, wp_pure := ⋯, wp_bind := ⋯ }

source
instance Std.Do.StateT.instWPMonad {m : Type u → Type v} {ps : PostShape} {σ : Type u} [Monad m] [WPMonad m ps] :
WPMonad (StateT σ m) (PostShape.arg σ ps)
Equations

- Std.Do.StateT.instWPMonad = { toLawfulMonad := ⋯, toWP := Std.Do.StateT.instWP, wp_pure := ⋯, wp_bind := ⋯ }

source
instance Std.Do.ReaderT.instWPMonad {m : Type u → Type v} {ps : PostShape} {ρ : Type u} [Monad m] [WPMonad m ps] :
WPMonad (ReaderT ρ m) (PostShape.arg ρ ps)
Equations

- Std.Do.ReaderT.instWPMonad = { toLawfulMonad := ⋯, toWP := Std.Do.ReaderT.instWP, wp_pure := ⋯, wp_bind := ⋯ }

source
instance Std.Do.ExceptT.instWPMonad {m : Type u → Type v} {ps : PostShape} {ε : Type u} [Monad m] [WPMonad m ps] :
WPMonad (ExceptT ε m) (PostShape.except ε ps)
Equations

- Std.Do.ExceptT.instWPMonad = { toLawfulMonad := ⋯, toWP := Std.Do.ExceptT.instWP, wp_pure := ⋯, wp_bind := ⋯ }

source
instance Std.Do.OptionT.instWPMonad {m : Type u → Type v} {ps : PostShape} [Monad m] [WPMonad m ps] :
WPMonad (OptionT m) (PostShape.except PUnit ps)
Equations

- Std.Do.OptionT.instWPMonad = { toLawfulMonad := ⋯, toWP := Std.Do.OptionT.instWP, wp_pure := ⋯, wp_bind := ⋯ }

source
instance Std.Do.EStateM.instWPMonad {ε σ : Type u_1} :
WPMonad (EStateM ε σ) (PostShape.except ε (PostShape.arg σ PostShape.pure))
Equations

- Std.Do.EStateM.instWPMonad = { toLawfulMonad := ⋯, toWP := Std.Do.EStateM.instWP, wp_pure := ⋯, wp_bind := ⋯ }

source
instance Std.Do.Except.instWPMonad {ε : Type u_1} :
WPMonad (Except ε) (PostShape.except ε PostShape.pure)
Equations

- Std.Do.Except.instWPMonad = { toLawfulMonad := ⋯, toWP := Std.Do.Except.instWP, wp_pure := ⋯, wp_bind := ⋯ }

source
instance Std.Do.Option.instWPMonad :
WPMonad Option (PostShape.except PUnit PostShape.pure)
Equations

- Std.Do.Option.instWPMonad = { toLawfulMonad := instLawfulMonadOption_1, toWP := Std.Do.Option.instWP, wp_pure := @Std.Do.Option.instWPMonad._proof_2, wp_bind := ⋯ }

source
instance Std.Do.State.instWPMonad {σ : Type u_1} :
WPMonad (StateM σ) (PostShape.arg σ PostShape.pure)
Equations

- Std.Do.State.instWPMonad = inferInstanceAs (Std.Do.WPMonad (StateT σ Id) (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))

source
instance Std.Do.Reader.instWPMonad {ρ : Type u_1} :
WPMonad (ReaderM ρ) (PostShape.arg ρ PostShape.pure)
Equations

- Std.Do.Reader.instWPMonad = inferInstanceAs (Std.Do.WPMonad (ReaderT ρ Id) (Std.Do.PostShape.arg ρ Std.Do.PostShape.pure))