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

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