Predicate Transformers

This module defines the type PredTrans Pred EPred α of predicate transformers for weakest precondition reasoning over monadic programs with exception postconditions.

A predicate transformer x : PredTrans Pred EPred α takes a normal postcondition post : α → Pred, an exception postcondition epost : EPred, and returns a precondition of type Pred.

PredTrans forms a monad, so monadic programs can be interpreted by a monad morphism into PredTrans; this is exactly what WPMonad encodes.

Main definitions

• PredTrans Pred EPred α — the type of monotone predicate transformers
• PredTrans.pushExcept — adds an exception layer to a predicate transformer
• pushArg — adds a state argument to a predicate transformer
• Instances for Monad, LawfulMonad, MonadStateOf, MonadExceptOf, etc.

structure Std.Internal.Do.PredTrans (Pred : Type u) (EPred : Type v) (α : Type w) : Type (max (max u v) w)

A monotone predicate transformer from postconditions to preconditions.

Given a return type α, a lattice Pred for assertions, and an exception assertion type EPred, PredTrans Pred EPred α wraps a function (α → Pred) → EPred → Pred.

• apply : (α → Pred) → EPred → Pred

  Apply the predicate transformer to a postcondition and exception postcondition.

theorem Std.Internal.Do.PredTrans.ext {Pred : Type u_1} {EPred : Type u_2} {α : Type u_3} {x y : PredTrans Pred EPred α} (h : ∀ (post : α → Pred) (epost : EPred), x.apply post epost = y.apply post epost) : x = y

Extensionality for predicate transformers.

theorem Std.Internal.Do.PredTrans.ext_iff {Pred : Type u_1} {EPred : Type u_2} {α : Type u_3} {x y : PredTrans Pred EPred α} : x = y ↔ ∀ (post : α → Pred) (epost : EPred), x.apply post epost = y.apply post epost

@[implicit_reducible]

instance Std.Internal.Do.instPartialOrderPredTrans {Pred : Type u_1} {EPred : Type u_2} {α : Type u_3} [Lean.Order.PartialOrder Pred] : Lean.Order.PartialOrder (PredTrans Pred EPred α)

Partial order on predicate transformers, inherited from the function space.

Equations

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

@[implicit_reducible]

instance Std.Internal.Do.instCCPOPredTrans {Pred : Type u_1} {EPred : Type u_2} {α : Type u_3} [Lean.Order.CCPO Pred] : Lean.Order.CCPO (PredTrans Pred EPred α)

Chain-complete partial order on predicate transformers, for fixed-point reasoning.

Equations

• Std.Internal.Do.instCCPOPredTrans = { toPartialOrder := Std.Internal.Do.instPartialOrderPredTrans, has_csup := ⋯ }

@[implicit_reducible]

instance Std.Internal.Do.instMonadPredTrans (Pred : Type u) (EPred : Type v) : Monad (PredTrans Pred EPred)

Monad instance for PredTrans: pure returns the postcondition applied to the value, and bind threads the postcondition through the continuation.

Equations

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

instance Std.Internal.Do.instLawfulMonadPredTrans (Pred : Type u) (EPred : Type v) : LawfulMonad (PredTrans Pred EPred)

PredTrans is a lawful monad: all monad laws hold definitionally.

def Std.Internal.Do.PredTrans.monotone {Pred : Type u_1} {EPred : Type u_2} {α : Type u_3} [Lean.Order.PartialOrder Pred] [Lean.Order.PartialOrder EPred] (pt : PredTrans Pred EPred α) : Prop

Monotonicity property for a predicate transformer: if both post and epost grow, then the resulting precondition grows.

Equations

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

apply_* simp framework

Simp lemmas for reducing (expr).apply post epost for each monadic combinator.

@[simp]

theorem Std.Internal.Do.PredTrans.apply_pure {α : Type u_1} {Pred : Type u} {EPred : Type v} (a : α) (post : α → Pred) (epost : EPred) : (pure a).apply post epost = post a

Unfolding pure through apply.

@[simp]

theorem Std.Internal.Do.PredTrans.apply_bind {α β : Type u_1} {Pred : Type u} {EPred : Type v} (x : PredTrans Pred EPred α) (f : α → PredTrans Pred EPred β) (post : β → Pred) (epost : EPred) : (x >>= f).apply post epost = x.apply (fun (a : α) => (f a).apply post epost) epost

Unfolding >>= through apply.

@[simp]

theorem Std.Internal.Do.PredTrans.apply_map {β : Type w} {Pred : Type u} {EPred : Type v} {α : Type w} (trans : PredTrans Pred EPred α) (f : α → β) (post : β → Pred) (epost : EPred) : (f <$> trans).apply post epost = trans.apply (post ∘ f) epost

Unfolding <$> through apply.

@[simp]

theorem Std.Internal.Do.PredTrans.apply_seq {α β : Type u_1} {Pred : Type u} {EPred : Type v} (f : PredTrans Pred EPred (α → β)) (x : PredTrans Pred EPred α) (post : β → Pred) (epost : EPred) : (f <*> x).apply post epost = f.apply (fun (g : α → β) => x.apply (fun (a : α) => post (g a)) epost) epost

Unfolding <*> through apply.

@[simp]

theorem Std.Internal.Do.PredTrans.apply_dite {α : Type u_1} {Pred : Type u} {EPred : Type v} (c : Prop) [Decidable c] (t : c → PredTrans Pred EPred α) (e : ¬c → PredTrans Pred EPred α) (post : α → Pred) (epost : EPred) : (if h : c then t h else e h).apply post epost = if h : c then (t h).apply post epost else (e h).apply post epost

Unfolding dite through apply.

@[simp]

theorem Std.Internal.Do.PredTrans.apply_ite {α : Type u_1} {Pred : Type u} {EPred : Type v} (c : Prop) [Decidable c] (t e : PredTrans Pred EPred α) (post : α → Pred) (epost : EPred) : (if c then t else e).apply post epost = if c then t.apply post epost else e.apply post epost

Unfolding ite through apply.

Exception Handling

Definitions for pushing and lifting exception layers through predicate transformers.

@[reducible, inline]

abbrev Std.Internal.Do.EPost.cons.pushExcept {α : Type u} {ε : Type v} {Pred : Type w} {EPred : Type z} (post : α → Pred) (epost : EPost.cons✝ (ε → Pred) EPred) : Except ε α → Pred

Push an Except ε α result into separate normal and exception postconditions: ok a uses post a, and error e uses epost.head e.

Equations

• Std.Internal.Do.EPost.cons.pushExcept post epost (Except.ok a) = post a
• Std.Internal.Do.EPost.cons.pushExcept post epost (Except.error e) = epost.head e

def Std.Internal.Do.PredTrans.pushExcept {α : Type u} {ε : Type v} {Pred : Type w} {EPred : Type z} (x : PredTrans Pred EPred (Except ε α)) : PredTrans Pred (EPost.cons✝ (ε → Pred) EPred) α

Adds an exception layer to a predicate transformer.

Given a transformer over Except ε α, produces one over α with an additional exception postcondition for ε. The normal and error postconditions are combined via pushExcept.

Equations

• x.pushExcept = { apply := fun (post : α → Pred) (epost : EPost.cons✝ (ε → Pred) EPred) => x.apply (Std.Internal.Do.EPost.cons.pushExcept post epost) epost.tail }

@[reducible, inline]

abbrev Std.Internal.Do.EPost.cons.pushOption {α Pred : Type u} {EPred : Type v} (post : α → Pred) (epost : EPost.cons✝ Pred EPred) : Option α → Pred

Push an Option α result into separate normal and none postconditions: some a uses post a, and none uses epost.head.

Equations

• Std.Internal.Do.EPost.cons.pushOption post epost (some a) = post a
• Std.Internal.Do.EPost.cons.pushOption post epost none = epost.head

def Std.Internal.Do.PredTrans.pushOption {α Pred : Type u} {EPred : Type v} (x : PredTrans Pred EPred (Option α)) : PredTrans Pred (EPost.cons✝ Pred EPred) α

Adds an early-termination layer to a predicate transformer, modelling Option as early termination. Given a transformer over Option α, produces one over α with an additional exception postcondition for the none case.

Equations

• x.pushOption = { apply := fun (post : α → Pred) (epost : EPost.cons✝ Pred EPred) => x.apply (Std.Internal.Do.EPost.cons.pushOption post epost) epost.tail }

@[simp]

theorem Std.Internal.Do.PredTrans.apply_pushOption {α Pred : Type u} {EPred : Type v} (x : PredTrans Pred EPred (Option α)) (post : α → Pred) (epost : EPost.cons✝ Pred EPred) : x.pushOption.apply post epost = x.apply (EPost.cons.pushOption post epost) epost.tail

Unfolding pushOption through apply.

State Handling

Definitions for adding state arguments to predicate transformers.

def Std.Internal.Do.pushArg {σ : Type u} {Pred : Type v} {EPred : Type w} {α : Type z} (x : σ → PredTrans Pred EPred (α × σ)) : PredTrans (σ → Pred) EPred α

Adds a state argument to a predicate transformer.

Given a state-dependent transformer σ → PredTrans l e (α × σ), produces a transformer over σ → l that threads the state through postconditions.

Equations

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

@[simp]

theorem Std.Internal.Do.PredTrans.apply_pushArg {σ : Type u} {Pred : Type v} {EPred : Type w} {α : Type z} (x : σ → PredTrans Pred EPred (α × σ)) (post : α → σ → Pred) (epost : EPred) (s : σ) : (pushArg x).apply post epost s = (x s).apply (fun (x : α × σ) => match x with | (a, s) => post a s) epost

Unfolding lemma for pushArg: applies the state-threaded transformer at state s.

@[implicit_reducible]

instance Std.Internal.Do.instMonadLiftPredTransForall {σ : Type u} {Pred : Type v} {EPred : Type w} : MonadLift (PredTrans Pred EPred) (PredTrans (σ → Pred) EPred)

Lift a predicate transformer to one with a state argument (pointwise).

Equations

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

@[implicit_reducible, instance 10000]

instance Std.Internal.Do.instMonadLiftPredTransConsForall {ε Pred EPred : Type u} : MonadLift (PredTrans Pred EPred) (PredTrans Pred (EPost.cons✝ (ε → Pred) EPred))

Lift a predicate transformer to one with an additional exception layer (high priority).

Equations

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

Monad Instances

Standard monad class instances for PredTrans.

@[implicit_reducible]

instance Std.Internal.Do.instMonadStateOfPredTransForall {σ : Type u} {Pred : Type v} {EPred : Type w} : MonadStateOf σ (PredTrans (σ → Pred) EPred)

MonadStateOf instance: get returns the state, set replaces it, modifyGet applies a function to the state.

Equations

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

@[implicit_reducible]

instance Std.Internal.Do.instMonadReaderOfPredTransForall {σ : Type u} {Pred : Type v} {EPred : Type w} : MonadReaderOf σ (PredTrans (σ → Pred) EPred)

MonadReaderOf instance: read provides the state without consuming it.

Equations

• Std.Internal.Do.instMonadReaderOfPredTransForall = { read := { apply := fun (post : σ → σ → Pred) (_epost : EPred) (s : σ) => post s s } }

@[implicit_reducible]

instance Std.Internal.Do.instMonadExceptOfPredTransConsForall {ε : Type u} {Pred : Type v} {EPred : Type w} : MonadExceptOf ε (PredTrans Pred (EPost.cons✝ (ε → Pred) EPred))

MonadExceptOf instance for the outermost exception layer: throw invokes the head exception postcondition, tryCatch intercepts it.

Equations

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

@[implicit_reducible]

instance Std.Internal.Do.instMonadExceptOfPredTransForall {ε : Type u} {Pred : Type v} {EPred : Type w} {σ : Type z} [MonadExceptOf ε (PredTrans Pred EPred)] : MonadExceptOf ε (PredTrans (σ → Pred) EPred)

MonadExceptOf instance lifted through a state layer: delegates throw and tryCatch to the inner PredTrans l e instance.

Equations

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

@[implicit_reducible]

instance Std.Internal.Do.instMonadExceptOfPredTransConsForall_1 {ε : Type u} {Pred : Type v} {EPred : Type w} {ε' : Type u} [MonadExceptOf ε (PredTrans Pred EPred)] : MonadExceptOf ε (PredTrans Pred (EPost.cons✝ (ε' → Pred) EPred))

MonadExceptOf instance lifted through an unrelated exception layer: delegates to the inner instance, threading the extra exception postcondition.

Equations

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