From 4077bf2c05b74a2eaaf1db9be957236f29614f63 Mon Sep 17 00:00:00 2001
From: Sebastian Graf <sgraf1337@gmail.com>
Date: Wed, 15 Oct 2025 10:22:09 +0200
Subject: [PATCH] feat: implement `mvcgen?`, expanding to `mvcgen invariants?`
 (#10782)

This PR implements a hint tactic `mvcgen?`, expanding to `mvcgen
invariants?`

Example:
```
/--
info: Try this:
  [apply] mvcgen invariants?
---
info: Try this:
  [apply] mvcgen [mySum] invariants?
---
info: Try this:
  [apply] mvcgen +elimLets invariants?
---
info: Try this:
  [apply] mvcgen +elimLets [mySum] invariants?
-/
#guard_msgs (info) in
theorem mySum_suggest_invariant_short (l : List Nat) : mySum l = l.sum := by
  generalize h : mySum l = r
  apply Id.of_wp_run_eq h
  mvcgen?
  mvcgen? [mySum]
  mvcgen? +elimLets
  mvcgen? +elimLets [mySum]
  all_goals admit
```
---
 src/Lean/Elab/Tactic/Do/VCGen.lean            |  9 ++++++++
 src/Std/Tactic/Do/Syntax.lean                 |  8 ++++++-
 .../lean/run/mvcgenInvariantsSuggestions.lean | 23 +++++++++++++++++++
 3 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index 2a175654b9..0152545733 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -478,3 +478,12 @@ def elabMVCGen : Tactic := fun stx => withMainContext do
   trace[Elab.Tactic.Do.vcgen] "before replacing main goal {← (invariants ++ vcs).mapM fun m => m.getTag}"
   replaceMainGoal (invariants ++ vcs).toList
   -- trace[Elab.Tactic.Do.vcgen] "replaced main goal, new: {← getGoals}"
+
+@[builtin_tactic Lean.Parser.Tactic.mvcgenHint]
+def elabMVCGenHint : Tactic := fun stx => withMainContext do
+  let stx' : TSyntax ``mvcgen := TSyntax.mk <| stx
+    |>.setKind ``Lean.Parser.Tactic.mvcgen
+    |>.modifyArgs (·.set! 0 (mkAtom "mvcgen") |>.push (mkNullNode #[← `(invariantAlts| invariants?)]) |>.push mkNullNode)
+  -- logInfo m!"{stx}\n{toString stx}\n{repr stx}"
+  -- logInfo m!"{stx'}\n{toString stx'}\n{repr stx'}"
+  Lean.Meta.Tactic.TryThis.addSuggestion stx stx'
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index 268c72cbac..cdd0b5f7cd 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -365,5 +365,11 @@ syntax vcAlts := "with " (ppSpace colGt tactic)? withPosition((colGe vcAlt)*)
 
 @[tactic_alt Lean.Parser.Tactic.mvcgenMacro]
 syntax (name := mvcgen) "mvcgen" optConfig
-  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")?
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")?
   (invariantAlts)? (vcAlts)? : tactic
+
+/--
+A hint tactic that expands to `mvcgen invariants?`.
+-/
+syntax (name := mvcgenHint) "mvcgen?" optConfig
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "] ")? : tactic
diff --git a/tests/lean/run/mvcgenInvariantsSuggestions.lean b/tests/lean/run/mvcgenInvariantsSuggestions.lean
index 6e3dccf3a5..49188979d9 100644
--- a/tests/lean/run/mvcgenInvariantsSuggestions.lean
+++ b/tests/lean/run/mvcgenInvariantsSuggestions.lean
@@ -26,6 +26,29 @@ theorem mySum_suggest_invariant (l : List Nat) : mySum l = l.sum := by
   mvcgen invariants?
   all_goals admit
 
+/--
+info: Try this:
+  [apply] mvcgen invariants?
+---
+info: Try this:
+  [apply] mvcgen [mySum] invariants?
+---
+info: Try this:
+  [apply] mvcgen +elimLets invariants?
+---
+info: Try this:
+  [apply] mvcgen +elimLets [mySum] invariants?
+-/
+#guard_msgs (info) in
+theorem mySum_suggest_invariant_short (l : List Nat) : mySum l = l.sum := by
+  generalize h : mySum l = r
+  apply Id.of_wp_run_eq h
+  mvcgen?
+  mvcgen? [mySum]
+  mvcgen? +elimLets
+  mvcgen? +elimLets [mySum]
+  all_goals admit
+
 def mySum2 (l : List Nat) : Nat := Id.run do
   let mut acc := 0
   let mut acc2 := 0