Hoare triples

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

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

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

structure Std.WP.Triple {Pred : Type w} {EPosts : Type w'} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] (x : Prog) [WP Prog Value Pred EPosts] (pre : Pred) (post : Value → Pred) (eposts : EPosts) : Prop

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

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

  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} {EPosts : Type w'} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {pre : Pred} {post : Value → Pred} {eposts : EPosts} : ⦃ pre ⦄ x ⦃ post; eposts ⦄ ↔ Lean.Order.PartialOrder.rel pre (wp x post eposts)

theorem Std.WP.Triple.iff_conseq {Pred : Type w} {EPosts : Type w'} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {pre : Pred} {post : Value → Pred} {eposts : EPosts} : ⦃ pre ⦄ x ⦃ post; eposts ⦄ ↔ ∀ (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' eposts)

theorem Std.WP.Triple.entails_wp_of_pre_post {Pred : Type w} {EPosts : Type w'} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {pre pre' : Pred} {post post' : Value → Pred} {eposts : EPosts} (h : ⦃ pre' ⦄ x ⦃ post'; eposts ⦄) (hpre : Lean.Order.PartialOrder.rel pre pre') (hpost : Lean.Order.PartialOrder.rel post' post) : Lean.Order.PartialOrder.rel pre (wp x post eposts)

theorem Std.WP.Triple.entails_wp_of_pre {Pred : Type w} {EPosts : Type w'} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {pre pre' : Pred} {post : Value → Pred} {eposts : EPosts} (h : ⦃ pre' ⦄ x ⦃ post; eposts ⦄) (hpre : Lean.Order.PartialOrder.rel pre pre') : Lean.Order.PartialOrder.rel pre (wp x post eposts)

theorem Std.WP.Triple.entails_wp_of_post {Pred : Type w} {EPosts : Type w'} {Prog : Type u} {Value : Type v} [Assertion Pred] [Assertion EPosts] [WP Prog Value Pred EPosts] {x : Prog} {pre : Pred} {post post' : Value → Pred} {eposts : EPosts} (h : ⦃ pre ⦄ x ⦃ post'; eposts ⦄) (hpost : Lean.Order.PartialOrder.rel post' post) : Lean.Order.PartialOrder.rel pre (wp x post eposts)