feat: grind use/instantiate only can activate all scoped theorems in a namespace (#11335)

This PR enables the syntax `use [ns Foo]` and `instantiate only [ns
Foo]` inside a `grind` tactic block, and has the effect of activating
all grind patterns scoped to that namespace. We can use this to
implement specialized tactics using `grind`, but only controlled subsets
of theorems.

---------

Co-authored-by: Claude <noreply@anthropic.com>

src/Init/Data/Int/Order.lean

@@ -377,6 +377,15 @@ protected theorem le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1 := by
 
 @[grind =] protected theorem max_def (n m : Int) : max n m = if n ≤ m then m else n := rfl
 
+end Int
+namespace Lean.Meta.Grind.Lia
+
+scoped grind_pattern Int.min_def => min n m
+scoped grind_pattern Int.max_def => max n m
+
+end Lean.Meta.Grind.Lia
+namespace Int
+
 @[simp] protected theorem neg_min_neg (a b : Int) : min (-a) (-b) = -max a b := by
   rw [Int.min_def, Int.max_def]
   simp

src/Init/Grind/Interactive.lean

@@ -72,7 +72,9 @@ syntax (name := linarith) "linarith" : grind
 /-- The `sorry` tactic is a temporary placeholder for an incomplete tactic proof. -/
 syntax (name := «sorry») "sorry" : grind
 
-syntax thm := anchor <|> grindLemmaMin <|> grindLemma
+syntax thmNs := &"namespace" ident
+
+syntax thm := anchor <|> thmNs <|> grindLemmaMin <|> grindLemma
 
 /--
 Instantiates theorems using E-matching.

src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean

@@ -13,6 +13,7 @@ import Lean.Meta.Tactic.Grind.Arith.Linear.Search
 import Lean.Meta.Tactic.Grind.Arith.CommRing.EqCnstr
 import Lean.Meta.Tactic.Grind.AC.Eq
 import Lean.Meta.Tactic.Grind.EMatch
+import Lean.Meta.Tactic.Grind.EMatchTheorem
 import Lean.Meta.Tactic.Grind.PP
 import Lean.Meta.Tactic.Grind.Internalize
 import Lean.Meta.Tactic.Grind.Intro
@@ -152,6 +153,10 @@ def ematchThms (only : Bool) (thms : Array EMatchTheorem) : GrindTacticM Unit :=
   if let some thmRefs := thmRefs? then
     for thmRef in thmRefs do
       match thmRef with
+      | `(Parser.Tactic.Grind.thm| namespace $ns:ident) =>
+        let namespaceName := ns.getId
+        let scopedThms ← Grind.getEMatchTheoremsForNamespace namespaceName
+        thms := thms ++ scopedThms
       | `(Parser.Tactic.Grind.thm| #$anchor:hexnum) => thms := thms ++ (← withRef thmRef <| elabLocalEMatchTheorem anchor)
       | `(Parser.Tactic.Grind.thm| $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id false)
       | `(Parser.Tactic.Grind.thm| ! $[$mod?:grindMod]? $id:ident) => thms := thms ++ (← withRef thmRef <| elabThm mod? id true)

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

@@ -44,7 +44,9 @@ def collectInstantiateParams (params : Syntax.TSepArray `Lean.Parser.Tactic.Grin
       pushParam p
     | `(Lean.Parser.Tactic.Grind.thm| $a:anchor) =>
       pushAnchor a
-    | _ => pure ()
+    | _ =>
+      -- Namespace references (thmNs) are handled elsewhere, skip them
+      pure ()
 
 partial def collect (tac : TGrind) : Collect Unit := do
   match tac with

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

@@ -888,6 +888,13 @@ def addEMatchEqTheorem (declName : Name) : MetaM Unit := do
 def getEMatchTheorems : CoreM EMatchTheorems :=
   return ematchTheoremsExt.getState (← getEnv)
 
+/-- Returns the scoped E-matching theorems declared in the given namespace. -/
+def getEMatchTheoremsForNamespace (namespaceName : Name) : CoreM (Array EMatchTheorem) := do
+  let stateStack := ematchTheoremsExt.ext.getState (← getEnv)
+  match stateStack.scopedEntries.map.find? namespaceName with
+  | none => return #[]
+  | some entries => return entries.toArray
+
 /-- Returns the types of `xs` that are propositions. -/
 private def getPropTypes (xs : Array Expr) : MetaM (Array Expr) :=
   xs.filterMapM fun x => do

tests/lean/run/grind_pattern_scoped.lean

@@ -0,0 +1,16 @@
+import Lean.Meta.Tactic.Grind.EMatchTheorem
+
+open Lean
+open Lean.Meta.Grind
+
+/-- info: Namespace `Lean.Meta.Grind.Lia` has scoped theorems: true -/
+#guard_msgs in
+#eval show CoreM Unit from do
+  let theorems ← getEMatchTheoremsForNamespace `Lean.Meta.Grind.Lia
+  IO.println s!"Namespace `Lean.Meta.Grind.Lia` has scoped theorems: {decide (theorems.size > 0)}"
+
+-- Test namespace-based theorem instantiation
+example (x y : Int) (h : max x y < 7) : x + y < 13 := by
+  grind =>
+    use [namespace Lean.Meta.Grind.Lia]
+    repeat (first (lia) (cases_next))

tests/lean/run/lia_with_cases.lean

@@ -0,0 +1,30 @@
+-- Test that lia now uses grind tactic script with cases_next
+
+-- Basic linear arithmetic - should still work without case-splits
+example (x y : Int) : 2 * x + 4 * y ≠ 5 := by
+  lia
+
+example (x y : Int) : 2 * x + 3 * y = 0 → 1 ≤ x → y < 1 := by
+  lia
+
+example (a b : Int) : 2 ∣ a + 1 → 2 ∣ b + a → ¬ 2 ∣ b + 2 * a := by
+  lia
+
+-- Tests that require case-splitting
+-- These require the `cases_next` to split on hypotheses before lia can solve
+
+-- Case-split on hypothesis, then solve with lia
+example (x : Nat) (h : x = 0 ∨ x = 1) : x ≤ 1 := by
+  lia
+
+-- Multiple nested case-splits
+example (x y : Nat) (h1 : x = 0 ∨ x = 1) (h2 : y = 0 ∨ y = 1) : x + y ≤ 2 := by
+  lia
+
+-- Case-split on if-then-else
+example (x : Int) : (if x > 0 then x else -x) ≥ 0 := by
+  lia
+
+-- Case-split with arithmetic in branches
+example (x : Int) : (if x > 0 then 2*x else 0) ≥ 0 := by
+  lia