feat: grind? using finish?

Author: leodemoura

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

@@ -14,6 +14,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 import Lean.Meta.Tactic.Grind.AC.Eq
 import Lean.Meta.Tactic.Grind.EMatch
 import Lean.Meta.Tactic.Grind.PP
+import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Intro
 import Lean.Meta.Tactic.Grind.Split
 import Lean.Meta.Tactic.Grind.Anchor
@@ -134,7 +135,9 @@ def logTheoremAnchor (proof : Expr) : TermElabM Unit := do
   Term.addTermInfo' stx proof
 
 def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit := do
-  let progress ← liftGoalM <| if only then ematchOnly thms else ematch thms
+  let progress ← liftGoalM do
+    let thms ← thms.mapM (preprocessTheorem · 0)
+    if only then ematchOnly thms else ematch thms
   unless progress do
     throwError "`instantiate` tactic failed to instantiate new facts, use `show_patterns` to see active theorems and their patterns."
   let goal ← getMainGoal

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

@@ -14,6 +14,9 @@ import Lean.Meta.Tactic.Grind.SimpUtil
 import Lean.Meta.Tactic.Grind.EMatchTheoremParam
 import Lean.Elab.Tactic.Grind.Basic
 import Lean.Elab.Tactic.Grind.Param
+import Lean.Meta.Tactic.Grind.Action
+import Lean.Elab.Tactic.Grind.Trace
+import Lean.Meta.Tactic.Grind.CollectParams
 import Lean.Elab.MutualDef
 meta import Lean.Meta.Tactic.Grind.Parser
 public section
@@ -215,6 +218,7 @@ def filterSuggestionsFromConfig (config : TSyntax ``Lean.Parser.Tactic.optConfig
     | none => true
   ⟨config.raw.setArgs filteredItems⟩
 
+-- **TODO**: delete
 def mkGrindOnly
     (config : TSyntax ``Lean.Parser.Tactic.optConfig)
     (trace : Grind.Trace)
@@ -250,14 +254,35 @@ private def elabGrindConfig' (config : TSyntax ``Lean.Parser.Tactic.optConfig) (
   let config ← elabGrindConfig' config interactive
   discard <| evalGrindCore stx config only params seq
 
-@[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => do
-  let `(tactic| grind?%$tk $configStx:optConfig $[only%$only]?  $[ [$params:grindParam,*] ]?) := stx
+@[builtin_tactic Lean.Parser.Tactic.grindTrace] def evalGrindTrace : Tactic := fun stx => withMainContext do
+  let `(tactic| grind? $configStx:optConfig $[only%$only]?  $[ [$params?:grindParam,*] ]?) := stx
     | throwUnsupportedSyntax
   let config ← elabGrindConfig configStx
   let config := { config with trace := true }
-  let trace ← evalGrindCore stx config only params none
-  let stx ← mkGrindOnly configStx trace
-  Tactic.TryThis.addSuggestion tk stx (origSpan? := ← getRef)
+  let only := only.isSome
+  let params := if let some params := params? then params.getElems else #[]
+  let mvarId ← getMainGoal
+  let params ← mkGrindParams config only params mvarId
+  discard <| Grind.GrindTacticM.runAtGoal mvarId params do
+    let finish ← Grind.mkFinishAction
+    let goal :: _ ← Grind.getGoals
+      | let tac ← `(tactic| grind only)
+        Tactic.TryThis.addSuggestion stx { suggestion := .tsyntax tac }
+    Grind.liftGrindM do
+      -- **Note**: If we get failures when using the first suggestion, we should test is using `saved`
+      -- let saved ← saveState
+      match (← finish.run goal) with
+      | .closed seq =>
+        let configCtx' := filterSuggestionsFromConfig configStx
+        let tacs ← Grind.mkGrindOnlyTactics configCtx' seq
+        let seq := Grind.Action.mkGrindSeq seq
+        let tac ← `(tactic| grind => $seq:grindSeq)
+        let tacs := tacs.push tac
+        Tactic.TryThis.addSuggestions stx <| tacs.map fun tac => { suggestion := .tsyntax tac }
+      | .stuck gs =>
+        let goal :: _ := gs | throwError "`grind?` failed, but resulting goal is not available"
+        let result ← Grind.mkResult params (some goal)
+        throwError "`grind?` failed\n{← result.toMessageData}"
 
 @[builtin_tactic Lean.Parser.Tactic.cutsat] def evalCutsat : Tactic := fun stx => do
   let `(tactic| cutsat $config:optConfig) := stx | throwUnsupportedSyntax

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

@@ -21,19 +21,19 @@ open Meta.Grind
 def withTracing (x : GrindTacticM α) : GrindTacticM α := do
   withReader (fun ctx => { ctx with ctx.config.trace := true }) x
 
-def mkFinishAction (maxIterations : Nat) : IO Action := do
+public abbrev maxIterationsDefault := 10000 -- **TODO**: Add option
+
+public def mkFinishAction (maxIterations : Nat := maxIterationsDefault) : IO Action := do
   let solvers ← Solvers.mkAction
   let step : Action := Action.done <|> solvers <|> Action.instantiate <|> Action.splitNext <|> Action.mbtc
   return Action.checkTactic (warnOnly := true) >> step.loop maxIterations
 
-def maxIterations := 1000 -- **TODO**: Add option
-
 @[builtin_grind_tactic finishTrace] def evalFinishTrace : GrindTactic := fun stx => do
   let `(grind| finish? $[$configItems]* $[only%$only]? $[[$params?,*]]?) := stx | throwUnsupportedSyntax
   withConfigItems configItems do
   let params := params?.getD {}
   withParams (← read).params params only.isSome do
-    let a ← mkFinishAction maxIterations
+    let a ← mkFinishAction
     let goal ← getMainGoal
     let params := (← read).params
     withTracing do

src/Lean/Meta/Tactic/Grind/CollectParams.lean

@@ -19,6 +19,7 @@ namespace Collector
 structure State where
   params : Array TParam := #[]
   anchors : Array TAnchor := #[]
+  hasSorry : Bool := false
 
 abbrev Collect := StateRefT State CoreM
 
@@ -47,6 +48,7 @@ def collectInstantiateParams (params : Syntax.TSepArray `Lean.Parser.Tactic.Grin
 
 partial def collect (tac : TGrind) : Collect Unit := do
   match tac with
+  | `(grind| sorry) => modify fun s => { s with hasSorry := true }
   | `(grind| next => $$seq;*)
   | `(grind| · $$seq;*) =>
     for step in seq.getElems do
@@ -67,11 +69,15 @@ def main (seq : List TGrind) : Collect Unit :=
 
 end Collector
 
-def collectParams (seq : List TGrind) : CoreM (Array TParam) := do
+def collectParamsCore (seq : List TGrind) : CoreM (Bool × Array TParam × Array TParam) := do
   let (_, s) ← Collector.main seq |>.run {}
   let anchors ← s.anchors.mapM fun anchor =>
     `(Parser.Tactic.grindParam| $anchor:anchor)
-  return s.params ++ anchors
+  return (s.hasSorry, s.params, anchors)
+
+def collectParams (seq : List TGrind) : CoreM (Array TParam) := do
+  let (_, params, anchors) ← collectParamsCore seq
+  return params ++ anchors
 
 /--
 Given a `grind` tactic sequence, extracts parameters and builds an terminal `finish only` tactic.
@@ -80,4 +86,27 @@ public def mkFinishTactic (seq : List TGrind) : CoreM TGrind := do
   let params ← collectParams seq
   `(grind| finish only [$params,*])
 
+/--
+Given a `grind` tactic sequence, extracts parameters and builds a `grind only` tactics.
+It returns at most two. The first tactic uses anchors to restrict the search if applicable.
+The second does not restrict the search using anchors. The second option is included only if there
+are anchors.
+-/
+public def mkGrindOnlyTactics (cfg : TSyntax `Lean.Parser.Tactic.optConfig) (seq : List TGrind) : CoreM (Array (TSyntax `tactic)) := do
+  let (hasSorry, params, anchors) ← collectParamsCore seq
+  if hasSorry then return #[]
+  let allParams := params ++ anchors
+  let s₁ ← mkTac allParams
+  if anchors.isEmpty then
+    return #[s₁]
+  else
+    let s₂ ← mkTac params
+    return #[s₁, s₂]
+where
+  mkTac (params : Array TParam) : CoreM (TSyntax `tactic) :=
+    if params.isEmpty then
+      `(tactic| grind $cfg:optConfig only)
+    else
+      `(tactic| grind $cfg:optConfig only [$params,*])
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -209,11 +209,14 @@ where
       internalize e generation
     pushEq matchCond e (← mkEqRefl matchCond)
 
-def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+def preprocessTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM EMatchTheorem := do
   -- Recall that we use the proof as part of the key for a set of instances found so far.
   -- We don't want to use structural equality when comparing keys.
   let proof ← shareCommon thm.proof
-  let thm := { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation thm.origin)) }
+  return { thm with proof, patterns := (← thm.patterns.mapM (internalizePattern · generation thm.origin)) }
+
+def activateTheorem (thm : EMatchTheorem) (generation : Nat) : GoalM Unit := do
+  let thm ← preprocessTheorem thm generation
   trace_goal[grind.ematch] "activated `{thm.origin.pp}`, {thm.patterns.map ppPattern}"
   modify fun s => { s with ematch.newThms := s.ematch.newThms.push thm }
 

tests/lean/run/grind_ematch_gen_pattern.lean

@@ -9,8 +9,14 @@ example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = som
   grind [f]
 
 /--
-info: Try this:
+info: Try these:
+  [apply] grind only [= gen Option.pbind_some', f, #ebef]
   [apply] grind only [= gen Option.pbind_some', f]
+  [apply] grind =>
+    instantiate only [= gen Option.pbind_some']
+    instantiate only [f]
+    mbtc
+    cases #ebef
 -/
 #guard_msgs (info) in
 example (h : b = some a) : (b.pbind fun a h => some <| a + f b (by grind)) = some (a + a) := by

tests/lean/run/grind_option.lean

@@ -8,30 +8,41 @@ section
 variable [BEq α] {o₁ o₂ o₃ o₄ o₅ : Option α}
 
 /--
-info: Try this:
-  [apply] grind only [= Option.or_some, = Option.some_beq_none, = Option.getD_or, = Option.some_or, =_ Option.or_assoc,
-    = Option.or_assoc]
+info: Try these:
+  [apply] grind only [=_ Option.or_assoc, = Option.or_assoc, = Option.or_some, = Option.some_or, = Option.some_beq_none]
+  [apply] grind =>
+    instantiate only [=_ Option.or_assoc, = Option.or_assoc, = Option.or_some]
+    instantiate only [= Option.some_or, = Option.or_some]
+    instantiate only [= Option.some_beq_none]
 -/
 #guard_msgs in
 example : ((o₁.or (o₂.or (some x))).or (o₄.or o₅) == none) = false := by grind?
 
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [= Option.max_none_right, = Option.min_some_some, = Nat.min_def]
+  [apply] grind =>
+    instantiate only [= Option.max_none_right, = Option.min_some_some]
+    instantiate only [= Nat.min_def]
 -/
 #guard_msgs in
 example : max (some 7) none = min (some 13) (some 7) := by grind?
 
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [= Option.guard_apply]
+  [apply] grind => instantiate only [= Option.guard_apply]
 -/
 #guard_msgs in
 example : Option.guard (· ≤ 7) 3 = some 3 := by grind?
 
 /--
-info: Try this:
+info: Try these:
+  [apply] grind only [= Option.mem_bind_iff, #99bb]
   [apply] grind only [= Option.mem_bind_iff]
+  [apply] grind =>
+    instantiate only [= Option.mem_bind_iff]
+    instantiate only [#99bb]
 -/
 #guard_msgs in
 example {x : β} {o : Option α} {f : α → Option β} (h : a ∈ o) (h' : x ∈ f a) : x ∈ o.bind f := by grind?

tests/lean/run/grind_question_mark_suggestions.lean

@@ -10,3 +10,14 @@ info: Try this:
 #guard_msgs in
 example {x y : Nat} (h : x = y) : y = x := by
   grind? +suggestions
+
+def f (x : α) := x
+
+/--
+info: Try these:
+  [apply] grind only [f]
+  [apply] grind => instantiate only [f]
+-/
+#guard_msgs in
+example {x y : Nat} (h : x = y) : x = f y := by
+  grind? +suggestions [f]

tests/lean/run/grind_trace.lean

@@ -20,35 +20,57 @@ attribute [grind =] List.getElem_cons_zero in
 attribute [grind =] List.getElem?_cons_zero in
 
 /--
-info: Try this:
-  [apply] grind only [= List.getElem?_eq_none, = List.getElem?_replicate, = List.getElem?_eq_getElem]
+info: Try these:
+  [apply] grind only [= List.getElem?_replicate]
+  [apply] grind => instantiate only [= List.getElem?_replicate]
 -/
 #guard_msgs (info) in
 theorem getElem?_replicate' : (List.replicate n a)[m]? = if m < n then some a else none := by
   grind?
 
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [= List.length_cons]
+  [apply] grind => instantiate only [= List.length_cons]
 -/
 #guard_msgs (info) in
 example : 0 < (x :: t).length := by
   grind?
 
 attribute [grind ext] List.ext_getElem?
 /--
-info: Try this:
-  [apply] grind only [= List.getElem?_eq_some_iff, = List.length_replicate, = List.getElem?_eq_none,
-    = List.getElem_replicate, = Option.map_some, = Option.map_none, = List.getElem?_replicate,
-    = List.getElem?_eq_getElem, = List.getElem?_map]
+info: Try these:
+  [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
+    = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some,
+    = Option.map_none, #b53f, #3f91, #ea98]
+  [apply] grind only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
+    = List.getElem?_eq_getElem, = List.length_replicate, = List.getElem?_eq_some_iff, = Option.map_some,
+    = Option.map_none]
+  [apply] grind =>
+    cases #b53f
+    instantiate only [= List.getElem?_replicate, = List.getElem?_map, = List.getElem?_eq_none,
+      = List.getElem?_eq_getElem]
+    instantiate only [= List.getElem?_replicate, = List.getElem?_eq_none, = List.getElem?_eq_getElem,
+      = List.length_replicate]
+    instantiate only [= List.length_replicate]
+    cases #3f91
+    · instantiate only [= List.getElem?_eq_some_iff]
+      cases #ea98
+      · instantiate only [= Option.map_some]
+      · instantiate only [= Option.map_none]
+    · instantiate only [= Option.map_some]
 -/
 #guard_msgs (info) in
 theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) := by
   grind?
 
 /--
-info: Try this:
+info: Try these:
+  [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self, #e8ab]
   [apply] grind only [= List.getLast?_eq_some_iff, ← List.mem_concat_self]
+  [apply] grind =>
+    instantiate only [= List.getLast?_eq_some_iff]
+    cases #e8ab <;> instantiate only [← List.mem_concat_self]
 -/
 #guard_msgs (info) in
 theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
@@ -59,8 +81,9 @@ theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some
   | _ => 2
 
 /--
-info: Try this:
+info: Try these:
   [apply] grind only
+  [apply] grind => instantiate only
 -/
 #guard_msgs (info) in
 example : x = 0 → f x = 1 := by
@@ -70,8 +93,9 @@ example : x = 0 → f x = 1 := by
 attribute [grind] f
 
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [f]
+  [apply] grind => instantiate only [f]
 -/
 #guard_msgs (info) in
 example : x = 0 → f x = 1 := by
@@ -84,8 +108,9 @@ theorem gthm : g (g x) = g x := sorry
 grind_pattern gthm => g (g x)
 
 /--
-info: Try this:
+info: Try these:
   [apply] grind only [usr gthm]
+  [apply] grind => instantiate only [usr gthm]
 -/
 #guard_msgs (info) in
 example : g (g (g x)) = g x := by
@@ -109,6 +134,12 @@ example : (List.replicate n a)[m]? = if m < n then some a else none := by
 
 reset_grind_attrs%
 
+set_option warn.sorry false
+
+/--
+info: Try these:
+  [apply] grind => sorry
+-/
+#guard_msgs in
 example : (List.replicate n a)[m]? = if m < n then some a else none := by
-  fail_if_success grind?
-  sorry
+  grind?