WPMonad Instances

The weakest precondition interpretation of the base monads and of the monad transformers.

A monad that throws carries the exception postcondition itself. A transformer stacks a product layer on the exception postcondition of the monad below it, and EStack⟨⟩ closes the stack.

Pre-defined instances

• WPMonad Id Prop EStack⟨⟩ — pure computations.
• WPMonad (StateT σ m) (σ → Pred) EPred — stateful computations.
• WPMonad (ExceptT ε m) Pred ((ε → Pred) × EPred) — computations with exceptions.
• WPMonad (OptionT m) Pred ((Unit → Pred) × EPred) — computations with early termination.
• WPMonad (ReaderT ρ m) (ρ → Pred) EPred — reader computations.
• WPMonad Option Prop (Unit → Prop) — concrete early termination.
• WPMonad (Except ε) Prop (ε → Prop) — concrete exception type.
• WPMonad (EStateM ε σ) (σ → Prop) (ε → σ → Prop) — concrete error-state monad.

@[instance_reducible]

instance Std.WP.Id.wpInst {α : Type u} : WP (Id α) α Prop EStack⟨⟩

Id's WP interpretation: Prop assertions and no exceptions.

Equations

• Std.WP.Id.wpInst = { wpTrans := fun (x : Id α) => { apply := fun (post : α → Prop) (_epost : EStack⟨⟩) => post x }, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.WP.Id.instWPMonad : WPMonad Id Prop EStack⟨⟩

Id is a WPMonad with Prop assertions and no exceptions.

Equations

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

@[instance_reducible]

instance Std.WP.ExceptT.wpInst {m : Type u → Type z} {EPred : Type u_1} {ε α : Type u} {Pred : Type v} [Assertion Pred] [Assertion EPred] [WP (m (Except ε α)) (Except ε α) Pred EPred] : WP (ExceptT ε m α) α Pred ((ε → Pred) × EPred)

ExceptT's WP interpretation: lift the base interpretation by adding an exception postcondition layer.

Equations

• Std.WP.ExceptT.wpInst = { wpTrans := fun (x : ExceptT ε m α) => (Std.WP.WP.wpTrans x.run).pushExceptT, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.WP.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 ((ε → Pred) × EPred)

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

Equations

• Std.WP.ExceptT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.4) => inferInstance, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.WP.ExceptT.wp_apply_eq {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 : (ε → Pred) × EPred) : wp x post epost = wp x.run (Lean.Order.pushExcept post epost.fst) epost.snd

@[instance_reducible]

instance Std.WP.OptionT.wpInst {m : Type u → Type z} {EPred : Type u_1} {α Pred : Type u} [Assertion Pred] [Assertion EPred] [WP (m (Option α)) (Option α) Pred EPred] : WP (OptionT m α) α Pred ((Unit → Pred) × EPred)

OptionT's WP interpretation: lift the base interpretation by adding a Unit exception postcondition layer.

Equations

• Std.WP.OptionT.wpInst = { wpTrans := fun (x : OptionT m α) => (Std.WP.WP.wpTrans x.run).pushOptionT, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.WP.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 ((Unit → Pred) × EPred)

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

Equations

• Std.WP.OptionT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.3) => inferInstance, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.WP.OptionT.wp_apply_eq {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 : (Unit → Pred) × EPred) : wp x post epost = wp x.run (Lean.Order.pushOption post epost.fst) epost.snd

@[instance_reducible]

instance Std.WP.StateT.wpInst {m : Type u → Type z} {α : Type u} {EPred : Type v} {σ : Type u} {Pred : Type w} [Assertion Pred] [Assertion EPred] [WP (m (α × σ)) (α × σ) Pred EPred] : WP (StateT σ m α) α (σ → Pred) EPred

StateT's WP interpretation: lift the base interpretation by adding a state argument.

Equations

• Std.WP.StateT.wpInst = { wpTrans := fun (x : StateT σ m α) => Lean.Order.PredTrans.pushArg fun (x_1 : σ) => Std.WP.WP.wpTrans (x.run x_1), wp_trans_monotone := ⋯ }

@[instance_reducible, instance 100]

instance Std.WP.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

• Std.WP.StateT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.4) => inferInstance, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.WP.StateT.wp_apply_eq {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

@[instance_reducible]

instance Std.WP.ReaderT.wpInst {m : Type u → Type z} {EPred : Type u_1} {α ρ : Type u} {Pred : Type v} [Assertion Pred] [Assertion EPred] [WP (m α) α Pred EPred] : WP (ReaderT ρ m α) α (ρ → Pred) EPred

ReaderT's WP interpretation: lift the base interpretation by adding a reader argument.

Equations

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

@[instance_reducible]

instance Std.WP.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

• Std.WP.ReaderT.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.4) => inferInstance, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[simp]

theorem Std.WP.ReaderT.wp_apply_eq {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.

@[instance_reducible]

instance Std.WP.Option.wpInst {α : Type u} : WP (Option α) α Prop (Unit → Prop)

Option's WP interpretation: Prop assertions and a Unit-indexed exception postcondition.

Equations

• Std.WP.Option.wpInst = { wpTrans := fun (x : Option α) => { apply := fun (post : α → Prop) (epost : Unit → Prop) => Lean.Order.pushOption post epost x }, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.WP.Option.instWPMonad : WPMonad Option Prop (Unit → Prop)

Option is a WPMonad with Prop assertions and a Unit-indexed exception postcondition.

Equations

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

@[instance_reducible]

instance Std.WP.Except.wpInst {ε : Type u_1} {α : Type u} : WP (Except ε α) α Prop (ε → Prop)

Except ε's WP interpretation: Prop assertions and an ε-indexed exception postcondition.

Equations

• Std.WP.Except.wpInst = { wpTrans := fun (x : Except ε α) => { apply := fun (post : α → Prop) (epost : ε → Prop) => Lean.Order.pushExcept post epost x }, wp_trans_monotone := ⋯ }

@[instance_reducible]

instance Std.WP.Except.instWPMonad {ε : Type u_1} : WPMonad (Except ε) Prop (ε → Prop)

Except ε is a WPMonad with Prop assertions and an ε-indexed exception postcondition.

Equations

• Std.WP.Except.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type ?u.1) => inferInstance, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }

@[instance_reducible]

instance Std.WP.EStateM.wpInst {ε σ α : Type} : WP (EStateM ε σ α) α (σ → Prop) (ε → σ → Prop)

EStateM ε σ's WP interpretation combining state and exceptions.

Equations

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

@[instance_reducible]

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

EStateM ε σ is a WPMonad combining state and exceptions.

Equations

• Std.WP.EStateM.instWPMonad = { toLawfulMonad := ⋯, toWP := fun (x : Type) => inferInstance, pure_le_wp_pure := ⋯, bind_le_wp_bind := ⋯ }