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 Hoare triple 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 Hoare triple 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

Unexpands Hoare triples to their high-level syntax during pretty printing.

Equations

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

theorem Std.Do.Triple.iff {m : Type u → Type v} {ps : PostShape} [WP m ps] {α : Type u} {x : m α} {P : Assertion ps} {Q : PostCond α ps} : ⦃P⦄ x ⦃Q⦄ ↔ P ⊢ₛ wp⟦x⟧ Q

theorem Std.Do.Triple.iff_conseq {m : Type u → Type v} {ps : PostShape} [WP m ps] {α : Type u} {x : m α} {P : Assertion ps} {Q : PostCond α ps} : ⦃P⦄ x ⦃Q⦄ ↔ ∀ ⦃P' : SPred ps.args⦄ ⦃Q' : PostCond α ps⦄, (P' ⊢ₛ P) → Q.entails Q' → P' ⊢ₛ wp⟦x⟧ Q'

theorem Std.Do.Triple.entails_wp_of_pre_post {m : Type u → Type v} {ps : PostShape} [WP m ps] {α : Type u} {x : m α} {P P' : Assertion ps} {Q Q' : PostCond α ps} (h : ⦃P'⦄ x ⦃Q'⦄) (hpre : P ⊢ₛ P') (hpost : Q'.entails Q) : P ⊢ₛ wp⟦x⟧ Q

theorem Std.Do.Triple.entails_wp_of_pre {m : Type u → Type v} {ps : PostShape} [WP m ps] {α : Type u} {x : m α} {P P' : Assertion ps} {Q : PostCond α ps} (h : ⦃P'⦄ x ⦃Q⦄) (hpre : P ⊢ₛ P') : P ⊢ₛ wp⟦x⟧ Q

theorem Std.Do.Triple.entails_wp_of_post {m : Type u → Type v} {ps : PostShape} [WP m ps] {α : Type u} {x : m α} {P : Assertion ps} {Q Q' : PostCond α ps} (h : ⦃P⦄ x ⦃Q'⦄) (hpost : Q'.entails Q) : P ⊢ₛ wp⟦x⟧ Q

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.