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.

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 monad with weakest preconditions (WP) that is also a monad morphism, preserving pure and bind.

In practice, mvcgen is not useful for reasoning about programs in a monad that is without a WPMonad instance. The specification lemmas for Pure.pure and Bind.bind, as well as those for operators like Functor.map, require that their monad have a WPMonad instance.

• 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.

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.

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.

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

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)

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)

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)

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

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

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

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

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

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