Documentation

Std.Do.PredTrans

Predicate transformers for arbitrary postcondition shapes #

This module defines the type PredTrans ps of predicate transformers for a given ps : PostShape. PredTrans forms the semantic domain of the weakest precondition interpretation WP in which we interpret monadic programs.

A predicate transformer x : PredTrans ps α is a function that takes a postcondition Q : PostCond α ps and returns a precondition x.apply Q : Assertion ps, with the additional monotonicity property that the precondition is stronger the stronger the postcondition is: Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂.

Since PredTrans itself forms a monad, we can interpret monadic programs by writing a monad morphism into PredTrans; this is exactly what WP encodes. This module defines interpretations of common monadic operations, such as get, throw, liftM, etc.

def Std.Do.PredTrans.Monotonic {ps : PostShape} {α : Type u} (t : PostCond α ps → Assertion ps) :

The stronger the postcondition, the stronger the transformed precondition.

Equations

Std.Do.PredTrans.Monotonic t = ∀ (Q₁ Q₂ : Std.Do.PostCond α ps), Q₁.entails Q₂ → t Q₁ ⊢ₛ t Q₂

def Std.Do.PredTrans.Conjunctive {ps : PostShape} {α : Type u} (t : PostCond α ps → Assertion ps) :

Transforming a conjunction of postconditions is the same as the conjunction of transformed postconditions.

Equations

Std.Do.PredTrans.Conjunctive t = ∀ (Q₁ Q₂ : Std.Do.PostCond α ps), t (Q₁.and Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂

def Std.Do.PredTrans.Conjunctive.mono {ps : PostShape} {α : Type u} (t : PostCond α ps → Assertion ps) (h : Conjunctive t) :

Any predicate transformer that is conjunctive is also monotonic.

Equations

⋯ = ⋯

structure Std.Do.PredTrans (ps : PostShape) (α : Type u) :

The type of predicate transformers for a given ps : PostShape and return type α : Type. A predicate transformer x : PredTrans ps α is a function that takes a postcondition Q : PostCond α ps and returns a precondition x.apply Q : Assertion ps.

apply : PostCond α ps → Assertion ps
Apply the predicate transformer to a postcondition.
conjunctive : Conjunctive self.apply
The predicate transformer is conjunctive: t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂. So the stronger the postcondition, the stronger the resulting precondition.

Instances For

theorem Std.Do.PredTrans.ext_iff {ps : PostShape} {α : Type u} {x y : PredTrans ps α} :

x = y ↔ x.apply = y.apply

theorem Std.Do.PredTrans.ext {ps : PostShape} {α : Type u} {x y : PredTrans ps α} (apply : x.apply = y.apply) :

x = y

theorem Std.Do.PredTrans.mono {ps : PostShape} {α : Type u} (t : PredTrans ps α) :

Monotonic t.apply

def Std.Do.PredTrans.le {ps : PostShape} {α : Type u} (x y : PredTrans ps α) :

Given a fixed postcondition, the stronger predicate transformer will yield a weaker precondition.

Equations

x.le y = ∀ (Q : Std.Do.PostCond α ps), y.apply Q ⊢ₛ x.apply Q

instance Std.Do.PredTrans.instLE {ps : PostShape} {α : Type u} :

LE (PredTrans ps α)

Equations

Std.Do.PredTrans.instLE = { le := Std.Do.PredTrans.le }

def Std.Do.PredTrans.pure {ps : PostShape} {α : Type u} (a : α) :

PredTrans ps α

Equations

Std.Do.PredTrans.pure a = { apply := fun (Q : Std.Do.PostCond α ps) => Q.fst a, conjunctive := ⋯ }

def Std.Do.PredTrans.bind {ps : PostShape} {α β : Type u} (x : PredTrans ps α) (f : α → PredTrans ps β) :

PredTrans ps β

Equations

x.bind f = { apply := fun (Q : Std.Do.PostCond β ps) => x.apply (fun (a : α) => (f a).apply Q, Q.snd), conjunctive := ⋯ }

def Std.Do.PredTrans.const {ps : PostShape} {α : Type u} (P : Assertion ps) :

PredTrans ps α

The predicate transformer that always returns the same precondition P; (const P).apply Q = P.

Equations

Std.Do.PredTrans.const P = { apply := fun (Q : Std.Do.PostCond α ps) => P, conjunctive := ⋯ }

instance Std.Do.PredTrans.instMonad {ps : PostShape} :

Monad (PredTrans ps)

Equations

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

@[simp]

theorem Std.Do.PredTrans.pure_apply {ps : PostShape} {α : Type u} (a : α) (Q : PostCond α ps) :

(pure a).apply Q = Q.fst a

@[simp]

theorem Std.Do.PredTrans.Pure_pure_apply {ps : PostShape} {α : Type u} (a : α) (Q : PostCond α ps) :

(Pure.pure a).apply Q = Q.fst a

@[simp]

theorem Std.Do.PredTrans.map_apply {ps : PostShape} {α β : Type u} (f : α → β) (x : PredTrans ps α) (Q : PostCond β ps) :

(f <$> x).apply Q = x.apply (fun (a : α) => Q.fst (f a), Q.snd)

@[simp]

theorem Std.Do.PredTrans.bind_apply {ps : PostShape} {α β : Type u} (x : PredTrans ps α) (f : α → PredTrans ps β) (Q : PostCond β ps) :

(x >>= f).apply Q = x.apply (fun (a : α) => (f a).apply Q, Q.snd)

@[simp]

theorem Std.Do.PredTrans.seq_apply {ps : PostShape} {α β : Type u} (f : PredTrans ps (α → β)) (x : PredTrans ps α) (Q : PostCond β ps) :

(f <*> x).apply Q = f.apply (fun (g : α → β) => x.apply (fun (a : α) => Q.fst (g a), Q.snd), Q.snd)

@[simp]

theorem Std.Do.PredTrans.const_apply {ps : PostShape} {α : Type u} (p : Assertion ps) (Q : PostCond α ps) :

(const p).apply Q = p

theorem Std.Do.PredTrans.bind_mono {ps : PostShape} {α β : Type u} {x y : PredTrans ps α} {f : α → PredTrans ps β} (h : x ≤ y) :

x >>= f ≤ y >>= f

instance Std.Do.PredTrans.instLawfulMonad {ps : PostShape} :

LawfulMonad (PredTrans ps)

def Std.Do.PredTrans.pushArg {ps : PostShape} {α σ : Type u} (x : StateT σ (PredTrans ps) α) :

PredTrans (PostShape.arg σ ps) α

Equations

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

def Std.Do.PredTrans.pushExcept {ps : PostShape} {α ε : Type u_1} (x : ExceptT ε (PredTrans ps) α) :

PredTrans (PostShape.except ε ps) α

Equations

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

def Std.Do.PredTrans.pushOption {ps : PostShape} {α : Type u_1} (x : OptionT (PredTrans ps) α) :

PredTrans (PostShape.except PUnit ps) α

Equations

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

@[simp]

def Std.Do.PredTrans.pushArg_apply {ps : PostShape} {α σ : Type u} {Q : PostCond α (PostShape.arg σ ps)} (f : σ → PredTrans ps (α × σ)) :

(pushArg f).apply Q = fun (s : σ) => (f s).apply (fun (x : α × σ) => match x with | (a, s) => Q.fst a s, Q.snd)

Equations

⋯ = ⋯

@[simp]

def Std.Do.PredTrans.pushExcept_apply {ps : PostShape} {α ε : Type u} {Q : PostCond α (PostShape.except ε ps)} (x : PredTrans ps (Except ε α)) :

(pushExcept x).apply Q = x.apply (fun (x : Except ε α) => match x with | Except.ok a => Q.fst a | Except.error e => Q.snd.fst e, Q.snd.snd)

Equations

⋯ = ⋯

@[simp]

def Std.Do.PredTrans.pushOption_apply {ps : PostShape} {α : Type u} {Q : PostCond α (PostShape.except PUnit ps)} (x : PredTrans ps (Option α)) :

(pushOption x).apply Q = x.apply (fun (x : Option α) => match x with | some a => Q.fst a | none => Q.snd.fst PUnit.unit, Q.snd.snd)

Equations

⋯ = ⋯

def Std.Do.PredTrans.dite_apply {α : Type u} {ps : PostShape} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬c → PredTrans ps α) :

(if h : c then t h else e h).apply Q = if h : c then (t h).apply Q else (e h).apply Q

Equations

⋯ = ⋯

def Std.Do.PredTrans.ite_apply {α : Type u} {ps : PostShape} {Q : PostCond α ps} (c : Prop) [Decidable c] (t e : PredTrans ps α) :

(if c then t else e).apply Q = if c then t.apply Q else e.apply Q

Equations

⋯ = ⋯