feat: define Triple.iff, Triple.iff_conseq etc. and use defeq less (#12250)
This PR introduces the defining equality `Triple.iff` and uses that in proofs instead of relying on definitional equality. It also introduces `Triple.iff_conseq` that is useful for backward reasoning and introduces verification conditions. Similarly, `Triple.entails_wp_*` theorems are introduced for backward reasoning where the target is an stateful entailment rather than a triple.
This commit is contained in:
Sebastian Graf
GitHub
parent
5ce756f350
commit
2f3912df74
2 changed files with 134 additions and 89 deletions
|
|
@ -52,21 +52,44 @@ meta def unexpandTriple : Lean.PrettyPrinter.Unexpander
|
|||
|
||||
namespace Triple
|
||||
|
||||
theorem iff [WP m ps] {α : Type u} {x : m α} {P : Assertion ps} {Q : PostCond α ps} :
|
||||
(Triple x P Q) ↔ (P ⊢ₛ wp⟦x⟧ Q) := by rfl
|
||||
|
||||
theorem iff_conseq [WP m ps] {α : Type u} {x : m α} {P : Assertion ps} {Q : PostCond α ps} :
|
||||
(Triple x P Q) ↔ (∀ ⦃P' Q'⦄, (P' ⊢ₛ P) → (Q ⊢ₚ Q') → P' ⊢ₛ wp⟦x⟧ Q') := by
|
||||
constructor
|
||||
· intro h P' Q' hP hQ;
|
||||
apply SPred.entails.trans hP
|
||||
apply SPred.entails.trans h
|
||||
apply (wp x).mono _ _ hQ
|
||||
. intro h; apply h .rfl .rfl
|
||||
|
||||
theorem entails_wp_of_pre_post [WP m ps] {α : Type u} {x : m α} {P P' : Assertion ps} {Q Q' : PostCond α ps}
|
||||
(h : Triple x P' Q') (hpre : P ⊢ₛ P') (hpost : Q' ⊢ₚ Q) : P ⊢ₛ wp⟦x⟧ Q := Triple.iff_conseq.mp h hpre hpost
|
||||
|
||||
theorem entails_wp_of_pre [WP m ps] {α : Type u} {x : m α} {P P' : Assertion ps} {Q : PostCond α ps}
|
||||
(h : Triple x P' Q) (hpre : P ⊢ₛ P') : P ⊢ₛ wp⟦x⟧ Q := Triple.iff_conseq.mp h hpre .rfl
|
||||
|
||||
theorem entails_wp_of_post [WP m ps] {α : Type u} {x : m α} {P : Assertion ps} {Q Q' : PostCond α ps}
|
||||
(h : Triple x P Q') (hpost : Q' ⊢ₚ Q) : P ⊢ₛ wp⟦x⟧ Q := Triple.iff_conseq.mp h .rfl hpost
|
||||
|
||||
instance [WP m ps] (x : m α) : SPred.Tactic.PropAsSPredTautology (Triple x P Q) spred(P → wp⟦x⟧ Q) where
|
||||
iff := (SPred.entails_true_intro P (wp⟦x⟧ Q)).symm
|
||||
iff := Triple.iff |>.trans (SPred.entails_true_intro _ _).symm
|
||||
|
||||
theorem pure [Monad m] [WPMonad m ps] {α : Type u} {Q : PostCond α ps} (a : α) (himp : P ⊢ₛ Q.1 a) :
|
||||
Triple (pure (f:=m) a) P Q := himp.trans (by simp)
|
||||
Triple (pure (f:=m) a) P Q := Triple.iff.mpr (himp.trans (by simp))
|
||||
|
||||
theorem bind [Monad m] [WPMonad m ps] {α β : Type u} {P : Assertion ps} {Q : α → Assertion ps} {R : PostCond β ps} (x : m α) (f : α → m β)
|
||||
theorem bind [Monad m] [WPMonad m ps] {α β : Type u} {P : Assertion ps} {Q : α → Assertion ps} {R : PostCond β ps}
|
||||
(x : m α) (f : α → m β)
|
||||
(hx : Triple x P (Q, R.2))
|
||||
(hf : ∀ b, Triple (f b) (Q b) R) :
|
||||
Triple (x >>= f) P R := by
|
||||
apply SPred.entails.trans hx
|
||||
apply Triple.iff.mpr
|
||||
apply SPred.entails.trans (Triple.iff.mp hx)
|
||||
simp only [WP.bind]
|
||||
apply (wp x).mono _ _
|
||||
simp only [PostCond.entails, Assertion, ExceptConds.entails.refl, and_true]
|
||||
exact hf
|
||||
exact (fun b => Triple.iff.mp (hf b))
|
||||
|
||||
/--
|
||||
Conjunction for two Hoare triple specifications of a program `x`.
|
||||
|
|
@ -74,7 +97,7 @@ This theorem is useful for decomposing proofs, because unrelated facts about `x`
|
|||
separately and then combined with this theorem.
|
||||
-/
|
||||
theorem and [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ Q₂) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
|
||||
(SPred.and_mono h₁ h₂).trans ((wp x).conjunctive Q₁ Q₂).mpr
|
||||
Triple.iff.mpr <| (SPred.and_mono (Triple.iff.mp h₁) (Triple.iff.mp h₂)).trans ((wp x).conjunctive Q₁ Q₂).mpr
|
||||
|
||||
/--
|
||||
Modus ponens for two Hoare triple specifications of a program `x`.
|
||||
|
|
@ -83,6 +106,6 @@ This theorem is useful for separating proofs. If `h₁ : Triple x P₁ Q₁` pro
|
|||
for `Q₁`, then `mp x h₁ h₂` is a proof for `Q₂` about `x`.
|
||||
-/
|
||||
theorem mp [WP m ps] (x : m α) (h₁ : Triple x P₁ Q₁) (h₂ : Triple x P₂ (Q₁ →ₚ Q₂)) : Triple x spred(P₁ ∧ P₂) (Q₁ ∧ₚ Q₂) :=
|
||||
SPred.and_mono h₁ h₂ |>.trans ((wp x).conjunctive Q₁ (Q₁ →ₚ Q₂)).mpr |>.trans ((wp x).mono _ _ PostCond.and_imp)
|
||||
Triple.iff.mpr <| SPred.and_mono (Triple.iff.mp h₁) (Triple.iff.mp h₂) |>.trans ((wp x).conjunctive Q₁ (Q₁ →ₚ Q₂)).mpr |>.trans ((wp x).mono _ _ PostCond.and_imp)
|
||||
|
||||
end Triple
|
||||
|
|
|
|||
|
|
@ -172,51 +172,69 @@ variable {m : Type u → Type v} {ps : PostShape.{u}}
|
|||
|
||||
theorem Spec.pure' [Monad m] [WPMonad m ps] {P : Assertion ps} {Q : PostCond α ps}
|
||||
(h : P ⊢ₛ Q.1 a) :
|
||||
Triple (Pure.pure (f:=m) a) (spred(P)) spred(Q) := Triple.pure a h
|
||||
Triple (Pure.pure (f:=m) a) P Q := Triple.pure a h
|
||||
|
||||
@[spec]
|
||||
theorem Spec.pure [Monad m] [WPMonad m ps] {α} {a : α} {Q : PostCond α ps} :
|
||||
Triple (Pure.pure (f:=m) a) (spred(Q.1 a)) spred(Q) := Spec.pure' .rfl
|
||||
Triple (Pure.pure (f:=m) a) (spred(Q.1 a)) Q := Spec.pure' .rfl
|
||||
|
||||
theorem Spec.bind' [Monad m] [WPMonad m ps] {x : m α} {f : α → m β} {P : Assertion ps} {Q : PostCond β ps}
|
||||
(h : Triple x (spred(P)) (spred(fun a => wp⟦f a⟧ Q), Q.2)) :
|
||||
Triple (x >>= f) (spred(P)) spred(Q) := Triple.bind x f h (fun _ => .rfl)
|
||||
(h : Triple x P (spred(fun a => wp⟦f a⟧ Q), Q.2)) :
|
||||
Triple (x >>= f) P Q := Triple.bind x f h (fun _ => Triple.iff.mpr .rfl)
|
||||
|
||||
@[spec]
|
||||
theorem Spec.bind [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → m β} {Q : PostCond β ps} :
|
||||
Triple (x >>= f) (spred(wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2))) spred(Q) := Spec.bind' .rfl
|
||||
Triple (x >>= f) (spred(wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.2))) Q := Spec.bind' (Triple.iff.mpr .rfl)
|
||||
|
||||
theorem Spec.map' [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → β} {Q : PostCond β ps}
|
||||
(h : Triple x P (fun a => Q.1 (f a), Q.2)) :
|
||||
Triple (f <$> x) P Q := by
|
||||
apply Triple.iff.mpr
|
||||
rw [WPMonad.wp_map]
|
||||
apply h.entails_wp_of_post
|
||||
simp
|
||||
|
||||
@[spec]
|
||||
theorem Spec.map [Monad m] [WPMonad m ps] {α β} {x : m α} {f : α → β} {Q : PostCond β ps} :
|
||||
Triple (f <$> x) (spred(wp⟦x⟧ (fun a => Q.1 (f a), Q.2))) spred(Q) := by simp [Triple, SPred.entails.refl]
|
||||
Triple (f <$> x) (spred(wp⟦x⟧ (fun a => Q.1 (f a), Q.2))) Q := Spec.map' (Triple.iff.mpr .rfl)
|
||||
|
||||
theorem Spec.seq' [Monad m] [WPMonad m ps] {α β} {x : m (α → β)} {y : m α} {Q : PostCond β ps}
|
||||
(h : Triple x P (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2)) :
|
||||
Triple (x <*> y) P Q := by
|
||||
apply Triple.iff.mpr
|
||||
rw [WPMonad.wp_seq]
|
||||
apply h.entails_wp_of_post
|
||||
simp only [PostCond.entails, ExceptConds.entails.refl, and_true]
|
||||
intro _
|
||||
rfl
|
||||
|
||||
@[spec]
|
||||
theorem Spec.seq [Monad m] [WPMonad m ps] {α β} {x : m (α → β)} {y : m α} {Q : PostCond β ps} :
|
||||
Triple (x <*> y) (spred(wp⟦x⟧ (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2))) spred(Q) := by simp [Triple, SPred.entails.refl]
|
||||
Triple (x <*> y) (spred(wp⟦x⟧ (fun f => wp⟦y⟧ (fun a => Q.1 (f a), Q.2), Q.2))) Q := Spec.seq' (Triple.iff.mpr .rfl)
|
||||
|
||||
/-! # `MonadLift` -/
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadLift_StateT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg σ ps)) :
|
||||
Triple (MonadLift.monadLift x : StateT σ m α) (spred(fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))) spred(Q) := by simp [Triple, SPred.entails.refl]
|
||||
Triple (MonadLift.monadLift x : StateT σ m α) (spred(fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))) Q := by simp [Triple.iff, SPred.entails.refl]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadLift_ReaderT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.arg ρ ps)) :
|
||||
Triple (MonadLift.monadLift x : ReaderT ρ m α) (spred(fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))) spred(Q) := by simp [Triple, SPred.entails.refl]
|
||||
Triple (MonadLift.monadLift x : ReaderT ρ m α) (spred(fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))) Q := by simp [Triple.iff, SPred.entails.refl]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadLift_ExceptT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except ε ps)) :
|
||||
Triple (ps:=.except ε ps)
|
||||
(MonadLift.monadLift x : ExceptT ε m α)
|
||||
(wp⟦x⟧ (fun a => Q.1 a, Q.2.2))
|
||||
Q := by simp [Triple, SPred.entails.refl]
|
||||
Q := by simp [Triple.iff, SPred.entails.refl]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadLift_OptionT [Monad m] [WPMonad m ps] (x : m α) (Q : PostCond α (.except PUnit ps)) :
|
||||
Triple (ps:=.except PUnit ps)
|
||||
(MonadLift.monadLift x : OptionT m α)
|
||||
(wp⟦x⟧ (fun a => Q.1 a, Q.2.2))
|
||||
Q := by simp [Triple, SPred.entails.refl]
|
||||
Q := by simp [Triple.iff, SPred.entails.refl]
|
||||
|
||||
/-! # `MonadLiftT` -/
|
||||
|
||||
|
|
@ -227,12 +245,12 @@ attribute [spec] liftM instMonadLiftTOfMonadLift instMonadLiftT
|
|||
@[spec]
|
||||
theorem Spec.monadMap_StateT [Monad m] [WP m ps]
|
||||
(f : ∀{β}, m β → m β) {α} (x : StateT σ m α) (Q : PostCond α (.arg σ ps)) :
|
||||
Triple (MonadFunctor.monadMap (m:=m) f x) (spred(fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2))) spred(Q) := .rfl
|
||||
Triple (MonadFunctor.monadMap (m:=m) f x) (spred(fun s => wp⟦f (x.run s)⟧ (fun (a, s) => Q.1 a s, Q.2))) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadMap_ReaderT [Monad m] [WP m ps]
|
||||
(f : ∀{β}, m β → m β) {α} (x : ReaderT ρ m α) (Q : PostCond α (.arg ρ ps)) :
|
||||
Triple (MonadFunctor.monadMap (m:=m) f x) (spred(fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2))) spred(Q) := .rfl
|
||||
Triple (MonadFunctor.monadMap (m:=m) f x) (spred(fun s => wp⟦f (x.run s)⟧ (fun a => Q.1 a s, Q.2))) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadMap_ExceptT [Monad m] [WP m ps]
|
||||
|
|
@ -240,7 +258,7 @@ theorem Spec.monadMap_ExceptT [Monad m] [WP m ps]
|
|||
Triple (ps:=.except ε ps)
|
||||
(MonadFunctor.monadMap (m:=m) f x)
|
||||
(wp⟦f x.run⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadMap_OptionT [Monad m] [WP m ps]
|
||||
|
|
@ -248,7 +266,7 @@ theorem Spec.monadMap_OptionT [Monad m] [WP m ps]
|
|||
Triple (ps:=.except PUnit ps)
|
||||
(MonadFunctor.monadMap (m:=m) f x)
|
||||
(wp⟦f x.run⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
/-! # `MonadFunctorT` -/
|
||||
|
||||
|
|
@ -257,11 +275,11 @@ theorem Spec.monadMap_trans [WP o ps] [MonadFunctor n o] [MonadFunctorT m n] :
|
|||
Triple (ps:=ps)
|
||||
(MonadFunctorT.monadMap f x : o α)
|
||||
(wp⟦MonadFunctor.monadMap (m:=n) (MonadFunctorT.monadMap (m:=m) f) x : o α⟧ Q)
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.monadMap_refl [WP m ps] :
|
||||
Triple (MonadFunctorT.monadMap f x : m α) (spred(wp⟦f x : m α⟧ Q)) spred(Q) := by simp [Triple]
|
||||
Triple (MonadFunctorT.monadMap f x : m α) (spred(wp⟦f x : m α⟧ Q)) Q := by simp [Triple.iff]
|
||||
|
||||
/-! # `MonadControl` -/
|
||||
|
||||
|
|
@ -271,7 +289,7 @@ theorem Spec.liftWith_StateT [Monad m] [WPMonad m ps]
|
|||
Triple
|
||||
(MonadControl.liftWith (m:=m) f)
|
||||
(fun s => wp⟦f (fun x => x.run s)⟧ (fun a => Q.1 a s, Q.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.liftWith_ReaderT [Monad m] [WPMonad m ps]
|
||||
|
|
@ -279,7 +297,7 @@ theorem Spec.liftWith_ReaderT [Monad m] [WPMonad m ps]
|
|||
Triple
|
||||
(MonadControl.liftWith (m:=m) f)
|
||||
(fun s => wp⟦f (fun x => x.run s)⟧ (fun a => Q.1 a s, Q.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.liftWith_ExceptT [Monad m] [WPMonad m ps]
|
||||
|
|
@ -287,7 +305,7 @@ theorem Spec.liftWith_ExceptT [Monad m] [WPMonad m ps]
|
|||
Triple (ps := .except ε ps)
|
||||
(MonadControl.liftWith (m:=m) f)
|
||||
(wp⟦f (fun x => x.run)⟧ (Q.1, Q.2.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.liftWith_OptionT [Monad m] [WPMonad m ps]
|
||||
|
|
@ -295,35 +313,35 @@ theorem Spec.liftWith_OptionT [Monad m] [WPMonad m ps]
|
|||
Triple (ps := .except PUnit ps)
|
||||
(MonadControl.liftWith (m:=m) f)
|
||||
(wp⟦f (fun x => x.run)⟧ (Q.1, Q.2.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.restoreM_StateT [Monad m] [WPMonad m ps] (x : m (α × σ)) :
|
||||
Triple
|
||||
(MonadControl.restoreM x : StateT σ m α)
|
||||
(fun _ => wp⟦x⟧ (fun (a, s) => Q.1 a s, Q.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.restoreM_ReaderT [Monad m] [WPMonad m ps] (x : m α) :
|
||||
Triple (m := ReaderT ρ m)
|
||||
(MonadControl.restoreM (m:=m) x)
|
||||
(fun s => wp⟦x⟧ (fun a => Q.1 a s, Q.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.restoreM_ExceptT [Monad m] [WPMonad m ps] (x : m (Except ε α)) :
|
||||
Triple (ps := .except ε ps)
|
||||
(MonadControl.restoreM x : ExceptT ε m α)
|
||||
(wp⟦x⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.restoreM_OptionT [Monad m] [WPMonad m ps] (x : m (Option α)) :
|
||||
Triple (ps := .except PUnit ps)
|
||||
(MonadControl.restoreM x : OptionT m α)
|
||||
(wp⟦x⟧ (fun e => e.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
/-! # `MonadControlT` -/
|
||||
|
||||
|
|
@ -333,7 +351,7 @@ theorem Spec.liftWith_trans [WP o ps] [MonadControl n o] [MonadControlT m n]
|
|||
Triple (m:=o)
|
||||
(MonadControlT.liftWith (m:=m) f)
|
||||
(wp⟦MonadControl.liftWith (m:=n) fun x₂ => MonadControlT.liftWith fun x₁ => f (x₁ ∘ x₂) : o α⟧ Q)
|
||||
Q := .rfl
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.liftWith_refl [WP m ps] [Pure m]
|
||||
|
|
@ -341,7 +359,7 @@ theorem Spec.liftWith_refl [WP m ps] [Pure m]
|
|||
Triple (m:=m)
|
||||
(MonadControlT.liftWith (m:=m) f)
|
||||
(wp⟦f (fun x => x) : m α⟧ Q)
|
||||
Q := .rfl
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.restoreM_trans [WP o ps] [MonadControl n o] [MonadControlT m n]
|
||||
|
|
@ -349,7 +367,7 @@ theorem Spec.restoreM_trans [WP o ps] [MonadControl n o] [MonadControlT m n]
|
|||
Triple (m:=o)
|
||||
(MonadControlT.restoreM (m:=m) x)
|
||||
(wp⟦MonadControl.restoreM (m:=n) (MonadControlT.restoreM (m:=m) x) : o α⟧ Q)
|
||||
Q := .rfl
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.restoreM_refl [WP m ps] [Pure m]
|
||||
|
|
@ -357,7 +375,7 @@ theorem Spec.restoreM_refl [WP m ps] [Pure m]
|
|||
Triple (m:=m)
|
||||
(MonadControlT.restoreM (m:=m) x)
|
||||
(wp⟦Pure.pure x : m α⟧ Q)
|
||||
Q := .rfl
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
attribute [spec] controlAt control
|
||||
|
||||
|
|
@ -367,15 +385,15 @@ attribute [spec] ReaderT.run
|
|||
|
||||
@[spec]
|
||||
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]
|
||||
Triple (MonadReaderOf.read : ReaderT ρ m ρ) (spred(fun r => Q.1 r r)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
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]
|
||||
Triple (MonadWithReaderOf.withReader f x : ReaderT ρ m α) (spred(fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r))) Q := by simp [Triple.iff]
|
||||
|
||||
@[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]
|
||||
Triple (ReaderT.adapt f x : ReaderT ρ m α) spred(fun r => wp⟦x⟧ (fun a _ => Q.1 a r, Q.2) (f r)) Q := by simp [Triple.iff]
|
||||
|
||||
/-! # `StateT` -/
|
||||
|
||||
|
|
@ -383,16 +401,16 @@ attribute [spec] StateT.run
|
|||
|
||||
@[spec]
|
||||
theorem Spec.get_StateT [Monad m] [WPMonad m psm] :
|
||||
Triple (MonadStateOf.get : StateT σ m σ) (spred(fun s => Q.1 s s)) spred(Q) := by simp [Triple]
|
||||
Triple (MonadStateOf.get : StateT σ m σ) (spred(fun s => Q.1 s s)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.set_StateT [Monad m] [WPMonad m psm] :
|
||||
Triple (MonadStateOf.set s : StateT σ m PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) spred(Q) := by simp [Triple]
|
||||
Triple (MonadStateOf.set s : StateT σ m PUnit) (spred(fun _ => Q.1 ⟨⟩ s)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.modifyGet_StateT [Monad m] [WPMonad m ps] :
|
||||
Triple (MonadStateOf.modifyGet f : StateT σ m α) (spred(fun s => let t := f s; Q.1 t.1 t.2)) spred(Q) := by
|
||||
simp [Triple]
|
||||
Triple (MonadStateOf.modifyGet f : StateT σ m α) (spred(fun s => let t := f s; Q.1 t.1 t.2)) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
/-! # `ExceptT` -/
|
||||
|
||||
|
|
@ -401,42 +419,42 @@ theorem Spec.run_ExceptT [WP m ps] (x : ExceptT ε m α) :
|
|||
Triple (ps:=ps)
|
||||
(x.run : m (Except ε α))
|
||||
(wp⟦x⟧ (fun a => Q.1 (.ok a), fun e => Q.1 (.error e), Q.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_ExceptT [Monad m] [WPMonad m ps] :
|
||||
Triple (MonadExceptOf.throw e : ExceptT ε m α) (spred(Q.2.1 e)) spred(Q) := by
|
||||
simp [Triple]
|
||||
Triple (MonadExceptOf.throw e : ExceptT ε m α) (spred(Q.2.1 e)) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.tryCatch_ExceptT [Monad m] [WPMonad m ps] (Q : PostCond α (.except ε ps)) :
|
||||
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]
|
||||
Triple (MonadExceptOf.tryCatch x h : ExceptT ε m α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[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]
|
||||
Triple (OrElse.orElse x h : ExceptT ε m α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[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]
|
||||
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.iff]
|
||||
|
||||
/-! # `Except` -/
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_Except [Monad m] [WPMonad m ps] :
|
||||
Triple (MonadExceptOf.throw e : Except ε α) (spred(Q.2.1 e)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadExceptOf.throw e : Except ε α) (spred(Q.2.1 e)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
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]
|
||||
Triple (MonadExceptOf.tryCatch x h : Except ε α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[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]
|
||||
Triple (OrElse.orElse x h : Except ε α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
/-! # `OptionT` -/
|
||||
|
||||
|
|
@ -445,72 +463,71 @@ theorem Spec.run_OptionT [WP m ps] (x : OptionT m α) :
|
|||
Triple (ps:=ps)
|
||||
(x.run : m (Option α))
|
||||
(wp⟦x⟧ (fun a => Q.1 (.some a), fun _ => Q.1 .none, Q.2))
|
||||
Q := by simp [Triple]
|
||||
Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_OptionT [Monad m] [WPMonad m ps] :
|
||||
Triple (MonadExceptOf.throw e : OptionT m α) (spred(Q.2.1 e)) spred(Q) := by
|
||||
simp [Triple]
|
||||
Triple (MonadExceptOf.throw e : OptionT m α) (spred(Q.2.1 e)) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.tryCatch_OptionT [Monad m] [WPMonad m ps] (Q : PostCond α (.except PUnit ps)) :
|
||||
Triple (MonadExceptOf.tryCatch x h : OptionT m α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
Triple (MonadExceptOf.tryCatch x h : OptionT m α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.orElse_OptionT [Monad m] [WPMonad m ps] (Q : PostCond α (.except PUnit ps)) :
|
||||
Triple (OrElse.orElse x h : OptionT m α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
Triple (OrElse.orElse x h : OptionT m α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
/-! # `Option` -/
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_Option [Monad m] [WPMonad m ps] :
|
||||
Triple (MonadExceptOf.throw e : Option α) (spred(Q.2.1 e)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadExceptOf.throw e : Option α) (spred(Q.2.1 e)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.tryCatch_Option (Q : PostCond α (.except PUnit .pure)) :
|
||||
Triple (MonadExceptOf.tryCatch x h : Option α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
Triple (MonadExceptOf.tryCatch x h : Option α) (spred(wp⟦x⟧ (Q.1, fun e => wp⟦h e⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.orElse_Option (Q : PostCond α (.except PUnit .pure)) :
|
||||
Triple (OrElse.orElse x h : Option α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) spred(Q) := by
|
||||
simp [Triple]
|
||||
Triple (OrElse.orElse x h : Option α) (spred(wp⟦x⟧ (Q.1, fun _ => wp⟦h ()⟧ Q, Q.2.2))) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
/-! # `EStateM` -/
|
||||
|
||||
@[spec]
|
||||
theorem Spec.get_EStateM :
|
||||
Triple (MonadStateOf.get : EStateM ε σ σ) (spred(fun s => Q.1 s s)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadStateOf.get : EStateM ε σ σ) (spred(fun s => Q.1 s s)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.set_EStateM :
|
||||
Triple (MonadStateOf.set s : EStateM ε σ PUnit) (spred(fun _ => Q.1 () s)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadStateOf.set s : EStateM ε σ PUnit) (spred(fun _ => Q.1 () s)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.modifyGet_EStateM :
|
||||
Triple (MonadStateOf.modifyGet f : EStateM ε σ α) (spred(fun s => let t := f s; Q.1 t.1 t.2)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadStateOf.modifyGet f : EStateM ε σ α) (spred(fun s => let t := f s; Q.1 t.1 t.2)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_EStateM :
|
||||
Triple (MonadExceptOf.throw e : EStateM ε σ α) (spred(Q.2.1 e)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadExceptOf.throw e : EStateM ε σ α) (spred(Q.2.1 e)) Q := by simp [Triple.iff]
|
||||
|
||||
open EStateM.Backtrackable in
|
||||
@[spec]
|
||||
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]
|
||||
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)) Q := by simp [Triple.iff]
|
||||
|
||||
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]
|
||||
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)) Q := by
|
||||
simp [Triple.iff]
|
||||
|
||||
@[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]
|
||||
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.iff]
|
||||
|
||||
/-! # Lifting `MonadStateOf` -/
|
||||
|
||||
|
|
@ -529,19 +546,19 @@ attribute [spec] throwThe tryCatchThe
|
|||
|
||||
@[spec]
|
||||
theorem Spec.throw_MonadExcept [MonadExceptOf ε m] [WP m _]:
|
||||
Triple (throw e : m α) (spred(wp⟦MonadExceptOf.throw e : m α⟧ Q)) spred(Q) := SPred.entails.rfl
|
||||
Triple (throw e : m α) (spred(wp⟦MonadExceptOf.throw e : m α⟧ Q)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.tryCatch_MonadExcept [MonadExceptOf ε m] [WP m ps] (Q : PostCond α ps) :
|
||||
Triple (tryCatch x h : m α) (spred(wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q)) spred(Q) := SPred.entails.rfl
|
||||
Triple (tryCatch x h : m α) (spred(wp⟦MonadExceptOf.tryCatch x h : m α⟧ Q)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_ReaderT [WP m sh] [MonadExceptOf ε m] :
|
||||
Triple (MonadExceptOf.throw e : ReaderT ρ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadExceptOf.throw e : ReaderT ρ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : ReaderT ρ m α⟧ Q)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg σ ps)) :
|
||||
Triple (MonadExceptOf.throw e : StateT σ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT σ m α⟧ Q)) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadExceptOf.throw e : StateT σ m α) (spred(wp⟦MonadLift.monadLift (MonadExceptOf.throw (ε:=ε) e : m α) : StateT σ m α⟧ Q)) Q := by simp [Triple.iff]
|
||||
|
||||
@[spec]
|
||||
theorem Spec.throw_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) :
|
||||
|
|
@ -549,7 +566,7 @@ theorem Spec.throw_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α
|
|||
(MonadExceptOf.throw e : ExceptT ε' m α)
|
||||
(wp⟦MonadExceptOf.throw (ε:=ε) e : m (Except ε' α)⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
|
||||
Q := by
|
||||
simp [Triple]
|
||||
simp [Triple.iff]
|
||||
apply (wp _).mono
|
||||
simp
|
||||
intro x
|
||||
|
|
@ -561,7 +578,7 @@ theorem Spec.throw_Option_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (
|
|||
(MonadExceptOf.throw e : OptionT m α)
|
||||
(wp⟦MonadExceptOf.throw (ε:=ε) e : m (Option α)⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
|
||||
Q := by
|
||||
simp [Triple]
|
||||
simp [Triple.iff]
|
||||
apply (wp _).mono
|
||||
simp
|
||||
intro x
|
||||
|
|
@ -569,11 +586,15 @@ theorem Spec.throw_Option_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (
|
|||
|
||||
@[spec]
|
||||
theorem Spec.tryCatch_ReaderT [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.arg ρ ps)) :
|
||||
Triple (MonadExceptOf.tryCatch x h : ReaderT ρ m α) (spred(fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2))) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadExceptOf.tryCatch x h : ReaderT ρ m α) (spred(fun r => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run r) (fun e => (h e).run r) : m α⟧ (fun a => Q.1 a r, Q.2))) Q := by
|
||||
apply Triple.iff.mpr
|
||||
rfl
|
||||
|
||||
@[spec]
|
||||
theorem Spec.tryCatch_StateT [WP m ps] [Monad m] [MonadExceptOf ε m] (Q : PostCond α (.arg σ ps)) :
|
||||
Triple (MonadExceptOf.tryCatch x h : StateT σ m α) (spred(fun s => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run s) (fun e => (h e).run s) : m (α × σ)⟧ (fun xs => Q.1 xs.1 xs.2, Q.2))) spred(Q) := SPred.entails.rfl
|
||||
Triple (MonadExceptOf.tryCatch x h : StateT σ m α) (spred(fun s => wp⟦MonadExceptOf.tryCatch (ε:=ε) (x.run s) (fun e => (h e).run s) : m (α × σ)⟧ (fun xs => Q.1 xs.1 xs.2, Q.2))) Q := by
|
||||
apply Triple.iff.mpr
|
||||
rfl
|
||||
|
||||
@[spec]
|
||||
theorem Spec.tryCatch_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond α (.except ε' ps)) :
|
||||
|
|
@ -582,7 +603,7 @@ theorem Spec.tryCatch_ExceptT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond
|
|||
(MonadExceptOf.tryCatch x h : ExceptT ε' m α)
|
||||
(wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Except ε' α)⟧ (fun e => e.casesOn Q.2.1 Q.1, Q.2.2))
|
||||
Q := by
|
||||
simp only [Triple]
|
||||
simp only [Triple.iff]
|
||||
apply (wp _).mono
|
||||
simp
|
||||
intro x
|
||||
|
|
@ -595,7 +616,7 @@ theorem Spec.tryCatch_OptionT_lift [WP m ps] [MonadExceptOf ε m] (Q : PostCond
|
|||
(MonadExceptOf.tryCatch x h : OptionT m α)
|
||||
(wp⟦MonadExceptOf.tryCatch (ε:=ε) x h : m (Option α)⟧ (fun o => o.casesOn (Q.2.1 ⟨⟩) Q.1, Q.2.2))
|
||||
Q := by
|
||||
simp only [Triple]
|
||||
simp only [Triple.iff]
|
||||
apply (wp _).mono
|
||||
simp
|
||||
intro x
|
||||
|
|
@ -747,8 +768,9 @@ theorem Spec.foldlM_list
|
|||
simp only [List.forIn_yield_eq_foldlM, id_map']
|
||||
rw[this]
|
||||
apply Spec.forIn_list inv
|
||||
simp only [Triple, WPMonad.wp_map, PredTrans.map_apply]
|
||||
exact step
|
||||
intros
|
||||
apply Spec.map'
|
||||
apply step <;> assumption
|
||||
|
||||
-- using the postcondition as a constant invariant:
|
||||
theorem Spec.foldlM_list_const_inv
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue