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