fix: grind ematch theorem activation issue (#7861)

This PR fixes an issue that prevented theorems from being activated in
`grind`.

src/Lean/Meta/Tactic/Grind.lean

@@ -74,5 +74,7 @@ builtin_initialize registerTraceClass `grind.debug.mbtc
 builtin_initialize registerTraceClass `grind.debug.ematch
 builtin_initialize registerTraceClass `grind.debug.proveEq
 builtin_initialize registerTraceClass `grind.debug.pushNewFact
+builtin_initialize registerTraceClass `grind.debug.ematch.activate
+builtin_initialize registerTraceClass `grind.debug.appMap
 
 end Lean

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -42,6 +42,7 @@ adds entry `f ↦ e` to `appMap`. Recall that `appMap` is a multi-map.
 -/
 private def updateAppMap (e : Expr) : GoalM Unit := do
   let key := e.toHeadIndex
+  trace_goal[grind.debug.appMap] "{e} => {repr key}"
   modify fun s => { s with
     appMap := if let some es := s.appMap.find? key then
       s.appMap.insert key (e :: es)
@@ -168,13 +169,16 @@ private def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Un
     modify fun s => { s with ematch.thmMap := thmMap }
     let appMap := (← get).appMap
     for thm in thms do
+      trace[grind.debug.ematch.activate] "`{fName}` => `{thm.origin.key}`"
       unless (← get).ematch.thmMap.isErased thm.origin do
         let symbols := thm.symbols.filter fun sym => !appMap.contains sym
         let thm := { thm with symbols }
         match symbols with
-        | [] => activateTheorem thm generation
+        | [] =>
+          trace_goal[grind.debug.ematch.activate] "`{thm.origin.key}`"
+          activateTheorem thm generation
         | _ =>
-          trace_goal[grind.ematch] "reinsert `{thm.origin.key}`"
+          trace_goal[grind.debug.ematch.activate] "reinsert `{thm.origin.key}`"
           modify fun s => { s with ematch.thmMap := s.ematch.thmMap.insert thm }
 
 /--
@@ -256,6 +260,7 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
       internalizeMatchCond e generation
     else e.withApp fun f args => do
       mkENode e generation
+      updateAppMap e
       checkAndAddSplitCandidate e
       pushCastHEqs e
       addMatchEqns f generation
@@ -280,7 +285,6 @@ private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Opt
           internalize arg generation e
           registerParent e arg
       addCongrTable e
-      updateAppMap e
       Arith.internalize e parent?
       propagateUp e
       propagateBetaForNewApp e

tests/lean/run/grind_ematch_theorem_activation.lean

@@ -0,0 +1,13 @@
+reset_grind_attrs%
+set_option grind.warning false
+
+attribute [grind] List.length_set
+attribute [grind →] List.eq_nil_of_length_eq_zero
+attribute [grind] List.getElem_set
+
+open List in
+example {as : List α} {i : Nat} (h : i < as.length) :
+    as.set i as[i] = as := by
+  apply ext_getElem
+  · sorry
+  · grind

tests/lean/run/grind_erase_attr.lean

@@ -14,8 +14,6 @@ set_option trace.grind.assert true
 
 /--
 info: [grind.assert] ¬f (f (f a)) = f a
-[grind.assert] f (f (f (f a))) = f (f (f a))
-[grind.assert] f (f (f a)) = f (f a)
 [grind.assert] f (f a) = f a
 -/
 #guard_msgs (info) in

tests/lean/run/grind_pattern2.lean

@@ -22,10 +22,7 @@ example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
         s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
   grind
 
-/--
-info: [grind.ematch] reinsert `contains_insert`
-[grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0]
--/
+/-- info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/
 #guard_msgs (info) in
 example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
         ¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by

tests/lean/run/grind_usr.lean

@@ -14,9 +14,9 @@ example : f (f (f x)) = f x := by
   grind only [fthm]
 
 /--
-info: [grind.ematch.instance] fthm: f (f (f (f x))) = f (f (f x))
+info: [grind.ematch.instance] fthm: f (f x) = f x
 [grind.ematch.instance] fthm: f (f (f x)) = f (f x)
-[grind.ematch.instance] fthm: f (f x) = f x
+[grind.ematch.instance] fthm: f (f (f (f x))) = f (f (f x))
 -/
 #guard_msgs (info) in
 set_option trace.grind.ematch.instance true in