chore:

src/Init/Grind/CommRing.lean

@@ -9,3 +9,4 @@ import Init.Grind.CommRing.Int
 import Init.Grind.CommRing.UInt
 import Init.Grind.CommRing.SInt
 import Init.Grind.CommRing.BitVec
+import Init.Grind.CommRing.Poly

src/Init/Grind/CommRing/Poly.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Lemmas
+import Init.Data.Hashable
 import Init.Data.Ord
 import Init.Data.RArray
 import Init.Grind.CommRing.Basic
@@ -41,7 +42,7 @@ def Expr.denote {α} [CommRing α] (ctx : Context α) : Expr → α
 structure Power where
   x : Var
   k : Nat
-  deriving BEq, Repr
+  deriving BEq, Repr, Hashable
 
 instance : LawfulBEq Power where
   eq_of_beq {a} := by cases a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
@@ -58,14 +59,13 @@ def Power.denote {α} [CommRing α] (ctx : Context α) : Power → α
     | k => x.denote ctx ^ k
 
 inductive Mon where
-  | leaf (p : Power)
-  | cons (p : Power) (m : Mon)
+  | unit
+  | mult (p : Power) (m : Mon)
   deriving BEq, Repr
 
 instance : LawfulBEq Mon where
   eq_of_beq {a} := by
     induction a <;> intro b <;> cases b <;> simp_all! [BEq.beq]
-    next p₁ p₂ => cases p₁ <;> cases p₂ <;> simp <;> intros <;> simp [*]
     next p₁ m₁ p₂ m₂ ih =>
       cases p₁ <;> cases p₂ <;> simp <;> intros <;> simp [*]
       next h => exact ih h
@@ -75,45 +75,32 @@ instance : LawfulBEq Mon where
     assumption
 
 def Mon.denote {α} [CommRing α] (ctx : Context α) : Mon → α
-  | .leaf p => p.denote ctx
-  | .cons p m => p.denote ctx * denote ctx m
-
-def Mon.denote' {α} [CommRing α] (ctx : Context α) : Mon → α
-  | .leaf p => p.denote ctx
-  | .cons p m => go (p.denote ctx) m
-where
-  go (acc : α) : Mon → α
-    | .leaf p => acc * p.denote ctx
-    | .cons p m => go (acc * p.denote ctx) m
+  | unit => 1
+  | .mult p m => p.denote ctx * denote ctx m
 
 def Mon.ofVar (x : Var) : Mon :=
-  .leaf { x, k := 1 }
+  .mult { x, k := 1 } .unit
 
 def Mon.concat (m₁ m₂ : Mon) : Mon :=
   match m₁ with
-  | .leaf p => .cons p m₂
-  | .cons p m₁ => .cons p (concat m₁ m₂)
+  | .unit => m₂
+  | .mult pw m₁ => .mult pw (concat m₁ m₂)
 
-def Mon.mulPow (p : Power) (m : Mon) : Mon :=
+def Mon.mulPow (pw : Power) (m : Mon) : Mon :=
   match m with
-  | .leaf p' =>
-    bif p.varLt p' then
-      .cons p m
-    else bif p'.varLt p then
-      .cons p' (.leaf p)
+  | .unit =>
+    .mult pw .unit
+  | .mult pw' m =>
+    bif pw.varLt pw' then
+      .mult pw (.mult pw' m)
+    else bif pw'.varLt pw then
+      .mult pw' (mulPow pw m)
     else
-      .leaf { x := p.x, k := p.k + p'.k }
-  | .cons p' m =>
-    bif p.varLt p' then
-      .cons p (.cons p' m)
-    else bif p'.varLt p then
-      .cons p' (mulPow p m)
-    else
-      .cons { x := p.x, k := p.k + p'.k } m
+      .mult { x := pw.x, k := pw.k + pw'.k } m
 
 def Mon.length : Mon → Nat
-  | .leaf _ => 1
-  | .cons _ m => 1 + length m
+  | .unit => 0
+  | .mult _ m => 1 + length m
 
 def hugeFuel := 1000000
 
@@ -126,19 +113,19 @@ where
     | 0 => concat m₁ m₂
     | fuel + 1 =>
       match m₁, m₂ with
-      | m₁, .leaf p => m₁.mulPow p
-      | .leaf p, m₂ => m₂.mulPow p
-      | .cons p₁ m₁, .cons p₂ m₂ =>
-        bif p₁.varLt p₂ then
-          .cons p₁ (go fuel m₁ (.cons p₂ m₂))
-        else bif p₂.varLt p₁ then
-          .cons p₂ (go fuel (.cons p₁ m₁) m₂)
+      | m₁, .unit => m₁
+      | .unit, m₂ => m₂
+      | .mult pw₁ m₁, .mult pw₂ m₂ =>
+        bif pw₁.varLt pw₂ then
+          .mult pw₁ (go fuel m₁ (.mult pw₂ m₂))
+        else bif pw₂.varLt pw₁ then
+          .mult pw₂ (go fuel (.mult pw₁ m₁) m₂)
         else
-          .cons { x := p₁.x, k := p₁.k + p₂.k } (go fuel m₁ m₂)
+          .mult { x := pw₁.x, k := pw₁.k + pw₂.k } (go fuel m₁ m₂)
 
 def Mon.degree : Mon → Nat
-  | .leaf p => p.k
-  | .cons p m => p.k + degree m
+  | .unit => 0
+  | .mult pw m => pw.k + degree m
 
 def Var.revlex (x y : Var) : Ordering :=
   bif x.blt y then .gt
@@ -155,24 +142,16 @@ def Power.revlex (p₁ p₂ : Power) : Ordering :=
 
 def Mon.revlexWF (m₁ m₂ : Mon) : Ordering :=
   match m₁, m₂ with
-  | .leaf p₁, .leaf p₂ => p₁.revlex p₂
-  | .leaf p₁, .cons p₂ m₂ =>
-    bif p₁.x.ble p₂.x  then
-      .gt
+  | .unit, .unit => .eq
+  | .unit, .mult .. => .gt
+  | .mult .., .unit => .lt
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    bif pw₁.x == pw₂.x then
+      revlexWF m₁ m₂ |>.then (powerRevlex pw₁.k pw₂.k)
+    else bif pw₁.x.blt pw₂.x then
+      revlexWF m₁ (.mult pw₂ m₂) |>.then .gt
     else
-      revlexWF (.leaf p₁) m₂ |>.then .gt
-  | .cons p₁ m₁, .leaf p₂ =>
-    bif p₂.x.ble p₁.x then
-      .lt
-    else
-      revlexWF m₁ (.leaf p₂) |>.then .lt
-  | .cons p₁ m₁, .cons p₂ m₂ =>
-    bif p₁.x == p₂.x then
-      revlexWF m₁ m₂ |>.then (powerRevlex p₁.k p₂.k)
-    else bif p₁.x.blt p₂.x then
-      revlexWF m₁ (.cons p₂ m₂) |>.then .gt
-    else
-      revlexWF (.cons p₁ m₁) m₂ |>.then .lt
+      revlexWF (.mult pw₁ m₁) m₂ |>.then .lt
 
 def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering :=
   match fuel with
@@ -182,24 +161,16 @@ def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering :=
     revlexWF m₁ m₂
   | fuel + 1 =>
     match m₁, m₂ with
-    | .leaf p₁, .leaf p₂ => p₁.revlex p₂
-    | .leaf p₁, .cons p₂ m₂ =>
-      bif p₁.x.ble p₂.x  then
-        .gt
+    | .unit, .unit => .eq
+    | .unit, .mult ..  => .gt
+    | .mult .., .unit => .lt
+    | .mult pw₁ m₁, .mult pw₂ m₂ =>
+      bif pw₁.x == pw₂.x then
+        revlexFuel fuel m₁ m₂ |>.then (powerRevlex pw₁.k pw₂.k)
+      else bif pw₁.x.blt pw₂.x then
+        revlexFuel fuel m₁ (.mult pw₂ m₂) |>.then .gt
       else
-        revlexFuel fuel (.leaf p₁) m₂ |>.then .gt
-    | .cons p₁ m₁, .leaf p₂ =>
-      bif p₂.x.ble p₁.x then
-        .lt
-      else
-        revlexFuel fuel m₁ (.leaf p₂) |>.then .lt
-    | .cons p₁ m₁, .cons p₂ m₂ =>
-      bif p₁.x == p₂.x then
-        revlexFuel fuel m₁ m₂ |>.then (powerRevlex p₁.k p₂.k)
-      else bif p₁.x.blt p₂.x then
-        revlexFuel fuel m₁ (.cons p₂ m₂) |>.then .gt
-      else
-        revlexFuel fuel (.cons p₁ m₁) m₂ |>.then .lt
+        revlexFuel fuel (.mult pw₁ m₁) m₂ |>.then .lt
 
 def Mon.revlex (m₁ m₂ : Mon) : Ordering :=
   revlexFuel hugeFuel m₁ m₂
@@ -255,6 +226,8 @@ where
 def Poly.insert (k : Int) (m : Mon) (p : Poly) : Poly :=
   bif k == 0 then
     p
+  else bif m == .unit then
+    p.addConst k
   else
     go p
 where
@@ -291,6 +264,8 @@ where
 def Poly.mulMon (k : Int) (m : Mon) (p : Poly) : Poly :=
   bif k == 0 then
     .num 0
+  else bif m == .unit then
+    p.mulConst k
   else
     go p
 where
@@ -347,15 +322,17 @@ def Expr.toPoly : Expr → Poly
   | .pow a k =>
     match a with
     | .num n => .num (n^k)
-    | .var x => Poly.ofMon (.leaf {x, k})
+    | .var x => Poly.ofMon (.mult {x, k} .unit)
     | _ => a.toPoly.pow k
 
 /-!
 **Definitions for the `IsCharP` case**
 
-We considered using a single set of definitions parameterized by `Option c`, but decided against it to avoid
-unnecessary kernel‑reduction overhead. Once we can specialize definitions before they reach the kernel,
+We considered using a single set of definitions parameterized by `Option c` or simply set `c = 0` since
+`n % 0 = n` in Lean, but decided against it to avoid unnecessary kernel‑reduction overhead.
+Once we can specialize definitions before they reach the kernel,
 we can merge the two versions. Until then, the `IsCharP` definitions will carry the `C` suffix.
+We use them whenever we can infer the characteristic using type class instance synthesis.
 -/
 def Poly.addConstC (p : Poly) (k : Int) (c : Nat) : Poly :=
   match p with
@@ -469,7 +446,7 @@ where
     | .pow a k =>
       match a with
       | .num n => .num ((n^k) % c)
-      | .var x => Poly.ofMon (.leaf {x, k})
+      | .var x => Poly.ofMon (.mult {x, k} .unit)
       | _ => (go a).powC k c
 
 /-!
@@ -480,25 +457,13 @@ theorem Power.denote_eq {α} [CommRing α] (ctx : Context α) (p : Power)
     : p.denote ctx = p.x.denote ctx ^ p.k := by
   cases p <;> simp [Power.denote] <;> split <;> simp [pow_zero, pow_succ, one_mul]
 
-theorem Mon.denote'_go_eq_denote {α} [CommRing α] (ctx : Context α) (a : α) (m : Mon)
-    : denote'.go ctx a m = a * denote ctx m := by
-  induction m generalizing a <;> simp [Mon.denote, Mon.denote'.go]
-  next p' m ih =>
-    simp [Mon.denote] at ih
-    rw [ih, mul_assoc]
-
-theorem Mon.denote'_eq_denote {α} [CommRing α] (ctx : Context α) (m : Mon)
-    : denote' ctx m = denote ctx m := by
-  cases m <;> simp [Mon.denote, Mon.denote']
-  next p m => apply denote'_go_eq_denote
-
 theorem Mon.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var)
     : denote ctx (ofVar x) = x.denote ctx := by
-  simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul]
+  simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul, mul_one]
 
 theorem Mon.denote_concat {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
     : denote ctx (concat m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
-  induction m₁ <;> simp [concat, denote, *]
+  induction m₁ <;> simp [concat, denote, one_mul, *]
   next p₁ m₁ ih => rw [mul_assoc]
 
 private theorem le_of_blt_false {a b : Nat} : a.blt b = false → b ≤ a := by
@@ -513,14 +478,7 @@ private theorem eq_of_blt_false {a b : Nat} : a.blt b = false → b.blt a = fals
 
 theorem Mon.denote_mulPow {α} [CommRing α] (ctx : Context α) (p : Power) (m : Mon)
     : denote ctx (mulPow p m) = p.denote ctx * m.denote ctx := by
-  fun_induction mulPow <;> simp [mulPow, *]
-  next => simp [denote]
-  next => simp [denote]; rw [mul_comm]
-  next p' h₁ h₂ =>
-    have := eq_of_blt_false h₁ h₂
-    simp [denote, Power.denote_eq, this, pow_add]
-  next => simp [denote]
-  next => simp [denote, mul_assoc, mul_comm, mul_left_comm, *]
+  fun_induction mulPow <;> simp [mulPow, denote, mul_assoc, mul_comm, mul_left_comm, *]
   next h₁ h₂ =>
     have := eq_of_blt_false h₁ h₂
     simp [denote, Power.denote_eq, pow_add, this, mul_assoc]
@@ -529,10 +487,9 @@ theorem Mon.denote_mul {α} [CommRing α] (ctx : Context α) (m₁ m₂ : Mon)
     : denote ctx (mul m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
   unfold mul
   generalize hugeFuel = fuel
-  fun_induction mul.go <;> simp [mul.go, denote, denote_concat, denote_mulPow, *]
-  next => rw [mul_comm]
-  next => simp [mul_assoc]
-  next => simp [mul_assoc, mul_left_comm, mul_comm]
+  fun_induction mul.go
+    <;> simp [mul.go, denote, denote_concat, denote_mulPow, one_mul, mul_one,
+      mul_assoc, mul_left_comm, mul_comm, *]
   next h₁ h₂ _ =>
     have := eq_of_blt_false h₁ h₂
     simp [Power.denote_eq, pow_add, mul_assoc, mul_left_comm, mul_comm, this]
@@ -561,7 +518,6 @@ private theorem then_eq (o₁ o₂ : Ordering) : o₁.then o₂ = .eq ↔ o₁ =
 
 theorem Mon.eq_of_revlexWF {m₁ m₂ : Mon} : m₁.revlexWF m₂ = .eq → m₁ = m₂ := by
   fun_induction revlexWF <;> simp [revlexWF, *, then_gt, then_lt, then_eq]
-  next => apply Power.eq_of_revlex
   next p₁ m₁ p₂ m₂ h ih =>
     cases p₁; cases p₂; intro h₁ h₂; simp [ih h₁, h]
     simp at h h₂
@@ -570,7 +526,6 @@ theorem Mon.eq_of_revlexWF {m₁ m₂ : Mon} : m₁.revlexWF m₂ = .eq → m₁
 theorem Mon.eq_of_revlexFuel {fuel : Nat} {m₁ m₂ : Mon} : revlexFuel fuel m₁ m₂ = .eq → m₁ = m₂ := by
   fun_induction revlexFuel <;> simp [revlexFuel, *, then_gt, then_lt, then_eq]
   next => apply eq_of_revlexWF
-  next => apply Power.eq_of_revlex
   next p₁ m₁ p₂ m₂ h ih =>
     cases p₁; cases p₂; intro h₁ h₂; simp [ih h₁, h]
     simp at h h₂
@@ -603,13 +558,17 @@ theorem Poly.denote_insert {α} [CommRing α] (ctx : Context α) (k : Int) (m :
   simp [insert, cond_eq_if] <;> split
   next => simp [*, intCast_zero, zero_mul, zero_add]
   next =>
-    fun_induction insert.go <;> simp_all +zetaDelta [insert.go, denote, cond_eq_if]
-    next h₁ _ h₂ =>
-      rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add]
-    next h₁ _ _ =>
-      rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁]
+    split
+    next h =>
+      simp at h <;> simp [*, Mon.denote, denote_addConst, mul_one, add_comm]
     next =>
-      rw [add_left_comm]
+      fun_induction insert.go <;> simp_all +zetaDelta [insert.go, denote, cond_eq_if]
+      next h₁ h₂ =>
+        rw [← add_assoc, Mon.eq_of_grevlex h₁, ← right_distrib, ← intCast_add, h₂, intCast_zero, zero_mul, zero_add]
+      next h₁ _ =>
+        rw [intCast_add, right_distrib, add_assoc, Mon.eq_of_grevlex h₁]
+      next =>
+        rw [add_left_comm]
 
 theorem Poly.denote_concat {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (concat p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
@@ -632,10 +591,14 @@ theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m :
   simp [mulMon, cond_eq_if] <;> split
   next => simp [denote, *, intCast_zero, zero_mul]
   next =>
-    fun_induction mulMon.go <;> simp [mulMon.go, denote, *]
-    next h => simp +zetaDelta at h; simp [*, intCast_zero, mul_zero]
-    next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
-    next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_comm, mul_left_comm, mul_assoc]
+    split
+    next h =>
+      simp at h; simp [*, Mon.denote, mul_one, denote_mulConst]
+    next =>
+      fun_induction mulMon.go <;> simp [mulMon.go, denote, *]
+      next h => simp +zetaDelta at h; simp [*, intCast_zero, mul_zero]
+      next => simp [intCast_mul, intCast_zero, add_zero, mul_comm, mul_left_comm, mul_assoc]
+      next => simp [Mon.denote_mul, intCast_mul, left_distrib, mul_comm, mul_left_comm, mul_assoc]
 
 theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
     : (combine p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
@@ -668,11 +631,9 @@ theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr)
    : e.toPoly.denote ctx = e.denote ctx := by
   fun_induction toPoly
     <;> simp [toPoly, denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combine,
-          Poly.denote_mul, Poly.denote_mulConst, Poly.denote_pow, *]
-  next => rw [intCast_neg, neg_mul, intCast_one, one_mul]
-  next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg]
-  next => rw [intCast_pow]
-  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq]
+          Poly.denote_mul, Poly.denote_mulConst, Poly.denote_pow, intCast_pow, intCast_neg, intCast_one,
+          neg_mul, one_mul, sub_eq_add_neg, *]
+  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]
 
 theorem Expr.eq_of_toPoly_eq {α} [CommRing α] (ctx : Context α) (a b : Expr) (h : a.toPoly == b.toPoly) : a.denote ctx = b.denote ctx := by
   have h := congrArg (Poly.denote ctx) (eq_of_beq h)
@@ -789,7 +750,7 @@ theorem Expr.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context
   next => rw [intCast_neg, neg_mul, intCast_one, one_mul]
   next => rw [intCast_neg, neg_mul, intCast_one, one_mul, sub_eq_add_neg]
   next => rw [IsCharP.intCast_emod, intCast_pow]
-  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq]
+  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]
 
 theorem Expr.eq_of_toPolyC_eq {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr)
     (h : a.toPolyC c == b.toPolyC c) : a.denote ctx = b.denote ctx := by

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

@@ -9,3 +9,4 @@ import Lean.Meta.Tactic.Grind.Arith.Types
 import Lean.Meta.Tactic.Grind.Arith.Main
 import Lean.Meta.Tactic.Grind.Arith.Offset
 import Lean.Meta.Tactic.Grind.Arith.Cutsat
+import Lean.Meta.Tactic.Grind.Arith.CommRing

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

@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly

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

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Grind.CommRing.Poly
+namespace Lean.Grind.CommRing
+
+/-- `lcm m₁ m₂` returns the least common multiple of the given monomials. -/
+def Mon.lcm : Mon → Mon → Mon
+  | .unit, m₂ => m₂
+  | m₁, .unit => m₁
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq => .mult { x := pw₁.x, k := max pw₁.k pw₂.k } (lcm m₁ m₂)
+    | .lt => .mult pw₁ (lcm m₁ (.mult pw₂ m₂))
+    | .gt => .mult pw₂ (lcm (.mult pw₁ m₁) m₂)
+
+/--
+`divides m₁ m₂` returns `true` if monomial `m₁` divides `m₂`
+Example: `x^2.z` divides `w.x^3.y^2.z`
+-/
+def Mon.divides : Mon → Mon → Bool
+  | .unit, _ => true
+  | _, .unit => false
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq => pw₁.k ≤ pw₂.k && divides m₁ m₂
+    | .lt => false
+    | .gt => divides (.mult pw₁ m₁) m₂
+
+/--
+Given `m₁` and `m₂` such that `m₂.divides m₁`, then
+`m₁.div m₂` returns the result.
+Example `w.x^3.y^2.z` div `x^2.z` returns `w.x.y^2`
+-/
+def Mon.div : Mon → Mon → Mon
+  | m₁, .unit => m₁
+  | .unit, _  => .unit -- reachable only if pre-condition does not hold
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq =>
+      let k := pw₁.k - pw₂.k
+      if k == 0 then
+        div m₁ m₂
+      else
+        .mult { x := pw₁.x, k } (div m₁ m₂)
+    | .lt => .mult pw₁ (div m₁ (.mult pw₂ m₂))
+    | .gt => .unit -- reachable only if pre-condition does not hold
+
+/--
+`coprime m₁ m₂` returns `true` if the given monomials
+do not have any variable in common.
+-/
+def Mon.coprime : Mon → Mon → Bool
+  | .unit, _ => true
+  | _, .unit => true
+  | .mult pw₁ m₁, .mult pw₂ m₂ =>
+    match compare pw₁.x pw₂.x with
+    | .eq => false
+    | .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 :=
+  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
+
+end Lean.Grind.CommRing

tests/lean/run/grind_mon_order.lean

@@ -1,4 +1,4 @@
-import Init.Grind.CommRing.SOM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 open Lean.Grind.CommRing
 
 def w : Var := 0
@@ -7,9 +7,9 @@ def y : Var := 2
 def z : Var := 3
 
 macro:100 (priority:=high) a:ident "^" k:num : term => `(Power.mk $a $k)
-infixr:70 (priority:=high) "." => Mon.cons
+infixr:70 (priority:=high) "." => Mon.mult
 instance : Coe Power Mon where
-  coe p := Mon.leaf p
+  coe p := Mon.mult p .unit
 instance : Coe Var Power where
   coe x := x^1
 
@@ -54,3 +54,48 @@ example : check_revlex (z) (w^8) := rfl
 example : check_revlex (z) (x^100) := rfl
 example : check_revlex (z^100) (z) := rfl
 example : check_revlex (x^2 . y^2 . z^5) (x^2 . y^3 . z^4) := rfl
+
+example : Mon.div (w^2 . y^2 . z) (w^2 . y) = y . z := rfl
+example : Mon.div (w^2 . y^2 . z) y = w^2 . y . z := rfl
+example : Mon.div (w^2 . y^2 . z) (y^2) = w^2 . z := rfl
+example : Mon.div (w^2 . y^4) .unit = w^2 . y^4 := rfl
+example : Mon.div (w^2 . y^4) (w^2 . y^4) = .unit := rfl
+example : Mon.div (w^2 . y^4) (w^2 . y^5) = .unit := rfl
+example : Mon.div (w^5) w = w^4 := rfl
+example : Mon.div (w^5 . x^3 . y^2) (w^2 . x) = w^3 . x^2 . y^2 := rfl
+example : Mon.div (y^2 . z^3) (y . z) = y . z^2 := rfl
+example : Mon.div (x . y) (x . y) = .unit := rfl
+example : Mon.div (w . x^2 . y) (w . x . y) = x := rfl
+
+example : Mon.divides (x^2) (w^5) = false := rfl
+
+def check_divides (m₁ m₂ : Mon) :=
+  m₂.divides m₁ && (m₁ == m₂ || !m₁.divides m₂)
+
+example : check_divides (w^5) w := rfl
+example : check_divides (w^2 . y^2 . z) (w^2 . y) := rfl
+example : check_divides (w^2 . y^2 . z) y := rfl
+example : check_divides (w^2 . y^2 . z) (y^2) := rfl
+example : check_divides (w^2 . y^4) .unit  := rfl
+example : check_divides (w^2 . y^4) (w^2 . y^4) := rfl
+example : check_divides (w^5) w := rfl
+example : check_divides (w^5 . x^3 . y^2) (w^2 . x) := rfl
+example : check_divides (x . y) (x . y) := rfl
+
+#eval Mon.lcm Mon.unit (w^3 . y^2)
+
+def check_lcm (m₁ m₂ r : Mon) :=
+  m₁.lcm m₁ == m₁ &&
+  m₂.lcm m₂ == m₂ &&
+  m₁.lcm m₂ == r &&
+  m₂.lcm m₁ == r
+
+example : check_lcm (.unit) (w^3 . y^2) (w^3 . y^2) := by native_decide
+example : check_lcm (w^3 . y^2) Mon.unit (w^3 . y^2) := by native_decide
+example : check_lcm (w^2) (w^5) (w^5) := by native_decide
+example : check_lcm x y (x . y) := by native_decide
+example : check_lcm y z (y . z) := by native_decide
+example : check_lcm (w^2 . x^3) (w^5 . x . y^2) (w^5 . x^3 . y^2) := by native_decide
+example : check_lcm (w . x . y) z (w . x . y . z) := by native_decide
+example : check_lcm (x^2 . y^3) (x^2 . y^5) (x^2 . y^5) := by native_decide
+example : check_lcm (w^100 . x^2) (x^50 . y) (w^100 . x^50 . y) := by native_decide

tests/lean/run/grind_som1.lean

@@ -1,5 +1,4 @@
 import Lean
-import Init.Grind.CommRing.SOM
 
 open Lean.Grind
 open Lean.Grind.CommRing

tests/lean/run/grind_spoly.lean

@@ -0,0 +1,33 @@
+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
+def z : Expr := .var 3
+
+instance : Add Expr where
+  add a b := .add a b
+instance : Sub Expr where
+  sub a b := .sub a b
+instance : Neg Expr where
+  neg a := .neg a
+instance : Mul Expr where
+  mul a b := .mul a b
+instance : HPow Expr Nat Expr where
+  hPow a k := .pow a k
+instance : OfNat Expr n where
+  ofNat := .num n
+
+def check_spoly (e₁ e₂ r : Expr) : Bool :=
+  e₁.toPoly.superpose e₂.toPoly == r.toPoly &&
+  e₂.toPoly.superpose e₁.toPoly == (-r).toPoly
+
+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
+example : check_spoly (z^3 - x*y) (z*y - 1) (z^2 - x*y^2) := by native_decide
+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