fix: theorems without parameters in grind E-matching (#11604)

This PR fixes how theorems without parameters are handled in `grind`.

This is a better fix than #11579

---------

Co-authored-by: Kim Morrison <[email protected]>

Author: leodemoura

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

@@ -865,9 +865,15 @@ private def matchEqBwdPat (p : Expr) : M Unit := do
     if isSameExpr n.next false then return ()
     curr := n.next
 
+def instantiateGroundTheorem (thm : EMatchTheorem) : M Unit := do
+  if (← markTheoremInstance thm.proof #[]) then
+    addNewInstance thm thm.proof 0 []
+
 def ematchTheorem (thm : EMatchTheorem) : M Unit := do
   if (← checkMaxInstancesExceeded) then return ()
-  withReader (fun ctx => { ctx with thm }) do
+  if thm.numParams == 0 then
+    instantiateGroundTheorem thm
+  else withReader (fun ctx => { ctx with thm }) do
     let ps := thm.patterns
     match ps, (← read).useMT with
     | [p],   _     => if isEqBwdPattern p then matchEqBwdPat p else main p []
@@ -909,7 +915,8 @@ private def ematchCore (extraThms : Array EMatchTheorem) : GoalM InstanceMap :=
   else
     let (_, s) ← go (← get).ematch.thms (← get).ematch.newThms |>.run
     modify fun s => { s with
-      ematch.thms      := s.ematch.thms ++ s.ematch.newThms
+      -- **Note**: Ground theorems should be instantiated once. So, we filter them.
+      ematch.thms      := s.ematch.thms ++ (s.ematch.newThms.filter fun thm => thm.numParams > 0)
       ematch.newThms   := {}
       ematch.gmt       := s.ematch.gmt + 1
       ematch.num       := s.ematch.num + 1

tests/lean/run/grind_ctor_ematch.lean

@@ -24,11 +24,13 @@ h : ¬Even 16
   [facts] Asserted facts
     [prop] ¬Even 16
     [prop] Even 14 → Even 16
+    [prop] Even 0
     [prop] Even 12 → Even 14
     [prop] Even 10 → Even 12
     [prop] Even 8 → Even 10
     [prop] Even 6 → Even 8
   [eqc] True propositions
+    [prop] Even 0
     [prop] Even 14 → Even 16
     [prop] Even 12 → Even 14
     [prop] Even 10 → Even 12
@@ -43,12 +45,12 @@ h : ¬Even 16
     [prop] Even 6
   [ematch] E-matching patterns
     [thm] Even.plus_two: [Even (#1 + 2)]
-    [thm] Even.zero: [Even `[0]]
   [limits] Thresholds reached
     [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 5)`
 [grind] Diagnostics
   [thm] E-Matching instances
     [thm] Even.plus_two ↦ 5
+    [thm] Even.zero ↦ 1
 -/
 #guard_msgs (error) in
 example : Even 16 := by

tests/lean/run/grind_eq.lean

@@ -18,6 +18,7 @@ set_option trace.grind.assert true
 trace: [grind.assert] f (y + 1) = a
 [grind.assert] ¬a = g (f y)
 [grind.ematch.instance] f.eq_2: f y.succ = g (f y)
+[grind.ematch.instance] f.eq_1: f 0 = 10
 [grind.assert] f (y + 1) = g (f y)
 -/
 #guard_msgs (trace) in

tests/lean/run/grind_ground_thm.lean

@@ -0,0 +1,52 @@
+opaque π : Rat
+axiom pi_pos : 0 < π
+
+theorem two_pi_pos : 0 < 2 * π := by
+  grind [pi_pos]
+
+/--
+info: Try these:
+  [apply] grind only [pi_pos]
+  [apply] grind =>
+    instantiate only [pi_pos]
+    linarith
+-/
+#guard_msgs in
+theorem two_pi_pos' : 0 < 2 * π := by
+  grind? [pi_pos]
+
+attribute [grind .] pi_pos
+
+theorem two_pi_pos'' : 0 < 2 * π := by
+  grind
+
+/--
+info: Try these:
+  [apply] grind only [pi_pos]
+  [apply] grind =>
+    instantiate only [pi_pos]
+    linarith
+-/
+#guard_msgs in
+theorem two_pi_pos''' : 0 < 2 * π := by
+  grind?
+
+def f (x : Nat) := x
+
+-- Should not instantiate/activate pi_pos
+/--
+trace: [grind.ematch] activated `f.eq_1`, [f #0]
+[grind.ematch.instance] f.eq_1: f x = x
+-/
+#guard_msgs (drop error, trace) in
+example : 1 < x → 2 < f x := by
+  set_option trace.grind.ematch true in
+  set_option trace.grind.ematch.instance true in
+  grind [f]
+
+-- Should instantiate/activate pi_pos
+/-- trace: [grind.ematch] activated `pi_pos`, [@LT.lt `[Rat] `[Rat.instLT] `[0] `[π]] -/
+#guard_msgs in
+example : π < x → 0 < x := by
+  set_option trace.grind.ematch true in
+  grind