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.Internal.Do.WPMonad.read_ReaderT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ρ : Type u}
(post : ρ → ρ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (r : ρ) => post r r) (wp MonadReaderOf.read post epost)
@[simp]
theorem
Std.Internal.Do.WPMonad.adapt_ReaderT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ρ ρ' α : Type u}
{post : α → ρ → Pred}
{epost : 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.Internal.Do.WPMonad.get_StateT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{σ : Type u}
(post : σ → σ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (s : σ) => post s s) (wp MonadStateOf.get post epost)
theorem
Std.Internal.Do.WPMonad.set_StateT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{σ : Type u}
(x : σ)
(post : PUnit → σ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (x_1 : σ) => post PUnit.unit x) (wp (set x) post epost)
theorem
Std.Internal.Do.WPMonad.modifyGet_StateT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{σ α : Type u}
(f : σ → α × σ)
(post : α → σ → Pred)
(epost : EPred)
:
Lean.Order.PartialOrder.rel (fun (s : σ) => post (f s).fst (f s).snd) (wp (MonadStateOf.modifyGet f) post epost)
theorem
Std.Internal.Do.WPMonad.get_EStateM_wp
{ε σ : Type u_1}
{post : σ → σ → Prop}
{epost : ε → σ → Prop}
:
theorem
Std.Internal.Do.WPMonad.set_EStateM_wp
{σ ε : Type u_1}
{post : PUnit → σ → Prop}
{epost : ε → σ → Prop}
(x : σ)
:
theorem
Std.Internal.Do.WPMonad.modify_EStateM_wp
{σ ε : Type u_1}
{post : PUnit → σ → Prop}
{epost : ε → σ → Prop}
(f : σ → σ)
:
MonadExceptOf simp lemmas #
theorem
Std.Internal.Do.WPMonad.throw_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε → Pred) EPred}
(err : ε)
:
Lean.Order.PartialOrder.rel (epost.head err) (wp (MonadExceptOf.throw err) post epost)
@[simp]
theorem
Std.Internal.Do.WPMonad.throw_EStateM_wp
{ε σ α : Type u_1}
{post : α → σ → Prop}
{epost : ε → σ → Prop}
(e : ε)
:
@[simp]
theorem
Std.Internal.Do.WPMonad.throw_Option_wp
{α : Type u_1}
{post : α → Prop}
{epost : Prop}
(e : PUnit)
:
theorem
Std.Internal.Do.WPMonad.throw_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
(err : PUnit)
:
Lean.Order.PartialOrder.rel epost.head (wp (MonadExceptOf.throw err) post epost)
theorem
Std.Internal.Do.WPMonad.tryCatch_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε → 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.Internal.Do.WPMonad.tryCatch_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ 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.Internal.Do.WPMonad.modifyThe_StateT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{σ : Type u}
{post : PUnit → σ → Pred}
{epost : EPred}
(f : σ → σ)
:
wp (modifyThe σ f) post epost = wp (MonadStateOf.modifyGet fun (s : σ) => (PUnit.unit, f s)) post epost
@[simp]
@[simp]
MonadLift simp lemmas #
theorem
Std.Internal.Do.WPMonad.monadLift_StateT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α σ : Type u}
{epost : 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.Internal.Do.WPMonad.monadLift_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α ε : Type u}
(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.Internal.Do.WPMonad.monadLift_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
(x : m α)
:
Lean.Order.PartialOrder.rel (wp x post epost.tail) (wp (MonadLift.monadLift x) post epost)
@[simp]
theorem
Std.Internal.Do.WPMonad.lift_OptionT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
[Assertion (EPost.cons✝ Pred EPred)]
[WPMonad (OptionT m) Pred (EPost.cons✝ Pred EPred)]
(x : m α)
:
MonadFunctor simp lemmas #
@[simp]
@[simp]
@[simp]
theorem
Std.Internal.Do.WPMonad.monadMap_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ε : Type u}
(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.Internal.Do.WPMonad.monadMap_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad 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.Internal.Do.WPMonad.withReader_ReaderT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ρ α : Type u}
{post : α → ρ → Pred}
{epost : 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.Internal.Do.WPMonad.adapt_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ε ε' α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε' → 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.Internal.Do.WPMonad.adaptExcept_EStateM_wp
{ε ε' σ α : Type u_1}
{post : α → σ → Prop}
{epost : ε' → σ → Prop}
(f : ε → ε')
(x : EStateM ε σ α)
:
MonadControl simp lemmas #
@[simp]
@[simp]
theorem
Std.Internal.Do.WPMonad.liftWith_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε → Pred) EPred}
(f : ({β : Type u} → ExceptT ε m β → m (Except ε β)) → m α)
:
@[simp]
theorem
Std.Internal.Do.WPMonad.liftWith_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ 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.Internal.Do.WPMonad.restoreM_StateT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α σ : Type u}
{epost : EPred}
{post : α → σ → Pred}
(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.Internal.Do.WPMonad.controlAt_wp
{n : Type u_1 → Type u_2}
{m : Type u_1 → Type u_3}
{Pred : Type u_4}
{EPred : Type u_5}
{α : Type u_1}
{post : α → Pred}
{epost : EPred}
[Bind n]
[Monad m]
[Monad n]
[Assertion Pred]
[Assertion EPred]
[WPMonad n Pred EPred]
[MonadControlT m n]
(f : ({β : Type u_1} → n β → m (stM m n β)) → m (stM m n α))
:
@[simp]
theorem
Std.Internal.Do.WPMonad.control_wp
{n : Type u_1 → Type u_2}
{m : Type u_1 → Type u_3}
{Pred : Type u_4}
{EPred : Type u_5}
{α : Type u_1}
{post : α → Pred}
{epost : EPred}
[Bind n]
[Monad m]
[Monad n]
[Assertion Pred]
[Assertion EPred]
[WPMonad n Pred EPred]
[MonadControlT m n]
(f : ({β : Type u_1} → n β → m (stM m n β)) → m (stM m n α))
:
@[simp]
Transitive lift/map/control simp lemmas #
@[simp]
theorem
Std.Internal.Do.WPMonad.monadMap_trans_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m n o : Type u → Type v}
[Monad o]
[Assertion Pred]
[Assertion EPred]
[WPMonad o Pred EPred]
{α : Type u}
{f : {β : Type u} → m β → m β}
{post : α → Pred}
{epost : EPred}
[MonadFunctor n o]
[MonadFunctorT m n]
(x : o α)
:
@[simp]
theorem
Std.Internal.Do.WPMonad.liftWith_trans_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m n o : Type u → Type v}
[Monad o]
[Assertion Pred]
[Assertion EPred]
[WPMonad o Pred EPred]
{α : Type u}
{post : α → Pred}
{epost : EPred}
[MonadControl n o]
[MonadControlT m n]
(f : ({β : Type u} → o β → m (stM m o β)) → m α)
:
@[simp]
theorem
Std.Internal.Do.WPMonad.restoreM_trans_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m n o : Type u → Type v}
[Monad o]
[Assertion Pred]
[Assertion EPred]
[WPMonad o Pred EPred]
{α : Type u}
{post : α → Pred}
{epost : EPred}
[MonadControl n o]
[MonadControlT m n]
(x : stM m o α)
:
Lifted state/reader operations #
@[simp]
Lifted except operations #
@[simp]
theorem
Std.Internal.Do.WPMonad.throw_lift_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{ε : Type u}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{ε' α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε' → Pred) EPred}
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadExceptOf.throw err) (EPost.cons.pushExcept post epost) epost.tail
@[simp]
theorem
Std.Internal.Do.WPMonad.throw_lift_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{ε : Type u}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadExceptOf.throw err) (EPost.cons.pushOption post epost) epost.tail
@[simp]
theorem
Std.Internal.Do.WPMonad.tryCatch_lift_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{ε : Type u}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{ε' α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε' → Pred) EPred}
(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.Internal.Do.WPMonad.tryCatch_lift_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{ε : Type u}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ Pred EPred}
(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.Internal.Do.WPMonad.throw_ReaderT_lift_wp
{Pred : Type u_1}
{EPred : Type u_2}
{ε : Type u_3}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{ρ α : Type u}
{post : α → ρ → Pred}
{epost : EPred}
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost
@[simp]
theorem
Std.Internal.Do.WPMonad.throw_StateT_lift_wp
{Pred : Type u_1}
{EPred : Type u_2}
{ε : Type u_3}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{σ α : Type u}
{post : α → σ → Pred}
{epost : EPred}
(err : ε)
:
wp (MonadExceptOf.throw err) post epost = wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost
@[simp]
theorem
Std.Internal.Do.WPMonad.tryCatch_ReaderT_lift_wp
{Pred : Type u_1}
{EPred : Type u_2}
{ε : Type u_3}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{ρ α : Type u}
{post : α → ρ → Pred}
{epost : EPred}
(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.Internal.Do.WPMonad.tryCatch_StateT_lift_wp
{Pred : Type u_1}
{EPred : Type u_2}
{ε : Type u_3}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
[MonadExceptOf ε m]
{σ α : Type u}
{post : α → σ → Pred}
{epost : EPred}
(x : StateT σ m α)
(h : ε → StateT σ m α)
:
OrElse simp lemmas #
theorem
Std.Internal.Do.WPMonad.orElse_ExceptT_wp
{Pred : Type u_1}
{EPred : Type u_2}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{ε α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ (ε → 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.Internal.Do.WPMonad.orElse_OptionT_wp
{Pred : Type u}
{EPred : Type u_1}
{m : Type u → Type v}
[Monad m]
[Assertion Pred]
[Assertion EPred]
[WPMonad m Pred EPred]
{α : Type u}
{post : α → Pred}
{epost : EPost.cons✝ 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)