chore: add some missing spec lemmas (#10540)
This commit is contained in:
Sebastian Graf
GitHub
parent
b6198434f2
commit
eb9dd9a9e3
2 changed files with 80 additions and 5 deletions
|
|
@ -190,9 +190,13 @@ theorem Spec.read_ReaderT [Monad m] [WPMonad m psm] :
|
|||
Triple (MonadReaderOf.read : ReaderT ρ m ρ) (spred(fun r => Q.1 r r)) spred(Q) := by simp [Triple]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.withReader_ReaderT [Monad m] [WPMonad m psm] :
|
||||
theorem Spec.withReader_ReaderT [WP m psm] :
|
||||
Triple (MonadWithReaderOf.withReader f x : ReaderT ρ m α) (spred(fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r))) spred(Q) := by simp [Triple]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.adapt_ReaderT [WP m ps] (f : ρ → ρ') :
|
||||
Triple (ReaderT.adapt f x : ReaderT ρ m α) spred(fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r)) spred(Q) := by simp [Triple]
|
||||
|
||||
/-! # `StateT` -/
|
||||
|
||||
attribute [spec] StateT.run
|
||||
|
|
@ -229,6 +233,15 @@ theorem Spec.tryCatch_ExceptT [Monad m] [WPMonad m ps] (Q : PostCond α (.except
|
|||
Triple (MonadExceptOf.tryCatch x h : ExceptT ε m α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.orElse_ExceptT [Monad m] [WPMonad m ps] (Q : PostCond α (.except ε ps)) :
|
||||
Triple (OrElse.orElse x h : ExceptT ε m α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.adapt_ExceptT [Monad m] [WPMonad m ps] (f : ε → ε') (Q : PostCond α (.except ε' ps)) :
|
||||
Triple (ps := .except ε' ps) (ExceptT.adapt f x : ExceptT ε' m α) (wp⟦x⟧ (Q.1, fun e => Q.2.1 (f e), Q.2.2)) Q := by simp [Triple]
|
||||
|
||||
/-! # `Except` -/
|
||||
|
||||
@[spec]
|
||||
|
|
@ -240,6 +253,11 @@ theorem Spec.tryCatch_Except (Q : PostCond α (.except ε .pure)) :
|
|||
Triple (MonadExceptOf.tryCatch x h : Except ε α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.orElse_Except (Q : PostCond α (.except ε .pure)) :
|
||||
Triple (OrElse.orElse x h : Except ε α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
|
||||
/-! # `EStateM` -/
|
||||
|
||||
@[spec]
|
||||
|
|
@ -264,9 +282,19 @@ theorem Spec.tryCatch_EStateM (Q : PostCond α (.except ε (.arg σ .pure))) :
|
|||
Triple (MonadExceptOf.tryCatch x h : EStateM ε σ α) (spred(fun s => wp⟦x⟧ (Q.1, fun e s' => wp⟦h e⟧ Q (restore s' (save s)), Q.2.2) s)) spred(Q) := by
|
||||
simp [Triple]
|
||||
|
||||
open EStateM.Backtrackable in
|
||||
@[spec]
|
||||
theorem Spec.orElse_EStateM (Q : PostCond α (.except ε (.arg σ .pure))) :
|
||||
Triple (OrElse.orElse x h : EStateM ε σ α) (spred(fun s => wp⟦x⟧ (Q.1, fun _ s' => wp⟦h ()⟧ Q (restore s' (save s)), Q.2.2) s)) spred(Q) := by
|
||||
simp [Triple]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.adaptExcept_EStateM (f : ε → ε') (Q : PostCond α (.except ε' (.arg σ .pure))) :
|
||||
Triple (ps := .except ε' (.arg σ .pure)) (EStateM.adaptExcept f x : EStateM ε' σ α) (wp⟦x⟧ (Q.1, fun e => Q.2.1 (f e), Q.2.2)) Q := by simp [Triple]
|
||||
|
||||
/-! # Lifting `MonadStateOf` -/
|
||||
|
||||
attribute [spec] modify modifyThe getThe
|
||||
attribute [spec] modify modifyThe getThe getModify modifyGetThe
|
||||
instMonadStateOfMonadStateOf instMonadStateOfOfMonadLift
|
||||
|
||||
/-! # Lifting `MonadReaderOf` -/
|
||||
|
|
@ -328,6 +356,8 @@ theorem Spec.tryCatch_ExceptT_lift [WP m ps] [Monad m] [MonadExceptOf ε m] (Q :
|
|||
intro x
|
||||
split <;> rfl
|
||||
|
||||
/-! # Lifting `OrElse` -/
|
||||
|
||||
/-! # `ForIn` -/
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -109,7 +109,7 @@ theorem read_MonadReaderOf [MonadReaderOf ρ m] [MonadLift m n] [WP n _] :
|
|||
wp⟦MonadReaderOf.read : n ρ⟧ Q = wp⟦MonadLift.monadLift (MonadReader.read : m ρ) : n ρ⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem readThe [MonadReaderOf ρ m] [WP m ps] :
|
||||
theorem readThe_MonadReaderOf [MonadReaderOf ρ m] [WP m ps] :
|
||||
wp⟦readThe ρ : m ρ⟧ Q = wp⟦MonadReaderOf.read : m ρ⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
|
|
@ -159,6 +159,10 @@ theorem modify_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) :
|
|||
theorem modifyThe_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) :
|
||||
wp⟦modifyThe σ f : m PUnit⟧ Q = wp⟦MonadStateOf.modifyGet fun s => (⟨⟩, f s) : m PUnit⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem getModify_MonadStateOf [WP m ps] [MonadStateOf σ m] (f : σ → σ) :
|
||||
wp⟦getModify f : m σ⟧ Q = wp⟦MonadStateOf.modifyGet fun s => (s, f s) : m σ⟧ Q := rfl
|
||||
|
||||
-- instances
|
||||
|
||||
@[simp]
|
||||
|
|
@ -166,6 +170,10 @@ theorem read_ReaderT [Monad m] [WPMonad m ps] :
|
|||
wp⟦MonadReaderOf.read : ReaderT ρ m ρ⟧ Q = fun r => Q.1 r r := by
|
||||
simp [wp, MonadReaderOf.read, ReaderT.read]
|
||||
|
||||
@[simp]
|
||||
theorem adapt_ReaderT [WP m ps] (f : ρ → ρ') :
|
||||
wp⟦ReaderT.adapt f x : ReaderT ρ m α⟧ Q = fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r) := rfl
|
||||
|
||||
@[simp]
|
||||
theorem get_StateT [Monad m] [WPMonad m ps] :
|
||||
wp⟦MonadStateOf.get : StateT σ m σ⟧ Q = fun s => Q.1 s s := by
|
||||
|
|
@ -181,6 +189,14 @@ theorem modifyGet_StateT [Monad m] [WPMonad m ps] (f : σ → α × σ) :
|
|||
wp⟦MonadStateOf.modifyGet f : StateT σ m α⟧ Q = fun s => Q.1 (f s).1 (f s).2 := by
|
||||
simp [wp, MonadStateOf.modifyGet, StateT.modifyGet]
|
||||
|
||||
@[simp]
|
||||
theorem adapt_ExceptT [Monad m] [WPMonad m ps] (f : ε → ε') :
|
||||
wp⟦ExceptT.adapt f x : ExceptT ε' m α⟧ Q = wp⟦x⟧ (Q.1, fun e => Q.2.1 (f e), Q.2.2) := by
|
||||
simp [wp, ExceptT.adapt, ExceptT.mk, Except.mapError]
|
||||
congr
|
||||
ext x
|
||||
cases x <;> simp
|
||||
|
||||
@[simp]
|
||||
theorem get_EStateM :
|
||||
wp⟦MonadStateOf.get : EStateM ε σ σ⟧ Q = fun s => Q.1 s s := by
|
||||
|
|
@ -196,6 +212,13 @@ theorem modifyGet_EStateM (f : σ → α × σ) :
|
|||
wp⟦MonadStateOf.modifyGet f : EStateM ε σ α⟧ Q = fun s => Q.1 (f s).1 (f s).2 := by
|
||||
simp [wp, MonadStateOf.modifyGet, EStateM.modifyGet]
|
||||
|
||||
@[simp]
|
||||
theorem adaptExcept_EStateM (f : ε → ε') :
|
||||
wp⟦EStateM.adaptExcept f x : EStateM ε' σ α⟧ Q = wp⟦x⟧ (Q.1, fun e => Q.2.1 (f e), Q.2.2) := by
|
||||
simp [wp, EStateM.adaptExcept]
|
||||
ext s
|
||||
cases (x s) <;> simp
|
||||
|
||||
end MonadLift
|
||||
|
||||
/-! ## `MonadFunctor`
|
||||
|
|
@ -208,7 +231,7 @@ section MonadFunctor
|
|||
|
||||
open MonadFunctor renaming monadMap → mmap
|
||||
|
||||
-- The following 3 theorems are analogous to *.monadLift_apply.
|
||||
-- The following 3 theorems are analogous to monadLift_*.
|
||||
-- In the past, we experimented with a more tricky definition by rewriting to special monadMap defns on PredTrans, involving
|
||||
-- wp1 : (∀ {α}, m α → m α) → PredTrans ps α → PredTrans ps α
|
||||
-- that enjoys quite a tricky definition.
|
||||
|
|
@ -253,7 +276,7 @@ theorem withReader_MonadWithReader [MonadWithReaderOf ρ m] [WP m ps] (f : ρ
|
|||
wp⟦MonadWithReader.withReader f x⟧ Q = wp⟦MonadWithReaderOf.withReader f x⟧ Q := rfl
|
||||
|
||||
@[simp]
|
||||
theorem withTheReader [MonadWithReaderOf ρ m] [WP m ps] (f : ρ → ρ) (x : m α) :
|
||||
theorem withTheReader_MonadWithReaderOf [MonadWithReaderOf ρ m] [WP m ps] (f : ρ → ρ) (x : m α) :
|
||||
wp⟦withTheReader ρ f x⟧ Q = wp⟦MonadWithReaderOf.withReader f x⟧ Q := rfl
|
||||
|
||||
end MonadFunctor
|
||||
|
|
@ -376,3 +399,25 @@ example :
|
|||
-/
|
||||
|
||||
end MonadExceptOf
|
||||
|
||||
section OrElse
|
||||
|
||||
open EStateM.Backtrackable in
|
||||
@[simp]
|
||||
theorem orElse_EStateM {ε σ δ α x h Q} [EStateM.Backtrackable δ σ]:
|
||||
wp⟦OrElse.orElse x h : EStateM ε σ α⟧ Q = fun s => wp⟦x⟧ (Q.1, fun _ s' => wp⟦h ()⟧ Q (restore s' (save s)), Q.2.2) s := by
|
||||
ext s
|
||||
simp only [wp, OrElse.orElse, EStateM.orElse]
|
||||
cases x s <;> simp
|
||||
|
||||
@[simp]
|
||||
theorem orElse_Except :
|
||||
wp⟦OrElse.orElse x h : Except ε α⟧ Q = wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2) := by
|
||||
simp [OrElse.orElse, MonadExcept.orElse]
|
||||
|
||||
@[simp]
|
||||
theorem orElse_ExceptT [Monad m] [WPMonad m ps] :
|
||||
wp⟦OrElse.orElse x h : ExceptT ε m α⟧ Q = wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2) := by
|
||||
simp [OrElse.orElse, MonadExcept.orElse]
|
||||
|
||||
end OrElse
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue