fix

src/Init/MetaTypes.lean

@@ -290,6 +290,11 @@ structure Config where
   When `true` (default: `true`), the `^` simprocs generate an warning it the exponents are too big.
   -/
   warnExponents : Bool := true
+  /--
+  If `suggestions` is `true`, `simp?` will invoke the currently configured library suggestion engine on the current goal,
+  and attempt to use the resulting suggestions as parameters to the `simp` tactic.
+  -/
+  suggestions : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

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

@@ -205,7 +205,8 @@ def getGrindParams (stx : TSyntax `tactic) : Array Syntax :=
   stx.raw[grindParamsPos][1].getSepArgs
 
 /-- Filter out `+suggestions` from the config syntax -/
-def filterSuggestionsFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : TSyntax ``Lean.Parser.Tactic.optConfig :=
+def filterSuggestionsFromGrindConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) :
+    TSyntax ``Lean.Parser.Tactic.optConfig :=
   let configItems := config.raw.getArgs
   let filteredItems := configItems.filter fun item =>
     -- Keep all items except +suggestions
@@ -236,7 +237,7 @@ def mkGrindOnly
       else
         let param ← Grind.globalDeclToGrindParamSyntax declName kind minIndexable
         params := params.push param
-  let filteredConfig := filterSuggestionsFromConfig config
+  let filteredConfig := filterSuggestionsFromGrindConfig config
   let result ← `(tactic| grind $filteredConfig:optConfig only)
   return setGrindParams result params
 
@@ -274,7 +275,7 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
       -- let saved ← saveState
       match (← finish.run goal) with
       | .closed seq =>
-        let configCtx' := filterSuggestionsFromConfig configStx
+        let configCtx' := filterSuggestionsFromGrindConfig configStx
         let tacs ← Grind.mkGrindOnlyTactics configCtx' seq
         let seq := Grind.Action.mkGrindSeq seq
         let tac ← `(tactic| grind => $seq:grindSeq)

src/Lean/Elab/Tactic/Simp.lean

@@ -657,6 +657,8 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
 -/
 @[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let r@{ ctx, simprocs, dischargeWrapper, simpArgs } ← mkSimpContext stx (eraseLocal := false)
+  if ctx.config.suggestions then
+    throwError "+suggestions requires using simp? instead of simp"
   let stats ← dischargeWrapper.with fun discharge? =>
     withLoopChecking r do
       simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
@@ -669,6 +671,8 @@ def withSimpDiagnostics (x : TacticM Simp.Diagnostics) : TacticM Unit := do
 
 @[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   let r@{ ctx, simprocs, dischargeWrapper := _, simpArgs } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true)
+  if ctx.config.suggestions then
+    throwError "+suggestions requires using simp_all? instead of simp_all"
   let (result?, stats) ←
     withLoopChecking r do
       simpAll (← getMainGoal) ctx (simprocs := simprocs)

src/Lean/Elab/Tactic/SimpTrace.lean

@@ -9,6 +9,7 @@ prelude
 public import Lean.Elab.ElabRules
 public import Lean.Elab.Tactic.Simp
 public import Lean.Meta.Tactic.TryThis
+public import Lean.LibrarySuggestions.Basic
 
 public section
 
@@ -20,6 +21,26 @@ The `simp?` tactic is a simple wrapper around the simp with trace behavior.
 namespace Lean.Elab.Tactic
 open Lean Elab Parser Tactic Meta Simp Tactic.TryThis
 
+/-- Filter out `+suggestions` from the config syntax -/
+def filterSuggestionsFromSimpConfig (cfg : TSyntax ``Lean.Parser.Tactic.optConfig) :
+    MetaM (TSyntax ``Lean.Parser.Tactic.optConfig) := do
+  -- The config has one arg: a null node containing configItem nodes
+  let nullNode := cfg.raw.getArg 0
+  let configItems := nullNode.getArgs
+
+  -- Filter out configItem nodes that contain +suggestions
+  let filteredItems := configItems.filter fun item =>
+    match item[0]?, item.getKind with
+    | some posConfigItem, ``Lean.Parser.Tactic.configItem =>
+      match posConfigItem[1]?, posConfigItem.getKind with
+      | some ident, ``Lean.Parser.Tactic.posConfigItem => ident.getId != `suggestions
+      | _, _ => true
+    | _, _ => true
+
+  -- Reconstruct the config with filtered items
+  let newNullNode := nullNode.setArgs filteredItems
+  return ⟨cfg.raw.setArg 0 newNullNode⟩
+
 open TSyntax.Compat in
 /-- Constructs the syntax for a simp call, for use with `simp?`. -/
 def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tactic) := do
@@ -30,16 +51,34 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
   match stx with
   | `(tactic|
       simp?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?) =>
-    let stx ← if bang.isSome then
-      `(tactic| simp!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]? $(loc)?)
+    -- Check if premise selection is enabled
+    let config ← elabSimpConfig cfg (kind := .simp)
+    let mut argsArray : TSyntaxArray [`Lean.Parser.Tactic.simpStar, `Lean.Parser.Tactic.simpErase, `Lean.Parser.Tactic.simpLemma] :=
+      if let some a := args then a.getElems else #[]
+    if config.suggestions then
+      -- Get premise suggestions from the premise selector
+      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal)
+      -- Convert suggestions to simp argument syntax and add them to the args
+      for sugg in suggestions do
+        let arg ← `(Parser.Tactic.simpLemma| $(mkIdent sugg.name):term)
+        argsArray := argsArray.push arg
+    -- Build the simp syntax with the updated arguments
+    let stxForExecution ← if bang.isSome then
+      `(tactic| simp!%$tk $cfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*] $[$loc]?)
     else
-      `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]? $(loc)?)
-    let { ctx, simprocs, dischargeWrapper, ..} ← mkSimpContext stx (eraseLocal := false)
+      `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*] $[$loc]?)
+    -- Build syntax for suggestion (without +suggestions config)
+    let filteredCfg ← filterSuggestionsFromSimpConfig cfg
+    let stxForSuggestion ← if bang.isSome then
+      `(tactic| simp!%$tk $filteredCfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*] $[$loc]?)
+    else
+      `(tactic| simp%$tk $filteredCfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*] $[$loc]?)
+    let { ctx, simprocs, dischargeWrapper, ..} ← mkSimpContext stxForExecution (eraseLocal := false)
     let ctx := if bang.isSome then ctx.setAutoUnfold else ctx
     let stats ← dischargeWrapper.with fun discharge? =>
       simpLocation ctx (simprocs := simprocs) discharge? <|
         (loc.map expandLocation).getD (.targets #[] true)
-    let stx ← mkSimpCallStx stx stats.usedTheorems
+    let stx ← mkSimpCallStx stxForSuggestion stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
     return stats.diag
   | _ => throwUnsupportedSyntax
@@ -47,18 +86,50 @@ def mkSimpCallStx (stx : Syntax) (usedSimps : UsedSimps) : MetaM (TSyntax `tacti
 @[builtin_tactic simpAllTrace] def evalSimpAllTrace : Tactic := fun stx => withMainContext do withSimpDiagnostics do
   match stx with
   | `(tactic| simp_all?%$tk $[!%$bang]? $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) =>
-    let stx ← if bang.isSome then
-      `(tactic| simp_all!%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
-    else
-      `(tactic| simp_all%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?)
-    let { ctx, simprocs, .. } ← mkSimpContext stx (eraseLocal := true)
+    -- Check if premise selection is enabled
+    let config ← elabSimpConfig cfg (kind := .simpAll)
+    let mut argsArray : TSyntaxArray [`Lean.Parser.Tactic.simpErase, `Lean.Parser.Tactic.simpLemma] :=
+      if let some a := args then a.getElems else #[]
+    if config.suggestions then
+      -- Get premise suggestions from the premise selector
+      let suggestions ← Lean.LibrarySuggestions.select (← getMainGoal)
+      -- Convert suggestions to simp argument syntax and add them to the args
+      for sugg in suggestions do
+        let arg ← `(Parser.Tactic.simpLemma| $(mkIdent sugg.name):term)
+        argsArray := argsArray.push arg
+    -- Build the simp_all syntax with the updated arguments
+    let stxForExecution ←
+      if argsArray.isEmpty then
+        if bang.isSome then
+          `(tactic| simp_all!%$tk $cfg:optConfig $[$discharger]? $[only%$o]?)
+        else
+          `(tactic| simp_all%$tk $cfg:optConfig $[$discharger]? $[only%$o]?)
+      else
+        if bang.isSome then
+          `(tactic| simp_all!%$tk $cfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*])
+        else
+          `(tactic| simp_all%$tk $cfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*])
+    -- Build syntax for suggestion (without +suggestions config)
+    let filteredCfg ← filterSuggestionsFromSimpConfig cfg
+    let stxForSuggestion ←
+      if argsArray.isEmpty then
+        if bang.isSome then
+          `(tactic| simp_all!%$tk $filteredCfg:optConfig $[$discharger]? $[only%$o]?)
+        else
+          `(tactic| simp_all%$tk $filteredCfg:optConfig $[$discharger]? $[only%$o]?)
+      else
+        if bang.isSome then
+          `(tactic| simp_all!%$tk $filteredCfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*])
+        else
+          `(tactic| simp_all%$tk $filteredCfg:optConfig $[$discharger]? $[only%$o]? [$argsArray,*])
+    let { ctx, simprocs, .. } ← mkSimpContext stxForExecution (eraseLocal := true)
       (kind := .simpAll) (ignoreStarArg := true)
     let ctx := if bang.isSome then ctx.setAutoUnfold else ctx
     let (result?, stats) ← simpAll (← getMainGoal) ctx (simprocs := simprocs)
     match result? with
     | none => replaceMainGoal []
     | some mvarId => replaceMainGoal [mvarId]
-    let stx ← mkSimpCallStx stx stats.usedTheorems
+    let stx ← mkSimpCallStx stxForSuggestion stats.usedTheorems
     addSuggestion tk stx (origSpan? := ← getRef)
     return stats.diag
   | _ => throwUnsupportedSyntax

tests/lean/run/simp_suggestions.lean

@@ -0,0 +1,61 @@
+import Lean.LibrarySuggestions
+
+-- A custom function that simp doesn't know about
+def myCustomAdd (x y : Nat) : Nat := x + y
+
+-- A helper lemma about our custom function
+theorem myCustomAdd_comm (x y : Nat) : myCustomAdd x y = myCustomAdd y x := by
+  simp [myCustomAdd, Nat.add_comm]
+
+-- Set up a premise selector that suggests our helper theorem
+set_library_suggestions (fun _ _ => pure #[{ name := `myCustomAdd_comm, score := 1.0 }])
+
+-- Test that regular simp? fails without the premise
+example (a b : Nat) : myCustomAdd a b = myCustomAdd b a := by
+  fail_if_success simp?
+  exact myCustomAdd_comm a b
+
+-- Test that simp? +suggestions succeeds by using the selected premise
+/--
+info: Try this:
+  [apply] simp only [myCustomAdd_comm]
+-/
+#guard_msgs in
+example (a b : Nat) : myCustomAdd a b = myCustomAdd b a := by
+  simp? +suggestions
+
+-- Test that simp +suggestions (without ?) gives a helpful error
+/--
+error: +suggestions requires using simp? instead of simp
+-/
+#guard_msgs in
+example (a b : Nat) : myCustomAdd a b = myCustomAdd b a := by
+  simp +suggestions
+  sorry
+
+-- Test that simp_all? +suggestions works on the goal
+/--
+info: Try this:
+  [apply] simp_all only [myCustomAdd_comm]
+-/
+#guard_msgs in
+example (a b : Nat) : myCustomAdd a b = myCustomAdd b a := by
+  simp_all? +suggestions
+
+-- Test that simp_all? +suggestions works on a hypothesis
+/--
+info: Try this:
+  [apply] simp_all only [myCustomAdd_comm]
+-/
+#guard_msgs in
+example (a b c : Nat) (h : myCustomAdd a b = c) : myCustomAdd b a = c := by
+  simp_all? +suggestions
+
+-- Test that simp_all +suggestions (without ?) gives a helpful error
+/--
+error: +suggestions requires using simp_all? instead of simp_all
+-/
+#guard_msgs in
+example (a b : Nat) (h : myCustomAdd a b = myCustomAdd b a) : myCustomAdd a b = myCustomAdd b a := by
+  simp_all +suggestions
+  sorry