Predicate transformers

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

PredTrans Pred EPosts is a monad, so monadic programs can be interpreted by a monad morphism into it. This module provides that monad structure, the apply computation rules 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) (EPosts : 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 EPosts, PredTrans Pred EPosts α wraps a function (α → Pred) → EPosts → Pred.

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

  Apply the predicate transformer to a postcondition and exception postcondition.

theorem Lean.Order.PredTrans.ext {Pred : Type u} {EPosts : Type v} {α : Type w} {x y : PredTrans Pred EPosts α} (h : ∀ (post : α → Pred) (eposts : EPosts), x.apply post eposts = y.apply post eposts) : x = y

Extensionality for predicate transformers.

theorem Lean.Order.PredTrans.ext_iff {Pred : Type u} {EPosts : Type v} {α : Type w} {x y : PredTrans Pred EPosts α} : x = y ↔ ∀ (post : α → Pred) (eposts : EPosts), x.apply post eposts = y.apply post eposts

@[instance_reducible]

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

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

@[instance_reducible]

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

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

def Lean.Order.PredTrans.Monotone {Pred : Type u} {EPosts : Type v} {α : Type w} [PartialOrder Pred] [PartialOrder EPosts] (pt : PredTrans Pred EPosts α) : Prop

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

def Lean.Order.PredTrans.Conjunctive {Pred : Type u} {EPosts : Type v} {α : Type w} [CompleteLattice Pred] [CompleteLattice EPosts] (pt : PredTrans Pred EPosts α) : Prop

Conjunctivity property for a predicate transformer: the meet of two preconditions lies below the precondition of the componentwise meet of the postconditions.

Monad Structure

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

pure a applies the postcondition to a.

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

bind x f threads the postcondition through the continuation f.

@[instance_reducible]

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

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

apply_* computation rules

Equations that reduce (expr).apply post eposts for each monadic combinator.

@[simp]

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

Unfolding PredTrans.pure through apply.

@[simp]

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

Unfolding pure through apply.

@[simp]

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

Unfolding PredTrans.bind through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_Bind_bind {Pred : Type u} {EPosts : Type v} {α β : Type w} (x : PredTrans Pred EPosts α) (f : α → PredTrans Pred EPosts β) (post : β → Pred) (eposts : EPosts) : (x >>= f).apply post eposts = x.apply (fun (a : α) => (f a).apply post eposts) eposts

Unfolding >>= through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_Functor_map {Pred : Type u} {EPosts : Type v} {α β : Type w} (f : α → β) (x : PredTrans Pred EPosts α) (post : β → Pred) (eposts : EPosts) : (f <$> x).apply post eposts = x.apply (post ∘ f) eposts

Unfolding <$> through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_Seq_seq {Pred : Type u} {EPosts : Type v} {α β : Type w} (f : PredTrans Pred EPosts (α → β)) (x : PredTrans Pred EPosts α) (post : β → Pred) (eposts : EPosts) : (f <*> x).apply post eposts = f.apply (fun (g : α → β) => x.apply (fun (a : α) => post (g a)) eposts) eposts

Unfolding <*> through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_dite {Pred : Type u} {EPosts : Type v} {α : Type w} (c : Prop) [Decidable c] (t : c → PredTrans Pred EPosts α) (e : ¬c → PredTrans Pred EPosts α) (post : α → Pred) (eposts : EPosts) : (if h : c then t h else e h).apply post eposts = if h : c then (t h).apply post eposts else (e h).apply post eposts

Unfolding dite through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_ite {Pred : Type u} {EPosts : Type v} {α : Type w} (c : Prop) [Decidable c] (t e : PredTrans Pred EPosts α) (post : α → Pred) (eposts : EPosts) : (if c then t else e).apply post eposts = if c then t.apply post eposts else e.apply post eposts

Unfolding ite through apply.

Arguments

Combinators that add or remove a state argument.

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

Adds a state argument to a predicate transformer.

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

@[simp]

theorem Lean.Order.PredTrans.apply_pushArg {Pred : Type u} {EPosts : Type v} {α : Type w} {σ : Type z} (x : σ → PredTrans Pred EPosts (α × σ)) (post : α → σ → Pred) (eposts : EPosts) (s : σ) : (pushArg x).apply post eposts s = (x s).apply (fun (x : α × σ) => match x with | (a, s) => post a s) eposts

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

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

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

@[simp]

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

Unfolding popArg through apply.

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

Adds a state argument that the predicate transformer ignores.

@[simp]

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

Unfolding liftArg through apply.

@[instance_reducible]

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

@[simp]

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

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) (eposts : ε → Pred) : Except ε α → Pred

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

@[simp]

theorem Lean.Order.pushExcept_ok {α : Type u} {ε : Type v} {Pred : Type w} (post : α → Pred) (eposts : ε → Pred) (a : α) : pushExcept post eposts (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) (eposts : ε → Pred) (e : ε) : pushExcept post eposts (Except.error e) = eposts e

An exceptional result uses the exception postcondition.

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

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

@[simp]

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

A present result uses the normal postcondition.

@[simp]

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

An absent result uses the absent postcondition.

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

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.

@[simp]

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

Unfolding lemma for pushExceptT.

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

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.

@[simp]

theorem Lean.Order.PredTrans.apply_pushOptionT {Pred : Type u} {EPosts : Type v} {α : Type w} (x : PredTrans Pred EPosts (Option α)) (post : α → Pred) (eposts : (Unit → Pred) × EPosts) : x.pushOptionT.apply post eposts = x.apply (pushOption post eposts.fst) eposts.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} {EPosts : Type v} {α : Type w} {ε : Type z} (e : ε) : PredTrans Pred ((ε → Pred) × EPosts) α

throw e asserts the first exception postcondition at e.

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

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

@[instance_reducible]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem Lean.Order.PredTrans.apply_MonadExcept_throw {ε α Pred : Type u} {EPosts : Type w} (e : ε) (post : α → Pred) (eposts : (ε → Pred) × EPosts) : (MonadExcept.throw e).apply post eposts = eposts.fst e

@[simp]

theorem Lean.Order.PredTrans.apply_MonadExcept_tryCatch {ε α Pred : Type u} {EPosts : Type w} (x : PredTrans Pred ((ε → Pred) × EPosts) α) (handle : ε → PredTrans Pred ((ε → Pred) × EPosts) α) (post : α → Pred) (eposts : (ε → Pred) × EPosts) : (MonadExcept.tryCatch x handle).apply post eposts = x.apply post (fun (e : ε) => (handle e).apply post eposts, eposts.snd)

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

Adds a first exception postcondition that the predicate transformer ignores.

@[simp]

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

Unfolding liftExcept through apply.

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

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

@[simp]

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

Unfolding popExcept through apply.

@[instance_reducible]

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

State Instances

Standard state and reader class instances for PredTrans.

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

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

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

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

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

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

@[instance_reducible]

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

@[instance_reducible]

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

@[simp]

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

Unfolding get through apply.

@[simp]

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

Unfolding set through apply.

@[simp]

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

Unfolding modifyGet through apply.

@[simp]

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

Unfolding read through apply.

@[simp]

theorem Lean.Order.PredTrans.apply_MonadState_get {Pred : Type u} {EPosts : Type v} {σ : Type z} (post : σ → σ → Pred) (eposts : EPosts) (s : σ) : MonadState.get.apply post eposts s = post s s

@[simp]

theorem Lean.Order.PredTrans.apply_MonadState_modifyGet {Pred : Type u} {EPosts : Type v} {σ α : Type z} (f : σ → α × σ) (post : α → σ → Pred) (eposts : EPosts) (s : σ) : (MonadState.modifyGet f).apply post eposts s = post (f s).fst (f s).snd

@[simp]

theorem Lean.Order.PredTrans.apply_modify {Pred : Type u} {EPosts : Type v} {σ : Type z} (f : σ → σ) (post : PUnit → σ → Pred) (eposts : EPosts) (s : σ) : (modify f).apply post eposts s = post PUnit.unit (f s)

@[simp]

theorem Lean.Order.PredTrans.apply_modifyThe {Pred : Type u} {EPosts : Type v} {σ : Type z} (f : σ → σ) (post : PUnit → σ → Pred) (eposts : EPosts) (s : σ) : (modifyThe σ f).apply post eposts s = post PUnit.unit (f s)

@[simp]

theorem Lean.Order.PredTrans.apply_MonadReader_read {Pred : Type u} {EPosts : Type v} {σ : Type z} (post : σ → σ → Pred) (eposts : EPosts) (s : σ) : read.apply post eposts s = post s s

@[instance_reducible]

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