max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: simp? +suggestions (#11032)

Browse source 
This PR implements `simp? +suggestions`, which uses the configured
library suggestion engine to add relevant theorems to the `simp` call.
`simp +suggestions` without the `?` prints a message requiring adding
the `?`.
This commit is contained in:
Kim Morrison 2025-11-03 14:26:16 +11:00 • committed by GitHub
parent e05b0e097c
commit b8bd91d92b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 156 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/MetaTypes.lean
View file

@ -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`

7
src/Lean/Elab/Tactic/Grind/Main.lean
View file

@ -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)

4
src/Lean/Elab/Tactic/Simp.lean
View file

@ -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)

93
src/Lean/Elab/Tactic/SimpTrace.lean
View file

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

61
tests/lean/run/simp_suggestions.lean Normal file
View file

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