fix: do not include internal match equational theorems at simp trace (

#4274)

closes #4251

src/Lean/Elab/Tactic/Simp.lean

@@ -336,7 +336,9 @@ def mkSimpOnly (stx : Syntax) (usedSimps : Simp.UsedSimps) : MetaM Syntax := do
   for (thm, _) in usedSimps.toArray.qsort (·.2 < ·.2) do
     match thm with
     | .decl declName post inv => -- global definitions in the environment
-      if env.contains declName && (inv || !simpOnlyBuiltins.contains declName) then
+      if env.contains declName
+         && (inv || !simpOnlyBuiltins.contains declName)
+         && !Match.isMatchEqnTheorem env declName then
         let decl : Term ← `($(mkIdent (← unresolveNameGlobal declName)):ident)
         let arg ← match post, inv with
           | true,  true  => `(Parser.Tactic.simpLemma| ← $decl:term)

src/Lean/Meta/Match/MatchEqsExt.lean

@@ -19,19 +19,29 @@ def MatchEqns.size (e : MatchEqns) : Nat :=
 
 structure MatchEqnsExtState where
   map : PHashMap Name MatchEqns := {}
+  eqns : PHashSet Name := {}
   deriving Inhabited
 
 /- We generate the equations and splitter on demand, and do not save them on .olean files. -/
 builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ←
   registerEnvExtension (pure {})
 
-def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit :=
-  modifyEnv fun env => matchEqnsExt.modifyState env fun s => { s with map := s.map.insert matchDeclName matchEqns }
+def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit := do
+  modifyEnv fun env => matchEqnsExt.modifyState env fun { map, eqns } => {
+    eqns := matchEqns.eqnNames.foldl (init := eqns) fun eqns eqn => eqns.insert eqn
+    map := map.insert matchDeclName matchEqns
+  }
 
 /-
   Forward definition. We want to use `getEquationsFor` in the simplifier,
  `getEquationsFor` depends on `mkEquationsfor` which uses the simplifier. -/
 @[extern "lean_get_match_equations_for"]
 opaque getEquationsFor (matchDeclName : Name) : MetaM MatchEqns
 
+/--
+Returns `true` if `declName` is the name of a `match` equational theorem.
+-/
+def isMatchEqnTheorem (env : Environment) (declName : Name) : Bool :=
+  matchEqnsExt.getState env |>.eqns.contains declName
+
 end Lean.Meta.Match

tests/lean/run/4251.lean

@@ -0,0 +1,13 @@
+/--
+info: Try this: simp only [ha, Nat.reduceEqDiff, imp_self]
+-/
+#guard_msgs in
+theorem foo₁ (a : Nat) (ha : a = 37) :
+    (match h : a with | 42 => by simp_all | n => n) = 37 := by
+  simp? [ha]
+
+theorem foo₂ (a : Nat) (ha : a = 37) (hb : b = 37)  :
+    (match h : a with | 42 => by simp_all | n => n) = b := by
+  simp only [ha, Nat.reduceEqDiff, imp_self]
+  guard_target =ₛ 37 = b
+  rw [hb]