From 02b141ca151dea20b2fe3dffe61e4d60c1095d3b Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Tue, 11 Nov 2025 17:38:28 +1100 Subject: [PATCH] feat: add library suggestions support to `try?` tactic (#11132) This PR adds support for `grind +suggestions` and `simp_all? +suggestions` in `try?`. It outputs `grind only [X, Y, Z]` or `simp_all only [X, Y, Z]` suggestions (rather than just `+suggestions`). Co-authored-by: Claude --- src/Lean/Elab/Tactic/Try.lean | 89 +++++++++++++++++++-- tests/lean/run/try_library_suggestions.lean | 89 +++++++++++++++++++++ 2 files changed, 173 insertions(+), 5 deletions(-) create mode 100644 tests/lean/run/try_library_suggestions.lean diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index 7b7959af76..2e8adfc06f 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -197,6 +197,18 @@ private def evalSuggestAtomic (tac : TSyntax `tactic) : TacticM (TSyntax `tactic else return tac +/-- Check if a config contains `+suggestions` -/ +private def configHasSuggestions (config : TSyntax ``Lean.Parser.Tactic.optConfig) : Bool := + let configItems := config.raw.getArgs + configItems.any fun item => + match item[0]? with + | some configItem => match configItem[0]? with + | some posConfigItem => match posConfigItem[1]? with + | some ident => posConfigItem.getKind == ``Lean.Parser.Tactic.posConfigItem && ident.getId == `suggestions + | none => false + | none => false + | none => false + private def grindTraceToGrind (tac : TSyntax `tactic) : TacticM (TSyntax `tactic) := do match tac with | `(tactic| grind? $config:optConfig $[only%$only]? $[ [$params:grindParam,*] ]?) => @@ -389,25 +401,85 @@ private def evalSuggestGrindTrace : TryTactic := fun tac => do trace[try.debug] "`grind` succeeded" if (← read).config.only then let tac' ← mkGrindOnly configStx trace - mkTrySuggestions #[tac, tac'] + -- If config has +suggestions, only return the 'only' version, not the original + if configHasSuggestions configStx then + mkTrySuggestions #[tac'] + else + mkTrySuggestions #[tac, tac'] else return tac | _ => throwUnsupportedSyntax private def evalSuggestSimpTrace : TryTactic := fun tac => do (← getMainGoal).withContext do match tac with - | `(tactic| simp? $_:optConfig $[only%$only]? $[[$args,*]]? $(loc)?) => + | `(tactic| simp? $configStx:optConfig $[only%$only]? $[[$args,*]]? $(loc)?) => let tac ← simpTraceToSimp tac let { ctx, simprocs, .. } ← mkSimpContext tac (eraseLocal := false) let stats ← simpLocation ctx (simprocs := simprocs) none <| (loc.map expandLocation).getD (.targets #[] true) trace[try.debug] "`simp` succeeded" if (← read).config.only then let tac' ← mkSimpCallStx tac stats.usedTheorems - mkTrySuggestions #[tac, tac'] + -- If config has +suggestions, only return the 'only' version, not the original + if configHasSuggestions configStx then + mkTrySuggestions #[tac'] + else + mkTrySuggestions #[tac, tac'] else return tac | _ => throwUnsupportedSyntax +private def evalSuggestSimpAllTrace : TryTactic := fun tac => do + match tac with + | `(tactic| simp_all? $[!%$_bang]? $configStx:optConfig $(_discharger)? $[only%$_only]? $[[$_args,*]]?) => + (← getMainGoal).withContext do + let hasSuggestions := configHasSuggestions configStx + + -- Get library suggestions if +suggestions is present + let config ← elabSimpConfig configStx (kind := .simpAll) + let mut argsArray : TSyntaxArray [`Lean.Parser.Tactic.simpErase, `Lean.Parser.Tactic.simpLemma] := #[] + if config.suggestions then + let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal) + for sugg in suggestions do + let ident := mkIdent sugg.name + let candidates ← resolveGlobalConst ident + for candidate in candidates do + let arg ← `(Parser.Tactic.simpLemma| $(mkCIdentFrom ident candidate (canonical := true)):term) + argsArray := argsArray.push arg + + -- Build tactic with resolved suggestions for execution + -- If +suggestions was present, we need to create a tactic without +suggestions, + -- either with the resolved suggestions or without arguments if none were found + -- Note: We use simp_all (without ?) for execution, not simp_all? + let tacForExec ← if config.suggestions then + if argsArray.isEmpty then + `(tactic| simp_all) + else + `(tactic| simp_all [$argsArray,*]) + else + pure tac + + let { ctx, simprocs, .. } ← mkSimpContext tacForExec (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true) + let (result?, stats) ← simpAll (← getMainGoal) ctx (simprocs := simprocs) + match result? with + | none => replaceMainGoal [] + | some mvarId => replaceMainGoal [mvarId] + trace[try.debug] "`simp_all` succeeded" + if (← read).config.only then + -- Remove +suggestions from config for the output (similar to SimpTrace.lean) + let filteredCfg ← filterSuggestionsFromSimpConfig configStx + -- Convert simp_all? to simp_all for mkSimpCallStx (similar to simpTraceToSimp) + let tacWithoutTrace ← `(tactic| simp_all $filteredCfg:optConfig $[only%$_only]? $[[$_args,*]]?) + let tac' ← mkSimpCallStx tacWithoutTrace stats.usedTheorems + -- If config has +suggestions, only return the 'only' version, not the original + if hasSuggestions then + mkTrySuggestions #[tac'] + else + mkTrySuggestions #[tac, tac'] + else + return tac + | _ => throwUnsupportedSyntax + + @[extern "lean_eval_suggest_tactic"] -- forward definition to avoid mutual block opaque evalSuggest : TryTactic @@ -547,6 +619,8 @@ private partial def evalSuggestImpl : TryTactic := fun tac => do evalSuggestGrindTrace tac else if k == ``Parser.Tactic.simpTrace then evalSuggestSimpTrace tac + else if k == ``Parser.Tactic.simpAllTrace then + evalSuggestSimpAllTrace tac else if k == ``Parser.Tactic.exact? then evalSuggestExact else @@ -629,6 +703,11 @@ set_option hygiene false in -- Avoid tagger at `+arith` private def mkSimpStx : CoreM (TSyntax `tactic) := `(tactic| first | simp? | simp? [*] | simp? +arith | simp? +arith [*]) +set_option hygiene false in -- Avoid tagger at `+suggestions` +/-- Atomic tactics with library suggestions -/ +private def mkAtomicWithSuggestionsStx : CoreM (TSyntax `tactic) := + `(tactic| attempt_all | grind? +suggestions | simp_all? +suggestions) + /-- `simple` tactics -/ private def mkSimpleTacStx : CoreM (TSyntax `tactic) := `(tactic| attempt_all | rfl | assumption) @@ -668,13 +747,13 @@ private def mkTryEvalSuggestStx (info : Try.Info) : MetaM (TSyntax `tactic) := d let simp ← mkSimpStx let grind ← mkGrindStx info let atomic ← `(tactic| attempt_all | $simple:tactic | $simp:tactic | $grind:tactic | simp_all) + let atomicSuggestions ← mkAtomicWithSuggestionsStx let funInds ← mkAllFunIndStx info atomic let extra ← `(tactic| (intros; first | $simple:tactic | $simp:tactic | exact?)) - `(tactic| first | $atomic:tactic | $funInds:tactic | $extra:tactic) + `(tactic| first | $atomic:tactic | $atomicSuggestions:tactic | $funInds:tactic | $extra:tactic) -- TODO: vanilla `induction`. -- TODO: make it extensible. --- TODO: library suggestions. @[builtin_tactic Lean.Parser.Tactic.tryTrace] def evalTryTrace : Tactic := fun stx => do match stx with diff --git a/tests/lean/run/try_library_suggestions.lean b/tests/lean/run/try_library_suggestions.lean new file mode 100644 index 0000000000..5fadf8029a --- /dev/null +++ b/tests/lean/run/try_library_suggestions.lean @@ -0,0 +1,89 @@ +import Lean.LibrarySuggestions + +-- Test that try? can find solutions using grind? +suggestions and simp_all? +suggestions + +-- Test 1: Regular tactics should be tried first (rfl should win) +/-- +info: Try these: + [apply] rfl + [apply] simp + [apply] simp only + [apply] grind + [apply] grind only + [apply] simp_all +-/ +#guard_msgs in +example : 5 = 5 := by + try? + +-- Test 2: A theorem that requires library suggestions +-- Define an opaque constant so grind can't unfold it +axiom SpecialProperty : Nat → Prop + +-- A specific instance that's provable +axiom special_7 : SpecialProperty 7 + +-- Set up a premise selector that suggests special_7 +set_library_suggestions (fun _ _ => pure #[{ name := `special_7, score := 1.0 }]) + +-- Expected: try? should find grind only [special_7] and simp_all only [special_7] +/-- +info: Try these: + [apply] grind only [special_7] + [apply] simp_all only [special_7] +-/ +#guard_msgs in +example : SpecialProperty 7 := by + try? + +-- Test 3: For simp_all testing, use an axiom-based approach +axiom CustomOp : Nat → Nat → Nat + +-- A property about CustomOp that can't be proven by unfolding +axiom custom_comm : ∀ x y, CustomOp x y = CustomOp y x + +-- Set up a premise selector that suggests custom_comm +set_library_suggestions (fun _ _ => pure #[{ name := `custom_comm, score := 1.0 }]) + +-- Expected: try? should find grind only [custom_comm] and simp_all only [custom_comm] +/-- +info: Try these: + [apply] grind only [custom_comm] + [apply] simp_all only [custom_comm] +-/ +#guard_msgs in +example (a b : Nat) : CustomOp a b = CustomOp b a := by + try? + +-- Test 4: With a hypothesis that needs library suggestions +/-- +info: Try these: + [apply] grind only [custom_comm] + [apply] simp_all only [custom_comm] +-/ +#guard_msgs in +example (a b c : Nat) (h : CustomOp a b = c) : CustomOp b a = c := by + try? + +-- Test 5: Multiple library suggestions with grind +axiom Property1 : Nat → Prop +axiom Property2 : Nat → Prop + +axiom prop1_5 : Property1 5 +axiom prop2_5 : Property2 5 + +-- Set up a premise selector with multiple suggestions +set_library_suggestions (fun _ _ => pure #[ + { name := `prop1_5, score := 0.9 }, + { name := `prop2_5, score := 0.7 } +]) + +-- Expected: try? should use the best applicable one +/-- +info: Try these: + [apply] grind only [prop1_5] + [apply] simp_all only [prop1_5] +-/ +#guard_msgs in +example : Property1 5 := by + try?