Documentation

Loom.Triple.Basic

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 WP m Pred EPred.

source
inductive Std.Do'.Triple {m : Type u → Type v} {Pred EPred α : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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).

Instances For
    source
    def Std.Do'.«term⦃_⦄_⦃_⦄» :
    Lean.ParserDescr

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

    Instances For
      source
      def Std.Do'.«term⦃_⦄_⦃_,_⦄» :
      Lean.ParserDescr

      Hoare triple notation with a binder for the return value.

      Instances For
        source
        theorem Std.Do'.Triple.iff {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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)
        source
        theorem Std.Do'.Triple.iff_conseq {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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)
        source
        theorem Std.Do'.Triple.entails_wp_of_pre_post {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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)
        source
        theorem Std.Do'.Triple.entails_wp_of_pre {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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)
        source
        theorem Std.Do'.Triple.entails_wp_of_post {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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)
        source
        theorem Std.Do'.Triple.pure {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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
        source
        theorem Std.Do'.Triple.bind {m : Type u → Type v} {Pred EPred : Type u} [Monad m] [Assertion Pred] [Assertion EPred] [WP 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