Hoare triples

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

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

The triples for the monadic combinators are in Std.WP.Triple.Monad.

structure Std.WP.Triple {Pred : Type w} {EPred : Type w'} {Prog : Type u} {Value : Type v} [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.WP.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.WP.tripleExceptPost : 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.WP.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.WP.Triple.iff {Pred : Type w} {EPred : Type w'} {Prog : Type u} {Value : Type v} [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.WP.Triple.iff_conseq {Pred : Type w} {EPred : Type w'} {Prog : Type u} {Value : Type v} [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.WP.Triple.entails_wp_of_pre_post {Pred : Type w} {EPred : Type w'} {Prog : Type u} {Value : Type v} [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.WP.Triple.entails_wp_of_pre {Pred : Type w} {EPred : Type w'} {Prog : Type u} {Value : Type v} [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.WP.Triple.entails_wp_of_post {Pred : Type w} {EPred : Type w'} {Prog : Type u} {Value : Type v} [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)