feat: cutsat and grobner frontends for grind

src/Init/Grind/Tactics.lean

@@ -126,6 +126,52 @@ structure Config where
   abstractProof := true
   deriving Inhabited, BEq
 
+/--
+A minimal configuration, with ematching and splitting disabled, and all solver modules turned off.
+`grind` will not do anything in this configuration,
+which can be used a starting point for minimal configurations.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure NoopConfig extends Config where
+  -- Disable splitting
+  splits := 0
+  -- We don't override the various `splitMatch` / `splitIte` settings separately.
+
+  -- Disable e-matching
+  ematch := 0
+  -- We don't override `matchEqs` separately.
+
+  -- Disable extensionality
+  ext       := false
+  extAll    := false
+  etaStruct := false
+  funext    := false
+
+  -- Disable all solver modules
+  ring      := false
+  linarith  := false
+  cutsat    := false
+  ac        := false
+
+/--
+A `grind` configuration that only uses `cutsat` and splitting.
+
+Note: `cutsat` benefits from some amount of instantiation, e.g. `Nat.max_def`.
+We don't currently have a mechanism to enable only a small set of lemmas.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure CutsatConfig extends NoopConfig where
+  cutsat := true
+  -- Allow the default number of splits.
+  splits := ({} : Config).splits
+
+/--
+A `grind` configuration that only uses `ring`.
+-/
+-- This is a `structure` rather than `def` so we can use `declare_config_elab`.
+structure GrobnerConfig extends NoopConfig where
+  ring := true
+
 end Lean.Grind
 
 namespace Lean.Parser.Tactic
@@ -420,6 +466,23 @@ syntax (name := grindTrace)
   (" [" withoutPosition(grindParam,*) "]")?
   (&" on_failure " term)? : tactic
 
+/--
+`cutsat` solves linear integer arithmetic goals.
+
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `cutsat` solver.
+Please use `grind` instead if you need additional capabilities.
+-/
+syntax (name := cutsat) "cutsat" 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.
+
+It is a implemented as a thin wrapper around the `grind` tactic, enabling only the `grobner` solver.
+Please use `grind` instead if you need additional capabilities.
+-/
+syntax (name := grobner) "grobner" optConfig : tactic
+
 /-!
 Sets symbol priorities for the E-matching pattern inference procedure used in `grind`
 -/

src/Lean/Elab/Tactic/Grind.lean

@@ -22,6 +22,8 @@ namespace Lean.Elab.Tactic
 open Meta
 
 declare_config_elab elabGrindConfig Grind.Config
+declare_config_elab elabCutsatConfig Grind.CutsatConfig
+declare_config_elab elabGrobnerConfig Grind.GrobnerConfig
 
 open Command Term in
 @[builtin_command_elab Lean.Parser.Command.grindPattern]
@@ -317,4 +319,18 @@ def mkGrindOnly
     Tactic.TryThis.addSuggestion tk stx (origSpan? := ← getRef)
   | _ => throwUnsupportedSyntax
 
+@[builtin_tactic Lean.Parser.Tactic.cutsat] def evalCutsat : Tactic := fun stx => do
+  match stx with
+  | `(tactic| cutsat $config:optConfig) =>
+    let config ← elabCutsatConfig config
+    discard <| evalGrindCore stx { config with } none none none
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.grobner] def evalGrobner : Tactic := fun stx => do
+  match stx with
+  | `(tactic| grobner $config:optConfig) =>
+    let config ← elabGrobnerConfig config
+    discard <| evalGrindCore stx { config with } none none none
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic

tests/lean/run/grind_cutsat_tests.lean

@@ -1,3 +1,6 @@
+-- In this file we use the `cutsat` frontend for `grind`,
+-- as a minimal test that it is working.
+
 module
 example (w x y z : Int) :
   2*w + 3*x - 4*y + z = 10 →
@@ -5,7 +8,7 @@ example (w x y z : Int) :
   3*w - 2*x + y + z = 7 →
   4*w + x - y - z = 3 →
   w = 2 := by
-grind
+cutsat
 
 abbrev test1 (a b c d e : Int) :=
   1337*a + 424242*b - 23*c + 17*d - 101*e ≤ 12345 →
@@ -23,7 +26,7 @@ trace: [grind.cutsat.model] a := 101
 #guard_msgs (trace) in
 set_option trace.grind.cutsat.model true in
 example (a b c d e : Int) : test1 a b c d e  := by
-  (fail_if_success grind); sorry
+  (fail_if_success cutsat); sorry
 
 /-- info: false -/
 #guard_msgs (info) in
@@ -35,7 +38,7 @@ example : ∀ (x y z : Int),
     4*z + 2*x ≤ 300 →
     x ≥ 0 → y ≥ 0 → z ≥ 0 →
     x + y + z ≤ 150 := by
-  grind
+  cutsat
 
 example : ∀ (x y : Int),
     x > 0 →
@@ -45,7 +48,7 @@ example : ∀ (x y : Int),
     y ≤ 100 →
     2*x + 3*y = 47 →
     x = 22 ∨ x = 16 ∨ x = 10 ∨ x = 4 := by
-  grind
+  cutsat
 
 example : ∀ (x y : Int),
     x + y ≤ 10 →
@@ -53,19 +56,19 @@ example : ∀ (x y : Int),
     3*x - y ≤ 30 →
     x - 2*y ≥ -15 →
     x = 9 ∨ x = 10 := by
-  grind
+  cutsat
 
 example : ∀ (x y z : Int),
   ¬(2*x + 3*y + 4*z ≤ 100 ∧
     3*x + 4*y + 5*z ≥ 101 ∧
     x + y + z = 50 ∧ x ≠ 50 ∧
     x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0) := by
-  grind
+  cutsat
 
 example : ∀ (x y : Int),
     2*x + 3*y = 100 →
     x + y = 40 → x = y := by
-  grind
+  cutsat
 
 example : ∀ (x y z : Int),
     3 * x + 5 * y + 7 * z = 100 →
@@ -73,7 +76,7 @@ example : ∀ (x y z : Int),
     x + y + z ≤ 30 →
     x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 →
     z ≤ 15 := by
-  grind
+  cutsat
 
 example : ∀ (x y z : Int),
     2 * x + 3 * y + 4 * z = 100 →
@@ -81,7 +84,7 @@ example : ∀ (x y z : Int),
     x + y + z ≤ 40 →
     x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 →
     z ≥ 10 := by
-  grind
+  cutsat
 
 example : ∀ (x y z : Int),
     x / 4 + y / 3 = 50 →
@@ -90,7 +93,7 @@ example : ∀ (x y z : Int),
     x + y + z = 200 →
     x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 →
     z ≤ 50 := by
-  grind
+  cutsat
 
 example : ∀ (x : Int),
     x ≥ 0 →
@@ -98,31 +101,41 @@ example : ∀ (x : Int),
     x % 3 = 2 →
     x % 5 = 3 →
     x ≥ 23 := by
-  grind
+  cutsat
 
 example : ∀ (x : Int),
     x / 5 ≥ 20 →
     x % 5 = 3 →
     x ≥ 103 := by
-  grind
+  cutsat
 
 example : ∀ (x y z : Int),
     z > 0 →
     x + y + z = 100 →
     y = 2 * x →
     x ≤ 33 := by
-  grind
+  cutsat
 
 example : ∀ (x y : Int),
     2 * x + 3 * y ≤ 10 →
     x + y ≤ 5 →
     x ≥ 0 → y ≥ 0 →
     x + y ≤ 5 := by
-  grind
+  cutsat
 
-example  (x : Int) : x / 1 = x := by grind
-example (x : Int) : x % 1 = 0 := by grind
-example  (x : Nat) : x / 1 = x := by grind
-example (x : Nat) : x % 1 = 0 := by grind
-example  (x : Int) : x / -1 = -x := by grind
-example (x : Int) : x % -1 = 0 := by grind
+example  (x : Int) : x / 1 = x := by cutsat
+example (x : Int) : x % 1 = 0 := by cutsat
+example  (x : Nat) : x / 1 = x := by cutsat
+example (x : Nat) : x % 1 = 0 := by cutsat
+example  (x : Int) : x / -1 = -x := by cutsat
+example (x : Int) : x % -1 = 0 := by cutsat
+
+-- Verify that `cutsat` will not use the ring solver.
+example (x : Int) (h : x^2 = 0) : x^3 = 0 := by
+  fail_if_success cutsat
+  grobner
+
+-- Verify that `cutsat` will not instantiate theorems.
+example {xs ys zs : List α} : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
+  fail_if_success cutsat
+  grind

tests/lean/run/grind_ring_2.lean

@@ -1,70 +1,71 @@
+-- In this file we use the `grobner` frontend for `grind`.
 module
 set_option grind.debug true
 open Lean.Grind
 
 example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind
+  grobner
 
 example [CommRing α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  fail_if_success grind
+  fail_if_success grobner
   sorry
 
 example [CommRing α] (x y : α) : x = 1 → y = 2 → 2*x + y = 4 := by
-  grind
+  grobner
 
 example [CommRing α] [IsCharP α 7] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind
+  grobner
 
 example [CommRing α] [IsCharP α 7] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
-  grind
+  grobner
 
 example [CommRing α] [IsCharP α 8] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
-  fail_if_success grind
+  fail_if_success grobner
   sorry
 
 example [CommRing α] [IsCharP α 8] [NoNatZeroDivisors α] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
-  grind
+  grobner
 
 example (x y : UInt8) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind
+  grobner
 
 example (x y : UInt8) : 3*x = 1 → 3*y = 2 → False := by
-  fail_if_success grind
+  fail_if_success grobner
   sorry
 
 example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 6*x = 1 → 3*y = 2 → 2*x + y = 1 := by
-  grind
+  grobner
 
 example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 600000*x = 1 → 300*y = 2 → 200000*x + 100*y = 1 := by
-  grind
+  grobner
 
 example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
-  grind
+  grobner
 
 example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
-  grind
+  grobner
 
 example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by
-  grind
+  grobner
 
 example [CommRing α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
-  grind
+  grobner
 
 example (x y : BitVec 16) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
-  grind
+  grobner
 
 example [CommRing α] (x y : α) (f : α → Nat) : x^2*y = 1 → x*y^2 = y → f (y*x) = f 1 := by
-  grind
+  grobner
 
 example [CommRing α] (x y : α) (f : α → Nat) : x^2*y = 1 → x*y^2 - y = 0 → f (y*x) = f (y*x*y) := by
-  grind
+  grobner
 
 example [CommRing α] (a b c : α)
   : a + b + c = 3 →
     a^2 + b^2 + c^2 = 5 →
     a^3 + b^3 + c^3 = 7 →
     a^4 + b^4 + c^4 = 9 := by
-  grind
+  grobner
 
 /--
 trace: [grind.ring.assert.basis] a + b + c + -3 = 0
@@ -78,7 +79,7 @@ example [CommRing α] (a b c : α)
     a^3 + b^3 + c^3 = 7 →
     a^4 + b^4 = 9 - c^4 := by
   set_option trace.grind.ring.assert.basis true in
-  grind
+  grobner
 
 /--
 trace: [grind.ring.assert.basis] a + b + c + -3 = 0
@@ -92,64 +93,88 @@ example [CommRing α] [NoNatZeroDivisors α] (a b c : α)
     a^3 + b^3 + c^3 = 7 →
     a^4 + b^4 = 9 - c^4 := by
   set_option trace.grind.ring.assert.basis true in
-  grind
+  grobner
 
 example [CommRing α] (a b : α) (f : α → Nat) : a - b = 0 → f a = f b := by
-  grind
+  grobner
 
 example (a b : BitVec 8) (f : BitVec 8 → Nat) : a - b = 0 → f a = f b := by
-  grind
+  grobner
 
 example (a b c : BitVec 8) (f : BitVec 8 → Nat) : c = 255 → - a + b - 1 = c → f a = f b := by
-  grind
+  grobner
 
 example (a b c : BitVec 8) (f : BitVec 8 → Nat) : c = 255 → - a + b - 1 = c → f (2*a) = f (b + a) := by
-  grind
+  grobner
 
 /-- trace: [grind.ring.impEq] skip: b = a, k: 2, noZeroDivisors: false -/
 #guard_msgs (trace) in
 example (a b c : BitVec 8) (f : BitVec 8 → Nat) : 2*a = 1 → 2*b = 1 → f (a) = f (b) := by
   set_option trace.grind.ring.impEq true in
-  fail_if_success grind -cutsat
+  fail_if_success grobner -cutsat
   sorry
 
+-- This one requires the `cutsat` solver as well.
 example (a b c : Int) (f : Int → Nat)
   : a + b + c = 3 →
     a^2 + b^2 + c^2 = 5 →
     a^3 + b^3 + c^3 = 7 →
     f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
-  grind
+  grobner +cutsat
+
+-- Now we check the same example, calling `cutsat` but adding the `ring` solver.
+example (a b c : Int) (f : Int → Nat)
+  : a + b + c = 3 →
+    a^2 + b^2 + c^2 = 5 →
+    a^3 + b^3 + c^3 = 7 →
+    f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
+  cutsat +ring
 
 example [CommRing α] [NoNatZeroDivisors α] (a b c : α) (f : α → Nat)
   : a + b + c = 3 →
     a^2 + b^2 + c^2 = 5 →
     a^3 + b^3 + c^3 = 7 →
     f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
-  grind
+  grobner +cutsat
 
 example [CommRing α] [NoNatZeroDivisors α] (x y z : α) : 3*x = 1 → 3*z = 2 → 2*y = 2 → x + z + 3*y = 4 := by
-  grind
+  grobner
 
 example (x y : Fin 11) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
-  grind
+  grobner
 
 example (x y : Fin 11) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind
+  grobner
 
 example (x y z : Fin 13) :
     (x + y + z) ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 + 2 * (x * y + y * z + z * x) := by
-  grind
+  grobner
 
 example (x y : Fin 17) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x * y * (x + y) := by
-  grind
+  grobner
 
 example (x y : Fin 19) : (x - y) * (x ^ 2 + x * y + y ^ 2) = x ^ 3 - y ^ 3 := by
-  grind
+  grobner
 
 example (x : Fin 19) : (1 + x) ^ 5 = x ^ 5 + 5 * x ^ 4 + 10 * x ^ 3 + 10 * x ^ 2 + 5 * x + 1 := by
-  grind
+  grobner
 
 example (x : Fin 10) : (1 + x) ^ 5 = x ^ 5 + 5 * x ^ 4 - 5 * x + 1 := by
-  grind
+  grobner
 
-example (x y : Fin 3) (h : x = y) : ((x + y) ^ 3 : Fin 3) = - x^3 := by grind
+example (x y : Fin 3) (h : x = y) : ((x + y) ^ 3 : Fin 3) = - x^3 := by grobner
+
+-- Verify that `cutsat` is disabled when calling `grobner` directly.
+example (x : Nat) : x % 2 = 0 ∨ x % 2 = 1 := by
+  fail_if_success grobner
+  cutsat
+
+-- Verify that `grobner` will not perform case splits unless explicitly asked for.
+example (x : Int) (h : x^2 = 0) : (if x > 0 then x else x)^3 = 0 := by
+  fail_if_success grobner
+  grobner (splits := 1)
+
+-- Verify that `grobner` will not instantiate theorems.
+example {xs ys zs : List α} : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by
+  fail_if_success grobner
+  grind