Hoare triples

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

As usual, Triple x pre 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 {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [Assertion Pred] [Assertion EPred] (x : Prog) [WP Prog Value Pred EPred] (pre : Pred) (post : Value → Pred) (epost : EPred) : Prop

A Hoare triple for reasoning about programs. A Hoare triple Triple x pre 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.tripleNotation : Lean.ParserDescr

Hoare triple notation without exception postcondition (defaults to ⊥). An optional (m := …) after the precondition ascribes the program to monad ….

Equations

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

def Std.Internal.Do.tripleBinderNotation : 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 an exception postcondition: ⦃ P ⦄ x ⦃ Q; E ⦄ := Triple x P Q E.

Equations

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

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

Hoare triple notation with a binder for the return value and an exception postcondition.

Equations

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

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

Pretty-print Triple applications back as ⦃ … ⦄ notation.

Equations

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

theorem Std.Internal.Do.Triple.iff {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} {pre : Pred} {post : Value → Pred} {epost : EPred} : ⦃ pre ⦄ x ⦃ post; epost ⦄ ↔ Lean.Order.PartialOrder.rel pre (wp x post epost)

theorem Std.Internal.Do.Triple.iff_conseq {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} {pre : Pred} {post : Value → Pred} {epost : EPred} : ⦃ pre ⦄ x ⦃ post; epost ⦄ ↔ ∀ (pre' : Pred) (post' : Value → 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 {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} {pre pre' : Pred} {post post' : Value → Pred} {epost : EPred} (h : ⦃ 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 {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} {pre pre' : Pred} {post : Value → Pred} {epost : EPred} (h : ⦃ 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 {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [Assertion Pred] [Assertion EPred] [WP Prog Value Pred EPred] {x : Prog} {pre : Pred} {post post' : Value → Pred} {epost : EPred} (h : ⦃ 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} [Assertion Pred] [Assertion EPred] [Monad m] [WPMonad m Pred EPred] {α : Type u} {pre : Pred} {post : α → Pred} {epost : EPred} (a : α) (h : Lean.Order.PartialOrder.rel pre (post a)) : ⦃ pre ⦄ Pure.pure a ⦃ post; epost ⦄

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

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

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