From c1ad6aa0db6ddf7b93fe992e8b19171eec1ac07c Mon Sep 17 00:00:00 2001
From: Kim Morrison <477956+kim-em@users.noreply.github.com>
Date: Sat, 14 Feb 2026 07:41:12 +1100
Subject: [PATCH] fix: disable order and funCC modules in NoopConfig (#11744)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR fixes a bug where `lia` was incorrectly solving goals involving
ordered types like `Rat` that it shouldn't handle. The `lia` tactic is
intended for linear integer arithmetic only.

The fix adds `order := false` and `funCC := false` to `NoopConfig`,
which is the base configuration for `CutsatConfig` (used by `lia`).

Closes
https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/releases.20of.20new.20Lean.20versions/near/564688881

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
---
 src/Init/Grind/Config.lean           | 20 +++++++++++++++
 src/Init/Grind/Tactics.lean          | 16 ++++++++++++
 src/Lean/Elab/Tactic/Grind/Main.lean | 12 +++++++++
 tests/lean/run/lia_order_bug.lean    | 38 ++++++++++++++++++++++++++++
 tests/lean/run/string_pos_grind.lean |  5 +++-
 5 files changed, 90 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/lia_order_bug.lean

diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean
index 2981d2ecb4..44516ee0e2 100644
--- a/src/Init/Grind/Config.lean
+++ b/src/Init/Grind/Config.lean
@@ -247,12 +247,14 @@ structure NoopConfig extends Config where
   extAll    := false
   etaStruct := false
   funext    := false
+  funCC     := false
 
   -- Disable all solver modules
   ring      := false
   linarith  := false
   lia       := false
   ac        := false
+  order     := false
 
 /--
 A `grind` configuration that only uses `cutsat` and splitting.
@@ -266,6 +268,24 @@ structure CutsatConfig extends NoopConfig where
   -- Allow the default number of splits.
   splits := ({} : Config).splits
 
+/--
+A `grind` configuration that only uses `linarith`.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure LinarithConfig extends NoopConfig where
+  linarith := true
+  -- Allow the default number of splits.
+  splits := ({} : Config).splits
+
+/--
+A `grind` configuration that only uses `order`.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure OrderConfig extends NoopConfig where
+  order := true
+  -- Allow the default number of splits.
+  splits := ({} : Config).splits
+
 /--
 A `grind` configuration that only uses `ring`.
 -/
diff --git a/src/Init/Grind/Tactics.lean b/src/Init/Grind/Tactics.lean
index 1ca0f48ba9..0f0f95f267 100644
--- a/src/Init/Grind/Tactics.lean
+++ b/src/Init/Grind/Tactics.lean
@@ -313,6 +313,22 @@ Please use `grind` instead if you need additional capabilities.
 -/
 syntax (name := lia) "lia" optConfig : tactic
 
+/--
+`grind_order` solves simple goals about partial orders and linear orders.
+
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `order` solver.
+Please use `grind` instead if you need additional capabilities.
+-/
+syntax (name := grind_order) "grind_order" optConfig : tactic
+
+/--
+`grind_linarith` solves simple goals about linear arithmetic.
+
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `linarith` solver.
+Please use `grind` instead if you need additional capabilities.
+-/
+syntax (name := grind_linarith) "grind_linarith" optConfig : tactic
+
 /--
 `grobner` solves goals that can be phrased as polynomial equations (with further polynomial equations as hypotheses)
 over commutative (semi)rings, using the Grobner basis algorithm.
diff --git a/src/Lean/Elab/Tactic/Grind/Main.lean b/src/Lean/Elab/Tactic/Grind/Main.lean
index 82ef77bb06..ee4971b812 100644
--- a/src/Lean/Elab/Tactic/Grind/Main.lean
+++ b/src/Lean/Elab/Tactic/Grind/Main.lean
@@ -20,6 +20,8 @@ open Meta
 declare_config_elab elabGrindConfig Grind.Config
 declare_config_elab elabGrindConfigInteractive Grind.ConfigInteractive
 declare_config_elab elabCutsatConfig Grind.CutsatConfig
+declare_config_elab elabLinarithConfig Grind.LinarithConfig
+declare_config_elab elabOrderConfig Grind.OrderConfig
 declare_config_elab elabGrobnerConfig Grind.GrobnerConfig
 
 open Command Term in
@@ -420,6 +422,16 @@ def evalGrindTraceCore (stx : Syntax) (trace := true) (verbose := true) (useSorr
   let config ← elabCutsatConfig config
   evalGrindCore stx { config with } none none none
 
+@[builtin_tactic Lean.Parser.Tactic.grind_order] def evalOrder : Tactic := fun stx => do
+  let `(tactic| grind_order $config:optConfig) := stx | throwUnsupportedSyntax
+  let config ← elabOrderConfig config
+  evalGrindCore stx { config with } none none none
+
+@[builtin_tactic Lean.Parser.Tactic.grind_linarith] def evalLinarith : Tactic := fun stx => do
+  let `(tactic| grind_linarith $config:optConfig) := stx | throwUnsupportedSyntax
+  let config ← elabLinarithConfig config
+  evalGrindCore stx { config with } none none none
+
 @[builtin_tactic Lean.Parser.Tactic.grobner] def evalGrobner : Tactic := fun stx => do
   let `(tactic| grobner $config:optConfig) := stx | throwUnsupportedSyntax
   let config ← elabGrobnerConfig config
diff --git a/tests/lean/run/lia_order_bug.lean b/tests/lean/run/lia_order_bug.lean
new file mode 100644
index 0000000000..228fe9401f
--- /dev/null
+++ b/tests/lean/run/lia_order_bug.lean
@@ -0,0 +1,38 @@
+/-!
+# Test that `lia` does not use the order module
+
+The `lia` tactic is for linear integer arithmetic only.
+It should not solve rational number inequalities that require the order module.
+-/
+
+-- This should fail: lia should not handle rational inequalities
+/--
+error: `grind` failed
+case grind
+k : Rat
+hk : 2 ≤ k
+h : ¬1 ≤ k
+⊢ False
+[grind] Goal diagnostics
+  [facts] Asserted facts
+    [prop] 2 ≤ k
+    [prop] ¬1 ≤ k
+  [eqc] True propositions
+    [prop] 2 ≤ k
+  [eqc] False propositions
+    [prop] 1 ≤ k
+  [limits] Thresholds reached
+    [limit] maximum number of E-matching rounds has been reached, threshold: `(ematch := 0)`
+-/
+#guard_msgs in
+example (k : Rat) (hk : 2 ≤ k) : 1 ≤ k := by lia
+
+example (k : Rat) (hk : 2 ≤ k) : 1 ≤ k := by lia +order
+
+example (k : Rat) (hk : 2 ≤ k) : 1 ≤ k := by grind_order
+
+-- This should still work: natural number inequalities are handled by lia
+example (k : Nat) (hk : 2 ≤ k) : 1 ≤ k := by lia
+
+-- This should still work with explicit -order flag (no change in behavior)
+example (k : Nat) (hk : 2 ≤ k) : 1 ≤ k := by lia -order
diff --git a/tests/lean/run/string_pos_grind.lean b/tests/lean/run/string_pos_grind.lean
index e16af5a59e..cd6dea144e 100644
--- a/tests/lean/run/string_pos_grind.lean
+++ b/tests/lean/run/string_pos_grind.lean
@@ -1,7 +1,10 @@
 module
 
 example {p q r : String.Pos.Raw} : p < q → q ≤ r → p < r := by
-  lia
+  grind_order
+
+example {p q r : String.Pos.Raw} : p < q → q ≤ r → p < r := by
+  lia +order
 
 example {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by
   lia