chore: fix test

This PR adds the `grind` configuration option `verbose`.
For example, `grind -verbose` disables all diagnostics.
We are going to use this flag to implement `try?`.

src/Init.lean

@@ -38,3 +38,4 @@ import Init.Grind
 import Init.While
 import Init.Syntax
 import Init.Internal
+import Init.Try

src/Init/Grind/Tactics.lean

@@ -65,6 +65,8 @@ structure Config where
   canonHeartbeats : Nat := 1000
   /-- If `ext` is `true`, `grind` uses extensionality theorems available in the environment. -/
   ext : Bool := true
+  /-- If `verbose` is `false`, additional diagnostics information is not collected. -/
+  verbose : Bool := true
   deriving Inhabited, BEq
 
 end Lean.Grind

src/Init/Try.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Tactics
+
+namespace Lean.Try
+/--
+Configuration for `try?`.
+-/
+structure Config where
+  /-- If `main` is `true`, all functions in the current module are considered for function induction, unfolding, etc. -/
+  main := true
+  /-- If `name` is `true`, all functions in the same namespace are considere for function induction, unfolding, etc. -/
+  name := true
+  /-- If `lib` is `true`, uses `libSearch` results. -/
+  lib := true
+  /-- If `targetOnly` is `true`, `try?` collects information using the goal target only. -/
+  targetOnly := false
+  deriving Inhabited
+
+end Lean.Try
+
+namespace Lean.Parser.Tactic
+
+syntax (name := tryTrace) "try?" optConfig : tactic
+
+end Lean.Parser.Tactic

src/Lean/Elab/Tactic.lean

@@ -46,3 +46,4 @@ import Lean.Elab.Tactic.BoolToPropSimps
 import Lean.Elab.Tactic.Classical
 import Lean.Elab.Tactic.Grind
 import Lean.Elab.Tactic.Monotonicity
+import Lean.Elab.Tactic.Try

src/Lean/Elab/Tactic/Try.lean

@@ -0,0 +1,166 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Try
+import Init.Grind.Tactics
+import Lean.Meta.Tactic.Try
+import Lean.Meta.Tactic.TryThis
+import Lean.Elab.Tactic.Config
+
+namespace Lean.Elab.Tactic
+open Meta
+/-!
+A **very** simple `try?` tactic implementation.
+-/
+
+declare_config_elab elabTryConfig Try.Config
+
+structure Try.Context where
+  mvarId : MVarId
+  config : Try.Config
+  tk     : Syntax
+
+private abbrev M := ReaderT Try.Context TacticM
+
+instance : OrElse (M α) where
+  orElse a b := fun ctx => a ctx <|> b () ctx
+
+open Tactic in
+private def addSuggestion (stx : TryThis.Suggestion) : M Bool := do
+  TryThis.addSuggestion (← read).tk stx (origSpan? := (← getRef))
+  return true
+
+-- TODO: vanilla `induction`.
+-- TODO: cleanup the whole file, and use better combinators
+-- TODO: make it extensible.
+-- TODO: librarySearch integration.
+-- TODO: premise selection.
+
+private def failed (msg : MessageData) : M Bool := do
+  trace[«try»] msg
+  return false
+
+private def tryTac (stx : TSyntax `tactic) (msg : MessageData) : M Bool :=
+  (do
+    focusAndDone <| evalTactic stx
+    addSuggestion stx)
+  <|> failed msg
+
+private def trySimp : M Bool := do
+  tryTac (← `(tactic| simp)) "`simp` failed"
+
+set_option hygiene false in
+private def trySimpArith : M Bool := do
+  tryTac (← `(tactic| simp +arith)) "`simp +arith` failed"
+
+private def tryGrind : M Bool := do
+  (do
+    evalTactic (← `(tactic| grind -verbose))
+    addSuggestion (← `(tactic| grind?)))
+  <|> failed "`grind` failed"
+
+private def collect : M Try.Info := do
+  Try.collect (← read).mvarId (← read).config
+
+private def toIdent (declName : Name) : MetaM Ident := do
+  return mkIdent (← unresolveNameGlobalAvoidingLocals declName)
+
+inductive TacticKind where
+  | exec
+  | suggestion
+  | error
+
+private def mkGrindStx (params : Array (TSyntax ``Parser.Tactic.grindParam)) (kind : TacticKind) : MetaM (TSyntax `tactic) := do
+  let result ← match kind with
+    | .exec => `(tactic| grind -verbose)
+    | .suggestion => `(tactic| grind?)
+    | .error => `(tactic| grind)
+  if params.isEmpty then
+    return result
+  else
+    let paramsStx := #[mkAtom "[", (mkAtom ",").mkSep params, mkAtom "]"]
+    return ⟨result.raw.setArg 3 (mkNullNode paramsStx)⟩
+
+private def mkGrindEqnsStx (declNames : Std.HashSet Name) : M (TacticKind → MetaM (TSyntax `tactic)) := do
+  let mut params := #[]
+  for declName in declNames do
+    params := params.push (← `(Parser.Tactic.grindParam| = $(← toIdent declName)))
+  return mkGrindStx params
+
+private def tryTac' (mkTac : TacticKind → MetaM (TSyntax `tactic)) : M Bool := do
+  let stx ← mkTac .exec
+  (do
+    focusAndDone <| evalTactic stx
+    addSuggestion (← mkTac .suggestion))
+  <|>
+  (do failed m!"`{← mkTac .error}` failed")
+
+private def tryGrindEqns (info : Try.Info) : M Bool := do
+  if info.eqnCandidates.isEmpty then return false
+  tryTac' (← mkGrindEqnsStx info.eqnCandidates)
+
+private def tryGrindUnfold (info : Try.Info) : M Bool := do
+  if info.unfoldCandidates.isEmpty then return false
+  tryTac' (← mkGrindEqnsStx info.unfoldCandidates)
+
+private def allAccessible (majors : Array FVarId) : MetaM Bool :=
+  majors.allM fun major => do
+    let localDecl ← major.getDecl
+    -- TODO: we are not checking shadowed variables
+    return !localDecl.userName.hasMacroScopes
+
+open Try.Collector in
+private partial def tryFunIndsCore (info : Try.Info) (mkBody : TacticKind → MetaM (TSyntax `tactic)) : M Bool := do
+  go info.funIndCandidates.toList
+where
+  go' (c : FunIndCandidate) : M Bool := do
+    if (← allAccessible c.majors) then
+      let mut terms := #[]
+      for major in c.majors do
+        let localDecl ← major.getDecl
+        terms := terms.push (← `($(mkIdent localDecl.userName):term))
+      let indFn ← toIdent c.funIndDeclName
+      tryTac' fun k => do
+        let body ← mkBody k
+        `(tactic| induction $terms,* using $indFn <;> $body)
+    else
+      -- TODO: use `rename_i`
+      failed "`induction` failed, majors contain inaccessible vars {c.majors.map mkFVar}"
+
+  go (cs : List FunIndCandidate) : M Bool := do
+    match cs with
+    | [] => return false
+    | c::cs =>
+      trace[try.debug.funInd] "{c.funIndDeclName}, {c.majors.map mkFVar}"
+      go' c <||> go cs
+
+private partial def tryFunIndsGrind (info : Try.Info) : M Bool :=
+  tryFunIndsCore info (mkGrindStx #[])
+
+private partial def tryFunIndsGrindEqns (info : Try.Info) : M Bool := do
+  if info.eqnCandidates.isEmpty then return false
+  tryFunIndsCore info (← mkGrindEqnsStx info.eqnCandidates)
+
+private def evalTryTraceCore : M Unit := do
+  if (← trySimp) then return ()
+  if (← trySimpArith) then return ()
+  if (← tryGrind) then return ()
+  let info ← collect
+  if (← tryGrindEqns info) then return ()
+  if (← tryGrindUnfold info) then return ()
+  if (← tryFunIndsGrind info) then return ()
+  if (← tryFunIndsGrindEqns info) then return ()
+  Meta.throwTacticEx `«try?» (← read).mvarId "consider using `grind` manually, `set_option trace.try true` shows everything `try?` tried"
+
+@[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do
+  match stx with
+  | `(tactic| try?%$tk $config:optConfig) =>
+    let mvarId ← getMainGoal
+    let config ← elabTryConfig config
+    evalTryTraceCore { config, tk, mvarId }
+  | _ => throwUnsupportedSyntax
+
+end Lean.Elab.Tactic

src/Lean/Meta/Tactic.lean

@@ -42,3 +42,4 @@ import Lean.Meta.Tactic.Rfl
 import Lean.Meta.Tactic.Rewrites
 import Lean.Meta.Tactic.Grind
 import Lean.Meta.Tactic.Ext
+import Lean.Meta.Tactic.Try

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

@@ -60,7 +60,7 @@ private def isDefEqBounded (a b : Expr) (parent : Expr) : GoalM Bool := do
       withDefault <| isDefEq a b)
     fun ex => do
       if ex.isRuntime then
-        reportIssue m!"failed to show that{indentExpr a}\nis definitionally equal to{indentExpr b}\nwhile canonicalizing{indentExpr parent}\nusing `{curr}*1000` heartbeats, `(canonHeartbeats := {curr})`"
+        reportIssue! "failed to show that{indentExpr a}\nis definitionally equal to{indentExpr b}\nwhile canonicalizing{indentExpr parent}\nusing `{curr}*1000` heartbeats, `(canonHeartbeats := {curr})`"
         return false
       else
         throw ex

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

@@ -66,6 +66,10 @@ def resetCasesExt : CoreM Unit := do
 def getCasesTypes : CoreM CasesTypes :=
   return casesExt.getState (← getEnv)
 
+/-- Returns `true` is `declName` is a builtin split or has been tagged with `[grind]` attribute. -/
+def isSplit (declName : Name) : CoreM Bool := do
+  return (← getCasesTypes).isSplit declName
+
 private def getAlias? (value : Expr) : MetaM (Option Name) :=
   lambdaTelescope value fun _ body => do
     if let .const declName _ := body.getAppFn' then

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

@@ -20,7 +20,7 @@ private partial def propagateInjEqs (eqs : Expr) (proof : Expr) : GoalM Unit :=
   | HEq _ lhs _ rhs =>
     pushHEq (← shareCommon lhs) (← shareCommon rhs) proof
   | _ =>
-   reportIssue m!"unexpected injectivity theorem result type{indentExpr eqs}"
+   reportIssue! "unexpected injectivity theorem result type{indentExpr eqs}"
    return ()
 
 /--

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

@@ -268,7 +268,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   assert! c.assignment.size == numParams
   let (mvars, bis, _) ← forallMetaBoundedTelescope (← inferType proof) numParams
   if mvars.size != thm.numParams then
-    reportIssue m!"unexpected number of parameters at {← thm.origin.pp}"
+    reportIssue! "unexpected number of parameters at {← thm.origin.pp}"
     return ()
   -- Apply assignment
   for h : i in [:mvars.size] do
@@ -278,7 +278,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
       let mvarIdType ← mvarId.getType
       let vType ← inferType v
       let report : M Unit := do
-        reportIssue m!"type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
+        reportIssue! "type error constructing proof for {← thm.origin.pp}\nwhen assigning metavariable {mvars[i]} with {indentExpr v}\n{← mkHasTypeButIsExpectedMsg vType mvarIdType}"
       unless (← withDefault <| isDefEq mvarIdType vType) do
         let some heq ← proveEq? vType mvarIdType
           | report
@@ -297,7 +297,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstanceAndAssign mvar type) do
-        reportIssue m!"failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
+        reportIssue! "failed to synthesize instance when instantiating {← thm.origin.pp}{indentExpr type}"
         return ()
   let proof := mkAppN proof mvars
   if (← mvars.allM (·.mvarId!.isAssigned)) then
@@ -305,7 +305,7 @@ private partial def instantiateTheorem (c : Choice) : M Unit := withDefault do w
   else
     let mvars ← mvars.filterM fun mvar => return !(← mvar.mvarId!.isAssigned)
     if let some mvarBad ← mvars.findM? fun mvar => return !(← isProof mvar) then
-      reportIssue m!"failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
+      reportIssue! "failed to instantiate {← thm.origin.pp}, failed to instantiate non propositional argument with type{indentExpr (← inferType mvarBad)}"
     let proof ← mkLambdaFVars (binderInfoForMVars := .default) mvars (← instantiateMVars proof)
     addNewInstance thm proof c.gen
 

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

@@ -228,6 +228,10 @@ private builtin_initialize ematchTheoremsExt : SimpleScopedEnvExtension EMatchTh
     initial  := {}
   }
 
+/-- Returns `true` if `declName` has been tagged as an E-match theorem using `[grind]`. -/
+def isEMatchTheorem (declName : Name) : CoreM Bool := do
+  return ematchTheoremsExt.getState (← getEnv) |>.omap.contains (.decl declName)
+
 def resetEMatchTheoremsExt : CoreM Unit := do
   modifyEnv fun env => ematchTheoremsExt.modifyState env fun _ => {}
 

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

@@ -14,14 +14,14 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   let c ← mkConstWithFreshMVarLevels thm.declName
   let (mvars, bis, type) ← withDefault <| forallMetaTelescopeReducing (← inferType c)
   unless (← isDefEq e type) do
-    reportIssue m!"failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nis not definitionally equal to{indentExpr type}"
+    reportIssue! "failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nis not definitionally equal to{indentExpr type}"
     return ()
   -- Instantiate type class instances
   for mvar in mvars, bi in bis do
     if bi.isInstImplicit && !(← mvar.mvarId!.isAssigned) then
       let type ← inferType mvar
       unless (← synthesizeInstanceAndAssign mvar type) do
-        reportIssue m!"failed to synthesize instance when instantiating extensionality theorem `{thm.declName}` for {indentExpr e}"
+        reportIssue! "failed to synthesize instance when instantiating extensionality theorem `{thm.declName}` for {indentExpr e}"
         return ()
   -- Remark: `proof c mvars` has type `e`
   let proof ← instantiateMVars (mkAppN c mvars)
@@ -33,7 +33,7 @@ def instantiateExtTheorem (thm : Ext.ExtTheorem) (e : Expr) : GoalM Unit := with
   let proof' ← instantiateMVars (← mkLambdaFVars mvars proof)
   let prop' ← inferType proof'
   if proof'.hasMVar || prop'.hasMVar then
-    reportIssue m!"failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
+    reportIssue! "failed to apply extensionality theorem `{thm.declName}` for {indentExpr e}\nresulting terms contain metavariables"
     return ()
   addNewFact proof' prop' ((← getGeneration e) + 1)
 

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

@@ -78,7 +78,7 @@ private def addLocalEMatchTheorems (e : Expr) : GoalM Unit := do
     if let some thm ← mkEMatchTheoremWithKind'? origin proof .default then
       activateTheorem thm gen
   if (← get).newThms.size == size then
-    reportIssue m!"failed to create E-match local theorem for{indentExpr e}"
+    reportIssue! "failed to create E-match local theorem for{indentExpr e}"
 
 def propagateForallPropDown (e : Expr) : GoalM Unit := do
   let .forallE n a b bi := e | return ()

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

@@ -27,7 +27,7 @@ def addCongrTable (e : Expr) : GoalM Unit := do
     let g := e'.getAppFn
     unless isSameExpr f g do
       unless (← hasSameType f g) do
-        reportIssue m!"found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
+        reportIssue! "found congruence between{indentExpr e}\nand{indentExpr e'}\nbut functions have different types"
         return ()
     trace_goal[grind.debug.congr] "{e} = {e'}"
     pushEqHEq e e' congrPlaceholderProof
@@ -231,13 +231,13 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
   | .lit .. | .const .. =>
     mkENode e generation
   | .mvar .. =>
-    reportIssue m!"unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
+    reportIssue! "unexpected metavariable during internalization{indentExpr e}\n`grind` is not supposed to be used in goals containing metavariables."
     mkENode' e generation
   | .mdata .. =>
-    reportIssue m!"unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
+    reportIssue! "unexpected metadata found during internalization{indentExpr e}\n`grind` uses a pre-processing step that eliminates metadata"
     mkENode' e generation
   | .proj .. =>
-    reportIssue m!"unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
+    reportIssue! "unexpected kernel projection term during internalization{indentExpr e}\n`grind` uses a pre-processing step that folds them as projection applications, the pre-processor should have failed to fold this term"
     mkENode' e generation
   | .app .. =>
     if (← isLitValue e) then

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

@@ -131,14 +131,15 @@ def Result.hasFailures (r : Result) : Bool :=
 
 def Result.toMessageData (result : Result) : MetaM MessageData := do
   let mut msgs ← result.failures.mapM (goalToMessageData · result.config)
-  let mut issues := result.issues
-  unless result.skipped.isEmpty do
-    let m := m!"#{result.skipped.length} other goal(s) were not fully processed due to previous failures, threshold: `(failures := {result.config.failures})`"
-    issues := .trace { cls := `issue } m #[] :: issues
-  unless issues.isEmpty do
-    msgs := msgs ++ [.trace { cls := `grind } "Issues" issues.reverse.toArray]
-  if let some msg ← result.counters.toMessageData? then
-    msgs := msgs ++ [msg]
+  if result.config.verbose then
+    let mut issues := result.issues
+    unless result.skipped.isEmpty do
+      let m := m!"#{result.skipped.length} other goal(s) were not fully processed due to previous failures, threshold: `(failures := {result.config.failures})`"
+      issues := .trace { cls := `issue } m #[] :: issues
+    unless issues.isEmpty do
+      msgs := msgs ++ [.trace { cls := `grind } "Issues" issues.reverse.toArray]
+    if let some msg ← result.counters.toMessageData? then
+      msgs := msgs ++ [msg]
   return MessageData.joinSep msgs m!"\n"
 
 def main (mvarId : MVarId) (params : Params) (mainDeclName : Name) (fallback : Fallback) : MetaM Result := do profileitM Exception "grind" (← getOptions) do

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

@@ -301,7 +301,7 @@ where
     -- created when we infer the type of the `noConfusion` term below
     let lhs ← shareCommon lhs
     let some root ← getRootENode? lhs
-      | reportIssue "found term that has not been internalized{indentExpr lhs}\nwhile trying to construct a proof for `MatchCond`{indentExpr e}"
+      | reportIssue! "found term that has not been internalized{indentExpr lhs}\nwhile trying to construct a proof for `MatchCond`{indentExpr e}"
         return none
     let isHEq := α?.isSome
     let h ← if isHEq then
@@ -430,7 +430,7 @@ builtin_grind_propagator propagateMatchCondUp ↑Grind.MatchCond := fun e => do
   else
     if !(← isStatisfied e) then return ()
     let some h ← mkMatchCondProof? e
-       | reportIssue m!"failed to construct proof for{indentExpr e}"; return ()
+       | reportIssue! "failed to construct proof for{indentExpr e}"; return ()
     trace_goal[grind.debug.matchCond] "{← inferType h}"
     pushEqTrue e <| mkEqTrueCore e h
 

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

@@ -151,10 +151,13 @@ private def ppCasesTrace : M Unit := do
     pushMsg <| .trace { cls := `cases } "Case analyses" msgs
 
 def goalToMessageData (goal : Goal) (config : Grind.Config) : MetaM MessageData := goal.mvarId.withContext do
-  let (_, m) ← go goal |>.run #[]
-  let gm := MessageData.trace { cls := `grind, collapsed := false } "Diagnostics" m
-  let r := m!"{.ofGoal goal.mvarId}\n{gm}"
-  addMessageContextFull r
+  if config.verbose then
+    let (_, m) ← go goal |>.run #[]
+    let gm := MessageData.trace { cls := `grind, collapsed := false } "Diagnostics" m
+    let r := m!"{.ofGoal goal.mvarId}\n{gm}"
+    addMessageContextFull r
+  else
+    return .ofGoal goal.mvarId
 where
   go : M Unit := do
     pushMsg <| ppExprArray `facts "Asserted facts" goal.facts.toArray `prop

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

@@ -40,7 +40,7 @@ def pushFailure (goal : Goal) : M Unit := do
     x goal
   catch ex =>
     if ex.isMaxHeartbeat || ex.isMaxRecDepth then
-      reportIssue ex.toMessageData
+      reportIssue! ex.toMessageData
       pushFailure goal
       return true
     else

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

@@ -104,7 +104,7 @@ private def checkCaseSplitStatus (e : Expr) : GoalM CaseSplitStatus := do
     if e.isFVar then
       let type ← whnfD (← inferType e)
       let report : GoalM Unit := do
-        reportIssue "cannot perform case-split on {e}, unexpected type{indentExpr type}"
+        reportIssue! "cannot perform case-split on {e}, unexpected type{indentExpr type}"
       let .const declName _ := type.getAppFn | report; return .resolved
       let .inductInfo info ← getConstInfo declName | report; return .resolved
       return .ready info.ctors.length info.isRec

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

@@ -244,6 +244,15 @@ def reportIssue (msg : MessageData) : GrindM Unit := do
   -/
   trace[grind.issues] msg
 
+private def expandReportIssueMacro (s : Syntax) : MacroM (TSyntax `doElem) := do
+  let msg ← if s.getKind == interpolatedStrKind then `(m! $(⟨s⟩)) else `(($(⟨s⟩) : MessageData))
+  `(doElem| do
+    if (← getConfig).verbose then
+      reportIssue $msg)
+
+macro "reportIssue!" s:(interpolatedStr(term) <|> term) : doElem => do
+  expandReportIssueMacro s.raw
+
 /--
 Stores information for a node in the egraph.
 Each internalized expression `e` has an `ENode` associated with it.

src/Lean/Meta/Tactic/LibrarySearch.lean

@@ -58,7 +58,7 @@ inductive DeclMod
   | /-- the original declaration -/ none
   | /-- the forward direction of an `iff` -/ mp
   | /-- the backward direction of an `iff` -/ mpr
-deriving DecidableEq, Inhabited, Ord
+deriving DecidableEq, Inhabited, Ord, Hashable
 
 /--
 LibrarySearch has an extension mechanism for replacing the function used

src/Lean/Meta/Tactic/Try.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Try.Collect
+
+namespace Lean
+
+builtin_initialize registerTraceClass `try
+builtin_initialize registerTraceClass `try.collect
+builtin_initialize registerTraceClass `try.collect.funInd
+
+builtin_initialize registerTraceClass `try.debug.funInd
+
+end Lean

src/Lean/Meta/Tactic/Try/Collect.lean

@@ -0,0 +1,210 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Try
+import Lean.Meta.Tactic.LibrarySearch
+import Lean.Meta.Tactic.Util
+import Lean.Meta.Tactic.Grind.Cases
+import Lean.Meta.Tactic.Grind.EMatchTheorem
+
+namespace Lean.Meta.Try.Collector
+
+structure InductionCandidate where
+  fvarId : FVarId
+  val    : InductiveVal
+
+structure FunIndCandidate where
+  funIndDeclName : Name
+  majors : Array FVarId
+  deriving Hashable, BEq
+
+structure Result where
+  /-- All constant symbols occurring in the gal. -/
+  allConsts : Std.HashSet Name  := {}
+  /-- Unfolding candiates. -/
+  unfoldCandidates : Std.HashSet Name  := {}
+  /-- Equation function candiates. -/
+  eqnCandidates : Std.HashSet Name  := {}
+  /-- Function induction candidates. -/
+  funIndCandidates : Std.HashSet FunIndCandidate := {}
+  /-- Induction candidates. -/
+  indCandidates : Array InductionCandidate := #[]
+  /-- Relevant declarations by `libSearch` -/
+  libSearchResults : Std.HashSet (Name × Grind.EMatchTheoremKind) := {}
+
+structure Context where
+  config : Try.Config
+
+abbrev M := ReaderT Context <| StateRefT Result MetaM
+
+def getConfig : M Try.Config := do
+  return (← read).config
+
+def saveConst (declName : Name) : M Unit := do
+  modify fun s => { s with allConsts := s.allConsts.insert declName }
+
+/-- Returns `true` if `declName` is in the module being compiled. -/
+def inCurrentModule (declName : Name) : CoreM Bool := do
+  return ((← getEnv).getModuleIdxFor? declName).isNone
+
+def getFunInductName (declName : Name) : Name :=
+  declName ++ `induct
+
+def getFunInduct? (declName : Name) : MetaM (Option Name) := do
+  let .defnInfo _ ← getConstInfo declName | return none
+  try
+    let result ← realizeGlobalConstNoOverloadCore (getFunInductName declName)
+    return some result
+  catch _ =>
+    return none
+
+def isEligible (declName : Name) : M Bool := do
+  if declName.hasMacroScopes then
+    return false
+  if (← getConfig).main then
+    return (← inCurrentModule declName)
+  if (← getConfig).name then
+    let ns ← getCurrNamespace
+    return ns.isPrefixOf declName
+  return false
+
+def saveEqnCandidate (declName : Name) : M Unit := do
+  if (← isEligible declName) then
+    let some eqns ← getEqnsFor? declName | return ()
+    if eqns.isEmpty then return ()
+    unless (← Grind.isEMatchTheorem eqns[0]!) do
+      modify fun s => { s with eqnCandidates := s.eqnCandidates.insert declName }
+
+def getEqDefDecl? (declName : Name) : MetaM (Option Name) := do
+  let declName := declName ++ `eq_def
+  if (← Grind.isEMatchTheorem declName) then return none
+  try
+    let result ← realizeGlobalConstNoOverloadCore declName
+    return some result
+  catch _ =>
+    return none
+
+def saveUnfoldCandidate (declName : Name) : M Unit := do
+  if (← isEligible declName) then
+    let some eqDefName ← getEqDefDecl? declName | return ()
+    modify fun s => { s with unfoldCandidates := s.unfoldCandidates.insert eqDefName }
+
+def visitConst (declName : Name) : M Unit := do
+  saveConst declName
+  saveUnfoldCandidate declName
+
+-- Horrible temporary hack: compute the mask assuming parameters appear before a variable named `motive`
+-- It assumes major premises appear after variables with name `case?`
+-- It assumes if something is not a parameter, then it is major :(
+-- TODO: save the mask while generating the induction principle.
+def getFunIndMask? (declName : Name) (indDeclName : Name) : MetaM (Option (Array Bool)) := do
+  let info ← getConstInfo declName
+  let indInfo ← getConstInfo indDeclName
+  let (numParams, numMajor) ← forallTelescope indInfo.type fun xs _ => do
+    let mut foundCase := false
+    let mut foundMotive := false
+    let mut numParams : Nat := 0
+    let mut numMajor : Nat := 0
+    for x in xs do
+      let localDecl ← x.fvarId!.getDecl
+      let n := localDecl.userName
+      if n == `motive then
+        foundMotive := true
+      else if !foundMotive then
+        numParams := numParams + 1
+      else if n.isStr && "case".isPrefixOf n.getString! then
+        foundCase := true
+      else if foundCase then
+        numMajor := numMajor + 1
+    return (numParams, numMajor)
+  if numMajor == 0 then return none
+  forallTelescope info.type fun xs _ => do
+    if xs.size != numParams + numMajor then
+      return none
+    return some (mkArray numParams false ++ mkArray numMajor true)
+
+def saveFunInd (_e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
+  if (← isEligible declName) then
+    let some funIndDeclName ← getFunInduct? declName
+      | saveUnfoldCandidate declName; return ()
+    let some mask ← getFunIndMask? declName funIndDeclName | return ()
+    if mask.size != args.size then return ()
+    let mut majors := #[]
+    for arg in args, isMajor in mask do
+      if isMajor then
+        if !arg.isFVar then return ()
+        majors := majors.push arg.fvarId!
+    trace[try.collect.funInd] "{funIndDeclName}, {majors.map mkFVar}"
+    modify fun s => { s with funIndCandidates := s.funIndCandidates.insert { majors, funIndDeclName }}
+
+open LibrarySearch in
+def saveLibSearchCandidates (e : Expr) : M Unit := do
+  if (← getConfig).lib then
+    for (declName, declMod) in (← libSearchFindDecls e) do
+      unless (← Grind.isEMatchTheorem declName) do
+        let kind := match declMod with
+          | .none => .default
+          | .mp => .leftRight
+          | .mpr => .rightLeft
+        modify fun s => { s with libSearchResults := s.libSearchResults.insert (declName, kind) }
+
+def visitApp (e : Expr) (declName : Name) (args : Array Expr) : M Unit := do
+  saveEqnCandidate declName
+  saveFunInd e declName args
+  saveLibSearchCandidates e
+
+def checkInductive (localDecl : LocalDecl) : M Unit := do
+  let .const declName _ ← whnfD localDecl.type | return ()
+  let .inductInfo val ← getConstInfo declName | return ()
+  if (← isEligible declName) then
+    unless (← Grind.isSplit declName) do
+      modify fun s => { s with indCandidates := s.indCandidates.push { fvarId := localDecl.fvarId, val } }
+
+unsafe abbrev Cache := PtrSet Expr
+
+unsafe def visit (e : Expr) : StateRefT Cache M Unit := do
+  unless (← get).contains e do
+    modify fun s => s.insert e
+    match e with
+      | .const declName _ => visitConst declName
+      | .forallE _ d b _  => visit d; visit b
+      | .lam _ d b _      => visit d; visit b
+      | .mdata _ b        => visit b
+      | .letE _ t v b _   => visit t; visit v; visit b
+      | .app ..           => e.withApp fun f args => do
+        if let .const declName _ := f then
+          saveConst declName
+          unless e.hasLooseBVars do
+            visitApp e declName args
+        else
+          visit f
+        args.forM visit
+      | .proj _ _ b       => visit b
+      | _                 => return ()
+
+unsafe def main (mvarId : MVarId) (config : Try.Config) : MetaM Result := mvarId.withContext do
+  let (_, s) ← go |>.run mkPtrSet |>.run { config } |>.run {}
+  return s
+where
+  go : StateRefT Cache M Unit := do
+    unless (← getConfig).targetOnly do
+      for localDecl in (← getLCtx) do
+        unless localDecl.isAuxDecl do
+          if let some val := localDecl.value? then
+            visit val
+          else
+            checkInductive localDecl
+            visit localDecl.type
+    visit (← mvarId.getType)
+
+end Collector
+
+abbrev Info := Collector.Result
+
+def collect (mvarId : MVarId) (config : Try.Config) : MetaM Info := do
+  unsafe Collector.main mvarId config
+
+end Lean.Meta.Try

tests/lean/run/grind_constProp.lean

@@ -207,6 +207,11 @@ def evalExpr (e : Expr) : EvalM Val := do
 @[grind] theorem UnaryOp.simplify_eval (op : UnaryOp) : (op.simplify a).eval σ = (Expr.una op a).eval σ := by
   grind [UnaryOp.simplify.eq_def]
 
+/-- info: Try this: (induction e using Expr.simplify.induct) <;> grind? -/
+#guard_msgs (info) in
+example (e : Expr) : e.simplify.eval σ = e.eval σ := by
+  try?
+
 @[simp, grind =] theorem Expr.eval_simplify (e : Expr) : e.simplify.eval σ = e.eval σ := by
   induction e, σ using Expr.simplify.induct <;> grind
 
@@ -293,7 +298,7 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : (
   grind
 
 @[grind] theorem State.erase_le (σ : State) : σ.erase x ≼ σ := by
-  induction σ, x using State.erase.induct <;> grind
+  grind
 
 @[grind] theorem State.join_le_left (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₁ := by
   induction σ₁, σ₂ using State.join.induct <;> grind
@@ -301,6 +306,11 @@ theorem State.cons_le_of_eq (h₁ : σ' ≼ σ) (h₂ : σ.find? x = some v) : (
 @[grind] theorem State.join_le_left_of (h : σ₁ ≼ σ₂) (σ₃ : State) : σ₁.join σ₃ ≼ σ₂ := by
   grind
 
+/-- info: Try this: (induction σ₁, σ₂ using State.join.induct) <;> grind? -/
+#guard_msgs (info) in
+example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
+  try?
+
 @[grind] theorem State.join_le_right (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
   induction σ₁, σ₂ using State.join.induct <;> grind
 

tests/lean/run/grind_t1.lean

@@ -259,6 +259,19 @@ set_option trace.grind.split true in
 example (p q : Prop) : (p ↔ q) → p → False := by
   grind -- should not split on (p ↔ q)
 
+/--
+error: `grind` failed
+case grind
+p q : Prop
+a✝¹ : p = q
+a✝ : p
+⊢ False
+-/
+#guard_msgs (error) in
+example (p q : Prop) : (p ↔ q) → p → False := by
+  grind -verbose -- We should not get any diagnostics
+
+
 /--
 error: `grind` failed
 case grind

tests/lean/run/prelude-injectivity.lean

@@ -19,6 +19,7 @@ gen_injective_theorems% Macro.State
 gen_injective_theorems% Syntax.Preresolved
 gen_injective_theorems% Syntax.SepArray
 gen_injective_theorems% Syntax.TSepArray
+gen_injective_theorems% Try.Config
 gen_injective_theorems% Parser.Tactic.DecideConfig
 -/
 #guard_msgs in

tests/lean/run/try_trace1.lean

@@ -0,0 +1,44 @@
+set_option grind.warning false
+
+/-- info: Try this: simp -/
+#guard_msgs (info) in
+example : [1, 2] ≠ [] := by
+  try?
+
+/-- info: Try this: simp +arith -/
+#guard_msgs (info) in
+example : 4 + x + y ≥ 1 + x  := by
+  try?
+
+/-- info: Try this: grind? -/
+#guard_msgs (info) in
+example (f : Nat → Nat) : f a = b → a = c → f c = b := by
+  try?
+
+def f : Nat → Nat
+  | 0 => 1
+  | _ => 2
+
+/-- info: Try this: grind? [= f] -/
+#guard_msgs (info) in
+example : f (f 0) > 0 := by
+  try?
+
+/-- info: Try this: grind? [= f.eq_def] -/
+#guard_msgs (info) in
+example : f x > 0 := by
+  try?
+
+def app : List α → List α → List α
+  | [], bs => bs
+  | a::as, bs => a :: app as bs
+
+/-- info: Try this: grind? [= app] -/
+#guard_msgs (info) in
+example : app [a, b] [c] = [a, b, c] := by
+  try?
+
+/-- info: Try this: (induction as, bs using app.induct) <;> grind? [= app] -/
+#guard_msgs (info) in
+example : app (app as bs) cs = app as (app bs cs) := by
+  try?