Documentation

Std.Do.Triple.Basic

Hoare triples #

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

As usual, Triple x P Q holds iff the precondition P entails the weakest precondition wp⟦x⟧.apply Q of x : m α for the postcondition Q. It is thus defined in terms of an instance WP m ps.

source
def Std.Do.Triple {m : Type u → Type v} {ps : PostShape} [WP m ps] {α : Type u} (x : m α) (P : Assertion ps) (Q : PostCond α ps) :
Prop

A Hoare triple for reasoning about monadic programs. A proof for Triple x P Q is a specification for x: If assertion P holds before x, then postcondition Q holds after running x.

⦃P⦄ x ⦃Q⦄ is convenient syntax for Triple x P Q.

Equations
Instances For
    source
    def Std.Do.triple :
    Lean.ParserDescr

    A Hoare triple for reasoning about monadic programs. A proof for Triple x P Q is a specification for x: If assertion P holds before x, then postcondition Q holds after running x.

    ⦃P⦄ x ⦃Q⦄ is convenient syntax for Triple x P Q.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Std.Do.unexpandTriple :
      Lean.PrettyPrinter.Unexpander
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Std.Do.Triple.instPropAsSPredTautologyImpApplyWp {m : Type u → Type v} {ps : PostShape} {α : Type u} {P : Assertion ps} {Q : PostCond α ps} [WP m ps] (x : m α) :
        SPred.Tactic.PropAsSPredTautology (⦃P⦄ x ⦃Q⦄) spred(P → wp⟦x⟧ Q)
        source
        theorem Std.Do.Triple.pure {m : Type u → Type v} {ps : PostShape} {P : SPred ps.args} [Monad m] [WPMonad m ps] {α : Type u} {Q : PostCond α ps} (a : α) (himp : P ⊢ₛ Q.fst a) :
        ⦃P⦄ Pure.pure a ⦃Q⦄
        source
        theorem Std.Do.Triple.bind {m : Type u → Type v} {ps : PostShape} [Monad m] [WPMonad m ps] {α β : Type u} {P : Assertion ps} {Q : α → Assertion ps} {R : PostCond β ps} (x : m α) (f : α → m β) (hx : ⦃P⦄ x ⦃(Q, R.snd)⦄) (hf : ∀ (b : α), ⦃Q b⦄ f b ⦃R⦄) :
        ⦃P⦄ (x >>= f) ⦃R⦄
        source
        theorem Std.Do.Triple.and {m : Type u → Type v} {ps : PostShape} {α : Type u} {P₁ : Assertion ps} {Q₁ : PostCond α ps} {P₂ : Assertion ps} {Q₂ : PostCond α ps} [WP m ps] (x : m α) (h₁ : ⦃P₁⦄ x ⦃Q₁⦄) (h₂ : ⦃P₂⦄ x ⦃Q₂⦄) :
        ⦃P₁ ∧ P₂⦄ x ⦃Q₁.and Q₂⦄
        source
        theorem Std.Do.Triple.mp {m : Type u → Type v} {ps : PostShape} {α : Type u} {P₁ : Assertion ps} {Q₁ : PostCond α ps} {P₂ : Assertion ps} {Q₂ : PostCond α ps} [WP m ps] (x : m α) (h₁ : ⦃P₁⦄ x ⦃Q₁⦄) (h₂ : ⦃P₂⦄ x ⦃Q₁.imp Q₂⦄) :
        ⦃P₁ ∧ P₂⦄ x ⦃Q₁.and Q₂⦄