Weakest Precondition Interpretation

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

An instance WP 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 and Assertion are both just alias type classes for CompleteLattice. We introduce them for readability: Assertion Pred marks Pred as the assertion language for normal postconditions, while Assertion EPred marks EPred as the type of exception postconditions.

Pre-defined instances

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

class Std.Do'.Assertion (α : Type w) extends Lean.Order.CompleteLattice α : Type w

An assertion type is equipped with a CompleteLattice structure, used as the carrier for pre- and postconditions.

• rel : α → α → Prop
• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y
• has_sup (c : α → Prop) : Exists (is_sup c)

@[implicit_reducible]

def Std.Do'.instCCPOOfAssertion {EPred : Type u_1} [Assertion EPred] : Lean.Order.CCPO EPred

An assertion type is a chain-complete partial order.

WP Typeclass

The WP typeclass defines weakest precondition semantics for monads. A WP 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.Do'.WP (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 WP 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 WP of >>=.

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

  Monotonicity: weaker postconditions yield weaker preconditions.

def Std.Do'.wp {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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.

@[simp]

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

Derived WP Lemmas

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

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

theorem Std.Do'.WP.wp_bind {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α β : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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.Do'.WP.wp_consequence {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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.Do'.WP.wp_consequence_econs {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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.Do'.WP.wp_econs {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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.Do'.WP.wp_econs_bot {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (x : m α) (post : α → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x post Lean.Order.bot) (wp x post epost)

theorem Std.Do'.WP.wp_consequence_rel {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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.Do'.WP.wp_econs_rel {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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.Do'.WP.wp_econs_bot_rel {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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.Do'.WP.wp_map {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α β : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (f : α → β) (x : m α) (post : β → Pred) (epost : EPred) : Lean.Order.PartialOrder.rel (wp x (fun (a : α) => post (f a)) epost) (wp (f <$> x) post epost)

theorem Std.Do'.WP.wp_map' {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α β : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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)

theorem Std.Do'.WP.wp_seq {m : Type u → Type z} {Pred : Type u_1} {EPred : Type u_2} {α β : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] (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)

WP Instances

@[implicit_reducible]

instance Std.Do'.Id.instWP : WP Id Prop EPost⟨⟩

Id is a WP with Prop assertions and no exceptions.

@[simp]

theorem Std.Do'.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.Do'.ExceptT.instWP {m : Type u → Type z} {EPred : Type u_1} {ε : Type u} {Pred : Type v} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] : WP (ExceptT ε m) Pred (EPost.cons✝ (ε → Pred) EPred)

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

@[simp]

theorem Std.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] [WP 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.Do'.OptionT.instWP {m : Type u → Type z} {EPred : Type u_1} {Pred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] : WP (OptionT m) Pred (EPost.cons✝ Pred EPred)

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

@[simp]

theorem Std.Do'.OptionT.apply_wp {m : Type u → Type z} {α Pred : Type u} {EPred : Type u_1} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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.Do'.StateT.instWP {m : Type u → Type z} {EPred : Type v} {σ : Type u} {Pred : Type w} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] : WP (StateT σ m) (σ → Pred) EPred

StateT lifts a WP instance by adding a state argument.

@[simp]

theorem Std.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] [WP 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.Do'.ReaderT.instWP {m : Type u → Type z} {EPred : Type u_1} {ρ : Type u} {Pred : Type v} [Monad m] [Assertion Pred] [Assertion EPred] [WP m Pred EPred] : WP (ReaderT ρ m) (ρ → Pred) EPred

ReaderT lifts a WP instance by adding a reader argument.

@[simp]

theorem Std.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] [WP 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

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

@[implicit_reducible]

instance Std.Do'.Option.instWP : WP Option Prop Prop

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

@[implicit_reducible]

instance Std.Do'.Except.instWP {ε : Type u_1} : WP (Except ε) Prop EPost⟨ε → Prop⟩

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

@[implicit_reducible]

instance Std.Do'.EStateM.instWP {ε σ : Type u_1} : WP (EStateM ε σ) (σ → Prop) (ε → σ → Prop)

EStateM ε σ is a WP combining state and exceptions.

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.Do'.Id.of_wp_run_eq {α : Type u} {x : α} {prog : Id α} (h : prog.run = x) (P : α → Prop) (hwp : wp prog P epost⟨⟩) : P x

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

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

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

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

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

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