Simp lemmas for working with weakest preconditions #
Many weakest preconditions are so simple that we can compute them directly or
express them in terms of "simpler" weakest preconditions.
This module provides simp lemmas targeting expressions of the form wp⟦x⟧ Q
and rewrites them to expressions of simpler weakest preconditions.
WP #
WPMonad #
MonadLift #
The definitions that follow interpret liftM and thus instances of, e.g., MonadStateOf.
@[simp]
theorem
Std.Do.WP.lift_StateT
{m : Type u → Type v}
{ps : PostShape}
{α σ : Type u}
{Q : PostCond α (PostShape.arg σ ps)}
[WP m ps]
[Monad m]
(x : m α)
:
@[simp]
theorem
Std.Do.WP.lift_ExceptT
{m : Type u → Type v}
{ps : PostShape}
{α ε : Type u}
{Q : PostCond α (PostShape.except ε ps)}
[WP m ps]
[Monad m]
(x : m α)
:
@[simp]
@[simp]
theorem
Std.Do.WP.modifyGetThe_MonadStateOf
{m : Type u → Type v}
{ps : PostShape}
{σ α : Type u}
{Q : PostCond α ps}
[WP m ps]
[MonadStateOf σ m]
(f : σ → α × σ)
:
@[simp]
theorem
Std.Do.WP.read_ReaderT
{m : Type u → Type v}
{ps : PostShape}
{ρ : Type u}
{Q : PostCond ρ (PostShape.arg ρ ps)}
[Monad m]
[WPMonad m ps]
:
@[simp]
theorem
Std.Do.WP.get_StateT
{m : Type u → Type v}
{ps : PostShape}
{σ : Type u}
{Q : PostCond σ (PostShape.arg σ ps)}
[Monad m]
[WPMonad m ps]
:
@[simp]
theorem
Std.Do.WP.get_EStateM
{ε σ : Type u_1}
{Q : PostCond σ (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
@[simp]
theorem
Std.Do.WP.set_EStateM
{σ ε : Type u_1}
{Q : PostCond PUnit (PostShape.except ε (PostShape.arg σ PostShape.pure))}
(x : σ)
:
@[simp]
theorem
Std.Do.WP.modifyGet_EStateM
{σ α ε : Type u_1}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
(f : σ → α × σ)
:
@[simp]
theorem
Std.Do.WP.adaptExcept_EStateM
{ε ε' σ α : Type u_1}
{x : EStateM ε σ α}
{Q : PostCond α (PostShape.except ε' (PostShape.arg σ PostShape.pure))}
(f : ε → ε')
:
MonadFunctor #
The definitions that follow interpret monadMap and thus instances of, e.g., MonadReaderWithOf.
@[simp]
theorem
Std.Do.WP.monadMap_trans
{m : Type u → Type v}
{ps : PostShape}
{o : Type u → Type u_1}
{n : Type u → Type u_2}
{α : Type u}
{f : {β : Type u} → m β → m β}
{x : o α}
{Q : PostCond α ps}
[WP o ps]
[MonadFunctor n o]
[MonadFunctorT m n]
:
@[simp]
theorem
Std.Do.WP.withReader_MonadWithReaderOf
{m : Type u → Type v}
{ρ : Type u}
{n : Type u → Type v}
{nsh : PostShape}
{α : Type u}
{Q : PostCond α nsh}
[MonadWithReaderOf ρ m]
[WP n nsh]
[MonadFunctor m n]
(f : ρ → ρ)
(x : n α)
:
wp⟦MonadWithReaderOf.withReader f x⟧ Q = wp⟦MonadFunctor.monadMap (fun {β : Type u} => MonadWithReaderOf.withReader f) x⟧ Q
@[simp]
theorem
Std.Do.WP.withReader_MonadWithReader
{m : Type u → Type v}
{ps : PostShape}
{ρ α : Type u}
{Q : PostCond α ps}
[MonadWithReaderOf ρ m]
[WP m ps]
(f : ρ → ρ)
(x : m α)
:
@[simp]
theorem
Std.Do.WP.withTheReader_MonadWithReaderOf
{m : Type u → Type v}
{ps : PostShape}
{ρ α : Type u}
{Q : PostCond α ps}
[MonadWithReaderOf ρ m]
[WP m ps]
(f : ρ → ρ)
(x : m α)
:
MonadControl #
The definitions that follow interpret liftWith and thus instances of, e.g., MonadReaderWithOf.
@[simp]
theorem
Std.Do.WP.liftWith_trans
{m : Type u → Type v}
{ps : PostShape}
{o : Type u → Type u_1}
{n : Type u → Type u_2}
{α : Type u}
{Q : PostCond α ps}
[WP o ps]
[MonadControl n o]
[MonadControlT m n]
(f : ({β : Type u} → o β → m (stM m o β)) → m α)
:
@[simp]
theorem
Std.Do.WP.restoreM_ExceptT
{m : Type u → Type v}
{ps : PostShape}
{ε α : Type u}
{Q : PostCond α (PostShape.except ε ps)}
[Monad m]
[WPMonad m ps]
(x : m (Except ε α))
:
@[simp]
MonadExceptOf #
The definitions that follow interpret throw, throwThe, tryCatch, etc.
Since MonadExceptOf cannot be lifted through MonadLift or MonadFunctor, there is one lemma per
MonadExceptOf operation and instance to lift through; the classic m*n instances problem.
@[simp]
theorem
Std.Do.WP.throwThe
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α : Type u}
{e : ε}
{Q : PostCond α ps}
[MonadExceptOf ε m]
[WP m ps]
:
@[simp]
theorem
Std.Do.WP.throw_Except
{ε α : Type u_1}
{e : ε}
{Q : PostCond α (PostShape.except ε PostShape.pure)}
:
@[simp]
theorem
Std.Do.WP.throw_EStateM
{ε σ α : Type u_1}
{e : ε}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
:
@[simp]
theorem
Std.Do.WP.throw_ReaderT
{m : Type u → Type v}
{sh : PostShape}
{ε : Type u_1}
{ρ α : Type u}
{e : ε}
{Q : PostCond α (PostShape.arg ρ sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
@[simp]
theorem
Std.Do.WP.throw_StateT
{m : Type u → Type v}
{sh : PostShape}
{ε : Type u_1}
{ρ α : Type u}
{e : ε}
{Q : PostCond α (PostShape.arg ρ sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
@[simp]
theorem
Std.Do.WP.throw_lift_ExceptT
{m : Type u → Type v}
{sh : PostShape}
{ε ε' α : Type u}
{e : ε}
{Q : PostCond α (PostShape.except ε' sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
@[simp]
theorem
Std.Do.WP.tryCatchThe
{m : Type u → Type v}
{ps : PostShape}
{ε : Type u_1}
{α : Type u}
{x : m α}
{h : ε → m α}
{Q : PostCond α ps}
[MonadExceptOf ε m]
[WP m ps]
:
@[simp]
theorem
Std.Do.WP.tryCatch_EStateM
{ε σ δ α : Type u_1}
{x : EStateM ε σ α}
{h : ε → EStateM ε σ α}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
[EStateM.Backtrackable δ σ]
:
@[simp]
theorem
Std.Do.WP.tryCatch_ReaderT
{m : Type u → Type v}
{sh : PostShape}
{ε : Type u_1}
{ρ α : Type u}
{x : ReaderT ρ m α}
{h : ε → ReaderT ρ m α}
{Q : PostCond α (PostShape.arg ρ sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
@[simp]
theorem
Std.Do.WP.tryCatch_StateT
{m : Type u → Type v}
{sh : PostShape}
{ε : Type u_1}
{σ α : Type u}
{x : StateT σ m α}
{h : ε → StateT σ m α}
{Q : PostCond α (PostShape.arg σ sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
@[simp]
theorem
Std.Do.WP.tryCatch_lift_ExceptT
{m : Type u → Type v}
{sh : PostShape}
{ε ε' α : Type u}
{x : ExceptT ε' m α}
{h : ε → ExceptT ε' m α}
{Q : PostCond α (PostShape.except ε' sh)}
[WP m sh]
[Monad m]
[MonadExceptOf ε m]
:
@[simp]
theorem
Std.Do.WP.orElse_EStateM
{ε σ δ α : Type u_1}
{x : EStateM ε σ α}
{h : Unit → EStateM ε σ α}
{Q : PostCond α (PostShape.except ε (PostShape.arg σ PostShape.pure))}
[EStateM.Backtrackable δ σ]
: