From 097931bb4ce5a9e41c1199660019a5133470c1fb Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 20 Dec 2025 12:00:27 +1100 Subject: [PATCH 1/2] fix: disable order and funCC modules in NoopConfig 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 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 --- src/Init/Grind/Config.lean | 2 ++ tests/lean/run/lia_order_bug.lean | 36 ++++++++++++++++++++++++++++ tests/lean/run/string_pos_grind.lean | 2 +- 3 files changed, 39 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 49047bcb65b4..c90c8aec57d9 100644 --- a/src/Init/Grind/Config.lean +++ b/src/Init/Grind/Config.lean @@ -240,12 +240,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. diff --git a/tests/lean/run/lia_order_bug.lean b/tests/lean/run/lia_order_bug.lean new file mode 100644 index 000000000000..c1b0263aa1a3 --- /dev/null +++ b/tests/lean/run/lia_order_bug.lean @@ -0,0 +1,36 @@ +/-! +# 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 + +-- 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 e16af5a59e83..9eb9e2ebf511 100644 --- a/tests/lean/run/string_pos_grind.lean +++ b/tests/lean/run/string_pos_grind.lean @@ -1,7 +1,7 @@ module example {p q r : String.Pos.Raw} : p < q → q ≤ r → p < r := by - lia + lia +order example {s : String} {p q r : s.Pos} : p < q → q ≤ r → p < r := by lia From 4dc5d8d38fe3ca2e4be2d3aac474231debaef615 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 20 Dec 2025 12:34:33 +1100 Subject: [PATCH 2/2] add grind_order and grind_linarith wrappers while we're here --- src/Init/Grind/Config.lean | 18 ++++++++++++++++++ src/Init/Grind/Tactics.lean | 16 ++++++++++++++++ src/Lean/Elab/Tactic/Grind/Main.lean | 12 ++++++++++++ tests/lean/run/lia_order_bug.lean | 2 ++ tests/lean/run/string_pos_grind.lean | 3 +++ 5 files changed, 51 insertions(+) diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean index c90c8aec57d9..ad43a3bdcee7 100644 --- a/src/Init/Grind/Config.lean +++ b/src/Init/Grind/Config.lean @@ -261,6 +261,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 de5ecc74de40..28e1acad1855 100644 --- a/src/Init/Grind/Tactics.lean +++ b/src/Init/Grind/Tactics.lean @@ -314,6 +314,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 6b2846433de9..701982652280 100644 --- a/src/Lean/Elab/Tactic/Grind/Main.lean +++ b/src/Lean/Elab/Tactic/Grind/Main.lean @@ -27,6 +27,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 @@ -400,6 +402,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 index c1b0263aa1a3..228fe9401f5a 100644 --- a/tests/lean/run/lia_order_bug.lean +++ b/tests/lean/run/lia_order_bug.lean @@ -29,6 +29,8 @@ 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 diff --git a/tests/lean/run/string_pos_grind.lean b/tests/lean/run/string_pos_grind.lean index 9eb9e2ebf511..cd6dea144eec 100644 --- a/tests/lean/run/string_pos_grind.lean +++ b/tests/lean/run/string_pos_grind.lean @@ -1,5 +1,8 @@ module +example {p q r : String.Pos.Raw} : p < q → q ≤ r → p < r := by + grind_order + example {p q r : String.Pos.Raw} : p < q → q ≤ r → p < r := by lia +order