feat: better support for inductive predicates in grind (#6854)

This PR adds a convenience for inductive predicates in `grind`. Now,
give an inductive predicate `C`, `grind [C]` marks `C` terms as
case-split candidates **and** `C` constructors as E-matching theorems.
Here is an example:
```lean
example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
  grind [BigStep]
```
Users can still use `grind [cases BigStep]` to only mark `C` as a case
split candidate.

src/Lean/Elab/Tactic/Grind.lean

@@ -85,6 +85,11 @@ def elabGrindParams (params : Grind.Params) (ps :  TSyntaxArray ``Parser.Tactic.
       | .infer =>
         if (← Grind.isCasesAttrCandidate declName false) then
           params := { params with casesTypes := params.casesTypes.insert declName false }
+          if let some info ← isInductivePredicate? declName then
+            -- If it is an inductive predicate,
+            -- we also add the contructors (intro rules) as E-matching rules
+            for ctor in info.ctors do
+              params ← withRef p <| addEMatchTheorem params ctor .default
         else
           params ← withRef p <| addEMatchTheorem params declName .default
     | _ => throwError "unexpected `grind` parameter{indentD p}"

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

@@ -67,6 +67,11 @@ builtin_initialize
       | .infer =>
         if (← isCasesAttrCandidate declName false) then
           addCasesAttr declName false attrKind
+          if let some info ← isInductivePredicate? declName then
+            -- If it is an inductive predicate,
+            -- we also add the contructors (intro rules) as E-matching rules
+            for ctor in info.ctors do
+              addEMatchAttr ctor attrKind .default
         else
           addEMatchAttr declName attrKind .default
     erase := fun declName => MetaM.run' do

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

@@ -107,12 +107,13 @@ def Counters.toMessageData? (cs : Counters) : MetaM (Option MessageData) := do
     match origin with
     | .decl declName => some (declName, c)
     | _ => none
+  -- We do not report `cases` applications on builtin types
+  let cases := cs.case.toList.toArray.filter fun (declName, _) => !isBuiltinEagerCases declName
   let mut msgs := #[]
   unless thms.isEmpty do
     msgs := msgs.push <| (← countersToMessageData "E-Matching instances" `thm thms)
-  let cases := cs.case.toList.toArray
   unless cases.isEmpty do
-    msgs := msgs.push <| (← countersToMessageData "Case splits" `cases cases)
+    msgs := msgs.push <| (← countersToMessageData "Cases instances" `cases cases)
   if msgs.isEmpty then
     return none
   else

tests/lean/run/grind_bigstep.lean

@@ -0,0 +1,46 @@
+abbrev Variable := String
+
+def State := Variable → Nat
+
+inductive Stmt : Type where
+  | skip : Stmt
+  | assign : Variable → (State → Nat) → Stmt
+  | seq : Stmt → Stmt → Stmt
+  | ifThenElse : (State → Prop) → Stmt → Stmt → Stmt
+  | whileDo : (State → Prop) → Stmt → Stmt
+
+infix:60 ";; " => Stmt.seq
+
+export Stmt (skip assign seq ifThenElse whileDo)
+
+set_option quotPrecheck false in
+notation s:70 "[" x:70 "↦" n:70 "]" => (fun v ↦ if v = x then n else s v)
+
+inductive BigStep : Stmt → State → State → Prop where
+  | skip (s : State) : BigStep skip s s
+  | assign (x : Variable) (a : State → Nat) (s : State) : BigStep (assign x a) s (s[x ↦ a s])
+  | seq {S T : Stmt} {s t u : State} (hS : BigStep S s t) (hT : BigStep T t u) :
+    BigStep (S;; T) s u
+  | if_true {B : State → Prop} {s t : State} (hcond : B s) (S T : Stmt) (hbody : BigStep S s t) :
+    BigStep (ifThenElse B S T) s t
+  | if_false {B : State → Prop} {s t : State} (hcond : ¬ B s) (S T : Stmt) (hbody : BigStep T s t) :
+    BigStep (ifThenElse B S T) s t
+  | while_true {B S s t u} (hcond : B s) (hbody : BigStep S s t) (hrest : BigStep (whileDo B S) t u) :
+    BigStep (whileDo B S) s u
+  | while_false {B S s} (hcond : ¬ B s) : BigStep (whileDo B S) s s
+
+notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t
+
+example {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
+  grind [BigStep]
+
+attribute [grind] BigStep
+
+theorem cases_if_of_true {B S T s t} (hcond : B s) : (ifThenElse B S T, s) ==> t → (S, s) ==> t := by
+  grind
+
+theorem cases_if_of_false {B S T s t} (hcond : ¬ B s) : (ifThenElse B S T, s) ==> t → (T, s) ==> t := by
+  grind
+
+theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==> t ↔ (B s ∧ (S, s) ==> t) ∨ (¬ B s ∧ (T, s) ==> t) := by
+  grind

tests/lean/run/grind_ematch2.lean

@@ -45,8 +45,6 @@ info: [grind] Counters
   [thm] E-Matching instances
     [thm] Array.get_set_ne ↦ 3
     [thm] Array.size_set ↦ 3
-  [cases] Case splits
-    [cases] And ↦ 2
 ---
 info: [diag] Diagnostics
   [reduction] unfolded declarations (max: 11822, num: 2):

tests/lean/run/grind_pre.lean

@@ -34,9 +34,6 @@ h : c = true
     [eqc] {b = true, a = false}
     [eqc] {b, false}
     [eqc] {a, c, true}
-[grind] Counters
-  [cases] Case splits
-    [cases] And ↦ 2
 -/
 #guard_msgs (error) in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
@@ -70,8 +67,7 @@ h : b = false
     [eqc] {b, false}
     [eqc] {a, c, true}
 [grind] Counters
-  [cases] Case splits
-    [cases] And ↦ 3
+  [cases] Cases instances
     [cases] Or ↦ 3
 -/
 #guard_msgs (error) in

tests/lean/run/grind_split_issue.lean

@@ -5,25 +5,44 @@ inductive X : Nat → Prop
 
 /--
 error: `grind` failed
-case grind.1
+case grind.1.1
 c : Nat
 q : X c 0
+s✝ : Nat
+h✝² : 0 = s✝
+h✝¹ : HEq ⋯ ⋯
 s : Nat
-h✝ : 0 = s
+h✝ : c = s
 h : HEq ⋯ ⋯
 ⊢ False
 [grind] Diagnostics
   [facts] Asserted facts
     [prop] X c 0
-    [prop] 0 = s
+    [prop] X c 0
+    [prop] X c c → X c 0
+    [prop] X c c
+    [prop] 0 = s✝
+    [prop] HEq ⋯ ⋯
+    [prop] c = s
     [prop] HEq ⋯ ⋯
   [eqc] True propositions
     [prop] X c 0
+    [prop] X c c → X c 0
+    [prop] X c c
+    [prop] X c s✝
     [prop] X c s
   [eqc] Equivalence classes
-    [eqc] {s, 0}
+    [eqc] {c, s}
+    [eqc] {s✝, 0}
+  [ematch] E-matching patterns
+    [thm] X.f: [X #1 #0]
+    [thm] X.g: [X #2 #1]
 [grind] Issues
-  [issue] #1 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
+  [issue] #2 other goal(s) were not fully processed due to previous failures, threshold: `(failures := 1)`
+[grind] Counters
+  [thm] E-Matching instances
+    [thm] X.f ↦ 2
+    [thm] X.g ↦ 2
 -/
 #guard_msgs (error) in
 example {c : Nat} (q : X c 0) : False := by

tests/lean/run/grind_t1.lean

@@ -300,7 +300,7 @@ example : (replicate n a).map f = replicate n (f a) := by
 
 open List in
 example : (replicate n a).map f = replicate n (f a) := by
-  grind only [Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
+  grind only [cases Exists, Option.map_some', Option.map_none', getElem?_map, getElem?_replicate]
 
 open List in
 example : (replicate n a).map f = replicate n (f a) := by