feat: add [grind_cases] attribute

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

@@ -16,4 +16,54 @@ builtin_initialize grindNormExt : SimpExtension ←
 builtin_initialize grindNormSimprocExt : SimprocExtension ←
   registerSimprocAttr `grind_norm_proc "simplification/normalization procedured for `grind`" none
 
+builtin_initialize grindCasesExt : SimpleScopedEnvExtension Name NameSet ←
+  registerSimpleScopedEnvExtension {
+    initial        := {}
+    addEntry       := fun s declName => s.insert declName
+  }
+
+/--
+Returns `true` if `declName` has been tagged with attribute `[grind_cases]`.
+-/
+def isGrindCasesTarget (declName : Name) : CoreM Bool :=
+  return grindCasesExt.getState (← getEnv) |>.contains declName
+
+private def getAlias? (value : Expr) : MetaM (Option Name) :=
+  lambdaTelescope value fun _ body => do
+    if let .const declName _ := body.getAppFn' then
+      return some declName
+    else
+      return none
+
+/--
+Throws an error if `declName` cannot be annotated with attribute `[grind_cases]`.
+We support the following cases:
+- `declName` is a non-recursive datatype.
+- `declName` is an abbreviation for a non-recursive datatype.
+-/
+private partial def validateGrindCasesAttr (declName : Name) : CoreM Unit := do
+  match (← getConstInfo declName) with
+  | .inductInfo info =>
+    if info.isRec then
+      throwError "`{declName}` is a recursive datatype"
+  | .defnInfo info =>
+    let failed := throwError "`{declName}` is a definition, but it is not an alias/abbreviation for an inductive datatype"
+    let some declName ← getAlias? info.value |>.run' {} {}
+      | failed
+    try
+      validateGrindCasesAttr declName
+    catch _ =>
+      failed
+  | _ =>
+    throwError "`{declName}` is not an inductive datatype or an alias for one"
+
+builtin_initialize
+  registerBuiltinAttribute {
+    name  := `grind_cases
+    descr := "`grind` tactic applies `cases` to (non-recursive) inductives during pre-processing step"
+    add   := fun declName _ attrKind => do
+      validateGrindCasesAttr declName
+      grindCasesExt.add declName attrKind
+  }
+
 end Lean.Meta.Grind

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

@@ -107,10 +107,9 @@ def introNext (goal : Goal) : PreM IntroResult := do
 def pushResult (goal : Goal) : PreM Unit :=
   modifyThe Grind.State fun s => { s with goals := s.goals.push goal }
 
--- TODO: use `[grind_cases]` attribute
 def isCasesCandidate (fvarId : FVarId) : MetaM Bool := do
-  let type ← fvarId.getType
-  return type.isAppOf ``And
+  let .const declName _ := (← fvarId.getType).getAppFn | return false
+  isGrindCasesTarget declName
 
 def applyCases? (goal : Goal) (fvarId : FVarId) : MetaM (Option (List Goal)) := goal.mvarId.withContext do
   if (← isCasesCandidate fvarId) then

tests/lean/run/grind_cases.lean

@@ -0,0 +1,29 @@
+/--
+error: `List` is a recursive datatype
+-/
+#guard_msgs in
+attribute [grind_cases] List
+
+/--
+error: `Prod.mk` is not an inductive datatype or an alias for one
+-/
+#guard_msgs in
+attribute [grind_cases] Prod.mk
+
+/--
+error: `List.append` is a definition, but it is not an alias/abbreviation for an inductive datatype
+-/
+#guard_msgs in
+attribute [grind_cases] List.append
+
+attribute [grind_cases] Prod
+
+def Foo (α : Type u) := Sum α α
+
+attribute [grind_cases] Foo
+
+attribute [grind_cases] And
+
+attribute [grind_cases] False
+
+attribute [grind_cases] Empty

tests/lean/run/grind_pre.lean

@@ -9,23 +9,52 @@ elab "grind_pre" : tactic => do
 
 abbrev f (a : α) := a
 
+attribute [grind_cases] And Or
+
 /--
 warning: declaration uses 'sorry'
 ---
 info: a b c : Bool
 p q : Prop
 left✝ : a = true
-right✝ : b = true ∨ c = true
+h✝ : b = true
 left : p
 right : q
-x✝ : b = false ∨ a = false
+h : b = false
+⊢ False
+
+a b c : Bool
+p q : Prop
+left✝ : a = true
+h✝ : b = true
+left : p
+right : q
+h : a = false
+⊢ False
+
+a b c : Bool
+p q : Prop
+left✝ : a = true
+h✝ : c = true
+left : p
+right : q
+h : b = false
+⊢ False
+
+a b c : Bool
+p q : Prop
+left✝ : a = true
+h✝ : c = true
+left : p
+right : q
+h : a = false
 ⊢ False
 -/
 #guard_msgs in
 theorem ex (h : (f a && (b || f (f c))) = true) (h' : p ∧ q) : b && a := by
   grind_pre
   trace_state
-  sorry
+  all_goals sorry
 
 def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j
 
@@ -39,8 +68,8 @@ example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j +
 /--
 warning: declaration uses 'sorry'
 ---
-info: α✝ : Type ?u.1908
-β✝ : Type ?u.1907
+info: α✝ : Type u_1
+β✝ : Type u_2
 a₁ : α✝ × β✝
 a₂ : α✝
 a₃ : β✝
@@ -56,7 +85,7 @@ tail_eq : as = bs
 ⊢ False
 -/
 #guard_msgs in
-example (h : a₁ :: (a₂, a₃) :: as = b₁ :: (b₂, b₃) :: bs) : False := by
+theorem ex2 (h : a₁ :: (a₂, a₃) :: as = b₁ :: (b₂, b₃) :: bs) : False := by
   grind_pre
   trace_state
   sorry