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) : Prop

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) : Prop

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) : Monotonic t

Any predicate transformer that is conjunctive is also monotonic.

Equations

• ⋯ = ⋯

structure Std.Do.PredTrans (ps : PostShape) (α : Type u) : 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.

• trans : PostCond α ps → Assertion ps

  The function implementing the predicate transformer.

• conjunctiveRaw : Conjunctive self.trans

  The predicate transformer is conjunctive: t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂. So the stronger the postcondition, the stronger the resulting precondition.

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

Apply the predicate transformer to a postcondition.

Equations

• t.apply Q = t.trans Q

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

The predicate transformer is conjunctive: t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂. So the stronger the postcondition, the stronger the resulting precondition.

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

theorem Std.Do.PredTrans.ext {ps : PostShape} {α : Type u} {t₁ t₂ : PredTrans ps α} (h : ∀ (Q : PostCond α ps), t₁.apply Q = t₂.apply Q) : t₁ = t₂

theorem Std.Do.PredTrans.ext_iff {ps : PostShape} {α : Type u} {t₁ t₂ : PredTrans ps α} : t₁ = t₂ ↔ ∀ (Q : PostCond α ps), t₁.apply Q = t₂.apply Q

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

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

@[implicit_reducible]

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 α

The identity predicate transformer that transforms the postcondition's assertion about the return value into an assertion about a.

Equations

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

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

Sequences two predicate transformers by composing them.

Equations

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

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 = { trans := fun (Q : Std.Do.PostCond α ps) => P, conjunctiveRaw := ⋯ }

def Std.Do.PredTrans.throw {ps : PostShape} {α ε : Type u} (e : ε) : PredTrans (PostShape.except ε ps) α

The predicate transformer that asserts the first exception condition.

Equations

• Std.Do.PredTrans.throw e = { trans := fun (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)) => Q.snd.fst e, conjunctiveRaw := ⋯ }

@[implicit_reducible]

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.apply_Pure_pure {ps : PostShape} {α : Type u} (a : α) (Q : PostCond α ps) : (Pure.pure a).apply Q = Q.fst a

@[simp]

theorem Std.Do.PredTrans.apply_pure {ps : PostShape} {α : Type u} (a : α) (Q : PostCond α ps) : (pure a).apply Q = Q.fst a

@[simp]

theorem Std.Do.PredTrans.apply_Functor_map {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.apply_bind {ps : PostShape} {α β : Type u} (x : PredTrans ps α) (f : α → PredTrans ps β) (Q : PostCond β ps) : (x.bind f).apply Q = x.apply (fun (a : α) => (f a).apply Q, Q.snd)

@[simp]

theorem Std.Do.PredTrans.apply_Bind_bind {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.apply_Seq_seq {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.apply_const {ps : PostShape} {α : Type u} (p : Assertion ps) (Q : PostCond α ps) : (const p).apply Q = p

@[simp]

theorem Std.Do.PredTrans.apply_throw {ps : PostShape} {α ε : Type u} (e : ε) (Q : PostCond α (PostShape.except ε ps)) : (throw e).apply Q = Q.snd.fst e

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

Adds the ability to make assertions about a state of type σ to a predicate transformer with postcondition shape ps, resulting in postcondition shape .arg σ ps. This is done by interpreting StateT σ (PredTrans ps) α into PredTrans (.arg σ ps) α.

This can be used to for all kinds of state-like effects, including reader effects or append-only states, by interpreting them as states.

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

Adds the ability to make assertions about exceptions of type ε to a predicate transformer with postcondition shape ps, resulting in postcondition shape .except ε ps. This is done by interpreting ExceptT ε (PredTrans ps) α into PredTrans (.except ε ps) α.

This can be used for all kinds of exception-like effects, such as early termination, by interpreting them as exceptions.

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

Adds the ability to make assertions about early termination to a predicate transformer with postcondition shape ps, resulting in postcondition shape .except PUnit ps. This is done by interpreting OptionT (PredTrans ps) α into PredTrans (.except PUnit ps) α, which models the type Option as being equivalent to Except PUnit.

Equations

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

@[simp]

theorem Std.Do.PredTrans.apply_pushArg {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)

@[simp]

theorem Std.Do.PredTrans.apply_pushExcept {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)

@[simp]

theorem Std.Do.PredTrans.apply_pushOption {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)

@[simp]

theorem Std.Do.PredTrans.apply_dite {α : 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

@[simp]

theorem Std.Do.PredTrans.apply_ite {α : 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