fix: Remove simp annotations for Id.{pure_eq,map_eq,bind_eq}

This PR removes `simp` annotations for lemmas `Id.pure_eq`, `Id.map_eq`
and `Id.bind_eq` because they tend to break the abstraction of
computations in `Id`. In particular, they are problematic for
compositional reasoning about `do` notation.

While a better `simp` framework is on the horizon with #7352; this PR
simply adds the old simp lemmas wherever needed.

Breaking change: Remove the `simp` annotation from `Id.pure_eq`,
`Id.map_eq` and `Id.bind_eq`. Workaround: add manually to simp set.

Author: Sebastian Graf

src/Init/Control/Lawful/Basic.lean

@@ -238,9 +238,9 @@ theorem LawfulMonad.mk' (m : Type u → Type v) [Monad m]
 
 namespace Id
 
-@[simp] theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
-@[simp] theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
-@[simp] theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
+theorem map_eq (x : Id α) (f : α → β) : f <$> x = f x := rfl
+theorem bind_eq (x : Id α) (f : α → id β) : x >>= f = f x := rfl
+theorem pure_eq (a : α) : (pure a : Id α) = a := rfl
 
 instance : LawfulMonad Id := by
   refine LawfulMonad.mk' _ ?_ ?_ ?_ <;> intros <;> rfl

src/Init/Data/Array/Lemmas.lean

@@ -595,7 +595,7 @@ theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h :
       ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true := by
   unfold anyM.loop
   split <;> rename_i h₁
-  · dsimp
+  · dsimp [Id.pure_eq, Id.bind_eq]
     split <;> rename_i h₂
     · simp only [true_iff]
       refine ⟨start, by omega, by omega, by omega, h₂⟩
@@ -1322,8 +1322,8 @@ theorem mapM_map_eq_foldl {as : Array α} {f : α → β} {i : Nat} :
     -- Calling `split` here gives a bad goal.
     have : size as - i = Nat.succ (size as - i - 1) := by omega
     rw [this]
-    simp [foldl, foldlM, Id.run, Nat.sub_add_eq]
-  · dsimp [foldl, Id.run, foldlM]
+    simp [foldl, foldlM, Id.run, Nat.sub_add_eq, Id.pure_eq, Id.bind_eq]
+  · dsimp [foldl, Id.run, foldlM, Id.pure_eq, Id.bind_eq]
     rw [dif_pos (by omega), foldlM.loop, dif_neg h]
     rfl
 termination_by as.size - i
@@ -1539,8 +1539,8 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)
     as.toList ++ List.filterMap f xs := ?_
   exact this #[]
   induction xs
-  · simp_all [Id.run]
-  · simp_all [Id.run, List.filterMap_cons]
+  · simp_all [Id.run, Id.pure_eq]
+  · simp_all [Id.run, List.filterMap_cons, Id.bind_eq, Id.pure_eq]
     split <;> simp_all
 
 theorem toList_filterMap {f : α → Option β} {xs : Array α} :
@@ -3377,15 +3377,15 @@ theorem foldrM_append [Monad m] [LawfulMonad m] {f : α → β → m β} {b} {xs
     (w : start = xs.size + ys.size) :
     (xs ++ ys).foldr f b start 0 = xs.foldr f (ys.foldr f b) := by
   subst w
-  simp [foldr_eq_foldrM]
+  simp [foldr_eq_foldrM, Id.bind_eq]
 
 theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs ys : Array α} :
     (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by
-  simp [foldl_eq_foldlM]
+  simp [foldl_eq_foldlM, Id.bind_eq]
 
 theorem foldr_append {f : α → β → β} {b} {xs ys : Array α} :
     (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by
-  simp [foldr_eq_foldrM]
+  simp [foldr_eq_foldrM, Id.bind_eq]
 
 @[simp] theorem foldl_flatten' {f : β → α → β} {b} {xss : Array (Array α)} {stop : Nat}
     (w : stop = xss.flatten.size) :
@@ -3654,7 +3654,7 @@ abbrev pop_mkArray := @pop_replicate
 
 @[simp] theorem size_modify {xs : Array α} {i : Nat} {f : α → α} : (xs.modify i f).size = xs.size := by
   unfold modify modifyM Id.run
-  split <;> simp
+  split <;> simp [Id.pure_eq, Id.bind_eq]
 
 theorem getElem_modify {xs : Array α} {j i} (h : i < (xs.modify j f).size) :
     (xs.modify j f)[i] = if j = i then f (xs[i]'(by simpa using h)) else xs[i]'(by simpa using h) := by

src/Init/Data/Array/Lex/Lemmas.lean

@@ -26,11 +26,11 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by
-  simp [lex, Id.run]
+  simp [lex, Id.run, Id.pure_eq, Id.bind_eq]
 
 @[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b := by
   simp only [lex, List.getElem_toArray, List.getElem_singleton]
-  cases lt a b <;> cases a != b <;> simp [Id.run]
+  cases lt a b <;> cases a != b <;> simp [Id.run, Id.pure_eq, Id.bind_eq]
 
 private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} :
      (#[a] ++ xs).lex (#[b] ++ ys) lt =
@@ -42,16 +42,16 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs
     getElem_append_right]
   cases lt a b
   · rw [bne]
-    cases a == b <;> simp
-  · simp
+    cases a == b <;> simp [Id.pure_eq, Id.bind_eq]
+  · simp [Id.pure_eq, Id.bind_eq]
 
 @[simp] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} :
     l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by
   induction l₁ generalizing l₂ with
-  | nil => cases l₂ <;> simp [lex, Id.run]
+  | nil => cases l₂ <;> simp [lex, Id.run, Id.pure_eq, Id.bind_eq]
   | cons x l₁ ih =>
     cases l₂ with
-    | nil => simp [lex, Id.run]
+    | nil => simp [lex, Id.run, Id.pure_eq, Id.bind_eq]
     | cons y l₂ =>
       rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih]
 

src/Init/Data/Fin/Fold.lean

@@ -189,7 +189,7 @@ theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
 
 theorem foldl_eq_foldlM (f : α → Fin n → α) (x) :
     foldl n f x = foldlM (m:=Id) n f x := by
-  induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *]
+  induction n generalizing x <;> simp [foldl_succ, foldlM_succ, *, Id.pure_eq, Id.bind_eq]
 
 /-! ### foldr -/
 
@@ -222,7 +222,7 @@ theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
 
 theorem foldr_eq_foldrM (f : Fin n → α → α) (x) :
     foldr n f x = foldrM (m:=Id) n f x := by
-  induction n <;> simp [foldr_succ, foldrM_succ, *]
+  induction n <;> simp [foldr_succ, foldrM_succ, *, Id.pure_eq, Id.bind_eq]
 
 theorem foldl_rev (f : Fin n → α → α) (x) :
     foldl n (fun x i => f i.rev x) x = foldr n f x := by

src/Init/Data/List/Lemmas.lean

@@ -2558,11 +2558,11 @@ theorem flatMap_reverse {β} {l : List α} {f : α → List β} : (l.reverse.fla
 
 theorem foldl_eq_foldlM {f : β → α → β} {b : β} {l : List α} :
     l.foldl f b = l.foldlM (m := Id) f b := by
-  induction l generalizing b <;> simp [*, foldl]
+  induction l generalizing b <;> simp [*, foldl, Id.pure_eq, Id.bind_eq]
 
 theorem foldr_eq_foldrM {f : α → β → β} {b : β} {l : List α} :
     l.foldr f b = l.foldrM (m := Id) f b := by
-  induction l <;> simp [*, foldr]
+  induction l <;> simp [*, foldr, Id.pure_eq, Id.bind_eq]
 
 @[simp] theorem id_run_foldlM {f : β → α → Id β} {b : β} {l : List α} :
     Id.run (l.foldlM f b) = l.foldl f b := foldl_eq_foldlM.symm
@@ -2659,10 +2659,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   induction l <;> simp [*]
 
 @[simp] theorem foldl_append {β : Type _} {f : β → α → β} {b : β} {l l' : List α} :
-    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM]
+    (l ++ l').foldl f b = l'.foldl f (l.foldl f b) := by simp [foldl_eq_foldlM, Id.bind_eq]
 
 @[simp] theorem foldr_append {f : α → β → β} {b : β} {l l' : List α} :
-    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM]
+    (l ++ l').foldr f b = l.foldr f (l'.foldr f b) := by simp [foldr_eq_foldrM, Id.bind_eq]
 
 theorem foldl_flatten {f : β → α → β} {b : β} {L : List (List α)} :
     (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b := by

src/Init/Data/List/Monadic.lean

@@ -341,7 +341,7 @@ theorem forIn'_eq_foldlM [Monad m] [LawfulMonad m]
     forIn' (m := Id) l init (fun a m b => .yield (f a m b)) =
       l.attach.foldl (fun b ⟨a, h⟩ => f a h b) init := by
   simp only [forIn'_eq_foldlM]
-  induction l.attach generalizing init <;> simp_all
+  induction l.attach generalizing init <;> simp_all[Id.bind_eq, Id.pure_eq, Id.map_eq]
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     {l : List α} (g : α → β) (f : (b : β) → b ∈ l.map g → γ → m (ForInStep γ)) :
@@ -394,7 +394,7 @@ theorem forIn_eq_foldlM [Monad m] [LawfulMonad m]
     forIn (m := Id) l init (fun a b => .yield (f a b)) =
       l.foldl (fun b a => f a b) init := by
   simp only [forIn_eq_foldlM]
-  induction l generalizing init <;> simp_all
+  induction l generalizing init <;> simp_all[Id.bind_eq, Id.pure_eq, Id.map_eq]
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     {l : List α} {g : α → β} {f : β → γ → m (ForInStep γ)} :

src/Init/Data/Option/Monadic.lean

@@ -56,7 +56,7 @@ theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
     (o : Option α) (f : (a : α) → a ∈ o → β → β) (b : β) :
     forIn' (m := Id) o b (fun a m b => .yield (f a m b)) =
       o.pelim b (fun a h => f a h b) := by
-  cases o <;> simp
+  cases o <;> simp [Id.bind_eq, Id.pure_eq]
 
 @[simp] theorem forIn'_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : (b : β) → b ∈ o.map g → γ → m (ForInStep γ)) :
@@ -85,7 +85,7 @@ theorem forIn_eq_elim [Monad m] [LawfulMonad m]
     (o : Option α) (f : (a : α) → β → β) (b : β) :
     forIn (m := Id) o b (fun a b => .yield (f a b)) =
       o.elim b (fun a => f a b) := by
-  cases o <;> simp
+  cases o <;> simp [Id.bind_eq, Id.pure_eq]
 
 @[simp] theorem forIn_map [Monad m] [LawfulMonad m]
     (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)) :

src/Init/Data/Vector/Lemmas.lean

@@ -2397,10 +2397,10 @@ theorem foldr_map_hom {g : α → β} {f : α → α → α} {f' : β → β →
   simp
 
 @[simp] theorem foldl_append {β : Type _} {f : β → α → β} {b} {xs : Vector α n} {ys : Vector α k} :
-    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by simp [foldl_eq_foldlM]
+    (xs ++ ys).foldl f b = ys.foldl f (xs.foldl f b) := by simp [foldl_eq_foldlM, Id.pure_eq, Id.bind_eq]
 
 @[simp] theorem foldr_append {f : α → β → β} {b} {xs : Vector α n} {ys : Vector α k} :
-    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by simp [foldr_eq_foldrM]
+    (xs ++ ys).foldr f b = xs.foldr f (ys.foldr f b) := by simp [foldr_eq_foldrM, Id.pure_eq, Id.bind_eq]
 
 @[simp] theorem foldl_flatten {f : β → α → β} {b} {xss : Vector (Vector α m) n} :
     (flatten xss).foldl f b = xss.foldl (fun b xs => xs.foldl f b) b := by

src/Init/Data/Vector/Lex.lean

@@ -57,7 +57,7 @@ protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys
 
 @[simp] theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #v[a].lex #v[b] lt = lt a b := by
   simp only [lex, getElem_mk, List.getElem_toArray, List.getElem_singleton]
-  cases lt a b <;> cases a != b <;> simp [Id.run]
+  cases lt a b <;> cases a != b <;> simp [Id.run, Id.pure_eq, Id.bind_eq]
 
 protected theorem lt_irrefl [LT α] [Std.Irrefl (· < · : α → α → Prop)] (xs : Vector α n) : ¬ xs < xs :=
   Array.lt_irrefl xs.toArray

src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean

@@ -36,7 +36,7 @@ open Std.Internal
 @[simp]
 theorem foldl_eq {f : δ → (a : α) → β a → δ} {init : δ} {l : AssocList α β} :
     l.foldl f init = l.toList.foldl (fun d p => f d p.1 p.2) init := by
-  induction l generalizing init <;> simp_all [foldl, Id.run, foldlM]
+  induction l generalizing init <;> simp_all [foldl, Id.run, foldlM, Id.pure_eq, Id.bind_eq]
 
 @[simp]
 theorem length_eq {l : AssocList α β} : l.length = l.toList.length := by
@@ -260,11 +260,11 @@ end Const
 theorem foldl_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
     l.foldl (fun acc k v => f k v :: acc) acc =
       (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by
-  induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM, Id.run]
+  induction l generalizing acc <;> simp_all [AssocList.foldl, AssocList.foldlM, Id.run, Id.pure_eq, Id.bind_eq]
 
 theorem foldr_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) :
     l.foldr (fun k v acc => f k v :: acc) acc =
       (l.toList.map (fun p => f p.1 p.2)) ++ acc := by
-  induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM, Id.run]
+  induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM, Id.run, Id.pure_eq, Id.bind_eq]
 
 end Std.DHashMap.Internal.AssocList