Predicate transformers

PredTrans Pred EPred α wraps a map from a normal postcondition α → Pred and an exception postcondition EPred to a precondition Pred. The order and the chain-complete suprema are the pointwise ones of the function space.

PredTrans Pred EPred is a monad, so monadic programs can be interpreted by a monad morphism into it. This module provides that monad structure, the apply simp framework of the monadic combinators, the push family that moves a result type into a postcondition, and the standard monad class instances.

structure Lean.Order.PredTrans (Pred : Type u) (EPred : Type v) (α : Type w) : Type (max (max u v) w)

A 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 Lean.Order.PredTrans.ext {Pred : Type u} {EPred : Type v} {α : Type w} {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 Lean.Order.PredTrans.ext_iff {Pred : Type u} {EPred : Type v} {α : Type w} {x y : PredTrans Pred EPred α} : x = y ↔ ∀ (post : α → Pred) (epost : EPred), x.apply post epost = y.apply post epost

@[instance_reducible]

instance Lean.Order.PredTrans.instPartialOrder {Pred : Type u} {EPred : Type v} {α : Type w} [PartialOrder Pred] : PartialOrder (PredTrans Pred EPred α)

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

Equations

• Lean.Order.PredTrans.instPartialOrder = { rel := fun (x y : Lean.Order.PredTrans Pred EPred α) => Lean.Order.PartialOrder.rel x.apply y.apply, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

@[instance_reducible]

instance Lean.Order.PredTrans.instCCPO {Pred : Type u} {EPred : Type v} {α : Type w} [CCPO Pred] : CCPO (PredTrans Pred EPred α)

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

Equations

• Lean.Order.PredTrans.instCCPO = { toPartialOrder := Lean.Order.PredTrans.instPartialOrder, has_csup := ⋯ }

def Lean.Order.PredTrans.monotone {Pred : Type u} {EPred : Type v} {α : Type w} [PartialOrder Pred] [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.

Monad Structure

def Lean.Order.PredTrans.pure {Pred : Type u} {EPred : Type v} {α : Type w} (a : α) : PredTrans Pred EPred α

pure a applies the postcondition to a.

Equations

• Lean.Order.PredTrans.pure a = { apply := fun (post : α → Pred) (_epost : EPred) => post a }

def Lean.Order.PredTrans.bind {Pred : Type u} {EPred : Type v} {α β : Type w} (x : PredTrans Pred EPred α) (f : α → PredTrans Pred EPred β) : PredTrans Pred EPred β

bind x f threads the postcondition through the continuation f.

Equations

• x.bind f = { apply := fun (post : β → Pred) (epost : EPred) => x.apply (fun (a : α) => (f a).apply post epost) epost }

@[instance_reducible]

instance Lean.Order.PredTrans.instMonad {Pred : Type u} {EPred : Type v} : Monad (PredTrans Pred EPred)

Equations

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

instance Lean.Order.PredTrans.instLawfulMonad {Pred : Type u} {EPred : Type v} : LawfulMonad (PredTrans Pred EPred)

apply_* simp framework

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

@[simp]

theorem Lean.Order.PredTrans.apply_pure {Pred : Type u} {EPred : Type v} {α : Type w} (a : α) (post : α → Pred) (epost : EPred) : (pure a).apply post epost = post a

Unfolding PredTrans.pure through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_Pure_pure {Pred : Type u} {EPred : Type v} {α : Type w} (a : α) (post : α → Pred) (epost : EPred) : (Pure.pure a).apply post epost = post a

Unfolding pure through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_bind {Pred : Type u} {EPred : Type v} {α β : Type w} (x : PredTrans Pred EPred α) (f : α → PredTrans Pred EPred β) (post : β → Pred) (epost : EPred) : (x.bind f).apply post epost = x.apply (fun (a : α) => (f a).apply post epost) epost

Unfolding PredTrans.bind through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_Bind_bind {Pred : Type u} {EPred : Type v} {α β : Type w} (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 Lean.Order.PredTrans.apply_Functor_map {Pred : Type u} {EPred : Type v} {α β : Type w} (f : α → β) (x : PredTrans Pred EPred α) (post : β → Pred) (epost : EPred) : (f <$> x).apply post epost = x.apply (post ∘ f) epost

Unfolding <$> through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_Seq_seq {Pred : Type u} {EPred : Type v} {α β : Type w} (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 Lean.Order.PredTrans.apply_dite {Pred : Type u} {EPred : Type v} {α : Type w} (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 Lean.Order.PredTrans.apply_ite {Pred : Type u} {EPred : Type v} {α : Type w} (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.

Arguments

Combinators that add or remove a state argument.

def Lean.Order.PredTrans.pushArg {Pred : Type u} {EPred : Type v} {α : 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 Pred EPred (α × σ), produces a transformer over σ → Pred that threads the state through postconditions.

Equations

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

@[simp]

theorem Lean.Order.PredTrans.apply_pushArg {Pred : Type u} {EPred : Type v} {α : 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.

def Lean.Order.PredTrans.popArg {Pred : Type u} {EPred : Type v} {α : Type w} {σ : Type z} (x : PredTrans (σ → Pred) EPred α) (s : σ) : PredTrans Pred EPred (α × σ)

Removes the state argument of a predicate transformer by applying it at state s. The transformed result carries the final state.

Equations

• x.popArg s = { apply := fun (post : α × σ → Pred) (epost : EPred) => x.apply (fun (a : α) (s : σ) => post (a, s)) epost s }

@[simp]

theorem Lean.Order.PredTrans.apply_popArg {Pred : Type u} {EPred : Type v} {α : Type w} {σ : Type z} (x : PredTrans (σ → Pred) EPred α) (s : σ) (post : α × σ → Pred) (epost : EPred) : (x.popArg s).apply post epost = x.apply (fun (a : α) (s : σ) => post (a, s)) epost s

Unfolding popArg through apply.

def Lean.Order.PredTrans.liftArg {Pred : Type u} {EPred : Type v} {α : Type w} {σ : Type z} (x : PredTrans Pred EPred α) : PredTrans (σ → Pred) EPred α

Adds a state argument that the predicate transformer ignores.

Equations

• x.liftArg = { apply := fun (post : α → σ → Pred) (epost : EPred) (s : σ) => x.apply (fun (a : α) => post a s) epost }

@[simp]

theorem Lean.Order.PredTrans.apply_liftArg {Pred : Type u} {EPred : Type v} {α : Type w} {σ : Type z} (x : PredTrans Pred EPred α) (post : α → σ → Pred) (epost : EPred) (s : σ) : x.liftArg.apply post epost s = x.apply (fun (a : α) => post a s) epost

Unfolding liftArg through apply.

@[instance_reducible]

instance Lean.Order.PredTrans.instMonadLiftForall {Pred : Type u} {EPred : Type v} {σ : Type z} : MonadLift (PredTrans Pred EPred) (PredTrans (σ → Pred) EPred)

Equations

• Lean.Order.PredTrans.instMonadLiftForall = { monadLift := fun {α : Type ?u.1} => Lean.Order.PredTrans.liftArg }

@[simp]

theorem Lean.Order.PredTrans.apply_monadLift {Pred : Type u} {EPred : Type v} {α : Type w} {σ : Type z} (x : PredTrans Pred EPred α) (post : α → σ → Pred) (epost : EPred) (s : σ) : (MonadLift.monadLift x).apply post epost s = x.apply (fun (a : α) => post a s) epost

Unfolding monadLift through apply.

Results

Postconditions for Except and Option results, and the transformer combinators built on them.

def Lean.Order.pushExcept {α : Type u} {ε : Type v} {Pred : Type w} (post : α → Pred) (epost : ε → Pred) : Except ε α → Pred

The postcondition for an Except ε α result: ok a uses post a, and error e uses epost e.

Equations

• Lean.Order.pushExcept post epost (Except.ok a) = post a
• Lean.Order.pushExcept post epost (Except.error e) = epost e

@[simp]

theorem Lean.Order.pushExcept_ok {α : Type u} {ε : Type v} {Pred : Type w} (post : α → Pred) (epost : ε → Pred) (a : α) : pushExcept post epost (Except.ok a) = post a

A normal result uses the normal postcondition.

@[simp]

theorem Lean.Order.pushExcept_error {α : Type u} {ε : Type v} {Pred : Type w} (post : α → Pred) (epost : ε → Pred) (e : ε) : pushExcept post epost (Except.error e) = epost e

An exceptional result uses the exception postcondition.

def Lean.Order.pushOption {α : Type u} {Pred : Type w} (post : α → Pred) (epost : Unit → Pred) : Option α → Pred

The postcondition for an Option α result: some a uses post a, and none uses epost ().

Equations

• Lean.Order.pushOption post epost (some a) = post a
• Lean.Order.pushOption post epost none = epost ()

@[simp]

theorem Lean.Order.pushOption_some {α : Type u} {Pred : Type w} (post : α → Pred) (epost : Unit → Pred) (a : α) : pushOption post epost (some a) = post a

A present result uses the normal postcondition.

@[simp]

theorem Lean.Order.pushOption_none {α : Type u} {Pred : Type w} (post : α → Pred) (epost : Unit → Pred) : pushOption post epost none = epost ()

An absent result uses the absent postcondition.

def Lean.Order.PredTrans.pushExceptT {Pred : Type u} {EPred : Type v} {α : Type w} {ε : Type z} (x : PredTrans Pred EPred (Except ε α)) : PredTrans Pred ((ε → Pred) × EPred) α

Adds an exception postcondition layer to a predicate transformer, mirroring ExceptT.

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.pushExceptT = { apply := fun (post : α → Pred) (epost : (ε → Pred) × EPred) => x.apply (Lean.Order.pushExcept post epost.fst) epost.snd }

@[simp]

theorem Lean.Order.PredTrans.apply_pushExceptT {Pred : Type u} {EPred : Type v} {α : Type w} {ε : Type z} (x : PredTrans Pred EPred (Except ε α)) (post : α → Pred) (epost : (ε → Pred) × EPred) : x.pushExceptT.apply post epost = x.apply (pushExcept post epost.fst) epost.snd

Unfolding lemma for pushExceptT.

def Lean.Order.PredTrans.pushOptionT {Pred : Type u} {EPred : Type v} {α : Type w} (x : PredTrans Pred EPred (Option α)) : PredTrans Pred ((Unit → Pred) × EPred) α

Adds an early-termination layer to a predicate transformer, mirroring OptionT.

Given a transformer over Option α, produces one over α with an additional exception postcondition for the none case.

Equations

• x.pushOptionT = { apply := fun (post : α → Pred) (epost : (Unit → Pred) × EPred) => x.apply (Lean.Order.pushOption post epost.fst) epost.snd }

@[simp]

theorem Lean.Order.PredTrans.apply_pushOptionT {Pred : Type u} {EPred : Type v} {α : Type w} (x : PredTrans Pred EPred (Option α)) (post : α → Pred) (epost : (Unit → Pred) × EPred) : x.pushOptionT.apply post epost = x.apply (pushOption post epost.fst) epost.snd

Unfolding lemma for pushOptionT.

Exception Instances

throw and tryCatch on the first exception postcondition, and the combinators that lift the MonadExceptOf instance through further layers.

def Lean.Order.PredTrans.throw {Pred : Type u} {EPred : Type v} {α : Type w} {ε : Type z} (e : ε) : PredTrans Pred ((ε → Pred) × EPred) α

throw e asserts the first exception postcondition at e.

Equations

• Lean.Order.PredTrans.throw e = { apply := fun (_post : α → Pred) (epost : (ε → Pred) × EPred) => epost.fst e }

def Lean.Order.PredTrans.tryCatch {Pred : Type u} {EPred : Type v} {α : Type w} {ε : Type z} (x : PredTrans Pred ((ε → Pred) × EPred) α) (handle : ε → PredTrans Pred ((ε → Pred) × EPred) α) : PredTrans Pred ((ε → Pred) × EPred) α

tryCatch x handle replaces the first exception postcondition of x with the precondition of the handler.

Equations

• x.tryCatch handle = { apply := fun (post : α → Pred) (epost : (ε → Pred) × EPred) => x.apply post (fun (e : ε) => (handle e).apply post epost, epost.snd) }

@[instance_reducible]

instance Lean.Order.PredTrans.instMonadExceptOfProdForall {Pred : Type u} {EPred : Type v} {ε : Type z} : MonadExceptOf ε (PredTrans Pred ((ε → Pred) × EPred))

Equations

• Lean.Order.PredTrans.instMonadExceptOfProdForall = { throw := fun {α : Type ?u.1} => Lean.Order.PredTrans.throw, tryCatch := fun {α : Type ?u.1} => Lean.Order.PredTrans.tryCatch }

@[simp]

theorem Lean.Order.PredTrans.apply_throw {ε α Pred : Type u} {EPred : Type w} (e : ε) (post : α → Pred) (epost : (ε → Pred) × EPred) : (MonadExceptOf.throw e).apply post epost = epost.fst e

Unfolding throw through apply: the first exception postcondition at the thrown value.

@[simp]

theorem Lean.Order.PredTrans.apply_tryCatch {ε α Pred : Type u} {EPred : Type w} (x : PredTrans Pred ((ε → Pred) × EPred) α) (handle : ε → PredTrans Pred ((ε → Pred) × EPred) α) (post : α → Pred) (epost : (ε → Pred) × EPred) : (MonadExceptOf.tryCatch x handle).apply post epost = x.apply post (fun (e : ε) => (handle e).apply post epost, epost.snd)

Unfolding tryCatch through apply: the handler replaces the first exception postcondition.

def Lean.Order.PredTrans.liftExcept {Pred : Type u} {EPred : Type v} {α : Type w} {eh : Type z} (x : PredTrans Pred EPred α) : PredTrans Pred (eh × EPred) α

Adds a first exception postcondition that the predicate transformer ignores.

Equations

• x.liftExcept = { apply := fun (post : α → Pred) (epost : eh × EPred) => x.apply post epost.snd }

@[simp]

theorem Lean.Order.PredTrans.apply_liftExcept {Pred : Type u} {EPred : Type v} {α : Type w} {eh : Type z} (x : PredTrans Pred EPred α) (post : α → Pred) (epost : eh × EPred) : x.liftExcept.apply post epost = x.apply post epost.snd

Unfolding liftExcept through apply.

def Lean.Order.PredTrans.popExcept {Pred : Type u} {EPred : Type v} {α : Type w} {eh : Type z} (x : PredTrans Pred (eh × EPred) α) (h : eh) : PredTrans Pred EPred α

Removes the first exception postcondition of a predicate transformer by fixing it to h.

Equations

• x.popExcept h = { apply := fun (post : α → Pred) (epost : EPred) => x.apply post (h, epost) }

@[simp]

theorem Lean.Order.PredTrans.apply_popExcept {Pred : Type u} {EPred : Type v} {α : Type w} {eh : Type z} (x : PredTrans Pred (eh × EPred) α) (h : eh) (post : α → Pred) (epost : EPred) : (x.popExcept h).apply post epost = x.apply post (h, epost)

Unfolding popExcept through apply.

@[instance_reducible]

instance Lean.Order.PredTrans.instMonadExceptOfProdForall_1 {ε : Type u} {Pred : Type v} {EPred : Type w} {ε' : Type u} [MonadExceptOf ε (PredTrans Pred EPred)] : MonadExceptOf ε (PredTrans Pred ((ε' → Pred) × EPred))

Equations

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

State Instances

Standard state and reader class instances for PredTrans.

def Lean.Order.PredTrans.get {Pred : Type u} {EPred : Type v} {σ : Type z} : PredTrans (σ → Pred) EPred σ

get transforms the postcondition into its assertion at the current state.

Equations

• Lean.Order.PredTrans.get = { apply := fun (post : σ → σ → Pred) (_epost : EPred) (s : σ) => post s s }

def Lean.Order.PredTrans.set {Pred : Type u} {EPred : Type v} {σ : Type z} (s' : σ) : PredTrans (σ → Pred) EPred PUnit

set s' transforms the postcondition into its assertion at the state s'.

Equations

• Lean.Order.PredTrans.set s' = { apply := fun (post : PUnit → σ → Pred) (_epost : EPred) (_s : σ) => post PUnit.unit s' }

def Lean.Order.PredTrans.modifyGet {Pred : Type u} {EPred : Type v} {σ α : Type z} (f : σ → α × σ) : PredTrans (σ → Pred) EPred α

modifyGet f transforms the postcondition into its assertion at the result and state computed by f.

Equations

• Lean.Order.PredTrans.modifyGet f = { apply := fun (post : α → σ → Pred) (_epost : EPred) (s : σ) => post (f s).fst (f s).snd }

@[instance_reducible]

instance Lean.Order.PredTrans.instMonadStateOfForall {Pred : Type u} {EPred : Type v} {σ : Type z} : MonadStateOf σ (PredTrans (σ → Pred) EPred)

Equations

• Lean.Order.PredTrans.instMonadStateOfForall = { get := Lean.Order.PredTrans.get, set := Lean.Order.PredTrans.set, modifyGet := fun {α : Type ?u.1} => Lean.Order.PredTrans.modifyGet }

@[instance_reducible]

instance Lean.Order.PredTrans.instMonadReaderOfForall {Pred : Type u} {EPred : Type v} {σ : Type z} : MonadReaderOf σ (PredTrans (σ → Pred) EPred)

Equations

• Lean.Order.PredTrans.instMonadReaderOfForall = { read := Lean.Order.PredTrans.get }

@[simp]

theorem Lean.Order.PredTrans.apply_get {Pred : Type u} {EPred : Type v} {σ : Type z} (post : σ → σ → Pred) (epost : EPred) (s : σ) : MonadStateOf.get.apply post epost s = post s s

Unfolding get through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_set {Pred : Type u} {EPred : Type v} {σ : Type z} (s' : σ) (post : PUnit → σ → Pred) (epost : EPred) (s : σ) : (MonadStateOf.set s').apply post epost s = post PUnit.unit s'

Unfolding set through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_modifyGet {Pred : Type u} {EPred : Type v} {σ α : Type z} (f : σ → α × σ) (post : α → σ → Pred) (epost : EPred) (s : σ) : (MonadStateOf.modifyGet f).apply post epost s = post (f s).fst (f s).snd

Unfolding modifyGet through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_read {Pred : Type u} {EPred : Type v} {σ : Type z} (post : σ → σ → Pred) (epost : EPred) (s : σ) : MonadReaderOf.read.apply post epost s = post s s

Unfolding read through apply.

@[instance_reducible]

instance Lean.Order.PredTrans.instMonadExceptOfForall {Pred : Type u} {EPred : Type v} {ε : Type u'} {σ : Type z} [MonadExceptOf ε (PredTrans Pred EPred)] : MonadExceptOf ε (PredTrans (σ → Pred) EPred)

Equations

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