feat: try? tactic (#6905)

This PR adds the `try?` tactic. This is the first draft, but it can
already solve examples such as:
```lean
example (e : Expr) : e.simplify.eval σ = e.eval σ := by
  try?
```
in `grind_constProp.lean`. In the example above, it suggests:
```lean
induction e using Expr.simplify.induct <;> grind?
``` 
In the same test file, we have
```lean
example (σ₁ σ₂ : State) : σ₁.join σ₂ ≼ σ₂ := by
  try?
```
and the following suggestion is produced
```lean
induction σ₁, σ₂ using State.join.induct <;> grind? 
```

src/Init.lean

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

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/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/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/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