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

fix: grind? dropping options (#11481)

Browse source 
This PR fixes a bug in `grind?`. The suggestion using the `grind`
interactive mode was dropping the configuration options provided by the
user. In the following account, the third suggestion was dropping the
`-reducible` option.

```lean
/--
info: Try these:
  [apply] grind -reducible only [Equiv.congr_fun, #5103]
  [apply] grind -reducible only [Equiv.congr_fun]
  [apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
-/
example :
    (Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
    = (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
  grind? -reducible [Equiv.congr_fun]
```
This commit is contained in:
Leonardo de Moura 2025-12-02 11:00:29 -08:00 • committed by GitHub
parent 9263a6cc9c
commit f8866dcc59
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -342,10 +342,10 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
-- let saved ← saveState
match (← finish.run goal) with
| .closed seq =>
let configCtx' := filterSuggestionsFromGrindConfig configStx
let tacs ← Grind.mkGrindOnlyTactics configCtx' seq
let configStx' := filterSuggestionsFromGrindConfig configStx
let tacs ← Grind.mkGrindOnlyTactics configStx' seq
let seq := Grind.Action.mkGrindSeq seq
let tac ← `(tactic| grind => $seq:grindSeq)
let tac ← `(tactic| grind $configStx':optConfig => $seq:grindSeq)
let tacs := tacs.push tac
return tacs
| .stuck gs =>

12
tests/lean/run/grind_reducible.lean
View file

@ -48,3 +48,15 @@ example :
(Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
= (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
/--
info: Try these:
[apply] grind -reducible only [Equiv.congr_fun, #5103]
[apply] grind -reducible only [Equiv.congr_fun]
[apply] grind -reducible => cases #5103 <;> instantiate only [Equiv.congr_fun]
-/
#guard_msgs in
example :
(Equiv.sigmaCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂)
= (Equiv.sigmaEquivProd α₁ β₁).trans (prodCongrRight e) := by
grind? -reducible [Equiv.congr_fun]