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⟧ Q of x : m α for the postcondition Q. It is thus defined in terms of an instance WP m ps.

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

• ⦃P⦄ x ⦃Q⦄ = (P ⊢ₛ (Std.Do.wp x).apply Q)

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.

def Std.Do.unexpandTriple : Lean.PrettyPrinter.Unexpander

Equations

• One or more equations did not get rendered due to their size.

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)

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⦄

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⦄

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₂⦄

Conjunction for two Hoare triple specifications of a program x. This theorem is useful for decomposing proofs, because unrelated facts about x can be proven separately and then combined with this theorem.

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₂⦄

Modus ponens for two Hoare triple specifications of a program x. This theorem is useful for separating proofs. If h₁ : Triple x P₁ Q₁ proves a basic property about x and h₂ : Triple x P₂ (Q₁ →ₚ Q₂) is an advanced proof for Q₂ that builds on the basic proof for Q₁, then mp x h₁ h₂ is a proof for Q₂ about x.