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.

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 α.

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.

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

Equations

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

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 }

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) }

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) }

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) }

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) }

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.

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))

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))

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))

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))

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.

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.

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.

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.

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.

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.