test

src/Init/Grind/CommRing/Poly.lean

@@ -42,7 +42,7 @@ def Expr.denote {α} [CommRing α] (ctx : Context α) : Expr → α
 structure Power where
   x : Var
   k : Nat
-  deriving BEq, Repr, Hashable
+  deriving BEq, Repr, Inhabited
 
 instance : LawfulBEq Power where
   eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
@@ -61,7 +61,7 @@ def Power.denote {α} [CommRing α] (ctx : Context α) : Power → α
 inductive Mon where
   | unit
   | mult (p : Power) (m : Mon)
-  deriving BEq, Repr
+  deriving BEq, Repr, Inhabited
 
 instance : LawfulBEq Mon where
   eq_of_beq {a} := by
@@ -181,7 +181,7 @@ def Mon.grevlex (m₁ m₂ : Mon) : Ordering :=
 inductive Poly where
   | num (k : Int)
   | add (k : Int) (v : Mon) (p : Poly)
-  deriving BEq
+  deriving BEq, Inhabited
 
 instance : LawfulBEq Poly where
   eq_of_beq {a} := by

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean

@@ -62,14 +62,85 @@ def Mon.coprime : Mon → Mon → Bool
     | .lt => coprime m₁ (.mult pw₂ m₂)
     | .gt => coprime (.mult pw₁ m₁) m₂
 
-/-- Returns the S-polynomial for `p₁` and `p₂`. -/
-def Poly.superpose (p₁ p₂ : Poly) : Poly :=
+/--
+Contains the S-polynomial resulting from superposing two polynomials `p₁` and `p₂`,
+along with coefficients and monomials used in their construction.
+-/
+structure SPolResult where
+  /-- The computed S-polynomial. -/
+  spol : Poly := .num 0
+  /-- Coefficient applied to polynomial `p₁`. -/
+  c₁   : Int  := 0
+  /-- Monomial factor applied to polynomial `p₁`. -/
+  m₁   : Mon  := .unit
+  /-- Coefficient applied to polynomial `p₂`. -/
+  c₂   : Int  := 0
+  /-- Monomial factor applied to polynomial `p₂`. -/
+  m₂   : Mon  := .unit
+
+/--
+Returns the S-polynomial of polynomials `p₁` and `p₂`, and coefficients&terms used to construct it.
+Given polynomials with leading terms `k₁*m₁` and `k₂*m₂`, the S-polynomial is defined as:
+```
+S(p₁, p₂) = (k₂/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₁) * p₁ - (k₁/gcd(k₁, k₂)) * (lcm(m₁, m₂)/m₂) * p₂
+```
+-/
+def Poly.spol (p₁ p₂ : Poly) : SPolResult  :=
   match p₁, p₂ with
   | .add k₁ m₁ p₁, .add k₂ m₂ p₂ =>
-    let m   := m₁.lcm m₂
-    let p₁  := p₁.mulMon k₂ (m.div m₁)
-    let p₂  := p₂.mulMon (-k₁) (m.div m₂)
-    p₁.combine p₂
-  | _, _ => .num 0
+    let m    := m₁.lcm m₂
+    let m₁   := m.div m₁
+    let m₂   := m.div m₂
+    let g    := Nat.gcd k₁.natAbs k₂.natAbs
+    let c₁   := k₂/g
+    let c₂   := -k₁/g
+    let p₁   := p₁.mulMon c₁ m₁
+    let p₂   := p₂.mulMon c₂ m₂
+    let spol := p₁.combine p₂
+    { spol, c₁, m₁, c₂, m₂ }
+  | _, _ => {}
+
+/--
+Result of simplifying a polynomial `p₂` using a polynomial `p₁`.
+
+The simplification rewrites the first monomial of `p₂` that can be divided
+by the leading monomial of `p₁`.
+-/
+structure SimpResult where
+  /-- The resulting simplified polynomial after rewriting. -/
+  p  : Poly := .num 0
+  /-- The integer coefficient multiplied with polynomial `p₁` in the rewriting step. -/
+  c₁ : Int  := 0
+  /-- The integer coefficient multiplied with polynomial `p₂` during rewriting. -/
+  c₂ : Int  := 0
+  /-- The monomial factor applied to polynomial `p₁`. -/
+  m  : Mon  := .unit
+
+/--
+Simplifies polynomial `p₂` using polynomial `p₁` by rewriting.
+
+This function attempts to rewrite `p₂` by eliminating the first occurrence of
+the leading monomial of `p₁`.
+-/
+def Poly.simp? (p₁ p₂ : Poly) : Option SimpResult :=
+  match p₁ with
+  | .add k₁ m₁ p₁ =>
+    let rec go? (p₂ : Poly) : Option SimpResult :=
+      match p₂ with
+      | .add k₂ m₂ p₂ =>
+        if m₁.divides m₂ then
+          let m  := m₂.div m₁
+          let g  := Nat.gcd k₁.natAbs k₂.natAbs
+          let c₁ := -k₂/g
+          let c₂ := k₁/g
+          let p  := (p₁.mulMon c₁ m).combine (p₂.mulConst c₂)
+          some { p, c₁, c₂, m }
+        else if let some r := go? p₂ then
+          some { r with p := .add (k₂*r.c₂) m₂ r.p }
+        else
+          none
+      | .num _ => none
+    go? p₂
+  | _ => none
 
 end Lean.Grind.CommRing

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean

@@ -26,17 +26,6 @@ where
 end Int.Linear
 
 namespace Lean.Meta.Grind.Arith.Cutsat
-/--
-`gcdExt a b` returns the triple `(g, α, β)` such that
-- `g = gcd a b` (with `g ≥ 0`), and
-- `g = α * a + β * β`.
--/
-partial def gcdExt (a b : Int) : Int × Int × Int :=
-  if b = 0 then
-    (a.natAbs, if a = 0 then 0 else a / a.natAbs, 0)
-  else
-    let (g, α, β) := gcdExt b (a % b)
-    (g, β, α - (a / b) * β)
 
 def get' : GoalM State := do
   return (← get).arith.cutsat

src/Lean/Meta/Tactic/Grind/Arith/Util.lean

@@ -82,5 +82,16 @@ def quoteIfArithTerm (e : Expr) : MessageData :=
     aquote e
   else
     e
+/--
+`gcdExt a b` returns the triple `(g, α, β)` such that
+- `g = gcd a b` (with `g ≥ 0`), and
+- `g = α * a + β * β`.
+-/
+partial def gcdExt (a b : Int) : Int × Int × Int :=
+  if b = 0 then
+    (a.natAbs, if a = 0 then 0 else a / a.natAbs, 0)
+  else
+    let (g, α, β) := gcdExt b (a % b)
+    (g, β, α - (a / b) * β)
 
 end Lean.Meta.Grind.Arith

tests/lean/run/grind_spoly.lean

@@ -1,7 +1,6 @@
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 open Lean.Grind.CommRing
 
-
 def w : Expr := .var 0
 def x : Expr := .var 1
 def y : Expr := .var 2
@@ -20,9 +19,18 @@ instance : HPow Expr Nat Expr where
 instance : OfNat Expr n where
   ofNat := .num n
 
+def spol' (p₁ p₂ : Poly) : Poly :=
+  p₁.spol p₂ |>.spol
+
 def check_spoly (e₁ e₂ r : Expr) : Bool :=
-  e₁.toPoly.superpose e₂.toPoly == r.toPoly &&
-  e₂.toPoly.superpose e₁.toPoly == (-r).toPoly
+  let p₁ := e₁.toPoly
+  let p₂ := e₂.toPoly
+  let r  := r.toPoly
+  let s  := p₁.spol p₂
+  spol' p₁ p₂ == r &&
+  spol' p₂ p₁ == r.mulConst (-1) &&
+  s.spol == r &&
+  r == (p₁.mulMon s.c₁ s.m₁).combine (p₂.mulMon s.c₂ s.m₂)
 
 example : check_spoly (y^2 - x + 1) (x*y - 1 + y) (-x^2 + y + x - y^2) := by native_decide
 example : check_spoly (y - z + 1) (x*y - 1) (-x*z + 1 + x) := by native_decide
@@ -31,3 +39,26 @@ example : check_spoly (x + 1) (z + 1) (z - x) := by native_decide
 example : check_spoly (w^2*x - y) (w*x^2 - z) (-y*x + z*w) := by native_decide
 example : check_spoly (2*z^3 - x*y) (3*z*y - 1) (2*z^2 - 3*x*y^2) := by native_decide
 example : check_spoly (2*x + 3) (3*z + 1) (9*z - 2*x) := by native_decide
+
+example : check_spoly (2*y^2 - x + 1) (2*x*y - 1 + y) (-x^2 + y + x - y^2) := by native_decide
+example : check_spoly (2*y^2 - x + 1) (4*x*y - 1 + y) (-2*x^2 + y + 2*x - y^2) := by native_decide
+example : check_spoly (6*y^2 - x + 1) (4*x*y - 1 + y) (-2*x^2 + 3*y + 2*x - 3*y^2) := by native_decide
+
+def simp? (p₁ p₂ : Poly) : Option Poly :=
+  (·.p) <$> p₁.simp? p₂
+
+partial def simp' (p₁ p₂ : Poly) : Poly :=
+  if let some r := p₁.simp? p₂ then
+    assert! r.p == (p₁.mulMon r.c₁ r.m).combine (p₂.mulConst r.c₂)
+    simp' p₁ r.p
+  else
+    p₂
+
+def check_simp' (e₁ e₂ r : Expr) : Bool :=
+  r.toPoly == simp' e₁.toPoly e₂.toPoly
+
+example : check_simp' (x*y - y) (x^2*y - 1) (y - 1) := by native_decide
+example : check_simp' (2*x + 1) (x^2 + x + 1) 3 := by native_decide
+example : check_simp' (2*x + 1) (3*x^2 + x + y + 1) (4*y + 5) := by native_decide
+example : check_simp' (2*x + y) (3*x^2 + x + y + 1) (3*y^2 + 2*y + 4) := by native_decide
+example : check_simp' (2*x + 1) (z^4 + w^3 + x^2 + x + 1) (4*z^4 + 4*w^3 + 3) := by native_decide