Simp lemmas for weakest preconditions #
This module provides simp lemmas for simplifying weakest precondition expressions.
Unlike Std.Do, we use direct function application wp x post epost without notation.
Some lemmas prove only one direction (⊑) instead of equality because our wp_bind axiom
only provides one direction.
MonadReaderOf simp lemmas #
theorem
Std.Do'.WP.read_ReaderT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ρ : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(post : ρ → ρ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (r : ρ) => post r r) (wp MonadReaderOf.read post epost)
@[simp]
theorem
Std.Do'.WP.adapt_ReaderT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ρ ρ' α : Type u}
{post : α → ρ → Pred}
{epost : EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : ρ → ρ')
(x : ReaderT ρ' m α)
:
wp (ReaderT.adapt f x) post epost = fun (r : ρ) => wp x (fun (a : α) (x : ρ') => post a r) epost (f r)
MonadStateOf simp lemmas #
theorem
Std.Do'.WP.get_StateT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{σ : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(post : σ → σ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (s : σ) => post s s) (wp MonadStateOf.get post epost)
theorem
Std.Do'.WP.set_StateT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{σ : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : σ)
(post : PUnit → σ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (x_1 : σ) => post PUnit.unit x) (wp (set x) post epost)
theorem
Std.Do'.WP.modifyGet_StateT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{σ α : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : σ → α × σ)
(post : α → σ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (s : σ) => post (f s).fst (f s).snd) (wp (MonadStateOf.modifyGet f) post epost)
@[simp]
@[simp]
theorem
Std.Do'.WP.set_EStateM_wp
{σ ε : Type u_1}
{post : PUnit → σ → Prop}
{epost : ε → σ → Prop}
(x : σ)
:
@[simp]
theorem
Std.Do'.WP.modify_EStateM_wp
{σ ε : Type u_1}
{post : PUnit → σ → Prop}
{epost : ε → σ → Prop}
(f : σ → σ)
:
MonadExceptOf simp lemmas #
theorem
Std.Do'.WP.throw_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε → Pred) EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(err : ε)
:
Lean.Order.PartialOrder.rel (epost.head err) (wp (MonadExceptOf.throw err) post epost)
@[simp]
theorem
Std.Do'.WP.throw_EStateM_wp
{ε σ α : Type u_1}
{post : α → σ → Prop}
{epost : ε → σ → Prop}
(e : ε)
:
@[simp]
theorem
Std.Do'.WP.throw_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred : Type u_1}
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(err : PUnit)
:
Lean.Order.PartialOrder.rel epost.head (wp (MonadExceptOf.throw err) post epost)
theorem
Std.Do'.WP.tryCatch_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε → Pred) EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : ExceptT ε m α)
(h : ε → ExceptT ε m α)
:
Lean.Order.PartialOrder.rel (wp x post (EPost.cons.mk✝ (fun (e : ε) => wp (h e) post epost) epost.tail))
(wp (MonadExceptOf.tryCatch x h) post epost)
@[simp]
theorem
Std.Do'.WP.tryCatch_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred : Type u_1}
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : OptionT m α)
(h : PUnit → OptionT m α)
:
Lean.Order.PartialOrder.rel (wp x post (EPost.cons.mk✝ (wp (h PUnit.unit) post epost) epost.tail))
(wp (MonadExceptOf.tryCatch x h) post epost)
Additional state operation lemmas #
@[simp]
theorem
Std.Do'.WP.modifyThe_StateT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{σ : Type u}
{post : PUnit → σ → Pred}
{epost : EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : σ → σ)
:
wp (modifyThe σ f) post epost = wp (MonadStateOf.modifyGet fun (s : σ) => (PUnit.unit, f s)) post epost
@[simp]
MonadLift simp lemmas #
theorem
Std.Do'.WP.monadLift_StateT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{α σ : Type u}
{epost : EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : m α)
(post : α → σ → Pred)
:
Lean.Order.PartialOrder.rel (fun (s : σ) => wp x (fun (a : α) => post a s) epost)
(wp (MonadLift.monadLift x) post epost)
theorem
Std.Do'.WP.monadLift_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{α ε : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : m α)
(post : α → Pred)
(epost : EPost.cons✝ (ε → Pred) EPred)
:
Lean.Order.PartialOrder.rel (wp x post epost.tail) (wp (MonadLift.monadLift x) post epost)
@[simp]
theorem
Std.Do'.WP.monadLift_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred : Type u_1}
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : m α)
:
Lean.Order.PartialOrder.rel (wp x post epost.tail) (wp (MonadLift.monadLift x) post epost)
@[simp]
theorem
Std.Do'.WP.lift_OptionT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
[Assertion (EPost.cons✝ Pred EPred)]
[WP (OptionT m) Pred (EPost.cons✝ Pred EPred)]
(x : m α)
:
MonadFunctor simp lemmas #
@[simp]
theorem
Std.Do'.WP.monadMap_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ε : Type u}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : {β : Type u} → m β → m β)
{α : Type u}
(x : ExceptT ε m α)
(post : α → Pred)
(epost : EPost.cons✝ (ε → Pred) EPred)
:
wp (MonadFunctor.monadMap (fun {β : Type u} => f) x) post epost = wp (f x.run) (EPost.cons.pushExcept post epost) epost.tail
@[simp]
theorem
Std.Do'.WP.monadMap_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred : Type u_1}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : {β : Type u} → m β → m β)
{α : Type u}
(x : OptionT m α)
(post : α → Pred)
(epost : EPost.cons✝ Pred EPred)
:
wp (MonadFunctor.monadMap (fun {β : Type u} => f) x) post epost = wp (f x.run) (EPost.cons.pushOption post epost) epost.tail
@[simp]
theorem
Std.Do'.WP.withReader_ReaderT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ρ α : Type u}
{post : α → ρ → Pred}
{epost : EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : ρ → ρ)
(x : ReaderT ρ m α)
:
wp (MonadWithReaderOf.withReader f x) post epost = fun (r : ρ) => wp x (fun (a : α) (x : ρ) => post a r) epost (f r)
Transformer adapt lemmas #
theorem
Std.Do'.WP.adapt_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ε ε' α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε' → Pred) EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : ε → ε')
(x : ExceptT ε m α)
:
Lean.Order.PartialOrder.rel (wp x post (EPost.cons.mk✝ (fun (e : ε) => epost.head (f e)) epost.tail))
(wp (ExceptT.adapt f x) post epost)
@[simp]
theorem
Std.Do'.WP.adaptExcept_EStateM_wp
{ε ε' σ α : Type u_1}
{post : α → σ → Prop}
{epost : ε' → σ → Prop}
(f : ε → ε')
(x : EStateM ε σ α)
:
MonadControl simp lemmas #
@[simp]
@[simp]
theorem
Std.Do'.WP.liftWith_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred : Type u_1}
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(f : ({β : Type u} → OptionT m β → m (Option β)) → m α)
:
Lean.Order.PartialOrder.rel (wp (f fun {β : Type u} (x : OptionT m β) => x.run) post epost.tail)
(wp (MonadControl.liftWith f) post epost)
theorem
Std.Do'.WP.restoreM_StateT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{α σ : Type u}
{epost : EPred}
{post : α → σ → Pred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : m (α × σ))
:
Lean.Order.PartialOrder.rel
(fun (x_1 : σ) =>
wp x
(fun (x : α × σ) =>
match x with
| (a, s) => post a s)
epost)
(wp (MonadControl.restoreM x) post epost)
@[simp]
theorem
Std.Do'.WP.controlAt_wp
{m : Type u → Type v}
{n : Type u → Type u_1}
{Pred : Type u_2}
{EPred : Type u_3}
{α : Type u}
{post : α → Pred}
{epost : EPred}
[Bind n]
[Monad n]
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP n Pred EPred]
[MonadControlT m n]
(f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α))
:
@[simp]
theorem
Std.Do'.WP.control_wp
{m : Type u → Type v}
{n : Type u → Type u_1}
{Pred : Type u_2}
{EPred : Type u_3}
{α : Type u}
{post : α → Pred}
{epost : EPred}
[Bind n]
[Monad n]
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP n Pred EPred]
[MonadControlT m n]
(f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α))
:
Transitive lift/map simp lemmas #
@[simp]
@[simp]
theorem
Std.Do'.WP.monadMap_trans_wp
{m : Type u → Type v}
{o : Type u → Type u_1}
{Pred : Type u_2}
{EPred : Type u_3}
{n : Type u → Type u_4}
{α : Type u}
{f : {β : Type u} → m β → m β}
{post : α → Pred}
{epost : EPred}
[Monad o]
[Assertion Pred]
[Assertion EPred]
[WP o Pred EPred]
[MonadFunctor n o]
[MonadFunctorT m n]
(x : o α)
:
Lifted state/reader/except operations #
@[simp]
@[simp]
theorem
Std.Do'.WP.modifyGet_MonadStateOf_lift_wp
{m : Type u → Type v}
{σ : Type u}
{n : Type u → Type u_1}
{Pred : Type u_2}
{EPred' : Type u_3}
{α : Type u}
{post : α → Pred}
{epost : EPred'}
[MonadStateOf σ m]
[MonadLift m n]
[Monad m]
[Monad n]
[Assertion Pred]
[Assertion EPred']
[WP n Pred EPred']
(f : σ → α × σ)
:
@[simp]
theorem
Std.Do'.WP.throw_lift_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred' : Type u_2}
{ε ε' α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε' → Pred) EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadExceptOf.throw err) (EPost.cons.pushExcept post epost) epost.tail
@[simp]
theorem
Std.Do'.WP.throw_lift_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred' : Type u_1}
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadExceptOf.throw err) (EPost.cons.pushOption post epost) epost.tail
@[simp]
theorem
Std.Do'.WP.tryCatch_lift_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred' : Type u_2}
{ε ε' α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε' → Pred) EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(x : ExceptT ε' m α)
(h : ε → ExceptT ε' m α)
:
wp (MonadExceptOf.tryCatch x h) post epost = wp (MonadExceptOf.tryCatch x h) (EPost.cons.pushExcept post epost) epost.tail
@[simp]
theorem
Std.Do'.WP.tryCatch_lift_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred' : Type u_1}
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(x : OptionT m α)
(h : ε → OptionT m α)
:
wp (MonadExceptOf.tryCatch x h) post epost = wp (MonadExceptOf.tryCatch x h) (EPost.cons.pushOption post epost) epost.tail
@[simp]
theorem
Std.Do'.WP.throw_ReaderT_lift_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred' : Type u_2}
{ε : Type u_3}
{ρ α : Type u}
{post : α → ρ → Pred}
{epost : EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost
@[simp]
theorem
Std.Do'.WP.throw_StateT_lift_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred' : Type u_2}
{ε : Type u_3}
{σ α : Type u}
{post : α → σ → Pred}
{epost : EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost
@[simp]
theorem
Std.Do'.WP.tryCatch_ReaderT_lift_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred' : Type u_2}
{ε : Type u_3}
{ρ α : Type u}
{post : α → ρ → Pred}
{epost : EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(x : ReaderT ρ m α)
(h : ε → ReaderT ρ m α)
:
wp (MonadExceptOf.tryCatch x h) post epost = fun (r : ρ) =>
wp (MonadExceptOf.tryCatch (x.run r) fun (e : ε) => (h e).run r) (fun (a : α) => post a r) epost
@[simp]
theorem
Std.Do'.WP.tryCatch_StateT_lift_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred' : Type u_2}
{ε : Type u_3}
{σ α : Type u}
{post : α → σ → Pred}
{epost : EPred'}
[Monad m]
[LawfulMonad m]
[Assertion Pred]
[Assertion EPred']
[WP m Pred EPred']
[MonadExceptOf ε m]
(x : StateT σ m α)
(h : ε → StateT σ m α)
:
Transitive MonadControl lemmas #
@[simp]
theorem
Std.Do'.WP.liftWith_trans_wp
{m : Type u → Type v}
{o : Type u → Type u_1}
{Pred : Type u_2}
{EPred : Type u_3}
{n : Type u → Type u_4}
{α : Type u}
{post : α → Pred}
{epost : EPred}
[Monad o]
[Assertion Pred]
[Assertion EPred]
[WP o Pred EPred]
[MonadControl n o]
[MonadControlT m n]
(f : ({β : Type u} → o β → m (stM m o β)) → m α)
:
@[simp]
theorem
Std.Do'.WP.restoreM_trans_wp
{m : Type u → Type v}
{o : Type u → Type u_1}
{Pred : Type u_2}
{EPred : Type u_3}
{n : Type u → Type u_4}
{α : Type u}
{post : α → Pred}
{epost : EPred}
[Monad o]
[Assertion Pred]
[Assertion EPred]
[WP o Pred EPred]
[MonadControl n o]
[MonadControlT m n]
(x : stM m o α)
:
OrElse simp lemmas #
theorem
Std.Do'.WP.orElse_ExceptT_wp
{m : Type u → Type v}
{Pred : Type u_1}
{EPred : Type u_2}
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε → Pred) EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : ExceptT ε m α)
(h : Unit → ExceptT ε m α)
:
Lean.Order.PartialOrder.rel (wp x post (EPost.cons.mk✝ (fun (x : ε) => wp (h ()) post epost) epost.tail))
(wp (OrElse.orElse x h) post epost)
@[simp]
theorem
Std.Do'.WP.orElse_OptionT_wp
{m : Type u → Type v}
{Pred : Type u}
{EPred : Type u_1}
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WP m Pred EPred]
(x : OptionT m α)
(h : Unit → OptionT m α)
:
Lean.Order.PartialOrder.rel (wp x post (EPost.cons.mk✝ (wp (h ()) post epost) epost.tail))
(wp (OrElse.orElse x h) post epost)