fix: simp? suggests generated equations lemma names (#3573)

closes #3547

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

src/Lean/Meta/Eqns.lean

@@ -51,7 +51,8 @@ private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do
     return false
 
 structure EqnsExtState where
-  map : PHashMap Name (Array Name) := {}
+  map    : PHashMap Name (Array Name) := {}
+  mapInv : PHashMap Name Name := {}
   deriving Inhabited
 
 /- We generate the equations on demand, and do not save them on .olean files. -/
@@ -77,7 +78,22 @@ private def mkSimpleEqThm (declName : Name) : MetaM (Option Name) := do
     return none
 
 /--
-  Return equation theorems for the given declaration.
+Returns `some declName` if `thmName` is an equational theorem for `declName`.
+-/
+def isEqnThm? (thmName : Name) : CoreM (Option Name) := do
+  return eqnsExt.getState (← getEnv) |>.mapInv.find? thmName
+
+/--
+Stores in the `eqnsExt` environment extension that `eqThms` are the equational theorems for `declName`
+-/
+private def registerEqnThms (declName : Name) (eqThms : Array Name) : CoreM Unit := do
+  modifyEnv fun env => eqnsExt.modifyState env fun s => { s with
+    map := s.map.insert declName eqThms
+    mapInv := eqThms.foldl (init := s.mapInv) fun mapInv eqThm => mapInv.insert eqThm declName
+  }
+
+/--
+  Returns equation theorems for the given declaration.
   By default, we do not create equation theorems for nonrecursive definitions.
   You can use `nonRec := true` to override this behavior, a dummy `rfl` proof is created on the fly.
 -/
@@ -87,12 +103,12 @@ def getEqnsFor? (declName : Name) (nonRec := false) : MetaM (Option (Array Name)
   else if (← shouldGenerateEqnThms declName) then
     for f in (← getEqnsFnsRef.get) do
       if let some r ← f declName then
-        modifyEnv fun env => eqnsExt.modifyState env fun s => { s with map := s.map.insert declName r }
+        registerEqnThms declName r
         return some r
     if nonRec then
       let some eqThm ← mkSimpleEqThm declName | return none
       let r := #[eqThm]
-      modifyEnv fun env => eqnsExt.modifyState env fun s => { s with map := s.map.insert declName r }
+      registerEqnThms declName r
       return some r
   return none
 

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.AppBuilder
 import Lean.Meta.CongrTheorems
+import Lean.Meta.Eqns
 import Lean.Meta.Tactic.Replace
 import Lean.Meta.Tactic.Simp.SimpTheorems
 import Lean.Meta.Tactic.Simp.SimpCongrTheorems
@@ -256,7 +257,22 @@ def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
 @[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
   savingCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
 
-def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
+def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
+  /-
+  If `thmId` is an equational theorem (e.g., `foo._eq_1`), we should record `foo` instead.
+  See issue #3547.
+  -/
+  let thmId ← match thmId with
+    | .decl declName post false =>
+      /-
+      Remark: if `inv := true`, then the user has manually provided the theorem and wants to
+      use it in the reverse direction. So, we only performs the substitution when `inv := false`
+      -/
+      if let some declName ← isEqnThm? declName then
+        pure (Origin.decl declName post false)
+      else
+        pure thmId
+    | _ => pure thmId
   modify fun s => if s.usedTheorems.contains thmId then s else
     let n := s.usedTheorems.size
     { s with usedTheorems := s.usedTheorems.insert thmId n }

tests/lean/run/3547.lean

@@ -0,0 +1,11 @@
+def foo : Nat → Nat
+  | 0 => 0
+  | n+1 => foo n
+decreasing_by decreasing_tactic
+
+/--
+info: Try this: simp only [foo]
+-/
+#guard_msgs in
+def foo2 : foo 2 = 0 := by
+  simp? [foo]