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.

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.

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.

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.

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

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

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

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

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.

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

Sequences two predicate transformers by composing them.

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.

instance Std.Do.PredTrans.instMonad {ps : PostShape} : Monad (PredTrans ps)

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

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.

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.

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.

@[simp]

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

@[simp]

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

@[simp]

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

theorem 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

theorem 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