feat: grind "silent" have

This PR implements the `have <ident>? : <prop>` tactic for the `grind`
interactive mode. The proposition is proved using the default `grind`
search strategy. This tactic is also useful for inspecting or querying the
current `grind` state.

src/Init/Grind/Interactive.lean

@@ -198,5 +198,10 @@ syntax (name := exposeNames) "expose_names" : grind
 but it sets the option only within the tactics `tacs`. -/
 syntax (name := setOption) "set_option " (ident (noWs "." noWs ident)?) ppSpace optionValue " in " grindSeq : grind
 
+/--
+Proves `<term>` using the current `grind` state and default search strategy.
+-/
+syntax (name := haveSilent) "have" (ppSpace ident)? ppSpace ": " term : grind
+
 end Grind
 end Lean.Parser.Tactic

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

@@ -176,12 +176,12 @@ Runs `x` with only the first unsolved goal as the goal.
 Fails if there are no goal to be solved.
 -/
 def focus (k : GrindTacticM α) : GrindTacticM α := do
-  let mvarId :: mvarIds ← getUnsolvedGoals
+  let goal :: goals ← getUnsolvedGoals
     | throwNoGoalsToBeSolved
-  setGoals [mvarId]
+  setGoals [goal]
   let a ← k
-  let mvarIds' ← getUnsolvedGoals
-  setGoals (mvarIds' ++ mvarIds)
+  let goals' ← getUnsolvedGoals
+  setGoals (goals' ++ goals)
   pure a
 
 /--

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

@@ -7,7 +7,9 @@ module
 prelude
 public import Lean.Elab.Tactic.Grind.Basic
 import Lean.Meta.Tactic.Grind.Intro
+import Lean.Meta.Tactic.Grind.RevertAll
 import Lean.Elab.SyntheticMVars
+import Lean.Meta.Tactic.Grind.Solve
 namespace Lean.Elab.Tactic.Grind
 open Meta Grind
 
@@ -27,21 +29,41 @@ where
     return e
 
 @[builtin_grind_tactic Parser.Tactic.Grind.«have»] def evalHave : GrindTactic := fun stx => withMainContext do
-  match stx with
-  | `(grind| have $decl:letDecl) =>
-    let stx' ← `(have $decl:letDecl; False)
-    let e ← elabTerm stx' none
-    let .letE n t v _ _ := e
-      | throwError "elaborated term is not a `have` declaration{indentExpr e}"
-    if t.hasMVar then throwError "type has metavariables{indentExpr t}"
-    if v.hasMVar then throwError "value has metavariables{indentExpr v}"
-    let goal ← getMainGoal
-    let mvarId ← goal.mvarId.assert n t v
-    let goal := { goal with mvarId }
-    let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do
-      intros 0
-      getGoal
-    replaceMainGoal [goal]
-  | _ => throwUnsupportedSyntax
+  let `(grind| have $decl:letDecl) := stx | throwUnsupportedSyntax
+  let stx' ← `(have $decl:letDecl; False)
+  let e ← elabTerm stx' none
+  let .letE n t v _ _ := e
+    | throwError "elaborated term is not a `have` declaration{indentExpr e}"
+  if t.hasMVar then throwError "type has metavariables{indentExpr t}"
+  if v.hasMVar then throwError "value has metavariables{indentExpr v}"
+  let goal ← getMainGoal
+  let mvarId ← goal.mvarId.assert n t v
+  let goal := { goal with mvarId }
+  let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do
+    intros 0
+    getGoal
+  replaceMainGoal [goal]
+
+@[builtin_grind_tactic Parser.Tactic.Grind.haveSilent] def evalHaveSilent : GrindTactic := fun stx => withMainContext do
+  let `(grind| have $[$id?:ident]? : $prop:term) := stx | throwUnsupportedSyntax
+  let id := if let some id := id? then id.getId else `this
+  let id := if id.hasMacroScopes then id else markGrindName id
+  let prop ← elabTerm prop none
+  let mvar ← mkFreshExprMVar prop
+  let mvarId := mvar.mvarId!
+  let goal :: goals ← getGoals | throwNoGoalsToBeSolved
+  let goalNew := { goal with mvarId }
+  setGoals [goalNew]
+  if let some goal ← liftGrindM <| solve goalNew then
+    let params := (← read).params
+    let result ← liftGrindM do mkResult params (some goal)
+    throwError "`finish` failed\n{← result.toMessageData}"
+  let v ← instantiateMVars mvar
+  let mvarId ← goal.mvarId.assert id prop v
+  let goal := { goal with mvarId }
+  let (goal, _) ← liftGrindM <| withCheapCasesOnly <| SearchM.run goal do
+    intros 0
+    getGoal
+  setGoals (goal :: goals)
 
 end Lean.Elab.Tactic.Grind

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

@@ -21,6 +21,9 @@ def getOriginalName? (name : Name) : Option Name := do
   | .str p s => if s == grindMark then some p else none
   | _ => none
 
+def markGrindName (userName : Name) : Name :=
+  Name.str userName grindMark
+
 /--
 Helper tactic for marking accessible names in the local context.
 This is a trick used during `grind` preprocessing when `clean := false`.
@@ -41,7 +44,7 @@ def _root_.Lean.MVarId.markAccessible (mvarId : MVarId) : MetaM MVarId := mvarId
         continue
       if localDecl.userName.hasMacroScopes then
         continue
-      let markedName := Name.str localDecl.userName grindMark
+      let markedName := markGrindName localDecl.userName
       lctx := lctx.setUserName localDecl.fvarId markedName
   let mvarNew ← Meta.mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName
   mvarId.assign mvarNew

tests/lean/run/grind_interactive.lean

@@ -543,4 +543,27 @@ example : (a : Point Nat) → p a → x ≠ y → False := by
     cases #6ccb
     sorry
 
+opaque q : Nat → Nat → Prop
+axiom qax : x ≠ y → q x y
+
+example : x > y + 1 → q x y := by
+  grind =>
+    have h : x > y
+    have : x ≠ y
+    have : x > y := h
+    instantiate [qax]
+
+/--
+error: `finish` failed
+x y : Nat
+h✝² : y + 2 ≤ x
+h✝¹ : ¬q x y
+h✝ : x ≤ y + 2
+⊢ False
+-/
+#guard_msgs in
+example : x > y + 1 → q x y := by
+  grind -verbose =>
+    have h : x > y + 2
+
 end Ex1