Pre and postconditions

This module defines Assertion and PostCond, the types which constitute the pre and postconditions of a Hoare triple in the program logic.

Predicate shapes

Since WP supports arbitrary monads, PostCond must be general enough to cope with state and exceptions. For this reason, PostCond is indexed by a PostShape which is an abstraction of the stack of effects supported by the monad, corresponding directly to StateT and ExceptT layers in a transformer stack. For every StateT σ effect, we get one PostShape.arg σ layer, whereas for every ExceptT ε effect, we get one PostShape.except ε layer. Currently, the only supported base layer is PostShape.pure.

Pre and postconditions

The type of preconditions Assertion ps is distinct from the type of postconditions PostCond α ps.

This is because postconditions not only specify what happens upon successful termination of the program, but also need to specify a property that holds upon failure. We get one "barrel" for the success case, plus one barrel per PostShape.except layer.

It does not make much sense to talk about failure barrels in the context of preconditions. Hence, Assertion ps is defined such that all PostShape.except layers are discarded from ps, via PostShape.args.

inductive Std.Do.PostShape : Type 1

• pure : PostShape
• arg (σ : Type) : PostShape → PostShape
• except (ε : Type) : PostShape → PostShape

@[reducible, inline]

abbrev Std.Do.PostShape.args : PostShape → List Type

@[reducible, inline]

abbrev Std.Do.Assertion (ps : PostShape) : Type

An assertion on the .args in the given predicate shape.

example : Assertion (.arg ρ .pure) = (ρ → Prop) := rfl
example : Assertion (.except ε .pure) = Prop := rfl
example : Assertion (.arg σ (.except ε .pure)) = (σ → Prop) := rfl
example : Assertion (.except ε (.arg σ .pure)) = (σ → Prop) := rfl

This is an abbreviation for SPred under the hood, so all theorems about SPred apply.

def Std.Do.FailConds : PostShape → Type

Encodes one continuation barrel for each PostShape.except in the given predicate shape.

example : FailConds (.pure) = Unit := rfl
example : FailConds (.except ε .pure) = ((ε → Prop) × Unit) := rfl
example : FailConds (.arg σ (.except ε .pure)) = ((ε → Prop) × Unit) := rfl
example : FailConds (.except ε (.arg σ .pure)) = ((ε → σ → Prop) × Unit) := rfl

def Std.Do.FailConds.const {ps : PostShape} (p : Prop) : FailConds ps

def Std.Do.FailConds.true {ps : PostShape} : FailConds ps

def Std.Do.FailConds.false {ps : PostShape} : FailConds ps

instance Std.Do.instInhabitedFailConds {ps : PostShape} : Inhabited (FailConds ps)

def Std.Do.FailConds.entails {ps : PostShape} (x y : FailConds ps) : Prop

def Std.Do.«term_⊢ₑ_» : Lean.TrailingParserDescr

@[simp]

theorem Std.Do.FailConds.entails.refl {ps : PostShape} (x : FailConds ps) : x ⊢ₑ x

theorem Std.Do.FailConds.entails.rfl {ps : PostShape} {x : FailConds ps} : x ⊢ₑ x

theorem Std.Do.FailConds.entails.trans {ps : PostShape} {x y z : FailConds ps} : (x ⊢ₑ y) → (y ⊢ₑ z) → x ⊢ₑ z

@[simp]

theorem Std.Do.FailConds.entails_false {ps : PostShape} {x : FailConds ps} : false ⊢ₑ x

@[simp]

theorem Std.Do.FailConds.entails_true {ps : PostShape} {x : FailConds ps} : x ⊢ₑ true

def Std.Do.FailConds.and {ps : PostShape} (x y : FailConds ps) : FailConds ps

def Std.Do.«term_∧ₑ_» : Lean.TrailingParserDescr

theorem Std.Do.FailConds.and_true {ps : PostShape} {x : FailConds ps} : x ∧ₑ true ⊢ₑ x

theorem Std.Do.FailConds.true_and {ps : PostShape} {x : FailConds ps} : true ∧ₑ x ⊢ₑ x

theorem Std.Do.FailConds.and_false {ps : PostShape} {x : FailConds ps} : x ∧ₑ false ⊢ₑ false

theorem Std.Do.FailConds.false_and {ps : PostShape} {x : FailConds ps} : false ∧ₑ x ⊢ₑ false

theorem Std.Do.FailConds.and_eq_left {ps : PostShape} {p q : FailConds ps} (h : p ⊢ₑ q) : p = (p ∧ₑ q)

@[reducible, inline]

abbrev Std.Do.PostCond (α : Type) (s : PostShape) : Type

A multi-barreled postcondition for the given predicate shape.

example : PostCond α (.arg ρ .pure) = ((α → ρ → Prop) × Unit) := rfl
example : PostCond α (.except ε .pure) = ((α → Prop) × (ε → Prop) × Unit) := rfl
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → Prop) × (ε → Prop) × Unit) := rfl
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → Prop) × (ε → σ → Prop) × Unit) := rfl

def Std.Do.«termPost⟨_,,⟩» : Lean.ParserDescr

@[reducible, inline]

abbrev Std.Do.PostCond.total {α : Type} {ps : PostShape} (p : α → Assertion ps) : PostCond α ps

A postcondition expressing total correctness.

@[reducible, inline]

abbrev Std.Do.PostCond.partial {α : Type} {ps : PostShape} (p : α → Assertion ps) : PostCond α ps

A postcondition expressing partial correctness.

instance Std.Do.instInhabitedPostCond {α : Type} {ps : PostShape} : Inhabited (PostCond α ps)

def Std.Do.PostCond.entails {α : Type} {ps : PostShape} (p q : PostCond α ps) : Prop

def Std.Do.«term_⊢ₚ_» : Lean.TrailingParserDescr

@[simp]

theorem Std.Do.PostCond.entails.refl {α : Type} {ps : PostShape} (Q : PostCond α ps) : Q ⊢ₚ Q

theorem Std.Do.PostCond.entails.rfl {α : Type} {ps : PostShape} {Q : PostCond α ps} : Q ⊢ₚ Q

theorem Std.Do.PostCond.entails.trans {α : Type} {ps : PostShape} {P Q R : PostCond α ps} (h₁ : P ⊢ₚ Q) (h₂ : Q ⊢ₚ R) : P ⊢ₚ R

@[simp]

theorem Std.Do.PostCond.entails_total {α : Type} {ps : PostShape} (p : α → Assertion ps) (q : PostCond α ps) : Std.Do.PostCond.total p ⊢ₚ q ↔ ∀ (a : α), p a ⊢ₛ q.fst a

@[simp]

theorem Std.Do.PostCond.entails_partial {α : Type} {ps : PostShape} (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ «partial» q ↔ ∀ (a : α), p.fst a ⊢ₛ q a

@[reducible, inline]

abbrev Std.Do.PostCond.and {α : Type} {ps : PostShape} (p q : PostCond α ps) : PostCond α ps

def Std.Do.«term_∧ₚ_» : Lean.TrailingParserDescr

theorem Std.Do.PostCond.and_eq_left {α : Type} {ps : PostShape} {p q : PostCond α ps} (h : p ⊢ₚ q) : p = (p ∧ₚ q)