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 → Type u} {ps : PostShape} [WP m ps] {α : Type} (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
      instance Std.Do.Triple.instPropAsSPredTautologyImpApplyWp {m : Type → Type u} {ps : PostShape} {α : Type} {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 → Type u} {ps : PostShape} {P : SPred ps.args} [Monad m] [WPMonad m ps] {α : Type} {Q : PostCond α ps} (a : α) (himp : P ⊢ₛ Q.fst a) :
      ⦃P⦄ Pure.pure a ⦃Q⦄
      source
      theorem Std.Do.Triple.bind {m : Type → Type u} {ps : PostShape} [Monad m] [WPMonad m ps] {α β : Type} {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 → Type u} {ps : PostShape} {α : Type} {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₁ ∧ₚ Q₂⦄
      source
      theorem Std.Do.Triple.rewrite_program {m : Type → Type u} {ps : PostShape} {α : Type} {P : Assertion ps} {Q : PostCond α ps} [WP m ps] {prog₁ prog₂ : m α} (heq : prog₁ = prog₂) (hprf : ⦃P⦄ prog₂ ⦃Q⦄) :
      ⦃P⦄ prog₁ ⦃Q⦄