Skip to content

Commit 78ab60d

Browse files
leodemouraleodemoura
authored
feat: cases? tactic for grind interactive mode (#10824)
This PR implements the `cases?` tactic for the `grind` interactive mode. It provides a convenient way to select anchors. Users can filter the candidates using the filter language. Examples: <img width="1454" height="399" alt="image" src="https://github.com/user-attachments/assets/fc370c2e-97f9-4d68-93a6-f0ebf33499f8" /> <img width="1447" height="166" alt="image" src="https://github.com/user-attachments/assets/6c9c3707-79f7-4c63-8007-8d0aaedecc45" />
1 parent f9adafe commit 78ab60d

File tree

8 files changed

+309
-224
lines changed

8 files changed

+309
-224
lines changed

‎src/Init/Grind/Interactive.lean‎

Lines changed: 27 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -50,46 +50,48 @@ syntax thm := anchor <|> grindLemma <|> grindLemmaMin
5050
/-- Instantiates theorems using E-matching. -/
5151
syntax (name := instantiate) "instantiate" (colGt thm),* : grind
5252

53-
declare_syntax_cat show_filter (behavior := both)
54-
55-
syntax:max ident : show_filter
56-
syntax:max &"gen" " < " num : show_filter
57-
syntax:max &"gen" " = " num : show_filter
58-
syntax:max &"gen" " != " num : show_filter
59-
syntax:max &"gen" " ≤ " num : show_filter
60-
syntax:max &"gen" " <= " num : show_filter
61-
syntax:max &"gen" " > " num : show_filter
62-
syntax:max &"gen" " ≥ " num : show_filter
63-
syntax:max &"gen" " >= " num : show_filter
64-
syntax:max "(" show_filter ")" : show_filter
65-
syntax:35 show_filter:35 " && " show_filter:36 : show_filter
66-
syntax:35 show_filter:35 " || " show_filter:36 : show_filter
67-
syntax:max "!" show_filter:40 : show_filter
68-
69-
syntax showFilter := (colGt show_filter)?
53+
declare_syntax_cat grind_filter (behavior := both)
54+
55+
syntax:max ident : grind_filter
56+
syntax:max &"gen" " < " num : grind_filter
57+
syntax:max &"gen" " = " num : grind_filter
58+
syntax:max &"gen" " != " num : grind_filter
59+
syntax:max &"gen" " ≤ " num : grind_filter
60+
syntax:max &"gen" " <= " num : grind_filter
61+
syntax:max &"gen" " > " num : grind_filter
62+
syntax:max &"gen" " ≥ " num : grind_filter
63+
syntax:max &"gen" " >= " num : grind_filter
64+
syntax:max "(" grind_filter ")" : grind_filter
65+
syntax:35 grind_filter:35 " && " grind_filter:36 : grind_filter
66+
syntax:35 grind_filter:35 " || " grind_filter:36 : grind_filter
67+
syntax:max "!" grind_filter:40 : grind_filter
68+
69+
syntax grindFilter := (colGt grind_filter)?
7070

7171
-- **Note**: Should we rename the following tactics to `trace_`?
7272
/-- Shows asserted facts. -/
73-
syntax (name := showAsserted) "show_asserted" ppSpace showFilter : grind
73+
syntax (name := showAsserted) "show_asserted" ppSpace grindFilter : grind
7474
/-- Shows propositions known to be `True`. -/
75-
syntax (name := showTrue) "show_true" ppSpace showFilter : grind
75+
syntax (name := showTrue) "show_true" ppSpace grindFilter : grind
7676
/-- Shows propositions known to be `False`. -/
77-
syntax (name := showFalse) "show_false" ppSpace showFilter : grind
77+
syntax (name := showFalse) "show_false" ppSpace grindFilter : grind
7878
/-- Shows equivalence classes of terms. -/
79-
syntax (name := showEqcs) "show_eqcs" ppSpace showFilter : grind
79+
syntax (name := showEqcs) "show_eqcs" ppSpace grindFilter : grind
8080
/-- Show case-split candidates. -/
81-
syntax (name := showSplits) "show_splits" ppSpace showFilter : grind
81+
syntax (name := showCases) "show_cases" ppSpace grindFilter : grind
8282
/-- Show `grind` state. -/
83-
syntax (name := «showState») "show_state" ppSpace showFilter : grind
83+
syntax (name := «showState») "show_state" ppSpace grindFilter : grind
8484
/-- Show active local theorems and their anchors for heuristic instantiation. -/
85-
syntax (name := showThms) "show_thms" : grind
85+
syntax (name := showLocalThms) "show_local_thms" : grind
8686

8787
declare_syntax_cat grind_ref (behavior := both)
8888

8989
syntax:max anchor : grind_ref
9090
syntax term : grind_ref
9191

92-
syntax (name := cases) "cases " grind_ref (" with " (colGt ident)+)? : grind
92+
syntax (name := cases) "cases " grind_ref : grind
93+
94+
syntax (name := casesTrace) "cases?" grindFilter : grind
9395

9496
/-- `done` succeeds iff there are no remaining goals. -/
9597
syntax (name := done) "done" : grind

‎src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean‎

Lines changed: 73 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
66
module
77
prelude
88
public import Lean.Elab.Tactic.Grind.Basic
9+
import Lean.Meta.Tactic.TryThis
910
import Lean.Meta.Tactic.Grind.Solve
1011
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Search
1112
import Lean.Meta.Tactic.Grind.Arith.Linear.Search
@@ -22,6 +23,7 @@ import Lean.Meta.Tactic.Grind.AC.PP
2223
import Lean.Meta.Tactic.ExposeNames
2324
import Lean.Elab.Tactic.Basic
2425
import Lean.Elab.Tactic.RenameInaccessibles
26+
import Lean.Elab.Tactic.Grind.Filter
2527
namespace Lean.Elab.Tactic.Grind
2628

2729
def evalSepTactics (stx : Syntax) : GrindTacticM Unit := do
@@ -126,17 +128,15 @@ def elabAnchor (anchor : TSyntax `hexnum) : CoreM (Nat × UInt64) := do
126128
return (numDigits, val)
127129

128130
@[builtin_grind_tactic instantiate] def evalInstantiate : GrindTactic := fun stx => withMainContext do
129-
match stx with
130-
| `(grind| instantiate $[$thmRefs:thm],*) =>
131-
let mut thms := #[]
132-
for thmRef in thmRefs do
133-
match thmRef with
134-
| `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
135-
| `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
136-
| `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)
137-
| _ => throwErrorAt thmRef "unexpected theorem reference"
138-
ematchThms thms
139-
| _ => throwUnsupportedSyntax
131+
let `(grind| instantiate $[$thmRefs:thm],*) := stx | throwUnsupportedSyntax
132+
let mut thms := #[]
133+
for thmRef in thmRefs do
134+
match thmRef with
135+
| `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
136+
| `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
137+
| `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)
138+
| _ => throwErrorAt thmRef "unexpected theorem reference"
139+
ematchThms thms
140140
where
141141
collectThms (numDigits : Nat) (anchorPrefix : UInt64) (thms : PArray EMatchTheorem) : StateT (Array EMatchTheorem) GrindTacticM Unit := do
142142
let mut found : Std.HashSet Expr := {}
@@ -248,31 +248,47 @@ def logAnchor (numDigits : Nat) (anchorPrefix : UInt64) (e : Expr) : TermElabM U
248248
m!"#{anchorToString numDigits anchorPrefix} := {e}"
249249

250250
@[builtin_grind_tactic cases] def evalCases : GrindTactic := fun stx => do
251-
match stx with
252-
| `(grind| cases #$anchor:hexnum) =>
253-
let (numDigits, val) ← elabAnchor anchor
254-
let goal ← getMainGoal
255-
let candidates := goal.split.candidates
256-
let (e, goals, genNew) ← liftSearchM do
257-
for c in candidates do
258-
let e := c.getExpr
259-
let anchor ← getAnchor c.getExpr
260-
if isAnchorPrefix numDigits val anchor then
261-
let some result ← split? c
262-
| throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}"
263-
return (e, result)
264-
throwError "`cases` tactic failed, invalid anchor"
265-
goal.withContext <| withRef anchor <| logAnchor numDigits val e
266-
let goals ← goals.filterMapM fun goal => do
267-
let (goal, _) ← liftGrindM <| SearchM.run goal do
268-
intros genNew
269-
getGoal
270-
if goal.inconsistent then
271-
return none
272-
else
273-
return some goal
274-
replaceMainGoal goals
275-
| _ => throwUnsupportedSyntax
251+
let `(grind| cases #$anchor:hexnum) := stx | throwUnsupportedSyntax
252+
let (numDigits, val) ← elabAnchor anchor
253+
let goal ← getMainGoal
254+
let candidates := goal.split.candidates
255+
let (e, goals, genNew) ← liftSearchM do
256+
for c in candidates do
257+
let e := c.getExpr
258+
let anchor ← getAnchor c.getExpr
259+
if isAnchorPrefix numDigits val anchor then
260+
let some result ← split? c
261+
| throwError "`cases` tactic failed, case-split is not ready{indentExpr c.getExpr}"
262+
return (e, result)
263+
throwError "`cases` tactic failed, invalid anchor"
264+
goal.withContext <| withRef anchor <| logAnchor numDigits val e
265+
let goals ← goals.filterMapM fun goal => do
266+
let (goal, _) ← liftGrindM <| SearchM.run goal do
267+
intros genNew
268+
getGoal
269+
if goal.inconsistent then
270+
return none
271+
else
272+
return some goal
273+
replaceMainGoal goals
274+
275+
def mkCasesSuggestions (candidates : Array SplitCandidateWithAnchor) (numDigits : Nat) : MetaM (Array Tactic.TryThis.Suggestion) := do
276+
candidates.mapM fun { anchor, e, .. } => do
277+
let anchorStx ← mkAnchorSyntax numDigits anchor
278+
let tac ← `(grind| cases $anchorStx:anchor)
279+
let msg ← addMessageContext m!"{tac} for{indentExpr e}"
280+
return {
281+
suggestion := .tsyntax tac
282+
messageData? := some msg
283+
}
284+
285+
@[builtin_grind_tactic casesTrace] def evalCasesTrace : GrindTactic := fun stx => withMainContext do
286+
let `(grind| cases? $[$filter?]?) := stx | throwUnsupportedSyntax
287+
let filter ← elabFilter filter?
288+
let { candidates, numDigits } ← liftGoalM <| getSplitCandidateAnchors filter.eval
289+
let suggestions ← mkCasesSuggestions candidates numDigits
290+
Tactic.TryThis.addSuggestions stx suggestions
291+
return ()
276292

277293
@[builtin_grind_tactic Parser.Tactic.Grind.focus] def evalFocus : GrindTactic := fun stx => do
278294
let mkInfo ← mkInitialTacticInfo stx[0]
@@ -335,28 +351,24 @@ public def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIden
335351
return mvarId
336352

337353
@[builtin_grind_tactic «next»] def evalNext : GrindTactic := fun stx => do
338-
match stx with
339-
| `(grind| next%$nextTk $hs* =>%$arr $seq:grindSeq) => do
340-
let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
341-
let mvarId ← renameInaccessibles goal.mvarId hs
342-
let goal := { goal with mvarId }
343-
setGoals [goal]
344-
goal.mvarId.setTag Name.anonymous
345-
withCaseRef arr seq <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[nextTk, arr]) <|
346-
evalGrindTactic stx[3]
347-
setGoals goals
348-
| _ => throwUnsupportedSyntax
354+
let `(grind| next%$nextTk $hs* =>%$arr $seq:grindSeq) := stx | throwUnsupportedSyntax
355+
let goal :: goals ← getUnsolvedGoals | throwNoGoalsToBeSolved
356+
let mvarId ← renameInaccessibles goal.mvarId hs
357+
let goal := { goal with mvarId }
358+
setGoals [goal]
359+
goal.mvarId.setTag Name.anonymous
360+
withCaseRef arr seq <| closeUsingOrAdmit <| withTacticInfoContext (mkNullNode #[nextTk, arr]) <|
361+
evalGrindTactic stx[3]
362+
setGoals goals
349363

350364
@[builtin_grind_tactic nestedTacticCore] def evalNestedTactic : GrindTactic := fun stx => do
351-
match stx with
352-
| `(grind| tactic%$tacticTk =>%$arr $seq:tacticSeq) => do
353-
let goal ← getMainGoal
354-
let recover := (← read).recover
355-
discard <| Tactic.run goal.mvarId <| withCaseRef arr seq <| Tactic.closeUsingOrAdmit
356-
<| Tactic.withTacticInfoContext (mkNullNode #[tacticTk, arr])
357-
<| Tactic.withRecover recover <| evalTactic seq
358-
replaceMainGoal []
359-
| _ => throwUnsupportedSyntax
365+
let `(grind| tactic%$tacticTk =>%$arr $seq:tacticSeq) := stx | throwUnsupportedSyntax
366+
let goal ← getMainGoal
367+
let recover := (← read).recover
368+
discard <| Tactic.run goal.mvarId <| withCaseRef arr seq <| Tactic.closeUsingOrAdmit
369+
<| Tactic.withTacticInfoContext (mkNullNode #[tacticTk, arr])
370+
<| Tactic.withRecover recover <| evalTactic seq
371+
replaceMainGoal []
360372

361373
@[builtin_grind_tactic «first»] partial def evalFirst : GrindTactic := fun stx => do
362374
let tacs := stx[1].getArgs
@@ -383,12 +395,11 @@ where
383395
| `(grind| fail $msg:str) => throwError "{msg.getString}\n{goalsMsg}"
384396
| _ => throwUnsupportedSyntax
385397

386-
@[builtin_grind_tactic «renameI»] def evalRenameInaccessibles : GrindTactic
387-
| `(grind| rename_i $hs*) => do
388-
let goal ← getMainGoal
389-
let mvarId ← renameInaccessibles goal.mvarId hs
390-
replaceMainGoal [{ goal with mvarId }]
391-
| _ => throwUnsupportedSyntax
398+
@[builtin_grind_tactic «renameI»] def evalRenameInaccessibles : GrindTactic := fun stx => do
399+
let `(grind| rename_i $hs*) := stx | throwUnsupportedSyntax
400+
let goal ← getMainGoal
401+
let mvarId ← renameInaccessibles goal.mvarId hs
402+
replaceMainGoal [{ goal with mvarId }]
392403

393404
@[builtin_grind_tactic exposeNames] def evalExposeNames : GrindTactic := fun _ => do
394405
let goal ← getMainGoal

‎src/Lean/Elab/Tactic/Grind/Filter.lean‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
/-
2+
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Leonardo de Moura
5+
-/
6+
module
7+
prelude
8+
public import Lean.Elab.Tactic.Grind.Basic
9+
import Init.Grind.Interactive
10+
namespace Lean.Elab.Tactic.Grind
11+
open Meta
12+
13+
public inductive Filter where
14+
| true
15+
| const (declName : Name)
16+
| fvar (fvarId : FVarId)
17+
| gen (pred : Nat → Bool)
18+
| or (a b : Filter)
19+
| and (a b : Filter)
20+
| not (a : Filter)
21+
22+
public partial def elabFilter (filter? : Option (TSyntax `grind_filter)) : GrindTacticM Filter := do
23+
let some filter := filter? | return .true
24+
go filter
25+
where
26+
go (filter : TSyntax `grind_filter) : GrindTacticM Filter := do
27+
match filter with
28+
| `(grind_filter| $id:ident) =>
29+
match (← Term.resolveId? id) with
30+
| some (.const declName _) => return .const declName
31+
| some (.fvar fvarId) => return .fvar fvarId
32+
| _ => throwErrorAt id "invalid identifier"
33+
| `(grind_filter| $a:grind_filter && $b:grind_filter) => return .and (← go a) (← go b)
34+
| `(grind_filter| $a:grind_filter || $b:grind_filter) => return .or (← go a) (← go b)
35+
| `(grind_filter| ! $a:grind_filter) => return .not (← go a)
36+
| `(grind_filter| ($a:grind_filter)) => go a
37+
| `(grind_filter| gen = $n:num) => let n := n.getNat; return .gen fun x => x == n
38+
| `(grind_filter| gen > $n:num) => let n := n.getNat; return .gen fun x => x > n
39+
| `(grind_filter| gen ≥ $n:num) => let n := n.getNat; return .gen fun x => x ≥ n
40+
| `(grind_filter| gen >= $n:num) => let n := n.getNat; return .gen fun x => x ≥ n
41+
| `(grind_filter| gen ≤ $n:num) => let n := n.getNat; return .gen fun x => x ≤ n
42+
| `(grind_filter| gen <= $n:num) => let n := n.getNat; return .gen fun x => x ≤ n
43+
| `(grind_filter| gen < $n:num) => let n := n.getNat; return .gen fun x => x < n
44+
| `(grind_filter| gen != $n:num) => let n := n.getNat; return .gen fun x => x != n
45+
| _ => throwUnsupportedSyntax
46+
47+
open Meta.Grind
48+
49+
-- **Note**: facts may not have been internalized if they are equalities.
50+
def getGen (e : Expr) : GoalM Nat := do
51+
if (← alreadyInternalized e) then
52+
getGeneration e
53+
else match_expr e with
54+
| Eq _ lhs rhs => return max (← getGeneration lhs) (← getGeneration rhs)
55+
| _ => return 0
56+
57+
public def Filter.eval (filter : Filter) (e : Expr) : GoalM Bool := do
58+
go filter
59+
where
60+
go (filter : Filter) : GoalM Bool := do
61+
match filter with
62+
| .true => return .true
63+
| .and a b => go a <&&> go b
64+
| .or a b => go a <||> go b
65+
| .not a => return !(← go a)
66+
| .const declName => return Option.isSome <| e.find? fun e => e.isConstOf declName
67+
| .fvar fvarId => return Option.isSome <| e.find? fun e => e.isFVar && e.fvarId! == fvarId
68+
| .gen pred => let gen ← getGen e; return pred gen
69+
70+
end Lean.Elab.Tactic.Grind

0 commit comments

Comments
 (0)