chore: finish dealing with #grind_lint (#11207)

This ensures that no `grind` annotated theorem, simply by being
instantiated, causes a chain of >20 further instantiations, with a small
list of documented exceptions.

src/Init/Data/Option/Lemmas.lean

@@ -212,10 +212,13 @@ theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β)
     (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by
   cases a <;> cases b <;> rfl
 
-@[grind =]
 theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) :
     (x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl
 
+grind_pattern bind_assoc => (x.bind f).bind g where
+  f =/= some
+  g =/= some
+
 theorem bind_congr {α β} {o : Option α} {f g : α → Option β} :
     (h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by
   cases o <;> simp

src/Init/Data/Vector/Extract.lean

@@ -176,7 +176,6 @@ theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i <
   rcases xs with ⟨as, rfl⟩
   simp [Array.set_eq_push_extract_append_extract]
 
-@[grind =]
 theorem extract_reverse {xs : Vector α n} {i j : Nat} :
     xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by
   ext i h
@@ -184,10 +183,17 @@ theorem extract_reverse {xs : Vector α n} {i j : Nat} :
   congr 1
   omega
 
-@[grind =]
+grind_pattern extract_reverse => xs.reverse.extract i j where
+  i =/= n - _
+  j =/= n - _
+
 theorem reverse_extract {xs : Vector α n} {i j : Nat} :
     (xs.extract i j).reverse = (xs.reverse.extract (n - j) (n - i)).cast (by omega) := by
   rcases xs with ⟨xs, rfl⟩
   simp [Array.reverse_extract]
 
+grind_pattern reverse_extract => (xs.extract i j).reverse where
+  i =/= n - _
+  j =/= n - _
+
 end Vector

src/Init/Data/Vector/Range.lean

@@ -74,12 +74,16 @@ theorem map_add_range' {a} (s n step) : map (a + ·) (range' s n step) = range'
 theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1) := by
   ext <;> simp <;> omega
 
-@[grind _=_]
 theorem range'_append {s m n step : Nat} :
     range' s m step ++ range' (s + step * m) n step = range' s (m + n) step := by
   rw [← toArray_inj]
   simp [Array.range'_append]
 
+grind_pattern range'_append => range' s m step ++ range' (s + step * m) n step
+
+grind_pattern range'_append => range' s (m + n) step where
+  s =/= _ + _ * _ -- This cuts off an infinite chain of instantiations.
+
 @[simp] theorem range'_append_1 {s m n : Nat} :
     range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
 

src/Lean/Elab/Tactic/Grind/Lint.lean

@@ -189,3 +189,11 @@ def elabGrindLintCheck : CommandElab := fun stx => liftTermElabM <| withTheReade
     Tactic.TryThis.addSuggestion stx { suggestion := .string suggestion }
 
 end Lean.Elab.Tactic.Grind
+
+-- We allow these as grind lemmas even though they triggers >20 further instantiations.
+-- See tests/lean/run/grind_lint.lean for more details.
+#grind_lint skip BitVec.msb_replicate
+#grind_lint skip BitVec.msb_signExtend
+#grind_lint skip List.replicate_sublist_iff
+#grind_lint skip List.Sublist.append
+#grind_lint skip List.Sublist.middle

src/Std/Data/DHashMap/RawLemmas.lean

@@ -2425,7 +2425,6 @@ theorem insertMany_list_singleton (h : m.WF)
   simp_to_raw
   rw [Raw₀.Const.insertMany_cons]
 
-@[grind _=_]
 theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} :
     insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by
   induction l₁ generalizing m with
@@ -2433,6 +2432,13 @@ theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} :
   | cons hd tl ih =>
     rw [List.cons_append, insertMany_cons h, insertMany_cons h, ih h.insert]
 
+grind_pattern insertMany_append => insertMany m (l₁ ++ l₂) where
+  l₁ =/= []
+  l₂ =/= []
+grind_pattern insertMany_append => insertMany (insertMany m l₁) l₂ where
+  l₁ =/= []
+  l₂ =/= []
+
 @[elab_as_elim]
 theorem insertMany_ind {motive : Raw α (fun _ => β) → Prop} (m : Raw α fun _ => β) (l : ρ)
     (init : motive m) (insert : ∀ m a b, motive m → motive (m.insert a b)) :

src/Std/Data/HashMap/RawLemmas.lean

@@ -1148,7 +1148,6 @@ theorem insertMany_cons (h : m.WF) {l : List (α × β)}
     insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l :=
   ext (DHashMap.Raw.Const.insertMany_cons h.out)
 
-@[grind _=_]
 theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} :
     insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by
   induction l₁ generalizing m with
@@ -1156,6 +1155,13 @@ theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} :
   | cons hd tl ih =>
     rw [List.cons_append, insertMany_cons h, insertMany_cons h, ih h.insert]
 
+grind_pattern insertMany_append => insertMany m (l₁ ++ l₂) where
+  l₁ =/= []
+  l₂ =/= []
+grind_pattern insertMany_append => insertMany (insertMany m l₁) l₂ where
+  l₁ =/= []
+  l₂ =/= []
+
 @[elab_as_elim]
 theorem insertMany_ind {motive : Raw α β → Prop} (m : Raw α β) {l : ρ}
     (init : motive m) (insert : ∀ m a b, motive m → motive (m.insert a b)) :

src/Std/Data/HashSet/RawLemmas.lean

@@ -655,7 +655,6 @@ theorem insertMany_cons (h : m.WF) {l : List α} {k : α} :
     insertMany m (k :: l) = insertMany (m.insert k) l :=
   ext (HashMap.Raw.insertManyIfNewUnit_cons h.1)
 
-@[grind _=_]
 theorem insertMany_append (h : m.WF) {l₁ l₂ : List α} :
     insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by
   induction l₁ generalizing m with
@@ -663,6 +662,13 @@ theorem insertMany_append (h : m.WF) {l₁ l₂ : List α} :
   | cons hd tl ih =>
     rw [List.cons_append, insertMany_cons h, insertMany_cons h, ih h.insert]
 
+grind_pattern insertMany_append => insertMany m (l₁ ++ l₂) where
+  l₁ =/= []
+  l₂ =/= []
+grind_pattern insertMany_append => insertMany (insertMany m l₁) l₂ where
+  l₁ =/= []
+  l₂ =/= []
+
 @[elab_as_elim]
 theorem insertMany_ind {motive : Raw α → Prop} (m : Raw α) (l : ρ)
     (init : motive m) (insert : ∀ m a, motive m → motive (m.insert a)) :

tests/lean/run/grind_lint.lean

@@ -1,51 +1,43 @@
--- Already working:
+import Std
+import Lean.Elab.Tactic.Grind.Lint
 
+/-! `BitVec` exceptions -/
+
+-- `BitVec.msb_replicate` is reasonable at 25.
 #guard_msgs in
-#grind_lint check (min := 20) in Array
+#grind_lint inspect (min := 30) BitVec.msb_replicate
 
--- In progress:
+-- `BitVec.msb_signExtend` is reasonable at 22.
+#guard_msgs in
+#grind_lint inspect (min := 25)  BitVec.msb_signExtend
+
+/-! `List` exceptions -/
 
 -- 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 inspect List.getLast?_concat
 #grind_lint skip 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?_pmap
 #grind_lint skip 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
-
 -- 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 inspect (min := 30) List.replicate_sublist_iff
-#grind_lint skip List.replicate_sublist_iff
 
 -- `List.Sublist.append` is reasonable at 25.
 #guard_msgs in
 #grind_lint inspect (min := 25) List.Sublist.append
-#grind_lint skip List.Sublist.append
 
 -- `List.Sublist.middle` is reasonable at 25.
 #guard_msgs in
 #grind_lint inspect (min := 25) List.Sublist.middle
-#grind_lint skip List.Sublist.middle
 
-#grind_lint check (min := 20) in List
+/-! Final check of everything: -/
 
--- 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
--- #grind_lint check (min := 20) in module Std
--- #grind_lint check (min := 20)
+#guard_msgs in
+#grind_lint check (min := 20)