feat: builtin case splits for grind (#6822)

This PR adds a few builtin case-splits for `grind`. They are similar to
builtin `simp` theorems. They reduce the noise in the tactics produced
by `grind?`.

Author: leodemoura

src/Lean/Elab/Tactic/Grind.lean

@@ -53,6 +53,7 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
     | `(Parser.Tactic.grindParam| - $id:ident) =>
       let declName ← realizeGlobalConstNoOverloadWithInfo id
       if (← Grind.isCasesAttrCandidate declName false) then
+        Grind.ensureNotBuiltinCases declName
         params := { params with casesTypes := (← params.casesTypes.eraseDecl declName) }
       else
         params := { params with ematch := (← params.ematch.eraseDecl declName) }
@@ -188,11 +189,12 @@ private def mkGrindOnly
             | .default => `(Parser.Tactic.grindParam| $decl:ident)
           params := params.push param
   for declName in trace.eagerCases.toList do
-    let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
-    let param ← `(Parser.Tactic.grindParam| cases eager $decl)
-    params := params.push param
+    unless Grind.isBuiltinEagerCases declName do
+      let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+      let param ← `(Parser.Tactic.grindParam| cases eager $decl)
+      params := params.push param
   for declName in trace.cases.toList do
-    unless trace.eagerCases.contains declName do
+    unless trace.eagerCases.contains declName || Grind.isBuiltinEagerCases declName do
       let decl : Ident := mkIdent (← unresolveNameGlobalAvoidingLocals declName)
       let param ← `(Parser.Tactic.grindParam| cases $decl)
       params := params.push param

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

@@ -18,6 +18,22 @@ structure CasesEntry where
   eager : Bool
   deriving Inhabited
 
+/--
+`grind` always case-splits on the following types. Even when using `grind only`.
+The goal is to reduce noise in the tactic generated by `grind?`
+-/
+private def builtinEagerCases : NameSet :=
+  RBTree.ofList [``And, ``Exists, ``True, ``False, ``Unit, ``Empty]
+
+/--
+Returns `true` if `declName` is the name of inductive type/predicate that
+even `grind only` case splits on.
+Remark: we added support for them to reduce the noise in the tactic generated by
+`grind?`
+-/
+def isBuiltinEagerCases (declName : Name) : Bool :=
+  builtinEagerCases.contains declName
+
 /-- Returns `true` if `s` contains a `declName`. -/
 def CasesTypes.contains (s : CasesTypes) (declName : Name) : Bool :=
   s.casesMap.contains declName
@@ -33,10 +49,10 @@ def CasesTypes.find? (s : CasesTypes) (declName : Name) : Option Bool :=
   s.casesMap.find? declName
 
 def CasesTypes.isEagerSplit (s : CasesTypes) (declName : Name) : Bool :=
-  s.casesMap.find? declName |>.getD false
+  (s.casesMap.find? declName |>.getD false) || isBuiltinEagerCases declName
 
 def CasesTypes.isSplit (s : CasesTypes) (declName : Name) : Bool :=
-  s.casesMap.find? declName |>.isSome
+  (s.casesMap.find? declName |>.isSome) || isBuiltinEagerCases declName
 
 builtin_initialize casesExt : SimpleScopedEnvExtension CasesEntry CasesTypes ←
   registerSimpleScopedEnvExtension {
@@ -80,7 +96,12 @@ def CasesTypes.eraseDecl (s : CasesTypes) (declName : Name) : CoreM CasesTypes :
   else
     throwError "`{declName}` is not marked with the `[grind]` attribute"
 
+def ensureNotBuiltinCases (declName : Name) : CoreM Unit := do
+  if isBuiltinEagerCases declName then
+    throwError "`{declName}` is marked as a built-in case-split for `grind` and cannot be erased"
+
 def eraseCasesAttr (declName : Name) : CoreM Unit := do
+  ensureNotBuiltinCases declName
   let s := casesExt.getState (← getEnv)
   let s ← s.eraseDecl declName
   modifyEnv fun env => casesExt.modifyState env fun _ => s

tests/lean/run/grind_trace.lean

@@ -33,14 +33,14 @@ example : 0 < (x :: t).length := by
 /--
 info: Try this: grind only [= List.getElem?_replicate, = List.getElem?_eq_some_iff, = List.getElem?_map, =
   List.getElem_replicate, = List.getElem?_eq_none, = Option.map_some', = Option.map_none', = List.length_replicate, →
-  List.getElem?_eq_getElem, cases And, cases Or, cases Exists]
+  List.getElem?_eq_getElem, cases Or]
 -/
 #guard_msgs (info) in
 theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) := by
   grind?
 
 /--
-info: Try this: grind only [= List.getLast?_eq_some_iff, List.mem_concat_self, cases Exists]
+info: Try this: grind only [= List.getLast?_eq_some_iff, List.mem_concat_self]
 -/
 #guard_msgs (info) in
 theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
@@ -79,3 +79,16 @@ info: Try this: grind only [usr gthm]
 #guard_msgs (info) in
 example : g (g (g x)) = g x := by
   grind?
+
+/--
+error: `And` is marked as a built-in case-split for `grind` and cannot be erased
+-/
+#guard_msgs (error) in
+attribute [-grind] And
+
+/--
+error: `And` is marked as a built-in case-split for `grind` and cannot be erased
+-/
+#guard_msgs (error) in
+example : p ∧ q → p := by
+  grind [-And]