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)

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

@[reducible, inline]

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

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 on the .args in the given predicate shape.

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

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.ExceptConds : PostShape → Type u

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

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

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

Equations

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

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

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

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

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

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

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

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

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

Equations

• p.entails q = ((∀ (a : α), p.fst a ⊢ₛ q.fst a) ∧ p.snd.entails 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 {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

Equations

• p.and 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))

@[reducible, inline]

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

Equations

• p.imp 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_→ₚ_» 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