chore: fixing grind annotations using #grind_lint (#11205)

src/Init/Data/List/Lemmas.lean

@@ -2463,16 +2463,28 @@ theorem getLast_of_mem_getLast? {l : List α} (hx : x ∈ l.getLast?) :
     simp only [reverse_cons, filterMap_append, filterMap_cons, ih]
     split <;> simp_all
 
-@[simp, grind _=_] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
+@[simp] theorem reverse_append {as bs : List α} : (as ++ bs).reverse = bs.reverse ++ as.reverse := by
   induction as <;> simp_all
 
+grind_pattern reverse_append => (as ++ bs).reverse where
+  as =/= []
+  bs =/= []
+grind_pattern reverse_append => bs.reverse ++ as.reverse where
+  as =/= []
+  bs =/= []
+
 @[simp] theorem reverse_eq_append_iff {xs ys zs : List α} :
     xs.reverse = ys ++ zs ↔ xs = zs.reverse ++ ys.reverse := by
   rw [reverse_eq_iff, reverse_append]
 
-@[grind _=_] theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
+theorem reverse_concat {l : List α} {a : α} : (l ++ [a]).reverse = a :: l.reverse := by
   rw [reverse_append]; rfl
 
+grind_pattern reverse_concat => (l ++ [a]).reverse where
+  l =/= []
+grind_pattern reverse_concat => a :: l.reverse where
+  l =/= []
+
 theorem reverse_eq_concat {xs ys : List α} {a : α} :
     xs.reverse = ys ++ [a] ↔ xs = a :: ys.reverse := by
   rw [reverse_eq_iff, reverse_concat]
@@ -2493,9 +2505,12 @@ theorem flatten_reverse {L : List (List α)} :
 grind_pattern reverse_flatMap => (l.flatMap f).reverse where
   f =/= List.reverse ∘ _
 
-@[grind =] theorem flatMap_reverse {β} {l : List α} {f : α → List β} : l.reverse.flatMap f = (l.flatMap (reverse ∘ f)).reverse := by
+theorem flatMap_reverse {β} {l : List α} {f : α → List β} : l.reverse.flatMap f = (l.flatMap (reverse ∘ f)).reverse := by
   induction l <;> simp_all
 
+grind_pattern flatMap_reverse => l.reverse.flatMap f where
+  f =/= List.reverse ∘ _
+
 @[simp] theorem reverseAux_eq {as bs : List α} : reverseAux as bs = reverse as ++ bs :=
   reverseAux_eq_append ..
 

src/Init/Data/List/Nat/Modify.lean

@@ -106,7 +106,9 @@ theorem eraseIdx_eq_modifyTailIdx : ∀ i (l : List α), eraseIdx l i = l.modify
   | _+1, [] => rfl
   | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
 
-@[simp, grind =] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
+-- This is not suitable as a `@[grind =]` lemma:
+-- as soon as it is instantiated the hypothesis `H` causes an infinite chain of instantiations.
+@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, (f l).length = l.length) :
     ∀ (l : List α) i, (l.modifyTailIdx i f).length = l.length
   | _, 0 => H _
   | [], _+1 => rfl

src/Init/Data/List/Sublist.lean

@@ -98,14 +98,18 @@ theorem eq_nil_of_subset_nil {l : List α} : l ⊆ [] → l = [] := subset_nil.m
 theorem map_subset {l₁ l₂ : List α} (f : α → β) (h : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
   fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@h _)
 
-grind_pattern map_subset => l₁ ⊆ l₂, map f l₁
-grind_pattern map_subset => l₁ ⊆ l₂, map f l₂
+grind_pattern map_subset => l₁ ⊆ l₂, map f l₁ where
+  l₂ =/= List.map _ _
+grind_pattern map_subset => l₁ ⊆ l₂, map f l₂ where
+  l₁ =/= List.map _ _
 
 theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=
   fun x => by simp_all [mem_filter, subset_def.1 H]
 
-grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₁
-grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₂
+grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₁ where
+  l₂ =/= List.filter _ _
+grind_pattern filter_subset => l₁ ⊆ l₂, filter p l₂ where
+  l₁ =/= List.filter _ _
 
 theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
     filterMap f l₁ ⊆ filterMap f l₂ := by
@@ -114,8 +118,10 @@ theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁
   rintro ⟨a, h, w⟩
   exact ⟨a, H h, w⟩
 
-grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₁
-grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₂
+grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₁ where
+  l₂ =/= List.filterMap _ _
+grind_pattern filterMap_subset => l₁ ⊆ l₂, filterMap f l₂ where
+  l₁ =/= List.filterMap _ _
 
 theorem subset_append_left (l₁ l₂ : List α) : l₁ ⊆ l₁ ++ l₂ := fun _ => mem_append_left _
 
@@ -282,20 +288,28 @@ protected theorem Sublist.map (f : α → β) {l₁ l₂} (s : l₁ <+ l₂) : m
 grind_pattern Sublist.map => l₁ <+ l₂, map f l₁
 grind_pattern Sublist.map => l₁ <+ l₂, map f l₂
 
-@[grind ←]
 protected theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
     filterMap f l₁ <+ filterMap f l₂ := by
   induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons]
 
-grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₁
-grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂
+grind_pattern Sublist.filterMap => filterMap f l₁ <+ filterMap f l₂ where
+  l₁ =/= List.filterMap _ _
+  l₂ =/= List.filterMap _ _
+grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₁ where
+  l₂ =/= List.filterMap _ _
+grind_pattern Sublist.filterMap => l₁ <+ l₂, filterMap f l₂ where
+  l₁ =/= List.filterMap _ _
 
-@[grind ←]
 protected theorem Sublist.filter (p : α → Bool) {l₁ l₂} (s : l₁ <+ l₂) : filter p l₁ <+ filter p l₂ := by
   rw [← filterMap_eq_filter]; apply s.filterMap
 
-grind_pattern Sublist.filter => l₁ <+ l₂, l₁.filter p
-grind_pattern Sublist.filter => l₁ <+ l₂, l₂.filter p
+grind_pattern Sublist.filter => filter p l₁ <+ filter p l₂ where
+  l₁ =/= List.filter _ _
+  l₂ =/= List.filter _ _
+grind_pattern Sublist.filter => l₁ <+ l₂, l₁.filter p where
+  l₂ =/= List.filter _ _
+grind_pattern Sublist.filter => l₁ <+ l₂, l₂.filter p where
+  l₁ =/= List.filter _ _
 
 theorem head_filter_mem (xs : List α) (p : α → Bool) (h) : (xs.filter p).head h ∈ xs :=
   filter_sublist.head_mem h

tests/lean/run/grind_lint.lean

@@ -1,55 +1,52 @@
 -- Already working:
 
--- #grind_lint check (min := 20) in Array
+#guard_msgs in
+#grind_lint check (min := 20) in Array
 
 -- In progress:
 
-#grind_lint check  (min := 20) in List
+#grind_lint check (min := 20) in List
+
+-- TODO: Not sure what to do here, see https://lean-fro.zulipchat.com/#narrow/channel/503415-grind/topic/.60.23grind_lint.60.20command/near/556730710
 #grind_lint inspect List.getLast?_concat
+#grind_lint mute List.getLast?_concat
+
+-- TODO: We should consider changing the grind annotation for `List.getElem?_eq_none`
+-- so it only fires if we've already proved the hypothesis holds. (i.e. the new gadget)
+-- Other than that, everything looks sane here:
 #grind_lint inspect List.getLast?_pmap
-#grind_lint inspect List.getLast_filter
-#grind_lint inspect List.head_filter
-#grind_lint inspect List.length_modifyTailIdx
-#grind_lint inspect List.replicate_sublist_iff
-#grind_lint inspect List.reverse_concat
-#grind_lint inspect List.reverse_flatMap
-#grind_lint inspect List.Sublist.append
-#grind_lint inspect List.Sublist.middle
+#grind_lint mute List.getLast?_pmap
 
+-- TODO: We should try to remove these attributes; if that's okay we can remove these mutes.
+attribute [-grind] List.Sublist.getLast_mem List.Sublist.head_mem
+-- #grind_lint inspect List.getLast_filter
+-- #grind_lint inspect List.head_filter
+#grind_lint mute List.getLast_filter
+#grind_lint mute List.head_filter
 
-/--
-info: instantiating `Vector.extract_reverse` triggers 22 additional `grind` theorem instantiations
----
-info: instantiating `Vector.range'_one` triggers more than 100 additional `grind` theorem instantiations
----
-info: Vector.range'_one
-[thm] instances
-  [thm] Vector.append_assoc ↦ 29
-  [thm] Vector.range'_append ↦ 15
-  [thm] Vector.append_assoc_symm ↦ 12
-  [thm] Vector.empty_append ↦ 11
-  [thm] List.size_toArray ↦ 8
-  [thm] Vector.range'_one ↦ 8
-  [thm] Vector.range'_zero ↦ 7
-  [thm] List.length_cons ↦ 6
-  [thm] Array.size_empty ↦ 1
-  [thm] List.length_nil ↦ 1
-  [thm] Vector.append_empty ↦ 1
-  [thm] Vector.toArray_empty ↦ 1
----
-info: instantiating `Vector.reverse_extract` triggers 22 additional `grind` theorem instantiations
----
-info: Try this:
-  [apply] #grind_lint check  (min := 20) in Vector
-  #grind_lint inspect Vector.extract_reverse
-  #grind_lint inspect Vector.range'_one
-  #grind_lint inspect Vector.reverse_extract
--/
+-- TODO: `List.Sublist.eq_of_length` should probably only fire when we've already proved the hypotheses.
+
+-- `List.replicate_sublist_iff` is reasonable at 30.
 #guard_msgs in
-#grind_lint check (min := 20) in Vector
+#grind_lint inspect (min := 30) List.replicate_sublist_iff
+#grind_lint mute List.replicate_sublist_iff
+
+-- `List.Sublist.append` is reasonable at 25.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.Sublist.append
+#grind_lint mute List.Sublist.append
+
+-- `List.Sublist.middle` is reasonable at 25.
+#guard_msgs in
+#grind_lint inspect (min := 25) List.Sublist.middle
+#grind_lint mute List.Sublist.middle
+
+-- FIXME: I think I've muted all of these, but they are still being reported.
+#grind_lint check (min := 20) in List
 
 -- TODO:
 
+-- #grind_lint check (min := 20) in Vector
 -- #grind_lint check (min := 20) in Option
 -- #grind_lint check (min := 20) in Nat Int Rat Dyadic
 -- #grind_lint check (min := 20) in Prod Sum