From 485efbc439ee0ebdeae8afb0acd24a5e82e2f771 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 19 Nov 2024 20:53:19 +1100 Subject: [PATCH] chore: remove @[simp] attributes from monad-specific SatisfiesM lemmas (#1054) --- Batteries/Classes/SatisfiesM.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/Batteries/Classes/SatisfiesM.lean b/Batteries/Classes/SatisfiesM.lean index 834cbbea68..9b34cf475b 100644 --- a/Batteries/Classes/SatisfiesM.lean +++ b/Batteries/Classes/SatisfiesM.lean @@ -185,14 +185,15 @@ theorem SatisfiesM_EStateM_eq : rw [EStateM.run_map, EStateM.run] split <;> simp_all -@[simp] theorem SatisfiesM_ReaderT_eq [Monad m] : +theorem SatisfiesM_ReaderT_eq [Monad m] : SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x.run s) := (exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm theorem SatisfiesM_StateRefT_eq [Monad m] : - SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp [ReaderT.run] + SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by + simp [SatisfiesM_ReaderT_eq, ReaderT.run] -@[simp] theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] : +theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] : SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by change SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s) refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm @@ -201,7 +202,7 @@ theorem SatisfiesM_StateRefT_eq [Monad m] : · refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩ show _ >>= _ = _; simp [← h] -@[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] : +theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] : SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x.run := by change _ ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x