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 eposts without notation.

Some lemmas prove only one direction (⊑) instead of equality because our bind_le_wp_bind axiom only provides one direction.

MonadReaderOf simp lemmas

theorem Std.WP.WPMonad.le_wp_read_ReaderT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ : Type u} (post : ρ → ρ → Pred) (eposts : EPosts) : Lean.Order.PartialOrder.rel (fun (r : ρ) => post r r) (wp MonadReaderOf.read post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_adapt_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ ρ' α : Type u} {post : α → ρ → Pred} {eposts : EPosts} (f : ρ → ρ') (x : ReaderT ρ' m α) : wp (ReaderT.adapt f x) post eposts = fun (r : ρ) => wp x (fun (a : α) (x : ρ') => post a r) eposts (f r)

MonadStateOf simp lemmas

theorem Std.WP.WPMonad.le_wp_get_StateT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} (post : σ → σ → Pred) (eposts : EPosts) : Lean.Order.PartialOrder.rel (fun (s : σ) => post s s) (wp MonadStateOf.get post eposts)

theorem Std.WP.WPMonad.le_wp_set_StateT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} (x : σ) (post : PUnit → σ → Pred) (eposts : EPosts) : Lean.Order.PartialOrder.rel (fun (x_1 : σ) => post PUnit.unit x) (wp (set x) post eposts)

theorem Std.WP.WPMonad.le_wp_modifyGet_StateT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ α : Type u} (f : σ → α × σ) (post : α → σ → Pred) (eposts : EPosts) : Lean.Order.PartialOrder.rel (fun (s : σ) => post (f s).fst (f s).snd) (wp (MonadStateOf.modifyGet f) post eposts)

theorem Std.WP.WPMonad.wp_get_EStateM_apply_eq {ε σ : Type} {post : σ → σ → Prop} {eposts : ε → σ → Prop} : wp MonadStateOf.get post eposts = fun (s : σ) => post s s

theorem Std.WP.WPMonad.wp_set_EStateM_apply_eq {σ ε : Type} {post : PUnit → σ → Prop} {eposts : ε → σ → Prop} (x : σ) : wp (set x) post eposts = fun (x_1 : σ) => post PUnit.unit x

theorem Std.WP.WPMonad.wp_modifyGet_EStateM_apply_eq {σ α ε : Type} {post : α → σ → Prop} {eposts : ε → σ → Prop} (f : σ → α × σ) : wp (MonadStateOf.modifyGet f) post eposts = fun (s : σ) => post (f s).fst (f s).snd

@[simp]

theorem Std.WP.WPMonad.wp_modify_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} {post : PUnit → σ → Pred} {eposts : EPosts} (f : σ → σ) : wp (modify f) post eposts = wp (MonadStateOf.modifyGet fun (s : σ) => (PUnit.unit, f s)) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_getModify_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} {post : σ → σ → Pred} {eposts : EPosts} (f : σ → σ) : wp (getModify f) post eposts = wp (MonadStateOf.modifyGet fun (s : σ) => (s, f s)) post eposts

theorem Std.WP.WPMonad.wp_modify_EStateM_apply_eq {σ ε : Type} {post : PUnit → σ → Prop} {eposts : ε → σ → Prop} (f : σ → σ) : wp (modify f) post eposts = wp (MonadStateOf.modifyGet fun (s : σ) => (PUnit.unit, f s)) post eposts

theorem Std.WP.WPMonad.wp_getModify_EStateM_apply_eq {σ ε : Type} {post : σ → σ → Prop} {eposts : ε → σ → Prop} (f : σ → σ) : wp (getModify f) post eposts = wp (MonadStateOf.modifyGet fun (s : σ) => (s, f s)) post eposts

MonadExceptOf simp lemmas

@[simp]

theorem Std.WP.WPMonad.wp_throwThe_apply_eq {Pred : Type u_2} {EPosts : Type u_3} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε : Type u_1} {α : Type u} {post : α → Pred} {eposts : EPosts} [MonadExceptOf ε m] (err : ε) : wp (throwThe ε err) post eposts = wp (MonadExceptOf.throw err) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_throw_Except_apply_eq {ε : Type u_1} {α : Type u_2} {post : α → Prop} {eposts : ε → Prop} (e : ε) : wp (MonadExceptOf.throw e) post eposts = eposts e

theorem Std.WP.WPMonad.le_wp_throw_ExceptT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε α : Type u} {post : α → Pred} {eposts : (ε → Pred) × EPosts} (err : ε) : Lean.Order.PartialOrder.rel (eposts.fst err) (wp (MonadExceptOf.throw err) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_throw_EStateM_apply_eq {ε σ α : Type} {post : α → σ → Prop} {eposts : ε → σ → Prop} (e : ε) : wp (MonadExceptOf.throw e) post eposts = eposts e

@[simp]

theorem Std.WP.WPMonad.wp_throw_Option_apply_eq {α : Type u_1} {post : α → Prop} {eposts : Unit → Prop} (e : PUnit) : wp (MonadExceptOf.throw e) post eposts = eposts ()

theorem Std.WP.WPMonad.le_wp_throw_OptionT_apply {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (err : PUnit) : Lean.Order.PartialOrder.rel (eposts.fst ()) (wp (MonadExceptOf.throw err) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_tryCatch_MonadExcept_apply_eq {Pred : Type u_2} {EPosts : Type u_3} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε : Type u_1} {α : Type u} {post : α → Pred} {eposts : EPosts} [MonadExceptOf ε m] (x : m α) (h : ε → m α) : wp (tryCatch x h) post eposts = wp (MonadExceptOf.tryCatch x h) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_tryCatchThe_apply_eq {Pred : Type u_2} {EPosts : Type u_3} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε : Type u_1} {α : Type u} {post : α → Pred} {eposts : EPosts} [MonadExceptOf ε m] (x : m α) (h : ε → m α) : wp (tryCatchThe ε x h) post eposts = wp (MonadExceptOf.tryCatch x h) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_tryCatch_Except_apply_eq {ε : Type u_1} {α : Type u_2} {post : α → Prop} {eposts : ε → Prop} (x : Except ε α) (h : ε → Except ε α) : wp (MonadExceptOf.tryCatch x h) post eposts = wp x post fun (e : ε) => wp (h e) post eposts

theorem Std.WP.WPMonad.le_wp_tryCatch_ExceptT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε α : Type u} {post : α → Pred} {eposts : (ε → Pred) × EPosts} (x : ExceptT ε m α) (h : ε → ExceptT ε m α) : Lean.Order.PartialOrder.rel (wp x post (fun (e : ε) => wp (h e) post eposts, eposts.snd)) (wp (MonadExceptOf.tryCatch x h) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_tryCatch_Option_apply_eq {α : Type u_1} {post : α → Prop} {eposts : Unit → Prop} (x : Option α) (h : PUnit → Option α) : wp (MonadExceptOf.tryCatch x h) post eposts = wp x post fun (x : Unit) => wp (h PUnit.unit) post eposts

theorem Std.WP.WPMonad.wp_tryCatch_EStateM_apply_eq {ε σ α : Type} {post : α → σ → Prop} {eposts : ε → σ → Prop} (x : EStateM ε σ α) (h : ε → EStateM ε σ α) : wp (MonadExceptOf.tryCatch x h) post eposts = fun (s : σ) => wp x post (fun (e : ε) (s' : σ) => wp (h e) post eposts s') s

@[simp]

theorem Std.WP.WPMonad.le_wp_tryCatch_OptionT_apply {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (x : OptionT m α) (h : PUnit → OptionT m α) : Lean.Order.PartialOrder.rel (wp x post (fun (x : Unit) => wp (h PUnit.unit) post eposts, eposts.snd)) (wp (MonadExceptOf.tryCatch x h) post eposts)

Additional state operation lemmas

@[simp]

theorem Std.WP.WPMonad.wp_getThe_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} {post : σ → σ → Pred} {eposts : EPosts} : wp (getThe σ) post eposts = wp MonadStateOf.get post eposts

@[simp]

theorem Std.WP.WPMonad.wp_modifyThe_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} {post : PUnit → σ → Pred} {eposts : EPosts} (f : σ → σ) : wp (modifyThe σ f) post eposts = wp (MonadStateOf.modifyGet fun (s : σ) => (PUnit.unit, f s)) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_modifyGetThe_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ α : Type u} {post : α → σ → Pred} {eposts : EPosts} (f : σ → α × σ) : wp (modifyGetThe σ f) post eposts = wp (MonadStateOf.modifyGet f) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_get_MonadState_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} {post : σ → Pred} {eposts : EPosts} [MonadStateOf σ m] : wp get post eposts = wp MonadStateOf.get post eposts

@[simp]

theorem Std.WP.WPMonad.wp_set_MonadState_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} {post : PUnit → Pred} {eposts : EPosts} [MonadStateOf σ m] (x : σ) : wp (MonadState.set x) post eposts = wp (set x) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_modifyGet_MonadState_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ α : Type u} {post : α → Pred} {eposts : EPosts} [MonadStateOf σ m] (f : σ → α × σ) : wp (modifyGet f) post eposts = wp (MonadStateOf.modifyGet f) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_read_MonadReader_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ : Type u} {post : ρ → Pred} {eposts : EPosts} [MonadReaderOf ρ m] : wp read post eposts = wp MonadReaderOf.read post eposts

@[simp]

theorem Std.WP.WPMonad.wp_readThe_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ : Type u} {post : ρ → ρ → Pred} {eposts : EPosts} : wp (readThe ρ) post eposts = wp MonadReaderOf.read post eposts

MonadLift simp lemmas

theorem Std.WP.WPMonad.le_wp_monadLift_StateT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α σ : Type u} {eposts : EPosts} (x : m α) (post : α → σ → Pred) : Lean.Order.PartialOrder.rel (fun (s : σ) => wp x (fun (a : α) => post a s) eposts) (wp (MonadLift.monadLift x) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_monadLift_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α ρ : Type u} {post : α → ρ → Pred} {eposts : EPosts} (x : m α) : wp (MonadLift.monadLift x) post eposts = fun (r : ρ) => wp x (fun (a : α) => post a r) eposts

theorem Std.WP.WPMonad.le_wp_monadLift_ExceptT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α ε : Type u} (x : m α) (post : α → Pred) (eposts : (ε → Pred) × EPosts) : Lean.Order.PartialOrder.rel (wp x post eposts.snd) (wp (MonadLift.monadLift x) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_lift_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α σ : Type u} {post : α → σ → Pred} {eposts : EPosts} (x : m α) : wp (StateT.lift x) post eposts = wp (MonadLift.monadLift x) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_lift_ExceptT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α ε : Type u} {post : α → Pred} {eposts : (ε → Pred) × EPosts} (x : m α) : wp (ExceptT.lift x) post eposts = wp (MonadLift.monadLift x) post eposts

@[simp]

theorem Std.WP.WPMonad.le_wp_monadLift_OptionT_apply {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (x : m α) : Lean.Order.PartialOrder.rel (wp x post eposts.snd) (wp (MonadLift.monadLift x) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_lift_OptionT_apply_eq {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (x : m α) : wp (OptionT.lift x) post eposts = wp (MonadLift.monadLift x) post eposts

MonadFunctor simp lemmas

@[simp]

theorem Std.WP.WPMonad.wp_monadMap_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ : Type u} (f : {β : Type u} → m β → m β) {α : Type u} (x : StateT σ m α) (post : α → σ → Pred) (eposts : EPosts) : wp (MonadFunctor.monadMap (fun {β : Type u} => f) x) post eposts = fun (s : σ) => wp (f (x.run s)) (fun (x : α × σ) => match x with | (a, s') => post a s') eposts

@[simp]

theorem Std.WP.WPMonad.wp_monadMap_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ : Type u} (f : {β : Type u} → m β → m β) {α : Type u} (x : ReaderT ρ m α) (post : α → ρ → Pred) (eposts : EPosts) : wp (MonadFunctor.monadMap (fun {β : Type u} => f) x) post eposts = fun (r : ρ) => wp (f (x.run r)) (fun (a : α) => post a r) eposts

@[simp]

theorem Std.WP.WPMonad.wp_monadMap_ExceptT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε : Type u} (f : {β : Type u} → m β → m β) {α : Type u} (x : ExceptT ε m α) (post : α → Pred) (eposts : (ε → Pred) × EPosts) : wp (MonadFunctor.monadMap (fun {β : Type u} => f) x) post eposts = wp (f x.run) (Lean.Order.pushExcept post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_monadMap_OptionT_apply_eq {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] (f : {β : Type u} → m β → m β) {α : Type u} (x : OptionT m α) (post : α → Pred) (eposts : (Unit → Pred) × EPosts) : wp (MonadFunctor.monadMap (fun {β : Type u} => f) x) post eposts = wp (f x.run) (Lean.Order.pushOption post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_withReader_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ α : Type u} {post : α → ρ → Pred} {eposts : EPosts} (f : ρ → ρ) (x : ReaderT ρ m α) : wp (MonadWithReaderOf.withReader f x) post eposts = fun (r : ρ) => wp x (fun (a : α) (x : ρ) => post a r) eposts (f r)

@[simp]

theorem Std.WP.WPMonad.wp_withReader_MonadWithReader_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ α : Type u} {post : α → Pred} {eposts : EPosts} [MonadWithReaderOf ρ m] (f : ρ → ρ) (x : m α) : wp (withReader f x) post eposts = wp (MonadWithReaderOf.withReader f x) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_withTheReader_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ α : Type u} {post : α → ρ → Pred} {eposts : EPosts} (f : ρ → ρ) (x : ReaderT ρ m α) : wp (withTheReader ρ f x) post eposts = wp (MonadWithReaderOf.withReader f x) post eposts

Transformer adapt lemmas

theorem Std.WP.WPMonad.le_wp_adapt_ExceptT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε ε' α : Type u} {post : α → Pred} {eposts : (ε' → Pred) × EPosts} (f : ε → ε') (x : ExceptT ε m α) : Lean.Order.PartialOrder.rel (wp x post (fun (e : ε) => eposts.fst (f e), eposts.snd)) (wp (ExceptT.adapt f x) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_adaptExcept_EStateM_apply_eq {ε ε' σ α : Type} {post : α → σ → Prop} {eposts : ε' → σ → Prop} (f : ε → ε') (x : EStateM ε σ α) : wp (EStateM.adaptExcept f x) post eposts = wp x post fun (e : ε) => eposts (f e)

MonadControl simp lemmas

@[simp]

theorem Std.WP.WPMonad.wp_liftWith_StateT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {σ α : Type u} {post : α → σ → Pred} {eposts : EPosts} {s : σ} (f : ({β : Type u} → StateT σ m β → m (β × σ)) → m α) : wp (MonadControl.liftWith f) post eposts s = wp ((fun (a : α) => (a, s)) <$> f fun {β : Type u} (x : StateT σ m β) => x.run s) (fun (x : α × σ) => match x with | (a, s) => post a s) eposts

@[simp]

theorem Std.WP.WPMonad.wp_liftWith_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ρ α : Type u} {post : α → ρ → Pred} {eposts : EPosts} {r : ρ} (f : ({β : Type u} → ReaderT ρ m β → m β) → m α) : wp (MonadControl.liftWith f) post eposts r = wp (f fun {β : Type u} (x : ReaderT ρ m β) => x.run r) (fun (a : α) => post a r) eposts

@[simp]

theorem Std.WP.WPMonad.wp_liftWith_ExceptT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε α : Type u} {post : α → Pred} {eposts : (ε → Pred) × EPosts} (f : ({β : Type u} → ExceptT ε m β → m (Except ε β)) → m α) : wp (MonadControl.liftWith f) post eposts = wp (Except.ok <$> f fun {β : Type u} (x : ExceptT ε m β) => x.run) (Lean.Order.pushExcept post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.le_wp_liftWith_OptionT_apply {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (f : ({β : Type u} → OptionT m β → m (Option β)) → m α) : Lean.Order.PartialOrder.rel (wp (f fun {β : Type u} (x : OptionT m β) => x.run) post eposts.snd) (wp (MonadControl.liftWith f) post eposts)

theorem Std.WP.WPMonad.le_wp_restoreM_StateT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α σ : Type u} {eposts : EPosts} {post : α → σ → Pred} (x : m (α × σ)) : Lean.Order.PartialOrder.rel (fun (x_1 : σ) => wp x (fun (x : α × σ) => match x with | (a, s) => post a s) eposts) (wp (MonadControl.restoreM x) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_restoreM_ReaderT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α ρ : Type u} {post : α → ρ → Pred} {eposts : EPosts} (x : m α) : wp (MonadControl.restoreM x) post eposts = fun (r : ρ) => wp x (fun (a : α) => post a r) eposts

@[simp]

theorem Std.WP.WPMonad.wp_restoreM_ExceptT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε α : Type u} {post : α → Pred} {eposts : (ε → Pred) × EPosts} (x : m (Except ε α)) : wp (MonadControl.restoreM x) post eposts = wp x (Lean.Order.pushExcept post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_restoreM_OptionT_apply_eq {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (x : m (Option α)) : wp (MonadControl.restoreM x) post eposts = wp x (Lean.Order.pushOption post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_controlAt_apply_eq {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {Pred : Type u_4} {EPosts : Type u_5} {α : Type u_1} {post : α → Pred} {eposts : EPosts} [Bind n] [Monad m] [Monad n] [Assertion Pred] [Assertion EPosts] [(α : Type u_1) → WP (n α) α Pred EPosts] [MonadControlT m n] (f : ({β : Type u_1} → n β → m (stM m n β)) → m (stM m n α)) : wp (controlAt m f) post eposts = wp (liftWith f >>= restoreM) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_control_apply_eq {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_3} {Pred : Type u_4} {EPosts : Type u_5} {α : Type u_1} {post : α → Pred} {eposts : EPosts} [Bind n] [Monad m] [Monad n] [Assertion Pred] [Assertion EPosts] [(α : Type u_1) → WP (n α) α Pred EPosts] [MonadControlT m n] (f : ({β : Type u_1} → n β → m (stM m n β)) → m (stM m n α)) : wp (control f) post eposts = wp (liftWith f >>= restoreM) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_monadLift_refl_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : EPosts} [Pure m] (x : m α) : wp (monadLift x) post eposts = wp x post eposts

@[simp]

theorem Std.WP.WPMonad.wp_monadMap_refl_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {f : {β : Type u} → m β → m β} {post : α → Pred} {eposts : EPosts} [Pure m] (x : m α) : wp (monadMap f x) post eposts = wp (f x) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_liftWith_refl_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : EPosts} [Pure m] (f : ({β : Type u} → m β → m β) → m α) : wp (liftWith f) post eposts = wp (f fun {β : Type u} (x : m β) => x) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_restoreM_refl_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : EPosts} [Pure m] (x : stM m m α) : wp (restoreM x) post eposts = wp (pure x) post eposts

Transitive lift/map/control simp lemmas

@[simp]

theorem Std.WP.WPMonad.wp_monadLift_trans_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n o : Type u → Type v} [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (o α) α Pred EPosts] {α : Type u} {post : α → Pred} {eposts : EPosts} [MonadLift n o] [MonadLiftT m n] (x : m α) : wp (monadLift x) post eposts = wp (MonadLift.monadLift (monadLift x)) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_monadMap_trans_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n o : Type u → Type v} [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (o α) α Pred EPosts] {α : Type u} {f : {β : Type u} → m β → m β} {post : α → Pred} {eposts : EPosts} [MonadFunctor n o] [MonadFunctorT m n] (x : o α) : wp (monadMap f x) post eposts = wp (MonadFunctor.monadMap (fun {β : Type u} => monadMap fun {β : Type u} => f) x) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_liftWith_trans_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n o : Type u → Type v} [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (o α) α Pred EPosts] {α : Type u} {post : α → Pred} {eposts : EPosts} [MonadControl n o] [MonadControlT m n] (f : ({β : Type u} → o β → m (stM m o β)) → m α) : wp (liftWith f) post eposts = wp (MonadControl.liftWith fun (x₂ : {β : Type u} → o β → n (MonadControl.stM n o β)) => liftWith fun (x₁ : {β : Type u} → n β → m (stM m n β)) => f fun {β : Type u} => x₁ ∘ x₂) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_restoreM_trans_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n o : Type u → Type v} [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (o α) α Pred EPosts] {α : Type u} {post : α → Pred} {eposts : EPosts} [MonadControl n o] [MonadControlT m n] (x : stM m o α) : wp (restoreM x) post eposts = wp (MonadControl.restoreM (restoreM x)) post eposts

Lifted state/reader operations

@[simp]

theorem Std.WP.WPMonad.wp_get_MonadStateOf_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n : Type u → Type v} [MonadLift m n] [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (n α) α Pred EPosts] {σ : Type u} {post : σ → Pred} {eposts : EPosts} [MonadStateOf σ m] : wp MonadStateOf.get post eposts = wp (MonadLift.monadLift MonadStateOf.get) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_set_MonadStateOf_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n : Type u → Type v} [MonadLift m n] [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (n α) α Pred EPosts] {σ : Type u} {post : PUnit → Pred} {eposts : EPosts} [MonadStateOf σ m] (x : σ) : wp (set x) post eposts = wp (MonadLift.monadLift (set x)) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_modifyGet_MonadStateOf_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n : Type u → Type v} [MonadLift m n] [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (n α) α Pred EPosts] {σ α : Type u} {post : α → Pred} {eposts : EPosts} [MonadStateOf σ m] (f : σ → α × σ) : wp (MonadStateOf.modifyGet f) post eposts = wp (MonadLift.monadLift (modifyGet f)) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_read_MonadReaderOf_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {m n : Type u → Type v} [MonadLift m n] [Assertion Pred] [Assertion EPosts] [(α : Type u) → WP (n α) α Pred EPosts] {ρ : Type u} {post : ρ → Pred} {eposts : EPosts} [MonadReaderOf ρ m] : wp MonadReaderOf.read post eposts = wp (MonadLift.monadLift read) post eposts

Lifted except operations

@[simp]

theorem Std.WP.WPMonad.wp_throw_lift_ExceptT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {ε : Type u} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {ε' α : Type u} {post : α → Pred} {eposts : (ε' → Pred) × EPosts} (err : ε) : wp (MonadExceptOf.throw err) post eposts = wp (MonadExceptOf.throw err) (Lean.Order.pushExcept post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_throw_lift_OptionT_apply_eq {Pred : Type u} {EPosts : Type u_1} {ε : Type u} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (err : ε) : wp (MonadExceptOf.throw err) post eposts = wp (MonadExceptOf.throw err) (Lean.Order.pushOption post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_tryCatch_lift_ExceptT_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {ε : Type u} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {ε' α : Type u} {post : α → Pred} {eposts : (ε' → Pred) × EPosts} (x : ExceptT ε' m α) (h : ε → ExceptT ε' m α) : wp (MonadExceptOf.tryCatch x h) post eposts = wp (MonadExceptOf.tryCatch x h) (Lean.Order.pushExcept post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_tryCatch_lift_OptionT_apply_eq {Pred : Type u} {EPosts : Type u_1} {ε : Type u} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (x : OptionT m α) (h : ε → OptionT m α) : wp (MonadExceptOf.tryCatch x h) post eposts = wp (MonadExceptOf.tryCatch x h) (Lean.Order.pushOption post eposts.fst) eposts.snd

@[simp]

theorem Std.WP.WPMonad.wp_throw_ReaderT_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {ε : Type u_3} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {ρ α : Type u} {post : α → ρ → Pred} {eposts : EPosts} (err : ε) : wp (MonadExceptOf.throw err) post eposts = wp (MonadLift.monadLift (MonadExceptOf.throw err)) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_throw_StateT_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {ε : Type u_3} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {σ α : Type u} {post : α → σ → Pred} {eposts : EPosts} (err : ε) : wp (MonadExceptOf.throw err) post eposts = wp (MonadLift.monadLift (MonadExceptOf.throw err)) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_tryCatch_ReaderT_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {ε : Type u_3} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {ρ α : Type u} {post : α → ρ → Pred} {eposts : EPosts} (x : ReaderT ρ m α) (h : ε → ReaderT ρ m α) : wp (MonadExceptOf.tryCatch x h) post eposts = fun (r : ρ) => wp (MonadExceptOf.tryCatch (x.run r) fun (e : ε) => (h e).run r) (fun (a : α) => post a r) eposts

@[simp]

theorem Std.WP.WPMonad.wp_tryCatch_StateT_lift_apply_eq {Pred : Type u_1} {EPosts : Type u_2} {ε : Type u_3} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] [MonadExceptOf ε m] {σ α : Type u} {post : α → σ → Pred} {eposts : EPosts} (x : StateT σ m α) (h : ε → StateT σ m α) : wp (MonadExceptOf.tryCatch x h) post eposts = fun (s : σ) => wp (MonadExceptOf.tryCatch (x.run s) fun (e : ε) => (h e).run s) (fun (x : α × σ) => match x with | (a, s') => post a s') eposts

OrElse simp lemmas

@[simp]

theorem Std.WP.WPMonad.wp_orElse_Except_apply_eq {ε : Type u_1} {α : Type u_2} {post : α → Prop} {eposts : ε → Prop} (x : Except ε α) (h : Unit → Except ε α) : wp (OrElse.orElse x h) post eposts = wp x post fun (x : ε) => wp (h ()) post eposts

theorem Std.WP.WPMonad.le_wp_orElse_ExceptT_apply {Pred : Type u_1} {EPosts : Type u_2} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {ε α : Type u} {post : α → Pred} {eposts : (ε → Pred) × EPosts} (x : ExceptT ε m α) (h : Unit → ExceptT ε m α) : Lean.Order.PartialOrder.rel (wp x post (fun (x : ε) => wp (h ()) post eposts, eposts.snd)) (wp (OrElse.orElse x h) post eposts)

@[simp]

theorem Std.WP.WPMonad.le_wp_orElse_OptionT_apply {Pred : Type u} {EPosts : Type u_1} {m : Type u → Type v} [Monad m] [Assertion Pred] [Assertion EPosts] [WPMonad m Pred EPosts] {α : Type u} {post : α → Pred} {eposts : (Unit → Pred) × EPosts} (x : OptionT m α) (h : Unit → OptionT m α) : Lean.Order.PartialOrder.rel (wp x post (fun (x : Unit) => wp (h ()) post eposts, eposts.snd)) (wp (OrElse.orElse x h) post eposts)

@[simp]

theorem Std.WP.WPMonad.wp_orElse_Option_apply_eq {α : Type u_1} (x : Option α) (h : Unit → Option α) (post : α → Prop) (eposts : Unit → Prop) : wp (OrElse.orElse x h) post eposts = wp x post fun (x : Unit) => wp (h ()) post eposts

@[simp]

theorem Std.WP.WPMonad.wp_orElse_EStateM_apply_eq {ε σ α : Type} {post : α → σ → Prop} {eposts : ε → σ → Prop} (x : EStateM ε σ α) (h : Unit → EStateM ε σ α) : wp (OrElse.orElse x h) post eposts = fun (s : σ) => wp x post (fun (x : ε) (s' : σ) => wp (h ()) post eposts s') s