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 α

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

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

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

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

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

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

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

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