The Weakest Precondition Interpretation of a Monad

WPMonad m Pred EPred carries a WP (m α) α Pred EPred interpretation for every result type α, together with soundness of that interpretation for pure and bind. An instance supplies the WP interpretation of m α at low priority, so a program type with a bespoke interpretation keeps its own.

class Std.WP.WPMonad (m : Type u → Type v) (Pred : outParam (Type w)) (EPred : outParam (Type w')) [Monad m] [Assertion Pred] [Assertion EPred] extends LawfulMonad m : Type (max (max (max (u + 1) v) w) w')

Weakest precondition monad: a monad m whose weakest precondition interpretation is sound for pure and bind. The interpretation for every result type is carried as the toWP field; an instance exposes it as a WP (m α) … interpretation.

• 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
• toWP (α : Type u) : WP (m α) α Pred EPred

  The weakest precondition interpretation of m at every result type.

• pure_le_wp_pure {α : Type u} (x : α) (post : α → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (post x) (wp (pure x) post epost)

  Soundness of pure: the postcondition applied to x implies the weakest precondition of pure x.

• bind_le_wp_bind {α β : Type u} (x : m α) (f : α → m β) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x (fun (a : α) => wp (f a) post epost) epost) (wp (x >>= f) post epost)

  Soundness of bind: composing weakest preconditions is at least as strong as the weakest precondition of >>=.

@[instance_reducible, instance 100]

instance Std.WP.instWPOfWPMonad {m : Type u → Type v} {Pred : Type w} {EPred : Type w'} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [inst : WPMonad m Pred EPred] : WP (m α) α Pred EPred

A monadic WP interpretation is sourced from the monad's WPMonad instance. Low priority so a program type with a bespoke WP instance (e.g. a non-monadic one) is preferred.

Equations

• Std.WP.instWPOfWPMonad = Std.WP.WPMonad.toWP α

Derived WPMonad Lemmas

One-directional consequences of the WPMonad axioms for pure, bind, map, and seq.

theorem Std.WP.WPMonad.map_le_wp_map {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} (f : α → β) (x : m α) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x (fun (a : α) => post (f a)) epost) (wp (f <$> x) post epost)

Soundness of Functor.map: mapping f over x preserves the WP.

theorem Std.WP.WPMonad.seq_le_wp_seq {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} (f : m (α → β)) (x : m α) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp f (fun (g : α → β) => wp x (fun (a : α) => post (g a)) epost) epost) (wp (f <*> x) post epost)

Soundness of Seq.seq: sequencing f <*> x preserves the WP.