# Weakest precondition interpretation #

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

This interpretation forms the basis of our notion of Hoare triples. It is the main mechanism of this library for reasoning about monadic programs.

An instance `WP m ps` determines an interpretation `wp⟦x⟧` of a program `x : m α` in terms of a predicate transformer `PredTrans ps α`; The monad `m` determines `ps : PostShape` and hence the particular shape of the predicate transformer.

This library comes with pre-defined instances for common monads and transformers such as

- `WP Id .pure`, interpreting pure computations `x : Id α` in terms of a function (isomorphic to) `(α → Prop) → Prop`.
- `WP (StateT σ m) (.arg σ ps)` given an instance `WP m ps`, interpreting `StateM σ α` in terms of a function `(α → σ → Prop) → σ → Prop`.
- `WP (ExceptT ε m) (.except ε ps)` given an instance `WP m ps`, interpreting `Except ε α` in terms of `(α → Prop) → (ε → Prop) → Prop`.
- `WP (EStateM ε σ) (.except ε (.arg σ .pure))` interprets `EStateM ε σ α` in terms of a function `(α → σ → Prop) → (ε → σ → Prop) → σ → Prop`.

These instances are all monad morphisms, a fact which is properly encoded and exploited by the subclass `WPMonad`.

source
class Std.Do.WP (m : Type u → Type v) (ps : outParam PostShape) :
Type (max (u + 1) v)

A weakest precondition interpretation of a monadic program `x : m α` in terms of a predicate transformer `PredTrans ps α`. The monad `m` determines `ps : PostShape`. See the module comment for more details.

- wp {α : Type u} (x : m α) : PredTrans ps α

  Interpret a monadic program `x : m α` in terms of a predicate transformer `PredTrans ps α`.

Instances

source
def Std.Do.«termWp⟦_:_⟧» :
Lean.ParserDescr

`wp⟦x⟧ Q` is defined as `(WP.wp x).apply Q`.

Equations

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

Instances For

source
def Std.Do.unexpandWP :
Lean.PrettyPrinter.Unexpander
Equations

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

Instances For

source
instance Std.Do.Id.instWP :
WP Id PostShape.pure
Equations

- Std.Do.Id.instWP = { wp := fun {α : Type ?u.7} (x : Id α) => Std.Do.PredTrans.pure x.run }

source
instance Std.Do.StateT.instWP {m : Type u → Type v} {ps : PostShape} {σ : Type u} [WP m ps] :
WP (StateT σ m) (PostShape.arg σ ps)
Equations

- Std.Do.StateT.instWP = { wp := fun {α : Type ?u.30} (x : StateT σ m α) => Std.Do.PredTrans.pushArg fun (s : σ) => Std.Do.wp (x s) }

source
instance Std.Do.ReaderT.instWP {m : Type u → Type v} {ps : PostShape} {ρ : Type u} [WP m ps] :
WP (ReaderT ρ m) (PostShape.arg ρ ps)
Equations

- Std.Do.ReaderT.instWP = { wp := fun {α : Type ?u.31} (x : ReaderT ρ m α) => Std.Do.PredTrans.pushArg fun (s : ρ) => (fun (x : α) => (x, s)) <$> Std.Do.wp (x s) }

source
instance Std.Do.ExceptT.instWP {m : Type u → Type v} {ps : PostShape} {ε : Type u} [WP m ps] :
WP (ExceptT ε m) (PostShape.except ε ps)
Equations

- Std.Do.ExceptT.instWP = { wp := fun {α : Type ?u.29} (x : ExceptT ε m α) => Std.Do.PredTrans.pushExcept (Std.Do.wp x) }

source
instance Std.Do.OptionT.instWP {m : Type u → Type v} {ps : PostShape} [WP m ps] :
WP (OptionT m) (PostShape.except PUnit ps)
Equations

- Std.Do.OptionT.instWP = { wp := fun {α : Type ?u.25} (x : OptionT m α) => Std.Do.PredTrans.pushOption (Std.Do.wp x) }

source
instance Std.Do.EStateM.instWP {ε σ : Type u_1} :
WP (EStateM ε σ) (PostShape.except ε (PostShape.arg σ PostShape.pure))
Equations

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

source
instance Std.Do.State.instWP {σ : Type u_1} :
WP (StateM σ) (PostShape.arg σ PostShape.pure)
Equations

- Std.Do.State.instWP = inferInstanceAs (Std.Do.WP (StateT σ Id) (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))

source
instance Std.Do.Reader.instWP {ρ : Type u_1} :
WP (ReaderM ρ) (PostShape.arg ρ PostShape.pure)
Equations

- Std.Do.Reader.instWP = inferInstanceAs (Std.Do.WP (ReaderT ρ Id) (Std.Do.PostShape.arg ρ Std.Do.PostShape.pure))

source
instance Std.Do.Except.instWP {ε : Type u_1} :
WP (Except ε) (PostShape.except ε PostShape.pure)
Equations

- Std.Do.Except.instWP = inferInstanceAs (Std.Do.WP (ExceptT ε Id) (Std.Do.PostShape.except ε Std.Do.PostShape.pure))

source
instance Std.Do.Option.instWP :
WP Option (PostShape.except PUnit PostShape.pure)
Equations

- Std.Do.Option.instWP = inferInstanceAs (Std.Do.WP (OptionT Id) (Std.Do.PostShape.except PUnit Std.Do.PostShape.pure))

source
theorem Std.Do.Id.of_wp_run_eq {α : Type u} {x : α} {prog : Id α} (h : prog.run = x) (P : α → Prop) :
(⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) => { down := P a })) → P x

Adequacy lemma for `Id.run`. Useful if you want to prove a property about an expression `x` defined as `Id.run prog` and you want to use `mvcgen` to reason about `prog`.

source
theorem Std.Do.StateM.of_wp_run_eq {σ : Type u_1} {s : σ} {α : Type u_1} {x : α × σ} {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σ → Prop) :
(⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) (s' : σ) => ⌜P (a, s')⌝) s) → P x

Adequacy lemma for `StateM.run`. Useful if you want to prove a property about an expression `x` defined as `StateM.run prog s` and you want to use `mvcgen` to reason about `prog`.

source
theorem Std.Do.StateM.of_wp_run'_eq {σ : Type u_1} {s : σ} {α : Type u_1} {x : α} {prog : StateM σ α} (h : StateT.run' prog s = x) (P : α → Prop) :
(⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) => ⌜P a⌝) s) → P x

Adequacy lemma for `StateM.run'`. Useful if you want to prove a property about an expression `x` defined as `StateM.run' prog s` and you want to use `mvcgen` to reason about `prog`.

source
theorem Std.Do.ReaderM.of_wp_run_eq {ρ : Type u_1} {r : ρ} {α : Type u_1} {x : α} {prog : ReaderM ρ α} (h : ReaderT.run prog r = x) (P : α → Prop) :
(⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun (a : α) (x : ρ) => ⌜P a⌝) r) → P x

Adequacy lemma for `ReaderM.run`. Useful if you want to prove a property about an expression `x` defined as `ReaderM.run prog r` and you want to use `mvcgen` to reason about `prog`.

source
theorem Std.Do.Except.of_wp {ε α : Type} {prog : Except ε α} (P : Except ε α → Prop) :
(⊢ₛ wp⟦prog⟧ (fun (a : α) => ⌜P (Except.ok a)⌝, fun (e : ε) => ⌜P (Except.error e)⌝, ())) → P prog

Adequacy lemma for `Except`. Useful if you want to prove a property about an expression `prog : Except ε α` and you want to use `mvcgen` to reason about `prog`.

source
theorem Std.Do.EStateM.of_wp_run_eq {ε σ : Type} {s : σ} {α : Type} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α} (h : prog.run s = x) (P : EStateM.Result ε σ α → Prop) :
(⊢ₛ wp⟦prog⟧ (fun (a : α) (s' : σ) => ⌜P (EStateM.Result.ok a s')⌝, fun (e : ε) (s' : σ) => ⌜P (EStateM.Result.error e s')⌝, ()) s) → P x

Adequacy lemma for `EStateM.run`. Useful if you want to prove a property about an expression `x` defined as `EStateM.run prog s` and you want to use `mvcgen` to reason about `prog`.