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

Equations

• Std.Do.PostShape.pure.args = []
• (Std.Do.PostShape.arg σ s).args = σ :: s.args
• (Std.Do.PostShape.except ε s).args = s.args

@[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.

Equations

• Std.Do.Assertion ps = Std.Do.SPred ps.args

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

Equations

• Std.Do.FailConds Std.Do.PostShape.pure = Unit
• Std.Do.FailConds (Std.Do.PostShape.arg σ s) = Std.Do.FailConds s
• Std.Do.FailConds (Std.Do.PostShape.except ε s) = ((ε → Std.Do.Assertion s) × Std.Do.FailConds s)

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

Equations

• Std.Do.FailConds.const p = ()
• Std.Do.FailConds.const p = Std.Do.FailConds.const p
• Std.Do.FailConds.const p = (fun (_ε : ε) => ⌜p⌝, Std.Do.FailConds.const p)

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

Equations

• Std.Do.FailConds.true = Std.Do.FailConds.const True

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

Equations

• Std.Do.FailConds.false = Std.Do.FailConds.const False

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

Equations

• Std.Do.instInhabitedFailConds = { default := Std.Do.FailConds.true }

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

Equations

• (x_2 ⊢ₑ y_2) = True
• (x_2 ⊢ₑ y_2) = (x_2 ⊢ₑ y_2)
• (x_2 ⊢ₑ y_2) = ((∀ (e : ε), x_2.fst e ⊢ₛ y_2.fst e) ∧ (x_2.snd ⊢ₑ y_2.snd))

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

Equations

• Std.Do.«term_⊢ₑ_» = Lean.ParserDescr.trailingNode `Std.Do.«term_⊢ₑ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ₑ ") (Lean.ParserDescr.cat `term 25))

@[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

Equations

• (x_2 ∧ₑ y_2) = ()
• (x_2 ∧ₑ y_2) = (x_2 ∧ₑ y_2)
• (x_2 ∧ₑ y_2) = (fun (e : ε) => spred(x_2.fst e ∧ y_2.fst e), x_2.snd ∧ₑ y_2.snd)

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

Equations

• Std.Do.«term_∧ₑ_» = Lean.ParserDescr.trailingNode `Std.Do.«term_∧ₑ_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ₑ ") (Lean.ParserDescr.cat `term 35))

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

Equations

• Std.Do.PostCond α s = ((α → Std.Do.Assertion s) × Std.Do.FailConds s)

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

Equations

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

@[reducible, inline]

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

A postcondition expressing total correctness.

Equations

• Std.Do.PostCond.total p = (p, Std.Do.FailConds.false)

@[reducible, inline]

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

A postcondition expressing partial correctness.

Equations

• Std.Do.PostCond.partial p = (p, Std.Do.FailConds.true)

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

Equations

• Std.Do.instInhabitedPostCond = { default := ⇓ (x : α) => default }

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

Equations

• (p ⊢ₚ q) = ((∀ (a : α), p.fst a ⊢ₛ q.fst a) ∧ (p.snd ⊢ₑ q.snd))

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

Equations

• Std.Do.«term_⊢ₚ_» = Lean.ParserDescr.trailingNode `Std.Do.«term_⊢ₚ_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ₚ ") (Lean.ParserDescr.cat `term 25))

@[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

Equations

• (p ∧ₚ q) = (fun (a : α) => spred(p.fst a ∧ q.fst a), p.snd ∧ₑ q.snd)

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

Equations

• Std.Do.«term_∧ₚ_» = Lean.ParserDescr.trailingNode `Std.Do.«term_∧ₚ_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ₚ ") (Lean.ParserDescr.cat `term 35))

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