chore: remove TODO

Symbols that have builtin support in `grind` are bad pattern candidates.

src/Lean/Elab/Tactic/Grind.lean

@@ -161,7 +161,8 @@ private def evalGrindCore
   let fallback ← elabFallback fallback?
   let only := only.isSome
   let params := if let some params := params then params.getElems else #[]
-  logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
+  if Grind.grind.warning.get (← getOptions) then
+    logWarningAt ref "The `grind` tactic is experimental and still under development. Avoid using it in production projects"
   let declName := (← Term.getDeclName?).getD `_grind
   let mut config ← elabGrindConfig config
   if trace then

src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean

@@ -653,11 +653,42 @@ private def addNewPattern (p : Expr) : CollectorM Unit := do
     trace[grind.ematch.pattern.search] "found full coverage"
   modify fun s => { s with patterns := s.patterns.push p, done }
 
+/-- Collect the pattern (i.e., de Bruijn) variables in the given pattern. -/
+private def collectPatternBVars (p : Expr) : List Nat :=
+  go p |>.run [] |>.2
+where
+  go (e : Expr) : StateM (List Nat) Unit := do
+    match e with
+    | .app f a    => go f; go a
+    | .mdata _ b  => go b
+    | .bvar idx   => modify fun s => if s.contains idx then s else idx :: s
+    | _           => return ()
+
+/--
+Returns `true` if pattern `p` contains a child `c` such that
+1- `p` and `c` have the same pattern variables.
+2- `c` is not a support argument. See `NormalizePattern.getPatternSupportMask` for definition.
+3- `c` is not an offset pattern.
+4- `c` is not a bound variable.
+-/
+private def hasChildWithSameBVars (p : Expr) (supportMask : Array Bool) : CoreM Bool := do
+  let s := collectPatternBVars p
+  for arg in p.getAppArgs, support in supportMask do
+    unless support do
+    unless arg.isBVar do
+    unless isOffsetPattern? arg |>.isSome do
+      let sArg := collectPatternBVars arg
+      if s ⊆ sArg then
+        trace[Meta.debug] "SKIPPED: {p}, {arg}, {s}, {sArg}"
+        return true
+  return false
+
 private partial def collect (e : Expr) : CollectorM Unit := do
   if (← get).done then return ()
   match e with
   | .app .. =>
     let f := e.getAppFn
+    let supportMask ← NormalizePattern.getPatternSupportMask f e.getAppNumArgs
     if (← isPatternFnCandidate f) then
       let saved ← getThe NormalizePattern.State
       try
@@ -668,8 +699,9 @@ private partial def collect (e : Expr) : CollectorM Unit := do
           return ()
         let p ← NormalizePattern.normalizePattern p
         if saved.bvarsFound.size < (← getThe NormalizePattern.State).bvarsFound.size then
-          addNewPattern p
-          return ()
+          unless (← hasChildWithSameBVars p supportMask) do
+            addNewPattern p
+            return ()
         trace[grind.ematch.pattern.search] "skip, no new variables covered"
         -- restore state and continue search
         set saved
@@ -678,8 +710,8 @@ private partial def collect (e : Expr) : CollectorM Unit := do
         -- restore state and continue search
         set saved
     let args := e.getAppArgs
-    for arg in args, flag in (← NormalizePattern.getPatternSupportMask f args.size) do
-      unless flag do
+    for arg in args, support in supportMask do
+      unless support do
         collect arg
   | .forallE _ d b _ =>
     if (← pure e.isArrow <&&> isProp d <&&> isProp b) then

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -45,6 +45,12 @@ register_builtin_option grind.debug.proofs : Bool := {
   descr    := "check proofs between the elements of all equivalence classes"
 }
 
+register_builtin_option grind.warning : Bool := {
+  defValue := true
+  group    := "debug"
+  descr    := "disable `grind` usage warning"
+}
+
 /-- Context for `GrindM` monad. -/
 structure Context where
   simp         : Simp.Context

tests/lean/run/grind_constProp.lean

@@ -1,5 +1,7 @@
 %reset_grind_attrs
 
+set_option grind.warning false
+
 attribute [grind cases] Or
 attribute [grind =] List.length_nil List.length_cons Option.getD
 
@@ -186,7 +188,7 @@ def evalExpr (e : Expr) : EvalM Val := do
   next op arg ih_arg =>
     simp only [simplify, UnaryOp.simplify, eval, ← ih_arg, UnaryOp.eval]
     split
-    · grind (splits := 0) [Expr.eval] -- TODO: investigate: why do we need Expr.eval here
+    · grind
     · simp only [eval, UnaryOp.eval] -- TODO: `grind` failes here
 
 @[simp, grind =] def Stmt.simplify : Stmt → Stmt
@@ -205,10 +207,8 @@ def evalExpr (e : Expr) : EvalM Val := do
 
 theorem Stmt.simplify_correct (h : (σ, s) ⇓ σ') : (σ, s.simplify) ⇓ σ' := by
   -- TODO: we need a mechanism for saying we just want the intro rules
-  induction h <;> try grind [Bigstep]
-  next => grind [=_ Expr.eval_simplify, Bigstep.ifTrue]
-  next => grind [=_ Expr.eval_simplify, Bigstep.ifFalse]
-  next => grind [=_ Expr.eval_simplify, Bigstep.whileTrue]
+  induction h <;> grind [=_ Expr.eval_simplify, Bigstep.skip, Bigstep.assign,
+    Bigstep.seq, Bigstep.whileFalse, Bigstep.whileTrue, Bigstep.ifTrue, Bigstep.ifFalse]
 
 @[simp, grind =] def Expr.constProp (e : Expr) (σ : State) : Expr :=
   match e with
@@ -225,9 +225,8 @@ theorem Stmt.simplify_correct (h : (σ, s) ⇓ σ') : (σ, s.simplify) ⇓ σ' :
 @[grind] theorem State.length_erase_le (σ : State) (x : Var) : (σ.erase x).length ≤ σ.length := by
   induction σ, x using erase.induct <;> grind [State.erase] -- TODO add missing theorem(s)
 
-def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ :=
-  -- TODO: offset issues?
-  Nat.lt_of_le_of_lt (length_erase_le ..) (by grind)
+def State.length_erase_lt (σ : State) (x : Var) : (σ.erase x).length < σ.length.succ := by
+  grind
 
 @[simp, grind =] def State.join (σ₁ σ₂ : State) : State :=
   match σ₁ with

tests/lean/run/grind_ematch1.lean

@@ -110,9 +110,7 @@ opaque P : Nat → Prop
 opaque Q : Nat → Prop
 opaque f : Nat → Nat → Nat
 
-/--
-info: [grind.ematch.pattern] pqf: [P (f #2 #1)]
--/
+/-- info: [grind.ematch.pattern] pqf: [f #2 #1] -/
 #guard_msgs (info) in
 @[grind←] theorem pqf : Q x → P (f x y) := sorry
 

tests/lean/run/grind_ematch2.lean

@@ -47,15 +47,16 @@ info: [grind] Counters
     [thm] Array.size_set ↦ 3
 ---
 info: [diag] Diagnostics
-  [reduction] unfolded declarations (max: 11822, num: 2):
-    [reduction] LT.lt ↦ 11822
+  [reduction] unfolded declarations (max: 11829, num: 3):
+    [reduction] LT.lt ↦ 11829
     [reduction] getElem ↦ 64
+    [reduction] Nat.lt ↦ 22
   [reduction] unfolded instances (max: 32, num: 1):
     [reduction] Array.instGetElemNatLtSize ↦ 32
   [reduction] unfolded reducible declarations (max: 7079, num: 7):
     [reduction] Array.size ↦ 7079
     [reduction] Array.toList ↦ 1885
-    [reduction] autoParam ↦ 1694
+    [reduction] autoParam ↦ 1715
     [reduction] outParam ↦ 124
     [reduction] Ne ↦ 57
     [reduction] GT.gt ↦ 40

tests/lean/run/grind_erase_attr.lean

@@ -14,6 +14,7 @@ set_option trace.grind.assert true
 
 /--
 info: [grind.assert] ¬f (f (f a)) = f a
+[grind.assert] f (f (f (f a))) = f (f (f a))
 [grind.assert] f (f (f a)) = f (f a)
 [grind.assert] f (f a) = f a
 -/

tests/lean/run/grind_usr.lean

@@ -7,16 +7,15 @@ error: the modifier `usr` is only relevant in parameters for `grind only`
 @[grind usr]
 theorem fthm : f (f x) = f x := sorry
 
-/--
-info: [grind.ematch.pattern] fthm: [f (f #0)]
--/
+/-- info: [grind.ematch.pattern] fthm: [f #0] -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.pattern true in
 example : f (f (f x)) = f x := by
   grind only [fthm]
 
 /--
-info: [grind.ematch.instance] fthm: f (f (f x)) = f (f x)
+info: [grind.ematch.instance] fthm: f (f (f (f x))) = f (f (f x))
+[grind.ematch.instance] fthm: f (f (f x)) = f (f x)
 [grind.ematch.instance] fthm: f (f x) = f x
 -/
 #guard_msgs (info) in
@@ -24,6 +23,10 @@ set_option trace.grind.ematch.instance true in
 example : f (f (f x)) = f x := by
   grind only [fthm]
 
+/--
+info: [grind.ematch.instance] fthm: f (f x) = f x
+[grind.ematch.instance] fthm: f (f (f x)) = f (f x)
+-/
 #guard_msgs (info) in
 -- should not instantiate anything using pattern `f (f #0)`
 set_option trace.grind.ematch.instance true in
@@ -45,7 +48,7 @@ error: invalid use of `usr` modifier, `fthm` does not have patterns specified wi
 example : f (f (f x)) = f x := by
   grind only [usr fthm]
 
-grind_pattern fthm => f x
+grind_pattern fthm => f (f x)
 
 example : f (f (f x)) = f x := by
   grind only [usr fthm]
@@ -54,7 +57,7 @@ example : f (f (f x)) = f x := by
 -- should not instantiate anything using pattern `f (f #0)`
 set_option trace.grind.ematch.instance true in
 example : f x = x := by
-  fail_if_success grind only [fthm]
+  fail_if_success grind only [usr fthm]
   sorry
 
 /--
@@ -64,7 +67,7 @@ info: [grind.ematch.instance] fthm: f (f x) = f x
 #guard_msgs (info) in
 set_option trace.grind.ematch.instance true in
 example : f x = x := by
-  fail_if_success grind only [usr fthm]
+  fail_if_success grind only [fthm]
   sorry
 
 /--