tests for simp_all

Author: kim-em

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

@@ -22,9 +22,9 @@ namespace Lean.Elab.Tactic
 open Lean Elab Parser Tactic Meta Simp Tactic.TryThis
 
 /-- Filter out `+suggestions` from the config syntax -/
-def filterSuggestionsFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig) : MetaM (TSyntax ``Lean.Parser.Tactic.optConfig) := do
+def filterSuggestionsFromConfig (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 := config.raw.getArg 0
+  let nullNode := cfg.raw.getArg 0
   let configItems := nullNode.getArgs
 
   -- Filter out configItem nodes that contain +suggestions
@@ -38,7 +38,7 @@ def filterSuggestionsFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig
 
   -- Reconstruct the config with filtered items
   let newNullNode := nullNode.setArgs filteredItems
-  return ⟨config.raw.setArg 0 newNullNode⟩
+  return ⟨cfg.raw.setArg 0 newNullNode⟩
 
 open TSyntax.Compat in
 /-- Constructs the syntax for a simp call, for use with `simp?`. -/
@@ -85,18 +85,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.PremiseSelection.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 ← filterSuggestionsFromConfig 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

@@ -23,3 +23,39 @@ info: Try this:
 #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