From 38a76b9b407c215aa206222b8891070b0b52a649 Mon Sep 17 00:00:00 2001
From: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Date: Mon, 6 Jan 2025 13:12:17 -0500
Subject: [PATCH] feat: add `simp?` and `dsimp?` in conversion mode

---
 src/Init/Conv.lean                  |  7 +++++++
 src/Lean/Elab/Tactic/Conv/Simp.lean | 27 ++++++++++++++++++++++++++-
 tests/lean/run/6164.lean            | 29 +++++++++++++++++++++++++++++
 3 files changed, 62 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/6164.lean

diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean
index 323abdf177e..4bd2f9c3e09 100644
--- a/src/Init/Conv.lean
+++ b/src/Init/Conv.lean
@@ -150,6 +150,10 @@ See the `simp` tactic for more information. -/
 syntax (name := simp) "simp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
 
+/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
+that would be sufficient to close the goal. See the `simp?` tactic for more information. -/
+syntax (name := simpTrace) "simp?" optConfig (discharger)? (&" only")? (simpArgs)? : conv
+
 /--
 `dsimp` is the definitional simplifier in `conv`-mode. It differs from `simp` in that it only
 applies theorems that hold by reflexivity.
@@ -167,6 +171,9 @@ example (a : Nat): (0 + 0) = a - a := by
 syntax (name := dsimp) "dsimp" optConfig (discharger)? (&" only")?
   (" [" withoutPosition((simpErase <|> simpLemma),*) "]")? : conv
 
+@[inherit_doc simpTrace]
+syntax (name := dsimpTrace) "dsimp?" optConfig (&" only")? (dsimpArgs)? : conv
+
 /-- `simp_match` simplifies match expressions. For example,
 ```
 match [a, b] with
diff --git a/src/Lean/Elab/Tactic/Conv/Simp.lean b/src/Lean/Elab/Tactic/Conv/Simp.lean
index 17c7f0648bf..b764034d327 100644
--- a/src/Lean/Elab/Tactic/Conv/Simp.lean
+++ b/src/Lean/Elab/Tactic/Conv/Simp.lean
@@ -7,9 +7,10 @@ prelude
 import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.Split
 import Lean.Elab.Tactic.Conv.Basic
+import Lean.Elab.Tactic.SimpTrace
 
 namespace Lean.Elab.Tactic.Conv
-open Meta
+open Meta Tactic TryThis
 
 def applySimpResult (result : Simp.Result) : TacticM Unit := do
   if result.proof?.isNone then
@@ -23,6 +24,19 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let (result, _) ← dischargeWrapper.with fun d? => simp lhs ctx (simprocs := simprocs) (discharge? := d?)
   applySimpResult result
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.simpTrace] def evalSimpTrace : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(conv| simp?%$tk $cfg:optConfig $(discharger)? $[only%$o]? $[[$args,*]]?) => do
+    let stx ← `(tactic| simp%$tk $cfg:optConfig $[$discharger]? $[only%$o]? $[[$args,*]]?)
+    let { ctx, simprocs, dischargeWrapper, .. } ← mkSimpContext stx (eraseLocal := false)
+    let lhs ← getLhs
+    let (result, stats) ← dischargeWrapper.with fun d? =>
+      simp lhs ctx (simprocs := simprocs) (discharge? := d?)
+    applySimpResult result
+    let stx ← mkSimpCallStx stx stats.usedTheorems
+    addSuggestion tk stx (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
 @[builtin_tactic Lean.Parser.Tactic.Conv.simpMatch] def evalSimpMatch : Tactic := fun _ => withMainContext do
   applySimpResult (← Split.simpMatch (← getLhs))
 
@@ -30,4 +44,15 @@ def applySimpResult (result : Simp.Result) : TacticM Unit := do
   let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
   changeLhs (← Lean.Meta.dsimp (← getLhs) ctx).1
 
+@[builtin_tactic Lean.Parser.Tactic.Conv.dsimpTrace] def evalDSimpTrace : Tactic := fun stx => withMainContext do
+  match stx with
+  | `(conv| dsimp?%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?) =>
+    let stx ← `(tactic| dsimp%$tk $cfg:optConfig $[only%$o]? $[[$args,*]]?)
+    let { ctx, .. } ← mkSimpContext stx (eraseLocal := false) (kind := .dsimp)
+    let (result, stats) ← Lean.Meta.dsimp (← getLhs) ctx
+    changeLhs result
+    let stx ← mkSimpCallStx stx stats.usedTheorems
+    addSuggestion tk stx (origSpan? := ← getRef)
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic.Conv
diff --git a/tests/lean/run/6164.lean b/tests/lean/run/6164.lean
new file mode 100644
index 00000000000..62145603e68
--- /dev/null
+++ b/tests/lean/run/6164.lean
@@ -0,0 +1,29 @@
+/-!
+  # `simp?` in conversion mode
+
+  Tests that `simp?` and `dsimp?` work properly in `conv` mode: namely, that each displays the
+  appropriate suggestion and applies the corresponding simplification to the focused expression.
+-/
+
+attribute [simp] Nat.two_mul
+
+/--
+info: Try this: simp only [Nat.two_mul]
+-/
+#guard_msgs in
+example (n : Nat) : 123 + 2 * n = 123 + (n + n) := by
+  conv =>
+    enter [1, 2]
+    simp?
+
+
+@[simp] def foo (n : Nat) := n + 1
+
+/--
+info: Try this: dsimp only [foo]
+-/
+#guard_msgs in
+example (n : Nat) : foo n = n + 1 := by
+  conv =>
+    lhs
+    dsimp?