From 2f3912df74fc89d2d52e832ee18179137aae45f5 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Fri, 30 Jan 2026 15:03:22 +0100 Subject: [PATCH] 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. --- src/Std/Do/Triple/Basic.lean | 37 ++++-- src/Std/Do/Triple/SpecLemmas.lean | 186 +++++++++++++++++------------- 2 files changed, 134 insertions(+), 89 deletions(-) diff --git a/src/Std/Do/Triple/Basic.lean b/src/Std/Do/Triple/Basic.lean index 3e8cf5b1fa..fae333f9e6 100644 --- a/src/Std/Do/Triple/Basic.lean +++ b/src/Std/Do/Triple/Basic.lean @@ -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 diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean index 89b52c7309..5bd5f1cf18 100644 --- a/src/Std/Do/Triple/SpecLemmas.lean +++ b/src/Std/Do/Triple/SpecLemmas.lean @@ -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