Weakest Precondition Interpretation

This module defines the weakest precondition interpretation WPMonad of monadic programs in terms of predicate transformers PredTrans.

An instance WPMonad m Pred EPred determines a function wpTrans : m α → PredTrans Pred EPred α that interprets a program x : m α as a predicate transformer. The function wp is the user-facing wrapper: wp x post epost computes the weakest precondition for x to satisfy normal postcondition post and exception postcondition epost.

Assertion Language Classes

Assertion is an alias type class for CompleteLattice. We use Assertion Pred for the assertion language of normal postconditions and Assertion EPred for exception postconditions.

Pre-defined instances

• WPMonad Id Prop EPost.nil — pure computations.
• WPMonad (StateT σ m) (σ → Pred) EPred — stateful computations.
• WPMonad (ExceptT ε m) Pred (EPost.cons (ε → Pred) EPred) — computations with exceptions.
• WPMonad (ReaderT ρ m) (ρ → Pred) EPred — reader computations.
• WPMonad (Except ε) Prop EPost⟨ε → Prop⟩ — concrete exception type.
• WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop) — concrete error-state monad.

WPMonad Typeclass

The WPMonad typeclass defines weakest precondition semantics for monads. A WPMonad m Pred EPred instance provides a monad morphism wpTrans : m α → PredTrans Pred EPred α satisfying:

• wp_trans_pure: pure x is at least as strong as its predicate transformer.
• wp_trans_bind: sequential composition is sound.
• wp_trans_monotone: the transformer is monotone in both postconditions.

class Std.Internal.Do.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 with a sound interpretation as predicate transformers over assertion language Pred with exception postconditions EPred.

• 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
• wpTrans {α : Type u} : m α → PredTrans Pred EPred α

  The weakest precondition transformer for a monadic program.

• wp_trans_pure {α : Type u} (x : α) : Lean.Order.PartialOrder.rel (pure x) (wpTrans (pure x))

  Soundness of pure: the postcondition applied to x implies the WPMonad of pure x.

• wp_trans_bind {α β : Type u} (x : m α) (f : α → m β) : Lean.Order.PartialOrder.rel (do let x ← wpTrans x wpTrans (f x)) (wpTrans (x >>= f))

  Soundness of bind: composing WPs is at least as strong as the WPMonad of >>=.

• wp_trans_monotone {α : Type u} (x : m α) : (wpTrans x).monotone

  Monotonicity: weaker postconditions yield weaker preconditions.

def Std.Internal.Do.wp {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : m α) (post : α → Pred) (epost : EPred) : Pred

Compute the weakest precondition of x for normal postcondition post and exception postcondition epost.

Equations

• Std.Internal.Do.wp x post epost = (Std.Internal.Do.WPMonad.wpTrans x).apply post epost

@[simp]

theorem Std.Internal.Do.WPMonad.wp_impl_eq_wp {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : m α) : (wpTrans x).apply = wp x

Derived WPMonad Lemmas

One-directional consequences of the WPMonad axioms for pure, bind, monotonicity, and weakening.

theorem Std.Internal.Do.WPMonad.wp_pure {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} (x : α) (post : α → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (post x) (wp (pure x) post epost)

theorem Std.Internal.Do.WPMonad.wp_bind {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} (x : m α) (f : α → m β) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x (fun (x : α) => wp (f x) post epost) epost) (wp (x >>= f) post epost)

theorem Std.Internal.Do.WPMonad.wp_consequence {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} (x : m α) (post post' : α → Pred) (epost : EPred) (h : Lean.Order.PartialOrder.rel post post') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post' epost)

theorem Std.Internal.Do.WPMonad.wp_consequence_econs {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} (x : m α) (post post' : α → Pred) (epost epost' : EPred) (h : Lean.Order.PartialOrder.rel post post') (h' : Lean.Order.PartialOrder.rel epost epost') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post' epost')

theorem Std.Internal.Do.WPMonad.wp_econs {Pred : Type u_2} {EPred : Type u_1} {m : Type u → Type z} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : m α) (post : α → Pred) (epost epost' : EPred) (h' : Lean.Order.PartialOrder.rel epost epost') : Lean.Order.PartialOrder.rel (wp x post epost) (wp x post epost')

theorem Std.Internal.Do.WPMonad.wp_econs_bot {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} (x : m α) (post : α → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x post Lean.Order.bot) (wp x post epost)

theorem Std.Internal.Do.WPMonad.wp_consequence_rel {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} (x : m α) (post post' : α → Pred) (epost : EPred) (h : Lean.Order.PartialOrder.rel post post') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post epost)) : Lean.Order.PartialOrder.rel pre (wp x post' epost)

theorem Std.Internal.Do.WPMonad.wp_econs_rel {Pred : Type u_2} {EPred : Type u_1} {m : Type u → Type z} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} (x : m α) (post : α → Pred) (epost epost' : EPred) (h : Lean.Order.PartialOrder.rel epost epost') {pre : Pred} (h' : Lean.Order.PartialOrder.rel pre (wp x post epost)) : Lean.Order.PartialOrder.rel pre (wp x post epost')

theorem Std.Internal.Do.WPMonad.wp_econs_bot_rel {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} (x : m α) (post : α → Pred) (epost : EPred) {pre : Pred} (h : Lean.Order.PartialOrder.rel pre (wp x post Lean.Order.bot)) : Lean.Order.PartialOrder.rel pre (wp x post epost)

Derived Theorems for map and seq

One direction of the derived theorems wp_map and wp_seq. The full bidirectional equality from Std.Do cannot be proven with our current axioms since wp_bind only gives one direction (⊑).

theorem Std.Internal.Do.WPMonad.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.Internal.Do.WPMonad.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) (post' : β → Pred) (epost : EPred) : (post = fun (a : α) => post' (f a)) → Lean.Order.PartialOrder.rel (wp x post epost) (wp (f <$> x) post' epost)

Variant of wp_map with an explicit postcondition equality hypothesis.

theorem Std.Internal.Do.WPMonad.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.

WPMonad Instances

@[implicit_reducible]

instance Std.Internal.Do.Id.instWPMonad : WPMonad Id Prop EPost⟨⟩

Id is a WPMonad with Prop assertions and no exceptions.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.Internal.Do.PredTrans.apply_pushExcept {α : Type u_1} {ε : Type u_2} {Pred : Type u_3} {EPred : Type u_4} (x : PredTrans Pred EPred (Except ε α)) (post : α → Pred) (epost : EPost.cons✝ (ε → Pred) EPred) : x.pushExcept.apply post epost = x.apply (EPost.cons.pushExcept post epost) epost.tail

@[implicit_reducible]

instance Std.Internal.Do.ExceptT.instWPMonad {m : Type u → Type z} {EPred : Type u_1} {ε : Type u} {Pred : Type v} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (ExceptT ε m) Pred (EPost.cons✝ (ε → Pred) EPred)

ExceptT lifts a WPMonad instance by adding an exception postcondition layer.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.Internal.Do.ExceptT.apply_wp {m : Type u → Type z} {α ε : Type u} {Pred : Type u_1} {EPred : Type u_2} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : ExceptT ε m α) (post : α → Pred) (epost : EPost.cons✝ (ε → Pred) EPred) : wp x post epost = wp x.run (EPost.cons.pushExcept post epost) epost.tail

@[implicit_reducible]

instance Std.Internal.Do.OptionT.instWPMonad {m : Type u → Type z} {EPred : Type u_1} {Pred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (OptionT m) Pred (EPost.cons✝ Pred EPred)

OptionT lifts a WPMonad instance by adding a PUnit exception postcondition layer.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.Internal.Do.OptionT.apply_wp {m : Type u → Type z} {α Pred : Type u} {EPred : Type u_1} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : OptionT m α) (post : α → Pred) (epost : EPost.cons✝ Pred EPred) : wp x post epost = wp x.run (EPost.cons.pushOption post epost) epost.tail

@[implicit_reducible, instance 100]

instance Std.Internal.Do.StateT.instWPMonad {m : Type u → Type z} {EPred : Type v} {σ : Type u} {Pred : Type w} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (StateT σ m) (σ → Pred) EPred

StateT lifts a WPMonad instance by adding a state argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.Internal.Do.StateT.apply_wp {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α σ : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : StateT σ m α) (post : α → σ → Pred) (epost : EPred) (s : σ) : wp x post epost s = wp (x.run s) (fun (x : α × σ) => match x with | (a, s) => post a s) epost

@[implicit_reducible]

instance Std.Internal.Do.ReaderT.instWPMonad {m : Type u → Type z} {EPred : Type u_1} {ρ : Type u} {Pred : Type v} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] : WPMonad (ReaderT ρ m) (ρ → Pred) EPred

ReaderT lifts a WPMonad instance by adding a reader argument.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Std.Internal.Do.ReaderT.apply_wp {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α ρ : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (x : ReaderT ρ m α) (post : α → ρ → Pred) (epost : EPred) (r : ρ) : wp x post epost r = wp (x.run r) (fun (a : α) => post a r) epost

Type Alias Instances

WPMonad instances for concrete monads that are type aliases for transformer stacks.

@[implicit_reducible]

instance Std.Internal.Do.Option.instWPMonad : WPMonad Option Prop Prop

Option is a WPMonad with Prop assertions and a single Prop exception postcondition.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Internal.Do.Except.instWPMonad {ε : Type u_1} : WPMonad (Except ε) Prop EPost⟨ε → Prop⟩

Except ε is a WPMonad with Prop assertions and a single exception postcondition.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Std.Internal.Do.EStateM.instWPMonad {ε σ : Type u_1} : WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop)

EStateM ε σ is a WPMonad combining state and exceptions.

Equations

• One or more equations did not get rendered due to their size.

Adequacy Lemmas

These lemmas bridge wp reasoning to concrete program properties. Each one says: if wp prog ... holds, then a property P holds of the program's result.

theorem Std.Internal.Do.Id.of_wp_run_eq {α : Type u} {x : α} {prog : Id α} (h : prog.run = x) (P : α → Prop) (hwp : wp prog P epost⟨⟩) : P x

Adequacy for Id: if wp prog P holds, then P holds of the result.

theorem Std.Internal.Do.Option.of_wp_eq {α : Type u} {x prog : Option α} (h : prog = x) (P : Option α → Prop) (hwp : wp prog (fun (a : α) => P (some a)) (P none)) : P x

Adequacy for Option: if wp prog P holds, then P holds of the result.

theorem Std.Internal.Do.StateM.of_wp_run_eq {α σ : Type u_1} {x : α × σ} {prog : StateM σ α} {s : σ} (h : StateT.run prog s = x) (P : α × σ → Prop) (hwp : wp prog (fun (a : α) (s' : σ) => P (a, s')) epost⟨⟩ s) : P x

Adequacy for StateM: if wp prog P s holds, then P holds of (prog.run s).

theorem Std.Internal.Do.StateM.of_wp_run'_eq {α σ : Type} {x : α} {prog : StateM σ α} {s : σ} (h : StateT.run' prog s = x) (P : α → Prop) (hwp : wp prog (fun (a : α) (x : σ) => P a) epost⟨⟩ s) : P x

Adequacy for StateM (discarding final state).

theorem Std.Internal.Do.ReaderM.of_wp_run_eq {α ρ : Type} {x : α} {prog : ReaderM ρ α} {r : ρ} (h : ReaderT.run prog r = x) (P : α → Prop) (hwp : wp prog (fun (a : α) (x : ρ) => P a) epost⟨⟩ r) : P x

Adequacy for ReaderM: if wp prog P r holds, then P holds of (prog.run r).

theorem Std.Internal.Do.Except.of_wp_eq {ε α : Type} {x prog : Except ε α} (h : prog = x) (P : Except ε α → Prop) (hwp : wp prog (fun (a : α) => P (Except.ok a)) epost⟨fun (e : ε) => P (Except.error e)⟩) : P x

Adequacy for Except: if wp prog P holds, then P holds of the result.

theorem Std.Internal.Do.EStateM.of_wp_run_eq {ε σ α : Type} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} {s : σ} (h : prog.run s = x) (P : EStateM.Result ε σ α → Prop) (hwp : wp prog (fun (a : α) (s' : σ) => P (EStateM.Result.ok a s')) (fun (e : ε) (s' : σ) => P (EStateM.Result.error e s')) s) : P x

Adequacy for EStateM: if wp prog P s holds, then P holds of (prog.run s).