fix: grind parameter issues and configuration (#6686)

This PR fixes parameter processing, initialization, and attribute
handling issues in the `grind` tactic.

src/Lean/Declaration.lean

@@ -469,6 +469,10 @@ def isInductive : ConstantInfo → Bool
   | .inductInfo _ => true
   | _             => false
 
+def isDefinition : ConstantInfo → Bool
+  | .defnInfo _ => true
+  | _           => false
+
 def isTheorem : ConstantInfo → Bool
   | .thmInfo _ => true
   | _          => false

src/Lean/Elab/Tactic/Grind.lean

@@ -49,13 +49,25 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
       let kind ← if let some mod := mod? then Grind.getTheoremKindCore mod else pure .default
       if (← isInductivePredicate declName) then
         throwErrorAt p "NIY"
-      else if (← getConstInfo declName).isTheorem then
-        params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
-      else if let some eqns ← getEqnsFor? declName then
-        for eqn in eqns do
-          params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl eqn kind) }
       else
-        throwError "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type"
+        let info ← getConstInfo declName
+        match info with
+        | .thmInfo _ =>
+          if kind == .eqBoth then
+            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqLhs) }
+            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName .eqRhs) }
+          else
+            params := { params with extra := params.extra.push (← Grind.mkEMatchTheoremForDecl declName kind) }
+        | .defnInfo _ =>
+          if (← isReducible declName) then
+            throwErrorAt p "`{declName}` is a reducible definition, `grind` automatically unfolds them"
+          if kind != .eqLhs && kind != .default then
+            throwErrorAt p "invalid `grind` parameter, `{declName}` is a definition, the only acceptable (and redundant) modifier is '='"
+          let some thms ← Grind.mkEMatchEqTheoremsForDef? declName
+            | throwErrorAt p "failed to genereate equation theorems for `{declName}`"
+          params := { params with extra := params.extra ++ thms.toPArray' }
+        | _ =>
+          throwErrorAt p "invalid `grind` parameter, `{declName}` is not a theorem, definition, or inductive type"
     | _ => throwError "unexpected `grind` parameter{indentD p}"
   return params
 

src/Lean/Meta/Tactic/Grind.lean

@@ -67,4 +67,6 @@ builtin_initialize registerTraceClass `grind.debug.split
 builtin_initialize registerTraceClass `grind.debug.canon
 builtin_initialize registerTraceClass `grind.debug.offset
 builtin_initialize registerTraceClass `grind.debug.offset.proof
+builtin_initialize registerTraceClass `grind.debug.ematch.pattern
+
 end Lean

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

@@ -516,7 +516,9 @@ def mkEMatchEqTheoremCore (origin : Origin) (levelParams : Array Name) (proof :
       | HEq _ lhs _ rhs => pure (lhs, rhs)
       | _ => throwError "invalid E-matching equality theorem, conclusion must be an equality{indentExpr type}"
     let pat := if useLhs then lhs else rhs
+    trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: origin: {← origin.pp}, pat: {pat}, useLhs: {useLhs}"
     let pat ← preprocessPattern pat normalizePattern
+    trace[grind.debug.ematch.pattern] "mkEMatchEqTheoremCore: after preprocessing: {pat}, {← normalize pat}"
     let pats := splitWhileForbidden (pat.abstract xs)
     return (xs.size, pats)
   mkEMatchTheoremCore origin levelParams numParams proof patterns
@@ -651,9 +653,9 @@ private def collectPatterns? (proof : Expr) (xs : Array Expr) (searchPlaces : Ar
 
 def mkEMatchTheoremWithKind? (origin : Origin) (levelParams : Array Name) (proof : Expr) (kind : TheoremKind) : MetaM (Option EMatchTheorem) := do
   if kind == .eqLhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := true))
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := true))
   else if kind == .eqRhs then
-    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := false) (useLhs := false))
+    return (← mkEMatchEqTheoremCore origin levelParams proof (normalizePattern := true) (useLhs := false))
   let type ← inferType proof
   forallTelescopeReducing type fun xs type => do
     let searchPlaces ← match kind with
@@ -694,22 +696,26 @@ def getTheoremKindFromOpt (stx : Syntax) : CoreM TheoremKind := do
   else
     getTheoremKindCore stx[1][0]
 
+def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do
+  let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
+    | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
+  return thm
+
+def mkEMatchEqTheoremsForDef? (declName : Name) : MetaM (Option (Array EMatchTheorem)) := do
+  let some eqns ← getEqnsFor? declName | return none
+  eqns.mapM fun eqn => do
+    mkEMatchEqTheorem eqn (normalizePattern := true)
+
 private def addGrindEqAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) (useLhs := true) : MetaM Unit := do
   if (← getConstInfo declName).isTheorem then
     ematchTheoremsExt.add (← mkEMatchEqTheorem declName (normalizePattern := true) (useLhs := useLhs)) attrKind
-  else if let some eqns ← getEqnsFor? declName then
+  else if let some thms ← mkEMatchEqTheoremsForDef? declName then
     unless useLhs do
       throwError "`{declName}` is a definition, you must only use the left-hand side for extracting patterns"
-    for eqn in eqns do
-      ematchTheoremsExt.add (← mkEMatchEqTheorem eqn) attrKind
+    thms.forM (ematchTheoremsExt.add · attrKind)
   else
     throwError s!"`{thmKind.toAttribute}` attribute can only be applied to equational theorems or function definitions"
 
-def mkEMatchTheoremForDecl (declName : Name) (thmKind : TheoremKind) : MetaM EMatchTheorem := do
-  let some thm ← mkEMatchTheoremWithKind? (.decl declName) #[] (← getProofFor declName) thmKind
-    | throwError "`@{thmKind.toAttribute} theorem {declName}` {thmKind.explainFailure}, consider using different options or the `grind_pattern` command"
-  return thm
-
 private def addGrindAttr (declName : Name) (attrKind : AttributeKind) (thmKind : TheoremKind) : MetaM Unit := do
   if thmKind == .eqLhs then
     addGrindEqAttr declName attrKind thmKind (useLhs := true)

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

@@ -7,14 +7,30 @@ prelude
 import Lean.Meta.Tactic.Simp.Simproc
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.DoNotSimp
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.List
 
 namespace Lean.Meta.Grind
 
 /-- Returns the array of simprocs used by `grind`. -/
 protected def getSimprocs : MetaM (Array Simprocs) := do
   let s ← grindNormSimprocExt.getSimprocs
   let s ← addDoNotSimp s
-  return #[s, (← Simp.getSEvalSimprocs)]
+  let e ← Simp.getSEvalSimprocs
+  /-
+  We don't want to apply `List.reduceReplicate` as a normalization operation in
+  `grind`. Consider the following example:
+  ```
+  example (ys : List α) : n = 0 → List.replicate n ys = [] := by
+    grind only [List.replicate]
+  ```
+  The E-matching module generates the following instance for `List.replicate.eq_1`
+  ```
+  List.replicate 0 [] = []
+  ```
+  We don't want it to be simplified to `[] = []`.
+  -/
+  let e := e.erase ``List.reduceReplicate
+  return #[s, e]
 
 /-- Returns the simplification context used by `grind`. -/
 protected def getSimpContext : MetaM Simp.Context := do

tests/lean/run/grind_ematch_patterns.lean

@@ -0,0 +1,48 @@
+def replicate : (n : Nat) → (a : α) → List α
+  | 0,   _ => []
+  | n+1, a => a :: replicate n a
+
+/--
+info: [grind.ematch.pattern] replicate.eq_1: [@replicate #1 `[0] #0]
+[grind.ematch.pattern] replicate.eq_2: [@replicate #2 (Lean.Grind.offset #0 (1)) #1]
+-/
+#guard_msgs (info) in
+set_option trace.grind.ematch.pattern true in
+attribute [grind] replicate
+
+example : ys = [] → replicate 0 [] = ys := by
+  grind only [replicate]
+
+/--
+error: invalid `grind` parameter, `replicate` is a definition, the only acceptable (and redundant) modifier is '='
+-/
+#guard_msgs (error) in
+example : ys = [] → replicate 0 [] = ys := by
+  grind only [←replicate]
+
+example : ys = [] → replicate 0 [] = ys := by
+  fail_if_success grind only
+  sorry
+
+example (ys : List α) : n = 0 → replicate n ys = [] := by
+  grind only [replicate]
+
+example (ys : List α) : n = 0 → List.replicate n ys = [] := by
+  grind only [List.replicate]
+
+opaque foo : Nat → Nat
+opaque bla : Nat → Nat
+
+theorem foo_bla : foo x = bla x := sorry
+
+example : foo x = bla x := by
+  grind only [_=_ foo_bla]
+
+@[reducible] def inc (_ : Nat) := 1
+
+/--
+error: `inc` is a reducible definition, `grind` automatically unfolds them
+-/
+#guard_msgs (error) in
+example : a = 1 → inc x = a := by
+  grind [inc]