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} (t : PostCond α ps → Assertion ps) : Prop

The stronger the postcondition, the stronger the transformed precondition.

def Std.Do.PredTrans.Conjunctive {ps : PostShape} {α : Type} (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} (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) : Type

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, with the additional monotonicity property that the precondition is stronger the stronger the postcondition is: Q₁ ⊢ₚ Q₂ → x.apply Q₁ ⊢ₛ x.apply Q₂.

• apply : PostCond α ps → Assertion ps
• conjunctive : Conjunctive self.apply

theorem Std.Do.PredTrans.ext_iff {ps : PostShape} {α : Type} {x y : PredTrans ps α} : x = y ↔ x.apply = y.apply

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

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

def Std.Do.PredTrans.le {ps : PostShape} {α : Type} (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} : LE (PredTrans ps α)

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Std.Do.PredTrans.map_apply {ps : PostShape} {α β : Type} (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} (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} (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)

theorem Std.Do.PredTrans.bind_mono {ps : PostShape} {α β : Type} {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} (x : StateT σ (PredTrans ps) α) : PredTrans (PostShape.arg σ ps) α

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

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

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

instance Std.Do.PredTrans.instMonadLiftArg {m : PostShape} {σ : Type} : MonadLift (PredTrans m) (PredTrans (PostShape.arg σ m))

instance Std.Do.PredTrans.instMonadLiftExcept {m : PostShape} {ε : Type} : MonadLift (PredTrans m) (PredTrans (PostShape.except ε m))

instance Std.Do.PredTrans.instMonadFunctorArg {m : PostShape} {σ : Type} : MonadFunctor (PredTrans m) (PredTrans (PostShape.arg σ m))

instance Std.Do.PredTrans.instMonadFunctorExcept {m : PostShape} {ε : Type} : MonadFunctor (PredTrans m) (PredTrans (PostShape.except ε m))

@[simp]

def Std.Do.PredTrans.pushArg_apply {ps : PostShape} {α σ : Type} {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]

def Std.Do.PredTrans.pushExcept_apply {ps : PostShape} {α ε : Type} {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)

def Std.Do.PredTrans.dite_apply {α : Type} {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

def Std.Do.PredTrans.ite_apply {α : Type} {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

@[simp]

def Std.Do.PredTrans.monadLiftArg_apply {α σ : Type} {ps : PostShape} {Q : PostCond α (PostShape.arg σ ps)} (t : PredTrans ps α) : (MonadLift.monadLift t).apply Q = fun (s : σ) => t.apply (fun (a : α) => Q.fst a s, Q.snd)

@[simp]

def Std.Do.PredTrans.monadLiftExcept_apply {α ε : Type} {ps : PostShape} {Q : PostCond α (PostShape.except ε ps)} (t : PredTrans ps α) : (MonadLift.monadLift t).apply Q = t.apply (fun (a : α) => Q.fst a, Q.snd.snd)

@[simp]

def Std.Do.PredTrans.monadMapArg_apply {α σ : Type} {ps : PostShape} {Q : PostCond α (PostShape.arg σ ps)} (f : {β : Type} → PredTrans ps β → PredTrans ps β) (t : PredTrans (PostShape.arg σ ps) α) : (MonadFunctor.monadMap (fun {β : Type} => f) t).apply Q = fun (s : σ) => (f (t.popArg s)).apply (fun (x : α × σ) => match x with | (a, s) => Q.fst a s, Q.snd)

@[simp]

def Std.Do.PredTrans.monadMapExcept_apply {α ε : Type} {ps : PostShape} {Q : PostCond α (PostShape.except ε ps)} (f : {β : Type} → PredTrans ps β → PredTrans ps β) (t : PredTrans (PostShape.except ε ps) α) : (MonadFunctor.monadMap (fun {β : Type} => f) t).apply Q = (f t.popExcept).apply (fun (x : Except ε α) => match x with | Except.ok a => Q.fst a | Except.error e => Q.snd.fst e, Q.snd.snd)

@[simp]

def Std.Do.PredTrans.popArg_apply {α σ : Type} {s : σ} {ps : PostShape} {Q : PostCond (α × σ) ps} (t : PredTrans (PostShape.arg σ ps) α) : (t.popArg s).apply Q = t.apply (fun (a : α) (s : σ) => Q.fst (a, s), Q.snd) s

@[simp]

def Std.Do.PredTrans.popExcept_apply {ε α : Type} {ps : PostShape} {Q : PostCond (Except ε α) ps} (t : PredTrans (PostShape.except ε ps) α) : t.popExcept.apply Q = t.apply (fun (a : α) => Q.fst (Except.ok a), fun (e : ε) => Q.fst (Except.error e), Q.snd)

@[simp]

theorem Std.Do.PredTrans.pushArg_popArg {σ✝ : Type} {a✝ : PostShape} {α✝ : Type} {x : PredTrans (PostShape.arg σ✝ a✝) α✝} : pushArg x.popArg = x

@[simp]

theorem Std.Do.PredTrans.popArg_pushArg {σ✝ : Type} {ps✝ : PostShape} {α✝ : Type} {f : StateT σ✝ (PredTrans ps✝) α✝} : (pushArg f).popArg = f

@[simp]

theorem Std.Do.PredTrans.pushExcept_popExcept {ε✝ : Type} {a✝ : PostShape} {α✝ : Type} {x : PredTrans (PostShape.except ε✝ a✝) α✝} : pushExcept x.popExcept = x

@[simp]

theorem Std.Do.PredTrans.popExcept_pushExcept {ε✝ : Type} {ps✝ : PostShape} {α✝ : Type} {x : ExceptT ε✝ (PredTrans ps✝) α✝} : (pushExcept x).popExcept = x