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 (u + 1)

The “shape” of the postconditions that are used to reason about a monad.

A postcondition shape is an abstraction of many possible monadic effects, based on the structure of pure functions that can simulate them. The postcondition shape of a monad is given by its WP instance. This shape is used to determine both its Assertions and its PostConds.

• pure : PostShape

  The assertions and postconditions in this monad use neither state nor exceptions.

• arg (σ : Type u) : PostShape → PostShape

  The assertions in this monad may mention the current value of a state of type σ, and postconditions may mention the state's final value.

• except (ε : Type u) : PostShape → PostShape

  The postconditions in this monad include assertions about exceptional values of type ε that result from premature termination.

@[reducible, inline]

abbrev Std.Do.PostShape.args : PostShape → List (Type u)

Extracts the list of state types under PostShape.arg constructors, discarding exception types.

The state types determine the shape of assertions in the monad.

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 u

An assertion about the state fields for a monad whose postcondition shape is ps.

Concretely, this is an abbreviation for SPred applied to the .args in the given predicate shape, so all theorems about SPred apply.

Examples:

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

Equations

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

def Std.Do.ExceptConds : PostShape → Type u

An assertion about each potential exception that's declared in a postcondition shape.

Examples:

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

Equations

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

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

Lifts a proposition p to a set of assertions about the possible exceptions in ps. Each exception's postcondition holds when p is true.

Equations

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

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

An assertion about the possible exceptions in ps that always holds.

Equations

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

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

An assertion about the possible exceptions in ps that never holds.

Equations

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

@[simp]

theorem Std.Do.ExceptConds.fst_const {ε : Type u} {ps : PostShape} (p : Prop) : (const p).fst = fun (_ε : ε) => ⌜p⌝

@[simp]

theorem Std.Do.ExceptConds.snd_const {ε : Type u} {ps : PostShape} (p : Prop) : (const p).snd = const p

@[simp]

theorem Std.Do.ExceptConds.fst_true {ε : Type u} {ps : PostShape} : true.fst = fun (_ε : ε) => ⌜True⌝

@[simp]

theorem Std.Do.ExceptConds.snd_true {ε : Type u} {ps : PostShape} : true.snd = true

@[simp]

theorem Std.Do.ExceptConds.fst_false {ε : Type u} {ps : PostShape} : false.fst = fun (_ε : ε) => ⌜False⌝

@[simp]

theorem Std.Do.ExceptConds.snd_false {ε : Type u} {ps : PostShape} : false.snd = false

instance Std.Do.instInhabitedExceptConds {ps : PostShape} : Inhabited (ExceptConds ps)

Equations

• Std.Do.instInhabitedExceptConds = { default := Std.Do.ExceptConds.true }

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

Entailment of exception assertions is defined as pointwise entailment of the assertions for each potential exception.

While implication of exception conditions (ExceptConds.imp) is itself an exception condition, entailment is an ordinary proposition.

Equations

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

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

Entailment of exception assertions is defined as pointwise entailment of the assertions for each potential exception.

While implication of exception conditions (ExceptConds.imp) is itself an exception condition, entailment is an ordinary proposition.

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.ExceptConds.entails.refl {ps : PostShape} (x : ExceptConds ps) : x.entails x

theorem Std.Do.ExceptConds.entails.rfl {ps : PostShape} {x : ExceptConds ps} : x.entails x

theorem Std.Do.ExceptConds.entails.trans {ps : PostShape} {x y z : ExceptConds ps} : x.entails y → y.entails z → x.entails z

@[simp]

theorem Std.Do.ExceptConds.entails_false {ps : PostShape} {x : ExceptConds ps} : false.entails x

@[simp]

theorem Std.Do.ExceptConds.entails_true {ps : PostShape} {x : ExceptConds ps} : x.entails true

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

Conjunction of exception assertions is defined as pointwise conjunction of the assertions for each potential exception.

Equations

• (x_2 ∧ₑ y_2) = PUnit.unit
• (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

Conjunction of exception assertions is defined as pointwise conjunction of the assertions for each potential exception.

Equations

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

@[simp]

theorem Std.Do.ExceptConds.fst_and {ps : PostShape} {ε : Type u} {x₁ x₂ : ExceptConds (PostShape.except ε ps)} : (x₁ ∧ₑ x₂).fst = fun (e : ε) => spred(x₁.fst e ∧ x₂.fst e)

@[simp]

theorem Std.Do.ExceptConds.snd_and {ps : PostShape} {ε : Type u} {x₁ x₂ : ExceptConds (PostShape.except ε ps)} : (x₁ ∧ₑ x₂).snd = (x₁.snd ∧ₑ x₂.snd)

@[simp]

theorem Std.Do.ExceptConds.and_true {ps : PostShape} {x : ExceptConds ps} : (x ∧ₑ true).entails x

@[simp]

theorem Std.Do.ExceptConds.true_and {ps : PostShape} {x : ExceptConds ps} : (true ∧ₑ x).entails x

@[simp]

theorem Std.Do.ExceptConds.and_false {ps : PostShape} {x : ExceptConds ps} : (x ∧ₑ false).entails false

@[simp]

theorem Std.Do.ExceptConds.false_and {ps : PostShape} {x : ExceptConds ps} : (false ∧ₑ x).entails false

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

def Std.Do.ExceptConds.imp {ps : PostShape} (x y : ExceptConds ps) : ExceptConds ps

Implication of exception assertions is defined as pointwise implication of the assertion for each exception.

Unlike entailment (ExceptConds.entails), which is an ordinary proposition of type Prop, implication of exception assertions is itself an exception assertion.

Equations

• (x_2 →ₑ y_2) = PUnit.unit
• (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

Implication of exception assertions is defined as pointwise implication of the assertion for each exception.

Unlike entailment (ExceptConds.entails), which is an ordinary proposition of type Prop, implication of exception assertions is itself an exception assertion.

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.ExceptConds.fst_imp {ps : PostShape} {ε : Type u} {x₁ x₂ : ExceptConds (PostShape.except ε ps)} : (x₁ →ₑ x₂).fst = fun (e : ε) => spred(x₁.fst e → x₂.fst e)

@[simp]

theorem Std.Do.ExceptConds.snd_imp {ps : PostShape} {ε : Type u} {x₁ x₂ : ExceptConds (PostShape.except ε ps)} : (x₁ →ₑ x₂).snd = (x₁.snd →ₑ x₂.snd)

theorem Std.Do.ExceptConds.imp_intro {ps : PostShape} {P Q R : ExceptConds ps} (h : (P ∧ₑ Q).entails R) : P.entails (Q →ₑ R)

theorem Std.Do.ExceptConds.imp_elim {ps : PostShape} {P Q R : ExceptConds ps} (h : P.entails (Q →ₑ R)) : (P ∧ₑ Q).entails R

@[simp]

theorem Std.Do.ExceptConds.true_imp {ps : PostShape} {x : ExceptConds ps} : (true →ₑ x) = x

@[simp]

theorem Std.Do.ExceptConds.false_imp {ps : PostShape} {x : ExceptConds ps} : (false →ₑ x) = true

theorem Std.Do.ExceptConds.and_imp {ps : PostShape} {x₁ x₂ : ExceptConds ps} : (x₁ ∧ₑ (x₁ →ₑ x₂)).entails (x₁ ∧ₑ x₂)

@[reducible, inline]

abbrev Std.Do.PostCond (α : Type u) (ps : PostShape) : Type u

A postcondition for the given predicate shape, with one Assertion for the terminating case and one Assertion for each .except layer in the predicate shape.

variable (α σ ε : Type)
example : PostCond α (.arg σ .pure) = ((α → σ → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε .pure) = ((α → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → ULift Prop) × (ε → σ → ULift Prop) × PUnit) := rfl

Equations

• Std.Do.PostCond α ps = ((α → Std.Do.Assertion ps) × Std.Do.ExceptConds ps)

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

A postcondition for the given predicate shape, with one Assertion for the terminating case and one Assertion for each .except layer in the predicate shape.

variable (α σ ε : Type)
example : PostCond α (.arg σ .pure) = ((α → σ → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε .pure) = ((α → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → ULift Prop) × (ε → σ → ULift Prop) × PUnit) := rfl

Equations

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

@[reducible, inline]

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

A postcondition expressing total correctness. That is, it expresses that the asserted computation finishes without throwing an exception and the result satisfies the given predicate p.

Equations

• Std.Do.PostCond.noThrow p = (p, Std.Do.ExceptConds.false)

def Std.Do.«term_⇓_=>_» : Lean.ParserDescr

A postcondition expressing total correctness. That is, it expresses that the asserted computation finishes without throwing an exception and the result satisfies the given predicate p.

Equations

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

@[reducible, inline]

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

A postcondition expressing partial correctness. That is, it expresses that if the asserted computation finishes without throwing an exception then the result satisfies the given predicate p. Nothing is asserted when the computation throws an exception.

Equations

• Std.Do.PostCond.mayThrow p = (p, Std.Do.ExceptConds.true)

def Std.Do.«term_⇓?_=>_» : Lean.ParserDescr

A postcondition expressing partial correctness. That is, it expresses that if the asserted computation finishes without throwing an exception then the result satisfies the given predicate p. Nothing is asserted when the computation throws an exception.

Equations

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

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

Equations

• Std.Do.instInhabitedPostCond = { default := Std.Do.PostCond.noThrow fun (x : α) => default }

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

Entailment of postconditions.

This consists of:

• Entailment of the assertion about the return value, for all possible return values.
• Entailment of the exception conditions.

While implication of postconditions (PostCond.imp) results in a new postcondition, entailment is an ordinary proposition.

Equations

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

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

Entailment of postconditions.

This consists of:

• Entailment of the assertion about the return value, for all possible return values.
• Entailment of the exception conditions.

While implication of postconditions (PostCond.imp) results in a new postcondition, entailment is an ordinary proposition.

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 {ps : PostShape} {α : Type u} (Q : PostCond α ps) : Q.entails Q

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

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

@[simp]

theorem Std.Do.PostCond.entails_noThrow {ps : PostShape} {α : Type u} (p : α → Assertion ps) (q : PostCond α ps) : (noThrow p).entails q ↔ ∀ (a : α), p a ⊢ₛ q.fst a

@[simp]

theorem Std.Do.PostCond.entails_mayThrow {ps : PostShape} {α : Type u} (p : PostCond α ps) (q : α → Assertion ps) : p.entails (mayThrow q) ↔ ∀ (a : α), p.fst a ⊢ₛ q a

@[reducible, inline]

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

Conjunction of postconditions.

This is defined pointwise, as the conjunction of the assertions about the return value and the conjunctions of the assertions about each potential exception.

Equations

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

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

Conjunction of postconditions.

This is defined pointwise, as the conjunction of the assertions about the return value and the conjunctions of the assertions about each potential exception.

Equations

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

@[reducible, inline]

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

Implication of postconditions.

This is defined pointwise, as the implication of the assertions about the return value and the implications of each of the assertions about each potential exception.

While entailment of postconditions (PostCond.entails) is an ordinary proposition, implication of postconditions is itself a postcondition.

Equations

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

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

Implication of postconditions.

This is defined pointwise, as the implication of the assertions about the return value and the implications of each of the assertions about each potential exception.

While entailment of postconditions (PostCond.entails) is an ordinary proposition, implication of postconditions is itself a postcondition.

Equations

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

theorem Std.Do.PostCond.and_imp {α✝ : Type u_1} {ps✝ : PostShape} {P' Q' : PostCond α✝ ps✝} : (P'.and (P'.imp Q')).entails (P'.and Q')

theorem Std.Do.PostCond.and_left_of_entails {ps : PostShape} {α : Type u} {p q : PostCond α ps} (h : p.entails q) : p = p.and q