From 4a2210b7e631bf33170ca1d88442f73b68e80c05 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Tue, 2 Jul 2024 03:15:39 +0200
Subject: [PATCH] fix: unresolve name avoiding locals (#4593)

Fixes #4591. The extra code already existed in the only other user of
`unresolveNameGlobal` (in the pretty printer), although I did not make
it use this function because it has some additional behavior around
universes and in pattern position.
---
 src/Lean/Elab/Tactic/Simp.lean    |  2 +-
 src/Lean/ResolveName.lean         | 11 +++++++++++
 tests/lean/4591.lean              |  7 +++++++
 tests/lean/4591.lean.expected.out |  1 +
 4 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/4591.lean
 create mode 100644 tests/lean/4591.lean.expected.out

diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 59f5581372..2ac90f8935 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -347,7 +347,7 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
       if env.contains declName
          && (inv || !simpOnlyBuiltins.contains declName)
          && !Match.isMatchEqnTheorem env declName then
-        let decl : Term ← `($(mkIdent (← unresolveNameGlobal declName)):ident)
+        let decl : Term ← `($(mkIdent (← unresolveNameGlobalAvoidingLocals declName)):ident)
         let arg ← match post, inv with
           | true,  true  => `(Parser.Tactic.simpLemma| ← $decl:term)
           | true,  false => `(Parser.Tactic.simpLemma| $decl:term)
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index be872dfe97..46053c3db9 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -425,4 +425,15 @@ where
           return some candidate
     return none
 
+def unresolveNameGlobalAvoidingLocals [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m]
+    (n₀ : Name) (fullNames := false) : m Name := do
+  let mut n ← unresolveNameGlobal n₀ fullNames
+  unless (← getLCtx).usesUserName n do return n
+  -- `n` is also a local declaration
+  if n == n₀ then
+    -- `n` is the fully qualified name. So, we append the `_root_` prefix
+    return `_root_ ++ n
+  else
+    return n₀
+
 end Lean
diff --git a/tests/lean/4591.lean b/tests/lean/4591.lean
new file mode 100644
index 0000000000..cadfb18537
--- /dev/null
+++ b/tests/lean/4591.lean
@@ -0,0 +1,7 @@
+def Nat.foo : Nat → Nat
+  | 0 => 0
+  | n+1 => foo n
+decreasing_by decreasing_tactic
+
+theorem Nat.Bar.foo : foo 2 = 0 := by
+  simp? [Nat.foo]
diff --git a/tests/lean/4591.lean.expected.out b/tests/lean/4591.lean.expected.out
new file mode 100644
index 0000000000..1a05d83bb2
--- /dev/null
+++ b/tests/lean/4591.lean.expected.out
@@ -0,0 +1 @@
+Try this: simp only [Nat.foo]