diff --git a/src/Init/Grind/Config.lean b/src/Init/Grind/Config.lean index 49047bcb65b4..ad43a3bdcee7 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. @@ -259,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 new file mode 100644 index 000000000000..228fe9401f5a --- /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 e16af5a59e83..cd6dea144eec 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