# 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`.

source
inductive Std.Do.PostShape :
Type (u + 1)

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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev Std.Do.Assertion (ps : PostShape) :
Type u

An assertion on the `.arg`s 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

Instances For

source
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)

Instances For

source
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)

Instances For

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

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

Instances For

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

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

Instances For

source
@[simp]
theorem Std.Do.ExceptConds.fst_const {ε : Type u} {ps : PostShape} (p : Prop) :
(const p).fst = fun (_ε : ε) => ⌜p⌝
source
@[simp]
theorem Std.Do.ExceptConds.snd_const {ε : Type u} {ps : PostShape} (p : Prop) :
(const p).snd = const p
source
@[simp]
theorem Std.Do.ExceptConds.fst_true {ε : Type u} {ps : PostShape} :
true.fst = fun (_ε : ε) => ⌜True⌝
source
@[simp]
theorem Std.Do.ExceptConds.snd_true {ε : Type u} {ps : PostShape} :
true.snd = true
source
@[simp]
theorem Std.Do.ExceptConds.fst_false {ε : Type u} {ps : PostShape} :
false.fst = fun (_ε : ε) => ⌜False⌝
source
@[simp]
theorem Std.Do.ExceptConds.snd_false {ε : Type u} {ps : PostShape} :
false.snd = false
source
instance Std.Do.instInhabitedExceptConds {ps : PostShape} :
Inhabited (ExceptConds ps)
Equations

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

source
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)

Instances For

source
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))

Instances For

source
@[simp]
theorem Std.Do.ExceptConds.entails.refl {ps : PostShape} (x : ExceptConds ps) :
x.entails x
source
theorem Std.Do.ExceptConds.entails.rfl {ps : PostShape} {x : ExceptConds ps} :
x.entails x
source
theorem Std.Do.ExceptConds.entails.trans {ps : PostShape} {x y z : ExceptConds ps} :
x.entails y → y.entails z → x.entails z
source
@[simp]
theorem Std.Do.ExceptConds.entails_false {ps : PostShape} {x : ExceptConds ps} :
false.entails x
source
@[simp]
theorem Std.Do.ExceptConds.entails_true {ps : PostShape} {x : ExceptConds ps} :
x.entails true
source
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)

Instances For

source
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))

Instances For

source
@[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)
source
@[simp]
theorem Std.Do.ExceptConds.snd_and {ps : PostShape} {ε : Type u} {x₁ x₂ : ExceptConds (PostShape.except ε ps)} :
(x₁ ∧ₑ x₂).snd = (x₁.snd ∧ₑ x₂.snd)
source
@[simp]
theorem Std.Do.ExceptConds.and_true {ps : PostShape} {x : ExceptConds ps} :
(x ∧ₑ true).entails x
source
@[simp]
theorem Std.Do.ExceptConds.true_and {ps : PostShape} {x : ExceptConds ps} :
(true ∧ₑ x).entails x
source
@[simp]
theorem Std.Do.ExceptConds.and_false {ps : PostShape} {x : ExceptConds ps} :
(x ∧ₑ false).entails false
source
@[simp]
theorem Std.Do.ExceptConds.false_and {ps : PostShape} {x : ExceptConds ps} :
(false ∧ₑ x).entails false
source
theorem Std.Do.ExceptConds.and_eq_left {ps : PostShape} {p q : ExceptConds ps} (h : p.entails q) :
p = (p ∧ₑ q)
source
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)

Instances For

source
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))

Instances For

source
@[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)
source
@[simp]
theorem Std.Do.ExceptConds.snd_imp {ps : PostShape} {ε : Type u} {x₁ x₂ : ExceptConds (PostShape.except ε ps)} :
(x₁ →ₑ x₂).snd = (x₁.snd →ₑ x₂.snd)
source
theorem Std.Do.ExceptConds.imp_intro {ps : PostShape} {P Q R : ExceptConds ps} (h : (P ∧ₑ Q).entails R) :
P.entails (Q →ₑ R)
source
theorem Std.Do.ExceptConds.imp_elim {ps : PostShape} {P Q R : ExceptConds ps} (h : P.entails (Q →ₑ R)) :
(P ∧ₑ Q).entails R
source
@[simp]
theorem Std.Do.ExceptConds.true_imp {ps : PostShape} {x : ExceptConds ps} :
(true →ₑ x) = x
source
@[simp]
theorem Std.Do.ExceptConds.false_imp {ps : PostShape} {x : ExceptConds ps} :
(false →ₑ x) = true
source
theorem Std.Do.ExceptConds.and_imp {ps : PostShape} {x₁ x₂ : ExceptConds ps} :
(x₁ ∧ₑ (x₁ →ₑ x₂)).entails (x₁ ∧ₑ x₂)
source
@[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)

Instances For

source
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.

Instances For

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

Instances For

source
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.

Instances For

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

Instances For

source
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.

Instances For

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

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

source
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)

Instances For

source
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))

Instances For

source
@[simp]
theorem Std.Do.PostCond.entails.refl {ps : PostShape} {α : Type u} (Q : PostCond α ps) :
Q.entails Q
source
theorem Std.Do.PostCond.entails.rfl {ps : PostShape} {α : Type u} {Q : PostCond α ps} :
Q.entails Q
source
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
source
@[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
source
@[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
source
@[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)

Instances For

source
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))

Instances For

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

Instances For

source
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))

Instances For

source
theorem Std.Do.PostCond.and_imp {α✝ : Type u_1} {ps✝ : PostShape} {P' Q' : PostCond α✝ ps✝} :
(P'.and (P'.imp Q')).entails (P'.and Q')
source
theorem Std.Do.PostCond.and_left_of_entails {ps : PostShape} {α : Type u} {p q : PostCond α ps} (h : p.entails q) :
p = p.and q