fix: internalize nested ground patterns when activating ematch theore…

…ms (#6478)

This PR internalize nested ground patterns when activating ematch
theorems in the (WIP) `grind` tactic.

src/Lean/Meta/Tactic/Grind.lean

@@ -37,5 +37,6 @@ builtin_initialize registerTraceClass `grind.congr
 builtin_initialize registerTraceClass `grind.proof
 builtin_initialize registerTraceClass `grind.proof.detail
 builtin_initialize registerTraceClass `grind.pattern
+builtin_initialize registerTraceClass `grind.internalize
 
 end Lean

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

@@ -67,22 +67,25 @@ private def isForbidden (declName : Name) := forbiddenDeclNames.contains declNam
 
 private def dontCare := mkConst (Name.mkSimple "[grind_dontcare]")
 
-private def mkGroundPattern (e : Expr) : Expr :=
+def mkGroundPattern (e : Expr) : Expr :=
   mkAnnotation `grind.ground_pat e
 
-private def groundPattern? (e : Expr) : Option Expr :=
+def groundPattern? (e : Expr) : Option Expr :=
   annotation? `grind.ground_pat e
 
 private def isGroundPattern (e : Expr) : Bool :=
   groundPattern? e |>.isSome
 
+def isPatternDontCare (e : Expr) : Bool :=
+  e == dontCare
+
 private def isAtomicPattern (e : Expr) : Bool :=
-  e.isBVar || e == dontCare || isGroundPattern e
+  e.isBVar || isPatternDontCare e || isGroundPattern e
 
 partial def ppPattern (pattern : Expr) : MessageData := Id.run do
   if let some e := groundPattern? pattern then
     return m!"`[{e}]"
-  else if pattern == dontCare then
+  else if isPatternDontCare pattern then
     return m!"?"
   else match pattern with
     | .bvar idx => return m!"#{idx}"

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

@@ -7,6 +7,7 @@ prelude
 import Init.Grind.Util
 import Lean.Meta.LitValues
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Util
 
 namespace Lean.Meta.Grind
 
@@ -37,7 +38,19 @@ private def updateAppMap (e : Expr) : GoalM Unit := do
       s.appMap.insert key [e]
   }
 
-private def activateTheoremPatterns (fName : Name) : GoalM Unit := do
+mutual
+/-- Internalizes the nested ground terms in the given pattern. -/
+private partial def internalizePattern (pattern : Expr) (generation : Nat) : GoalM Expr := do
+  if pattern.isBVar || isPatternDontCare pattern then
+    return pattern
+  else if let some e := groundPattern? pattern then
+    let e ← shareCommon (← canon (← normalizeLevels (← unfoldReducible e)))
+    internalize e generation
+    return mkGroundPattern e
+  else pattern.withApp fun f args => do
+    return mkAppN f (← args.mapM (internalizePattern · generation))
+
+private partial def activateTheoremPatterns (fName : Name) (generation : Nat) : GoalM Unit := do
   if let some thms := (← get).thmMap.find? fName then
     modify fun s => { s with thmMap := s.thmMap.erase fName }
     let appMap := (← get).appMap
@@ -47,13 +60,15 @@ private def activateTheoremPatterns (fName : Name) : GoalM Unit := do
       match symbols with
       | [] =>
         trace[grind.pattern] "activated `{thm.origin.key}`"
+        let thm := { thm with patterns := (← thm.patterns.mapM (internalizePattern · generation)) }
         modify fun s => { s with newThms := s.newThms.push thm }
       | _ =>
         trace[grind.pattern] "reinsert `{thm.origin.key}`"
         modify fun s => { s with thmMap := s.thmMap.insert thm }
 
 partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
   if (← alreadyInternalized e) then return ()
+  trace[grind.internalize] "{e}"
   match e with
   | .bvar .. => unreachable!
   | .sort .. => return ()
@@ -79,7 +94,7 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
         registerParent e c
       else
         if let .const fName _ := f then
-          activateTheoremPatterns fName
+          activateTheoremPatterns fName generation
         else
           internalize f generation
           registerParent e f
@@ -91,5 +106,6 @@ partial def internalize (e : Expr) (generation : Nat) : GoalM Unit := do
       addCongrTable e
       updateAppMap e
       propagateUp e
+end
 
 end Lean.Meta.Grind

tests/lean/run/grind_pattern2.lean

@@ -37,3 +37,37 @@ example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
         ¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by
   fail_if_success grind
   sorry
+
+def a := 10
+def b := 20
+def foo (x : List Nat) (y : List Nat) := x ++ y ++ x
+
+theorem fooThm : foo x [a, b] = x ++ [a, b] ++ x := rfl
+
+/--
+info: [grind.pattern] fooThm: [foo #0 `[[a, b]]]
+-/
+#guard_msgs in
+grind_pattern fooThm => foo x [a, b]
+
+
+/--
+warning: declaration uses 'sorry'
+---
+info: [grind.internalize] foo x y
+[grind.pattern] activated `fooThm`
+[grind.internalize] [a, b]
+[grind.internalize] Nat
+[grind.internalize] a
+[grind.internalize] [b]
+[grind.internalize] b
+[grind.internalize] []
+[grind.internalize] x
+[grind.internalize] y
+[grind.internalize] z
+-/
+#guard_msgs in
+set_option trace.grind.internalize true in
+example : foo x y = z → False := by
+  fail_if_success grind
+  sorry