Hoare triples

Hoare triples form the basis for compositional functional correctness proofs about monadic programs.

As usual, Triple pre x post epost holds iff the precondition pre entails the weakest precondition wp x post epost of x : m α for the postcondition post and error postcondition epost. It is thus defined in terms of an instance WPMonad m Pred EPred.

structure Std.Internal.Do.Triple {m : Type u → Type v} {Pred EPred α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] (pre : Pred) (x : m α) (post : α → Pred) (epost : EPred) : Prop

A Hoare triple for reasoning about monadic programs. A Hoare triple Triple pre x post epost is a specification for x: if assertion pre holds before x, then postcondition post holds after running x (and epost handles any errors).

• intro :: (
• le_wp : Lean.Order.PartialOrder.rel pre (wp x post epost)

  The weakest precondition entailment witnessing the triple.

• )

def Std.Internal.Do.«term⦃_⦄_⦃_⦄» : Lean.ParserDescr

Hoare triple notation without exception postcondition (defaults to ⊥).

Equations

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

def Std.Internal.Do.«term⦃_⦄_⦃_,_⦄» : Lean.ParserDescr

Hoare triple notation with a binder for the return value.

Equations

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

def Std.Internal.Do.tripleEPost : Lean.ParserDescr

Hoare triple notation with explicit exception postconditions: ⦃ P ⦄ x ⦃ Q; E₁; … ⦄ := Triple P x Q epost⟨E₁, …⟩.

Equations

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

def Std.Internal.Do.unexpandTripleEPost : Lean.PrettyPrinter.Unexpander

Pretty-print Triple P c Q epost⟨E₁, …⟩ back as ⦃ P ⦄ c ⦃ Q; E₁; … ⦄.

Equations

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

theorem Std.Internal.Do.Triple.iff {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {x : m α} {pre : Pred} {post : α → Pred} {epost : EPred} : Triple pre x post epost ↔ Lean.Order.PartialOrder.rel pre (wp x post epost)

theorem Std.Internal.Do.Triple.iff_conseq {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {x : m α} {pre : Pred} {post : α → Pred} {epost : EPred} : Triple pre x post epost ↔ ∀ (pre' : Pred) (post' : α → Pred), Lean.Order.PartialOrder.rel pre' pre → Lean.Order.PartialOrder.rel post post' → Lean.Order.PartialOrder.rel pre' (wp x post' epost)

theorem Std.Internal.Do.Triple.entails_wp_of_pre_post {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {x : m α} {pre pre' : Pred} {post post' : α → Pred} {epost : EPred} (h : Triple pre' x post' epost) (hpre : Lean.Order.PartialOrder.rel pre pre') (hpost : Lean.Order.PartialOrder.rel post' post) : Lean.Order.PartialOrder.rel pre (wp x post epost)

theorem Std.Internal.Do.Triple.entails_wp_of_pre {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {x : m α} {pre pre' : Pred} {post : α → Pred} {epost : EPred} (h : Triple pre' x post epost) (hpre : Lean.Order.PartialOrder.rel pre pre') : Lean.Order.PartialOrder.rel pre (wp x post epost)

theorem Std.Internal.Do.Triple.entails_wp_of_post {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {x : m α} {pre : Pred} {post post' : α → Pred} {epost : EPred} (h : Triple pre x post' epost) (hpost : Lean.Order.PartialOrder.rel post' post) : Lean.Order.PartialOrder.rel pre (wp x post epost)

theorem Std.Internal.Do.Triple.pure {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α : Type u} {pre : Pred} {post : α → Pred} {epost : EPred} (a : α) (h : Lean.Order.PartialOrder.rel pre (post a)) : Triple pre (Pure.pure a) post epost

theorem Std.Internal.Do.Triple.bind {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} {pre : Pred} {epost : EPred} {post : β → Pred} (x : m α) (f : α → m β) (mid : α → Pred) (hx : Triple pre x mid epost) (hf : ∀ (a : α), Triple (mid a) (f a) post epost) : Triple pre (x >>= f) post epost

theorem Std.Internal.Do.Triple.map {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} {pre : Pred} {post : β → Pred} {epost : EPred} (f : α → β) (x : m α) (h : Triple pre x (fun (a : α) => post (f a)) epost) : Triple pre (f <$> x) post epost

theorem Std.Internal.Do.Triple.seq {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {α β : Type u} {pre : Pred} {post : β → Pred} {epost : EPred} (x : m (α → β)) (y : m α) (h : Triple pre x (fun (f : α → β) => wp y (fun (a : α) => post (f a)) epost) epost) : Triple pre (x <*> y) post epost