test:

feat: IsCharP support for non commutative rings
fix: Poly.mulMonC_nc
2026-04-16 09:04:09 +00:00 · 2025-09-14 00:16:05 -07:00 · 2025-09-14 00:15:28 -07:00 · 2025-09-14 00:09:05 -07:00 · 2025-09-14 00:00:01 -07:00 · 2025-09-13 23:59:47 -07:00
32 changed files with 725 additions and 326 deletions
--- a/src/Init/Grind/Ring.lean
+++ b/src/Init/Grind/Ring.lean
@@ -4,13 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 module
-
 prelude
 public import Init.Grind.Ring.Basic
-public import Init.Grind.Ring.Poly
 public import Init.Grind.Ring.Field
 public import Init.Grind.Ring.Envelope
-public import Init.Grind.Ring.OfSemiring
+public import Init.Grind.Ring.CommSolver
+public import Init.Grind.Ring.CommSemiringAdapter
 public import Init.Grind.Ring.ToInt
-
-public section
--- a/src/Init/Grind/Ring/Basic.lean
+++ b/src/Init/Grind/Ring/Basic.lean
@@ -179,6 +179,20 @@ theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a *
 theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by
  rw [← ofNat_eq_natCast, ofNat_mul, ofNat_eq_natCast, ofNat_eq_natCast]

+theorem natCast_mul_comm (a : Nat) (b : α) : a * b = b * a := by
+  induction a
+  next => simp [Semiring.natCast_zero, mul_zero, zero_mul]
+  next ih =>
+    rw [Semiring.natCast_succ, Semiring.left_distrib, Semiring.right_distrib, ih]
+    simp [Semiring.mul_one, Semiring.one_mul]
+
+theorem natCast_mul_left_comm (a : α) (b : Nat) (c : α) : a * (b * c) = b * (a * c) := by
+  induction b
+  next => simp [Semiring.natCast_zero, mul_zero, zero_mul]
+  next ih =>
+    rw [Semiring.natCast_succ, Semiring.right_distrib, Semiring.left_distrib, ih,
+        Semiring.right_distrib, Semiring.one_mul, Semiring.one_mul]
+
 theorem pow_one (a : α) : a ^ 1 = a := by
  rw [pow_succ, pow_zero, one_mul]

@@ -331,6 +345,18 @@ theorem intCast_mul (x y : Int) : ((x * y : Int) : α) = ((x : α) * (y : α)) :
    rw [Int.neg_mul_neg, intCast_neg, intCast_neg, neg_mul, mul_neg, neg_neg, intCast_mul_aux,
      intCast_natCast, intCast_natCast]

+theorem intCast_mul_comm (a : Int) (b : α) : a * b = b * a := by
+  have : a = a.natAbs ∨ a = -a.natAbs := by exact Int.natAbs_eq a
+  cases this
+  next h => rw [h, Ring.intCast_natCast, Semiring.natCast_mul_comm]
+  next h => rw [h, Ring.intCast_neg, Ring.intCast_natCast, Ring.mul_neg, Ring.neg_mul, Semiring.natCast_mul_comm]
+
+theorem intCast_mul_left_comm (a : α) (b : Int) (c : α) : a * (b * c) = b * (a * c) := by
+  have : b = b.natAbs ∨ b = -b.natAbs := by exact Int.natAbs_eq b
+  cases this
+  next h => rw [h, Ring.intCast_natCast, Semiring.natCast_mul_left_comm]
+  next h => rw [h, Ring.intCast_neg, Ring.intCast_natCast, Ring.neg_mul, Ring.neg_mul, Ring.mul_neg, Semiring.natCast_mul_left_comm]
+
 theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k := by
  induction k
  next => simp [pow_zero, Int.pow_zero, intCast_one]
--- a/src/Init/Grind/Ring/CommSemiringAdapter.lean
+++ b/src/Init/Grind/Ring/CommSemiringAdapter.lean
@@ -4,15 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Grind.Ring.Envelope
 public import Init.Data.Hashable
 public import Init.Data.RArray
-public import Init.Grind.Ring.Poly
-
+public import Init.Grind.Ring.CommSolver
@[expose] public section
-
 namespace Lean.Grind.Ring.OfSemiring
 /-!
 Helper definitions and theorems for converting `Semiring` expressions into `Ring` ones.
--- a/src/Init/Grind/Ring/CommSolver.lean
+++ b/src/Init/Grind/Ring/CommSolver.lean
@@ -4,27 +4,29 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Init.Data.Nat.Lemmas
 public import Init.Data.Int.LemmasAux
 public import Init.Data.Hashable
 public import Init.Data.Ord.Basic
-import all Init.Data.Ord.Basic
 public import Init.Data.RArray
 public import Init.Grind.Ring.Basic
 public import Init.Grind.Ring.Field
 public import Init.Grind.Ordered.Ring
 public import Init.GrindInstances.Ring.Int
-
+import all Init.Data.Ord.Basic
@[expose] public section
+namespace Lean.Grind.CommRing
+/-!
+Data-structures, definitions and theorems for implementing the
+`grind` solver and normalizer for commutative rings and its extensions (e.g., fields,
+commutative semirings, etc.)

+The solver uses proof-by-reflection.
+-/
 open Std
-
-namespace Lean.Grind
 -- These are no longer global instances, so we need to turn them on here.
 attribute [local instance] Semiring.natCast Ring.intCast
-namespace CommRing
 abbrev Var := Nat

 inductive Expr where
@@ -41,18 +43,15 @@ inductive Expr where

 abbrev Context (α : Type u) := RArray α

-@[expose]
 def Var.denote {α} (ctx : Context α) (v : Var) : α :=
  ctx.get v

-@[expose]
 noncomputable def denoteInt {α} [Ring α] (k : Int) : α :=
  Bool.rec
    (OfNat.ofNat (α := α) k.natAbs)
    (- OfNat.ofNat (α := α) k.natAbs)
    (Int.blt' k 0)

-@[expose]
 noncomputable def Expr.denote {α} [Ring α] (ctx : Context α) (e : Expr) : α :=
  Expr.rec
    (fun k => denoteInt k)
@@ -81,11 +80,9 @@ protected noncomputable def Power.beq' (pw₁ pw₂ : Power) : Bool :=
@[simp] theorem Power.beq'_eq (pw₁ pw₂ : Power) : pw₁.beq' pw₂ = (pw₁ = pw₂) := by
  cases pw₁; cases pw₂; simp [Power.beq']

-@[expose]
 def Power.varLt (p₁ p₂ : Power) : Bool :=
  p₁.x.blt p₂.x

-@[expose]
 def Power.denote {α} [Semiring α] (ctx : Context α) : Power → α
  | {x, k} =>
    match k with
@@ -121,12 +118,10 @@ protected noncomputable def Mon.beq' (m₁ : Mon) : Mon → Bool :=
  simp [← ih m₂, ← Bool.and'_eq_and]
  rfl

-@[expose]
 def Mon.denote {α} [Semiring α] (ctx : Context α) : Mon → α
  | unit => 1
  | .mult p m => p.denote ctx * denote ctx m

-@[expose]
 def Mon.denote' {α} [Semiring α] (ctx : Context α) (m : Mon) : α :=
  match m with
  | .unit => 1
@@ -137,17 +132,14 @@ where
    | .unit => acc
    | .mult pw m => go m (acc * (pw.denote ctx))

-@[expose]
 def Mon.ofVar (x : Var) : Mon :=
  .mult { x, k := 1 } .unit

-@[expose]
 def Mon.concat (m₁ m₂ : Mon) : Mon :=
  match m₁ with
  | .unit => m₂
  | .mult pw m₁ => .mult pw (concat m₁ m₂)

-@[expose]
 def Mon.mulPow (pw : Power) (m : Mon) : Mon :=
  match m with
  | .unit =>
@@ -160,15 +152,23 @@ def Mon.mulPow (pw : Power) (m : Mon) : Mon :=
    else
      .mult { x := pw.x, k := pw.k + pw'.k } m

-@[expose]
+-- **Note**: We use the `_nc` suffix for functions for the non-commutative case
+
+def Mon.mulPow_nc (pw : Power) (m : Mon) : Mon :=
+  match m with
+  | .unit      => .mult pw .unit
+  | .mult pw' m =>
+    bif pw.x == pw'.x then
+      .mult { x := pw.x, k := pw.k + pw'.k } m
+    else
+      .mult pw (.mult pw' m)
+
 def Mon.length : Mon → Nat
  | .unit => 0
  | .mult _ m => 1 + length m

-@[expose]
 def hugeFuel := 1000000

-@[expose]
 def Mon.mul (m₁ m₂ : Mon) : Mon :=
  -- We could use `m₁.length + m₂.length` to avoid hugeFuel
  go hugeFuel m₁ m₂
@@ -188,18 +188,21 @@ where
        else
          .mult { x := pw₁.x, k := pw₁.k + pw₂.k } (go fuel m₁ m₂)

-@[expose]
+def Mon.mul_nc (m₁ m₂ : Mon) : Mon :=
+  match m₁ with
+  | .unit          => m₂
+  | .mult pw .unit => m₂.mulPow_nc pw
+  | .mult pw m₁    => .mult pw (mul_nc m₁ m₂)
+
 def Mon.degree : Mon → Nat
  | .unit => 0
  | .mult pw m => pw.k + degree m

-@[expose]
 def Var.revlex (x y : Var) : Ordering :=
  bif x.blt y then .gt
  else bif y.blt x then .lt
  else .eq

-@[expose]
 def powerRevlex (k₁ k₂ : Nat) : Ordering :=
  bif k₁.blt k₂ then .gt
  else bif k₂.blt k₁ then .lt
@@ -212,11 +215,9 @@ theorem powerRevlex_k_eq_powerRevlex (k₁ k₂ : Nat) : powerRevlex_k k₁ k₂
  simp [powerRevlex_k, powerRevlex, cond] <;> split <;> simp [*]
  split <;> simp [*]

-@[expose]
 def Power.revlex (p₁ p₂ : Power) : Ordering :=
  p₁.x.revlex p₂.x |>.then (powerRevlex p₁.k p₂.k)

-@[expose]
 def Mon.revlexWF (m₁ m₂ : Mon) : Ordering :=
  match m₁, m₂ with
  | .unit, .unit => .eq
@@ -230,7 +231,6 @@ def Mon.revlexWF (m₁ m₂ : Mon) : Ordering :=
    else
      revlexWF (.mult pw₁ m₁) m₂ |>.then .gt

-@[expose]
 def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering :=
  match fuel with
  | 0 =>
@@ -250,11 +250,9 @@ def Mon.revlexFuel (fuel : Nat) (m₁ m₂ : Mon) : Ordering :=
      else
        revlexFuel fuel (.mult pw₁ m₁) m₂ |>.then .gt

-@[expose]
 def Mon.revlex (m₁ m₂ : Mon) : Ordering :=
  revlexFuel hugeFuel m₁ m₂

-@[expose]
 def Mon.grevlex (m₁ m₂ : Mon) : Ordering :=
  compare m₁.degree m₂.degree |>.then (revlex m₁ m₂)

@@ -360,13 +358,11 @@ instance : LawfulBEq Poly where
    change m == m ∧ p == p
    simp [ih]

-@[expose]
 def Poly.denote [Ring α] (ctx : Context α) (p : Poly) : α :=
  match p with
  | .num k => Int.cast k
  | .add k m p => k • (m.denote ctx) + denote ctx p

-@[expose]
 def Poly.denote' [Ring α] (ctx : Context α) (p : Poly) : α :=
  match p with
  | .num k => Int.cast k
@@ -384,21 +380,17 @@ where
    | .num k => acc + Int.cast k
    | .add k m p => go p (acc + denoteTerm k m)

-@[expose]
 def Poly.ofMon (m : Mon) : Poly :=
  .add 1 m (.num 0)

-@[expose]
 def Poly.ofVar (x : Var) : Poly :=
  ofMon (Mon.ofVar x)

-@[expose]
 def Poly.isSorted : Poly → Bool
  | .num _ => true
  | .add _ _ (.num _) => true
  | .add _ m₁ (.add k m₂ p) => m₁.grevlex m₂ == .gt && (Poly.add k m₂ p).isSorted

-@[expose]
 def Poly.addConst (p : Poly) (k : Int) : Poly :=
  bif k == 0 then
    p
@@ -424,7 +416,6 @@ theorem Poly.addConst_k_eq_addConst (p : Poly) (k : Int) : addConst_k p k = addC
    induction p <;> simp [addConst.go]
    next ih => rw [← ih]

-@[expose]
 def Poly.insert (k : Int) (m : Mon) (p : Poly) : Poly :=
  bif k == 0 then
    p
@@ -446,13 +437,11 @@ where
      | .gt => .add k m (.add k' m' p)
      | .lt => .add k' m' (go p)

-@[expose]
 def Poly.concat (p₁ p₂ : Poly) : Poly :=
  match p₁ with
  | .num k₁ => p₂.addConst k₁
  | .add k m p₁ => .add k m (concat p₁ p₂)

-@[expose]
 def Poly.mulConst (k : Int) (p : Poly) : Poly :=
  bif k == 0 then
    .num 0
@@ -491,7 +480,6 @@ noncomputable def Poly.mulConst_k (k : Int) (p : Poly) : Poly :=
      next => rfl
      next k m p ih => simp [mulConst.go, ← ih]

-@[expose]
 def Poly.mulMon (k : Int) (m : Mon) (p : Poly) : Poly :=
  bif k == 0 then
    .num 0
@@ -545,7 +533,19 @@ noncomputable def Poly.mulMon_k (k : Int) (m : Mon) (p : Poly) : Poly :=
          simp [h]
      next ih => simp [← ih]

-@[expose]
+def Poly.mulMon_nc (k : Int) (m : Mon) (p : Poly) : Poly :=
+  bif k == 0 then
+    .num 0
+  else bif m == .unit then
+    p.mulConst k
+  else
+    go p (.num 0)
+where
+  go (p : Poly) (acc : Poly) : Poly :=
+    match p with
+    | .num k' => acc.insert (k*k') m
+    | .add k' m' p => go p (acc.insert (k*k') (m.mul_nc m'))
+
 def Poly.combine (p₁ p₂ : Poly) : Poly :=
  go hugeFuel p₁ p₂
 where
@@ -609,7 +609,6 @@ noncomputable def Poly.combine_k : Poly → Poly → Poly :=
    next h => simp [h]; rw [← ih p₁ (add k₂ m₂ p₂)]; rfl
    next h => simp [h]; rw [← ih (add k₁ m₁ p₁) p₂]; rfl

-@[expose]
 def Poly.mul (p₁ : Poly) (p₂ : Poly) : Poly :=
  go p₁ (.num 0)
 where
@@ -618,14 +617,26 @@ where
    | .num k => acc.combine (p₂.mulConst k)
    | .add k m p₁ => go p₁ (acc.combine (p₂.mulMon k m))

-@[expose]
+def Poly.mul_nc (p₁ : Poly) (p₂ : Poly) : Poly :=
+  go p₁ (.num 0)
+where
+  go (p₁ : Poly) (acc : Poly) : Poly :=
+    match p₁ with
+    | .num k => acc.combine (p₂.mulConst k)
+    | .add k m p₁ => go p₁ (acc.combine (p₂.mulMon_nc k m))
+
 def Poly.pow (p : Poly) (k : Nat) : Poly :=
  match k with
  | 0 => .num 1
  | 1 => p
  | k+1 => p.mul (pow p k)

-@[expose]
+def Poly.pow_nc (p : Poly) (k : Nat) : Poly :=
+  match k with
+  | 0 => .num 1
+  | 1 => p
+  | k+1 => (pow_nc p k).mul_nc p
+
 def Expr.toPoly : Expr → Poly
  | .num k     => .num k
  | .intCast k => .num k
@@ -645,7 +656,7 @@ def Expr.toPoly : Expr → Poly
    | .var x => Poly.ofMon (.mult {x, k} .unit)
    | _ => a.toPoly.pow k

-@[expose] noncomputable def Expr.toPoly_k (e : Expr) : Poly :=
+noncomputable def Expr.toPoly_k (e : Expr) : Poly :=
  Expr.rec
    (fun k => .num k) (fun k => .num k) (fun k => .num k)
    (fun x => .ofVar x)
@@ -691,6 +702,25 @@ def Expr.toPoly : Expr → Poly
            | x => a.toPoly.pow k
      cases a <;> try simp [*]

+def Expr.toPoly_nc : Expr → Poly
+  | .num k     => .num k
+  | .intCast k => .num k
+  | .natCast k => .num k
+  | .var x     => Poly.ofVar x
+  | .add a b   => a.toPoly_nc.combine b.toPoly_nc
+  | .mul a b   => a.toPoly_nc.mul_nc b.toPoly_nc
+  | .neg a     => a.toPoly_nc.mulConst (-1)
+  | .sub a b   => a.toPoly_nc.combine (b.toPoly_nc.mulConst (-1))
+  | .pow a k   =>
+    bif k == 0 then
+      .num 1
+    else  match a with
+    | .num n => .num (n^k)
+    | .intCast n => .num (n^k)
+    | .natCast n => .num (n^k)
+    | .var x => Poly.ofMon (.mult {x, k} .unit)
+    | _ => a.toPoly_nc.pow_nc k
+
 def Poly.normEq0 (p : Poly) (c : Nat) : Poly :=
  match p with
  | .num a =>
@@ -707,13 +737,11 @@ 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.
 -/
-@[expose]
 def Poly.addConstC (p : Poly) (k : Int) (c : Nat) : Poly :=
  match p with
  | .num k' => .num ((k' + k) % c)
  | .add k' m p => .add k' m (addConstC p k c)

-@[expose]
 def Poly.insertC (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly :=
  let k := k % c
  bif k == 0 then
@@ -734,7 +762,6 @@ where
      | .gt => .add k m (.add k' m' p)
      | .lt => .add k' m' (go k p)

-@[expose]
 def Poly.mulConstC (k : Int) (p : Poly) (c : Nat) : Poly :=
  let k := k % c
  bif k == 0 then
@@ -753,7 +780,6 @@ where
    else
      .add k m (go p)

-@[expose]
 def Poly.mulMonC (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly :=
  let k := k % c
  bif k == 0 then
@@ -777,7 +803,20 @@ where
     else
       .add k (m.mul m') (go p)

-@[expose]
+def Poly.mulMonC_nc (k : Int) (m : Mon) (p : Poly) (c : Nat) : Poly :=
+  let k := k % c
+  bif k == 0 then
+    .num 0
+  else bif m == .unit then
+    p.mulConstC k c
+  else
+    go p (.num 0)
+where
+  go (p : Poly) (acc : Poly) : Poly :=
+    match p with
+    | .num k' => acc.insert (k*k' % c) m
+    | .add k' m' p => go p (acc.insert (k*k' % c) (m.mul_nc m'))
+
 def Poly.combineC (p₁ p₂ : Poly) (c : Nat) : Poly :=
  go hugeFuel p₁ p₂
 where
@@ -799,7 +838,6 @@ where
        | .gt => .add k₁ m₁ (go fuel p₁ (.add k₂ m₂ p₂))
        | .lt => .add k₂ m₂ (go fuel (.add k₁ m₁ p₁) p₂)

-@[expose]
 def Poly.mulC (p₁ : Poly) (p₂ : Poly) (c : Nat) : Poly :=
  go p₁ (.num 0)
 where
@@ -808,14 +846,26 @@ where
    | .num k => acc.combineC (p₂.mulConstC k c) c
    | .add k m p₁ => go p₁ (acc.combineC (p₂.mulMonC k m c) c)

-@[expose]
+def Poly.mulC_nc (p₁ : Poly) (p₂ : Poly) (c : Nat) : Poly :=
+  go p₁ (.num 0)
+where
+  go (p₁ : Poly) (acc : Poly) : Poly :=
+    match p₁ with
+    | .num k => acc.combineC (p₂.mulConstC k c) c
+    | .add k m p₁ => go p₁ (acc.combineC (p₂.mulMonC_nc k m c) c)
+
 def Poly.powC (p : Poly) (k : Nat) (c : Nat) : Poly :=
  match k with
  | 0 => .num 1
  | 1 => p
  | k+1 => p.mulC (powC p k c) c

-@[expose]
+def Poly.powC_nc (p : Poly) (k : Nat) (c : Nat) : Poly :=
+  match k with
+  | 0 => .num 1
+  | 1 => p
+  | k+1 => (powC_nc p k c).mulC_nc p c
+
 def Expr.toPolyC (e : Expr) (c : Nat) : Poly :=
  go e
 where
@@ -836,6 +886,26 @@ where
      | .var x => Poly.ofMon (.mult {x, k} .unit)
      | _ => (go a).powC k c

+def Expr.toPolyC_nc (e : Expr) (c : Nat) : Poly :=
+  go e
+where
+  go : Expr → Poly
+    | .num k     => .num (k % c)
+    | .natCast k => .num (k % c)
+    | .intCast k => .num (k % c)
+    | .var x     => Poly.ofVar x
+    | .add a b   => (go a).combineC (go b) c
+    | .mul a b   => (go a).mulC_nc (go b) c
+    | .neg a     => (go a).mulConstC (-1) c
+    | .sub a b   => (go a).combineC ((go b).mulConstC (-1) c) c
+    | .pow a k   =>
+      bif k == 0 then
+        .num 1
+      else match a with
+      | .num n => .num ((n^k) % c)
+      | .var x => Poly.ofMon (.mult {x, k} .unit)
+      | _ => (go a).powC_nc k c
+
 /-!
 Theorems for justifying the procedure for commutative rings in `grind`.
 -/
@@ -845,7 +915,7 @@ open Semiring hiding add_zero add_comm add_assoc
 open Ring hiding sub_eq_add_neg
 open CommSemiring

-theorem denoteInt_eq {α} [CommRing α] (k : Int) : denoteInt (α := α) k = k := by
+theorem denoteInt_eq {α} [Ring α] (k : Int) : denoteInt (α := α) k = k := by
  simp [denoteInt] <;> cases h : k.blt' 0 <;> simp <;> simp at h
  next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← Int.eq_natAbs_of_nonneg h]
  next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← Ring.intCast_neg, ← Int.eq_neg_natAbs_of_nonpos (Int.le_of_lt h)]
@@ -888,6 +958,13 @@ theorem Mon.denote_mulPow {α} [CommSemiring α] (ctx : Context α) (p : Power)
    have := eq_of_blt_false h₁ h₂
    simp [Power.denote_eq, pow_add, mul_assoc, this]

+theorem Mon.denote_mulPow_nc {α} [Semiring α] (ctx : Context α) (p : Power) (m : Mon)
+    : denote ctx (mulPow_nc p m) = p.denote ctx * m.denote ctx := by
+  fun_cases mulPow_nc <;> simp [denote, *]
+  next h =>
+    simp at h
+    simp [Power.denote_eq, pow_add, mul_assoc, h]
+
 theorem Mon.denote_mul {α} [CommSemiring α] (ctx : Context α) (m₁ m₂ : Mon)
    : denote ctx (mul m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
  unfold mul
@@ -899,6 +976,10 @@ theorem Mon.denote_mul {α} [CommSemiring α] (ctx : Context α) (m₁ m₂ : Mo
    have := eq_of_blt_false h₁ h₂
    simp [Power.denote_eq, pow_add, this]

+theorem Mon.denote_mul_nc {α} [Semiring α] (ctx : Context α) (m₁ m₂ : Mon)
+    : denote ctx (mul_nc m₁ m₂) = m₁.denote ctx * m₂.denote ctx := by
+  fun_induction mul_nc <;> simp [denote, Semiring.one_mul, Semiring.mul_one, denote_mulPow_nc, Semiring.mul_assoc, *]
+
 theorem Var.eq_of_revlex {x₁ x₂ : Var} : x₁.revlex x₂ = .eq → x₁ = x₂ := by
  simp [revlex, cond_eq_if] <;> split <;> simp
  next h₁ => intro h₂; exact Nat.le_antisymm h₂ (Nat.ge_of_not_lt h₁)
@@ -954,15 +1035,15 @@ theorem Poly.denote'_eq_denote {α} [Ring α] (ctx : Context α) (p : Poly) : p.
    fun_induction denote'.go <;> simp [denote, *, Ring.intCast_zero, Semiring.add_zero, denoteTerm_eq]
    next ih => simp [denoteTerm_eq] at ih; simp [ih, Semiring.add_assoc, zsmul_eq_intCast_mul]

-theorem Poly.denote_ofMon {α} [CommRing α] (ctx : Context α) (m : Mon)
+theorem Poly.denote_ofMon {α} [Ring α] (ctx : Context α) (m : Mon)
    : denote ctx (ofMon m) = m.denote ctx := by
  simp [ofMon, denote, intCast_one, intCast_zero, one_mul, add_zero, zsmul_eq_intCast_mul]

-theorem Poly.denote_ofVar {α} [CommRing α] (ctx : Context α) (x : Var)
+theorem Poly.denote_ofVar {α} [Ring α] (ctx : Context α) (x : Var)
    : denote ctx (ofVar x) = x.denote ctx := by
  simp [ofVar, denote_ofMon, Mon.denote_ofVar]

-theorem Poly.denote_addConst {α} [CommRing α] (ctx : Context α) (p : Poly) (k : Int) : (addConst p k).denote ctx = p.denote ctx + k := by
+theorem Poly.denote_addConst {α} [Ring α] (ctx : Context α) (p : Poly) (k : Int) : (addConst p k).denote ctx = p.denote ctx + k := by
  simp [addConst, cond_eq_if]; split
  next => simp [*, intCast_zero, add_zero]
  next =>
@@ -970,7 +1051,7 @@ theorem Poly.denote_addConst {α} [CommRing α] (ctx : Context α) (p : Poly) (k
    next => rw [intCast_add]
    next => simp [add_comm, add_left_comm]

-theorem Poly.denote_insert {α} [CommRing α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
+theorem Poly.denote_insert {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
    : (insert k m p).denote ctx = k * m.denote ctx + p.denote ctx := by
  simp [insert, cond_eq_if] <;> split
  next => simp [*, intCast_zero, zero_mul, zero_add]
@@ -987,13 +1068,13 @@ theorem Poly.denote_insert {α} [CommRing α] (ctx : Context α) (k : Int) (m :
      next =>
        rw [add_left_comm]

-theorem Poly.denote_concat {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
+theorem Poly.denote_concat {α} [Ring α] (ctx : Context α) (p₁ p₂ : Poly)
    : (concat p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
  fun_induction concat <;> simp [*, denote_addConst, denote]
  next => rw [add_comm]
  next => rw [add_assoc]

-theorem Poly.denote_mulConst {α} [CommRing α] (ctx : Context α) (k : Int) (p : Poly)
+theorem Poly.denote_mulConst {α} [Ring α] (ctx : Context α) (k : Int) (p : Poly)
    : (mulConst k p).denote ctx = k * p.denote ctx := by
  simp [mulConst, cond_eq_if] <;> split
  next => simp [denote, *, intCast_zero, zero_mul]
@@ -1017,7 +1098,28 @@ theorem Poly.denote_mulMon {α} [CommRing α] (ctx : Context α) (k : Int) (m :
      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_left_comm, mul_assoc]

-theorem Poly.denote_combine {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
+theorem Poly.denote_mulMon_nc_go {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly)
+    : (mulMon_nc.go k m p acc).denote ctx = k * m.denote ctx * p.denote ctx + acc.denote ctx := by
+  fun_induction mulMon_nc.go <;> simp [denote, denote_insert, zsmul_eq_intCast_mul]
+  next => rw [Ring.intCast_mul, Semiring.mul_assoc, Semiring.mul_assoc, ← Ring.intCast_mul_comm]
+  next ih =>
+    rw [ih, denote_insert, Mon.denote_mul_nc, Semiring.left_distrib, Ring.intCast_mul]
+    rw [Ring.intCast_mul_left_comm]; simp [← Semiring.mul_assoc]
+    conv => enter [1, 2, 1, 1, 1]; rw [Ring.intCast_mul_comm]
+    simp [Semiring.add_assoc, Semiring.add_comm, add_left_comm]
+
+theorem Poly.denote_mulMon_nc {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
+    : (mulMon_nc k m p).denote ctx = k * m.denote ctx * p.denote ctx := by
+  simp [mulMon_nc, cond_eq_if] <;> split
+  next => simp [denote, *, intCast_zero, zero_mul]
+  next =>
+    split
+    next h =>
+      simp at h; simp [*, Mon.denote, mul_one, denote_mulConst]
+    next =>
+      rw [denote_mulMon_nc_go]; simp [denote, Ring.intCast_zero, add_zero]
+
+theorem Poly.denote_combine {α} [Ring α] (ctx : Context α) (p₁ p₂ : Poly)
    : (combine p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx := by
  unfold combine; generalize hugeFuel = fuel
  fun_induction combine.go
@@ -1038,6 +1140,15 @@ theorem Poly.denote_mul {α} [CommRing α] (ctx : Context α) (p₁ p₂ : Poly)
    : (mul p₁ p₂).denote ctx = p₁.denote ctx * p₂.denote ctx := by
  simp [mul, denote_mul_go, denote, intCast_zero, zero_add]

+theorem Poly.denote_mul_nc_go {α} [Ring α] (ctx : Context α) (p₁ p₂ acc : Poly)
+    : (mul_nc.go p₂ p₁ acc).denote ctx = acc.denote ctx + p₁.denote ctx * p₂.denote ctx := by
+  fun_induction mul_nc.go
+    <;> simp [denote_combine, denote_mulConst, denote, *, right_distrib, denote_mulMon_nc, add_assoc, zsmul_eq_intCast_mul]
+
+theorem Poly.denote_mul_nc {α} [Ring α] (ctx : Context α) (p₁ p₂ : Poly)
+    : (mul_nc p₁ p₂).denote ctx = p₁.denote ctx * p₂.denote ctx := by
+  simp [mul_nc, denote_mul_nc_go, denote, intCast_zero, zero_add]
+
 theorem Poly.denote_pow {α} [CommRing α] (ctx : Context α) (p : Poly) (k : Nat)
   : (pow p k).denote ctx = p.denote ctx ^ k := by
 fun_induction pow
@@ -1045,6 +1156,13 @@ theorem Poly.denote_pow {α} [CommRing α] (ctx : Context α) (p : Poly) (k : Na
 next => simp [pow_succ, pow_zero, one_mul]
 next => simp [denote_mul, *, pow_succ, mul_comm]

+theorem Poly.denote_pow_nc {α} [Ring α] (ctx : Context α) (p : Poly) (k : Nat)
+   : (pow_nc p k).denote ctx = p.denote ctx ^ k := by
+ fun_induction pow_nc
+ next => simp [denote, intCast_one, pow_zero]
+ next => simp [pow_succ, pow_zero, one_mul]
+ next => simp [denote_mul_nc, *, pow_succ]
+
 theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr)
   : e.toPoly.denote ctx = e.denote ctx := by
  fun_induction toPoly
@@ -1056,21 +1174,37 @@ theorem Expr.denote_toPoly {α} [CommRing α] (ctx : Context α) (e : Expr)
  next => rw [Ring.intCast_natCast]
  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]

+theorem Expr.denote_toPoly_nc {α} [Ring α] (ctx : Context α) (e : Expr)
+   : e.toPoly_nc.denote ctx = e.denote ctx := by
+  fun_induction toPoly_nc
+    <;> simp [denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combine,
+          Poly.denote_mul_nc, Poly.denote_mulConst, Poly.denote_pow_nc, intCast_pow, intCast_neg, intCast_one,
+          neg_mul, one_mul, sub_eq_add_neg, denoteInt_eq, *]
+  next => rw [Ring.intCast_natCast]
+  next a k h => simp at h; simp [h, Semiring.pow_zero]
+  next => rw [Ring.intCast_natCast]
+  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)
  simp [denote_toPoly] at h
  assumption

+theorem Expr.eq_of_toPoly_nc_eq {α} [Ring α] (ctx : Context α) (a b : Expr) (h : a.toPoly_nc == b.toPoly_nc) : a.denote ctx = b.denote ctx := by
+  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  simp [denote_toPoly_nc] at h
+  assumption
+
 /-!
 Theorems for justifying the procedure for commutative rings with a characteristic in `grind`.
 -/

-theorem Poly.denote_addConstC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int) : (addConstC p k c).denote ctx = p.denote ctx + k := by
+theorem Poly.denote_addConstC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int) : (addConstC p k c).denote ctx = p.denote ctx + k := by
  fun_induction addConstC <;> simp [denote, *]
  next => rw [IsCharP.intCast_emod, intCast_add]
  next => simp [add_comm, add_left_comm]

-theorem Poly.denote_insertC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
+theorem Poly.denote_insertC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
    : (insertC k m p c).denote ctx = k * m.denote ctx + p.denote ctx := by
  simp [insertC, cond_eq_if] <;> split
  next =>
@@ -1087,7 +1221,7 @@ theorem Poly.denote_insertC {α c} [CommRing α] [IsCharP α c] (ctx : Context
    next => rw [IsCharP.intCast_emod]
    next => rw [add_left_comm]

-theorem Poly.denote_mulConstC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int) (p : Poly)
+theorem Poly.denote_mulConstC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (p : Poly)
    : (mulConstC k p c).denote ctx = k * p.denote ctx := by
  simp [mulConstC, cond_eq_if] <;> split
  next =>
@@ -1136,7 +1270,29 @@ theorem Poly.denote_mulMonC {α c} [CommRing α] [IsCharP α c] (ctx : Context
        simp +zetaDelta [*, IsCharP.intCast_emod, Mon.denote_mul, intCast_mul, left_distrib,
          mul_left_comm, mul_assoc, zsmul_eq_intCast_mul]

-theorem Poly.denote_combineC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
+theorem Poly.denote_mulMonC_nc_go {α c} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p acc : Poly)
+    : (mulMonC_nc.go k m c p acc).denote ctx = k * m.denote ctx * p.denote ctx + acc.denote ctx := by
+  fun_induction mulMonC_nc.go <;> simp [denote, denote_insert, zsmul_eq_intCast_mul]
+  next => rw [IsCharP.intCast_emod (x := k * _) (p := c), Ring.intCast_mul, Semiring.mul_assoc, Semiring.mul_assoc, ← Ring.intCast_mul_comm]
+  next ih =>
+    rw [ih, denote_insert, Mon.denote_mul_nc, IsCharP.intCast_emod (x := k * _) (p := c),
+        Semiring.left_distrib, Ring.intCast_mul]
+    rw [Ring.intCast_mul_left_comm]; simp [← Semiring.mul_assoc]
+    conv => enter [1, 2, 1, 1, 1]; rw [Ring.intCast_mul_comm]
+    simp [Semiring.add_assoc, Semiring.add_comm, add_left_comm]
+
+theorem Poly.denote_mulMonC_nc {α c} [Ring α] [IsCharP α c] (ctx : Context α) (k : Int) (m : Mon) (p : Poly)
+    : (mulMonC_nc k m p c).denote ctx = k * m.denote ctx * p.denote ctx := by
+  simp [mulMonC_nc, cond_eq_if] <;> split
+  next =>
+    rw [← IsCharP.intCast_emod (p := c)]
+    simp [denote, *, intCast_zero, zero_mul]
+  next =>
+    split
+    next h => simp at h; simp [*, Mon.denote, mul_one, denote_mulConstC, IsCharP.intCast_emod]
+    next => rw [Poly.denote_mulMonC_nc_go, denote, Ring.intCast_zero, add_zero]
+
+theorem Poly.denote_combineC {α c} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
    : (combineC p₁ p₂ c).denote ctx = p₁.denote ctx + p₂.denote ctx := by
  unfold combineC; generalize hugeFuel = fuel
  fun_induction combineC.go
@@ -1160,6 +1316,15 @@ theorem Poly.denote_mulC {α c} [CommRing α] [IsCharP α c] (ctx : Context α)
    : (mulC p₁ p₂ c).denote ctx = p₁.denote ctx * p₂.denote ctx := by
  simp [mulC, denote_mulC_go, denote, intCast_zero, zero_add]

+theorem Poly.denote_mulC_nc_go {α c} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ acc : Poly)
+    : (mulC_nc.go p₂ c p₁ acc).denote ctx = acc.denote ctx + p₁.denote ctx * p₂.denote ctx := by
+  fun_induction mulC_nc.go
+    <;> simp [denote_combineC, denote_mulConstC, denote, *, right_distrib, denote_mulMonC_nc, add_assoc, zsmul_eq_intCast_mul]
+
+theorem Poly.denote_mulC_nc {α c} [Ring α] [IsCharP α c] (ctx : Context α) (p₁ p₂ : Poly)
+    : (mulC_nc p₁ p₂ c).denote ctx = p₁.denote ctx * p₂.denote ctx := by
+  simp [mulC_nc, denote_mulC_nc_go, denote, intCast_zero, zero_add]
+
 theorem Poly.denote_powC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Nat)
   : (powC p k c).denote ctx = p.denote ctx ^ k := by
 fun_induction powC
@@ -1167,6 +1332,13 @@ theorem Poly.denote_powC {α c} [CommRing α] [IsCharP α c] (ctx : Context α)
 next => simp [pow_succ, pow_zero, one_mul]
 next => simp [denote_mulC, *, pow_succ, mul_comm]

+theorem Poly.denote_powC_nc {α c} [Ring α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Nat)
+   : (powC_nc p k c).denote ctx = p.denote ctx ^ k := by
+ fun_induction powC_nc
+ next => simp [denote, intCast_one, pow_zero]
+ next => simp [pow_succ, pow_zero, one_mul]
+ next => simp [denote_mulC_nc, *, pow_succ]
+
 theorem Expr.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (e : Expr)
   : (e.toPolyC c).denote ctx = e.denote ctx := by
  unfold toPolyC
@@ -1182,17 +1354,37 @@ theorem Expr.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context
  next => rw [IsCharP.intCast_emod, intCast_pow]
  next => simp [Poly.denote_ofMon, Mon.denote, Power.denote_eq, mul_one]

+theorem Expr.denote_toPolyC_nc {α c} [Ring α] [IsCharP α c] (ctx : Context α) (e : Expr)
+   : (e.toPolyC_nc c).denote ctx = e.denote ctx := by
+  unfold toPolyC_nc
+  fun_induction toPolyC_nc.go
+    <;> simp [denote, Poly.denote, Poly.denote_ofVar, Poly.denote_combineC,
+          Poly.denote_mulC_nc, Poly.denote_mulConstC, Poly.denote_powC_nc, denoteInt_eq, *]
+  next => rw [IsCharP.intCast_emod]
+  next => rw [IsCharP.intCast_emod, Ring.intCast_natCast]
+  next => rw [IsCharP.intCast_emod]
+  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 a k h => simp at h; simp [h, Semiring.pow_zero, Ring.intCast_one]
+  next => rw [IsCharP.intCast_emod, intCast_pow]
+  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
  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
  simp [denote_toPolyC] at h
  assumption

+theorem Expr.eq_of_toPolyC_nc_eq {α c} [Ring α] [IsCharP α c] (ctx : Context α) (a b : Expr)
+    (h : a.toPolyC_nc c == b.toPolyC_nc c) : a.denote ctx = b.denote ctx := by
+  have h := congrArg (Poly.denote ctx) (eq_of_beq h)
+  simp [denote_toPolyC_nc] at h
+  assumption
+
 namespace Stepwise
 /-!
 Theorems for stepwise proof-term construction
 -/
-@[expose]
 noncomputable def core_cert (lhs rhs : Expr) (p : Poly) : Bool :=
  (lhs.sub rhs).toPoly_k.beq' p

@@ -1202,7 +1394,6 @@ theorem core {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
  simp [Expr.denote_toPoly, Expr.denote]
  simp [sub_eq_zero_iff]

-@[expose]
 noncomputable def superpose_cert (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) : Bool :=
  (p₁.mulMon_k k₁ m₁).combine_k (p₂.mulMon_k k₂ m₂) |>.beq' p

@@ -1211,7 +1402,6 @@ theorem superpose {α} [CommRing α] (ctx : Context α) (k₁ : Int) (m₁ : Mon
  simp [superpose_cert]; intro _ h₁ h₂; subst p
  simp [Poly.denote_combine, Poly.denote_mulMon, h₁, h₂, mul_zero, add_zero]

-@[expose]
 noncomputable def simp_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) : Bool :=
  (p₁.mulConst_k k₁).combine_k (p₂.mulMon_k k₂ m₂) |>.beq' p

@@ -1220,32 +1410,26 @@ theorem simp {α} [CommRing α] (ctx : Context α) (k₁ : Int) (p₁ : Poly) (k
  simp [simp_cert]; intro _ h₁ h₂; subst p
  simp [Poly.denote_combine, Poly.denote_mulMon, Poly.denote_mulConst, h₁, h₂, mul_zero, add_zero]

-@[expose]
 noncomputable def mul_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
  p₁.mulConst_k k |>.beq' p

-@[expose]
 def mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
    : mul_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by
  simp [mul_cert]; intro _ h; subst p
  simp [Poly.denote_mulConst, *, mul_zero]

-@[expose]
 noncomputable def div_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
  !Int.beq' k 0 |>.and' (p.mulConst_k k |>.beq' p₁)

-@[expose]
 def div {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly)
    : div_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by
  simp [div_cert]; intro hnz _ h; subst p₁
  simp [Poly.denote_mulConst, ← zsmul_eq_intCast_mul] at h
  exact no_int_zero_divisors hnz h

-@[expose]
 noncomputable def unsat_eq_cert (p : Poly) (k : Int) : Bool :=
  !Int.beq' k 0 |>.and' (p.beq' (.num k))

-@[expose]
 def unsat_eq {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (p : Poly) (k : Int)
    : unsat_eq_cert p k → p.denote ctx = 0 → False := by
  simp [unsat_eq_cert]; intro h _; subst p; simp [Poly.denote]
@@ -1256,7 +1440,6 @@ def unsat_eq {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (p : Poly) (k
 theorem d_init {α} [CommRing α] (ctx : Context α) (p : Poly) : (1:Int) * p.denote ctx = p.denote ctx := by
  rw [intCast_one, one_mul]

-@[expose]
 noncomputable def d_step1_cert (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) : Bool :=
  p.beq' (p₁.combine_k (p₂.mulMon_k k₂ m₂))

@@ -1265,7 +1448,6 @@ theorem d_step1 {α} [CommRing α] (ctx : Context α) (k : Int) (init : Poly) (p
  simp [d_step1_cert]; intro _ h₁ h₂; subst p
  simp [Poly.denote_combine, Poly.denote_mulMon, h₂, mul_zero, add_zero, h₁]

-@[expose]
 noncomputable def d_stepk_cert (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) : Bool :=
  p.beq' ((p₁.mulConst_k k₁).combine_k (p₂.mulMon_k k₂ m₂))

@@ -1275,7 +1457,6 @@ theorem d_stepk {α} [CommRing α] (ctx : Context α) (k₁ : Int) (k : Int) (in
  simp [Poly.denote_combine, Poly.denote_mulMon, Poly.denote_mulConst, h₂, mul_zero, add_zero]
  rw [intCast_mul, mul_assoc, h₁]

-@[expose]
 noncomputable def imp_1eq_cert (lhs rhs : Expr) (p₁ p₂ : Poly) : Bool :=
  (lhs.sub rhs).toPoly_k.beq' p₁ |>.and' (p₂.beq' (.num 0))

@@ -1284,7 +1465,6 @@ theorem imp_1eq {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p₁ p
  simp [imp_1eq_cert, intCast_one, one_mul]; intro _ _; subst p₁ p₂
  simp [Expr.denote_toPoly, Expr.denote, sub_eq_zero_iff, Poly.denote, intCast_zero]

-@[expose]
 noncomputable def imp_keq_cert (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) : Bool :=
  !Int.beq' k 0 |>.and' ((lhs.sub rhs).toPoly_k.beq' p₁ |>.and' (p₂.beq' (.num 0)))

@@ -1295,7 +1475,6 @@ theorem imp_keq  {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (k
  intro h; replace h := no_int_zero_divisors hnz h
  rw [← sub_eq_zero_iff, h]

-@[expose]
 noncomputable def core_certC (lhs rhs : Expr) (p : Poly) (c : Nat) : Bool :=
  (lhs.sub rhs).toPolyC c |>.beq' p

@@ -1305,7 +1484,6 @@ theorem coreC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (lhs rhs :
  simp [Expr.denote_toPolyC, Expr.denote]
  simp [sub_eq_zero_iff]

-@[expose]
 noncomputable def superpose_certC (k₁ : Int) (m₁ : Mon) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) (c : Nat) : Bool :=
  (p₁.mulMonC k₁ m₁ c).combineC (p₂.mulMonC k₂ m₂ c) c |>.beq' p

@@ -1314,28 +1492,23 @@ theorem superposeC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁
  simp [superpose_certC]; intro _ h₁ h₂; subst p
  simp [Poly.denote_combineC, Poly.denote_mulMonC, h₁, h₂, mul_zero, add_zero]

-@[expose]
 noncomputable def mul_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) : Bool :=
  p₁.mulConstC k c |>.beq' p

-@[expose]
 def mulC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
    : mul_certC p₁ k p c → p₁.denote ctx = 0 → p.denote ctx = 0 := by
  simp [mul_certC]; intro _ h; subst p
  simp [Poly.denote_mulConstC, *, mul_zero]

-@[expose]
 noncomputable def div_certC (p₁ : Poly) (k : Int) (p : Poly) (c : Nat) : Bool :=
  !Int.beq' k 0 |>.and' ((p.mulConstC k c).beq' p₁)

-@[expose]
 def divC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly)
    : div_certC p₁ k p c → p₁.denote ctx = 0 → p.denote ctx = 0 := by
  simp [div_certC]; intro hnz _ h; subst p₁
  simp [Poly.denote_mulConstC, ← zsmul_eq_intCast_mul] at h
  exact no_int_zero_divisors hnz h

-@[expose]
 noncomputable def simp_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) (c : Nat) : Bool :=
  (p₁.mulConstC k₁ c).combineC (p₂.mulMonC k₂ m₂ c) c |>.beq' p

@@ -1344,11 +1517,9 @@ theorem simpC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁ : Int
  simp [simp_certC]; intro _ h₁ h₂; subst p
  simp [Poly.denote_combineC, Poly.denote_mulMonC, Poly.denote_mulConstC, h₁, h₂, mul_zero, add_zero]

-@[expose]
 noncomputable def unsat_eq_certC (p : Poly) (k : Int) (c : Nat) : Bool :=
  !Int.beq' (k % c) 0 |>.and' (p.beq' (.num k))

-@[expose]
 def unsat_eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly) (k : Int)
    : unsat_eq_certC p k c → p.denote ctx = 0 → False := by
  simp [unsat_eq_certC]; intro h _; subst p; simp [Poly.denote]
@@ -1356,7 +1527,6 @@ def unsat_eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (p : Poly)
  simp [h] at this
  assumption

-@[expose]
 noncomputable def d_step1_certC (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) (c : Nat) : Bool :=
  p.beq' (p₁.combineC (p₂.mulMonC k₂ m₂ c) c)

@@ -1365,7 +1535,6 @@ theorem d_step1C {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k : Int
  simp [d_step1_certC]; intro _ h₁ h₂; subst p
  simp [Poly.denote_combineC, Poly.denote_mulMonC, h₂, mul_zero, add_zero, h₁]

-@[expose]
 noncomputable def d_stepk_certC (k₁ : Int) (p₁ : Poly) (k₂ : Int) (m₂ : Mon) (p₂ : Poly) (p : Poly) (c : Nat) : Bool :=
  p.beq' ((p₁.mulConstC k₁ c).combineC (p₂.mulMonC k₂ m₂ c) c)

@@ -1375,7 +1544,6 @@ theorem d_stepkC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (k₁ :
  simp [Poly.denote_combineC, Poly.denote_mulMonC, Poly.denote_mulConstC, h₂, mul_zero, add_zero]
  rw [intCast_mul, mul_assoc, h₁]

-@[expose]
 noncomputable def imp_1eq_certC (lhs rhs : Expr) (p₁ p₂ : Poly) (c : Nat) : Bool :=
  ((lhs.sub rhs).toPolyC c).beq' p₁ |>.and' (p₂.beq' (.num 0))

@@ -1384,7 +1552,6 @@ theorem imp_1eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (lhs rhs
  simp [imp_1eq_certC, intCast_one, one_mul]; intro _ _; subst p₁ p₂
  simp [Expr.denote_toPolyC, Expr.denote, sub_eq_zero_iff, Poly.denote, intCast_zero]

-@[expose]
 noncomputable def imp_keq_certC (lhs rhs : Expr) (k : Int) (p₁ p₂ : Poly) (c : Nat) : Bool :=
  !Int.beq' k 0 |>.and' (((lhs.sub rhs).toPolyC c).beq' p₁ |>.and' (p₂.beq' (.num 0)))

@@ -1399,7 +1566,6 @@ end Stepwise

 /-! IntModule interface -/

-@[expose]
 def Mon.denoteAsIntModule [CommRing α] (ctx : Context α) (m : Mon) : α :=
  match m with
  | .unit => One.one
@@ -1410,7 +1576,6 @@ where
    | .unit => acc
    | .mult pw m => go m (acc * pw.denote ctx)

-@[expose]
 def Poly.denoteAsIntModule [CommRing α] (ctx : Context α) (p : Poly) : α :=
  match p with
  | .num k => k • (One.one : α)
@@ -1511,7 +1676,6 @@ theorem inv_split {α} [Field α] (a : α) : if a = 0 then a⁻¹ = 0 else a * a
  next h => simp [h, Field.inv_zero]
  next h => rw [Field.mul_inv_cancel h]

-@[expose]
 noncomputable def one_eq_zero_unsat_cert (p : Poly) :=
  p.beq' (.num 1) || p.beq' (.num (-1))

@@ -1551,7 +1715,6 @@ theorem Poly.normEq0_eq {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Na
    simp [denote, normEq0, cond_eq_if]; split <;> simp [denote, zsmul_eq_intCast_mul, *]
    next h' => rw [of_mod_eq_0 h h', Semiring.zero_mul, zero_add]

-@[expose]
 noncomputable def eq_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
  p₁.beq' (.num c) && (p.beq' (p₂.normEq0 c))

@@ -1571,7 +1734,6 @@ theorem gcd_eq_0 [CommRing α] (g n m a b : Int) (h : g = a * n + b * m)
  rw [← Ring.intCast_add, h₂, zero_add, ← h] at h₁
  rw [Ring.intCast_zero, h₁]

-@[expose]
 def eq_gcd_cert (a b : Int) (p₁ p₂ p : Poly) : Bool :=
  match p₁ with
  | .add .. => false
@@ -1589,7 +1751,6 @@ theorem eq_gcd {α} [CommRing α] (ctx : Context α) (a b : Int) (p₁ p₂ p :
  rename_i n m g
  apply gcd_eq_0 g n m a b

-@[expose]
 noncomputable def d_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
  p₂.beq' (.num c) |>.and' (p.beq' (p₁.normEq0 c))

@@ -1598,11 +1759,10 @@ theorem d_normEq0 {α} [CommRing α] (ctx : Context α) (k : Int) (c : Nat) (ini
  simp [d_normEq0_cert]; intro _ h₁ h₂; subst p p₂; simp [Poly.denote]
  intro h; rw [p₁.normEq0_eq] <;> assumption

-@[expose] noncomputable def norm_int_cert (e : Expr) (p : Poly) : Bool :=
+noncomputable def norm_int_cert (e : Expr) (p : Poly) : Bool :=
  e.toPoly_k.beq' p

 theorem norm_int (ctx : Context Int) (e : Expr) (p : Poly) : norm_int_cert e p → e.denote ctx = p.denote' ctx := by
  simp [norm_int_cert, Poly.denote'_eq_denote]; intro; subst p; simp [Expr.denote_toPoly]

-end CommRing
-end Lean.Grind
+end Lean.Grind.CommRing
--- a/src/Lean/Meta/Tactic/Grind/AC/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/AC/Util.lean
@@ -78,8 +78,8 @@ private def isArithOpInOtherModules (op : Expr) (f : Expr) : GoalM Bool := do
  if declName == ``HAdd.hAdd || declName == ``HMul.hMul || declName == ``HSub.hSub || declName == ``HDiv.hDiv || declName == ``HPow.hPow then
    if op.getAppNumArgs == 4 then
      let α := op.appFn!.appFn!.appArg!
-      if (← Arith.CommRing.getRingId? α).isSome then return true
-      if (← Arith.CommRing.getSemiringId? α).isSome then return true
+      if (← Arith.CommRing.getCommRingId? α).isSome then return true
+      if (← Arith.CommRing.getCommSemiringId? α).isSome then return true
  return false

 def getTermOpIds (e : Expr) : GoalM (List Nat) := do
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.OfSemiring
+public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
@@ -15,7 +15,7 @@ namespace Lean.Meta.Grind.Arith.CommRing
 Helper functions for converting reified terms back into their denotations.
 -/

-variable [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadRing M]
+variable [Monad M] [MonadError M] [MonadLiftT MetaM M] [MonadCanon M] [MonadRing M]

 def denoteNum (k : Int) : M Expr := do
  let ring ← getRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean
@@ -31,17 +31,24 @@ private def inSameSemiring? (a b : Expr) : GoalM (Option Nat) := do
  unless semiringId == semiringId' do return none -- This can happen when we have heterogeneous equalities
  return semiringId

+/-- Returns `some ringId` if `a` and `b` are elements of the same (non-commutative) ring. -/
+private def inSameNonCommRing? (a b : Expr) : GoalM (Option Nat) := do
+  let some ringId ← getTermNonCommRingId? a | return none
+  let some ringId' ← getTermNonCommRingId? b | return none
+  unless ringId == ringId' do return none -- This can happen when we have heterogeneous equalities
+  return ringId
+
 def mkEqCnstr (p : Poly) (h : EqCnstrProof) : RingM EqCnstr := do
-  let id := (← getRing).nextId
+  let id := (← getCommRing).nextId
  let sugar := p.degree
-  modifyRing fun s => { s with nextId := s.nextId + 1 }
+  modifyCommRing fun s => { s with nextId := s.nextId + 1 }
  return { sugar, p, h, id }

 /--
 Returns the ring expression denoting the given Lean expression.
 Recall that we compute the ring expressions during internalization.
 -/
-private def toRingExpr? (e : Expr) : RingM (Option RingExpr) := do
+private def toRingExpr? [Monad m] [MonadLiftT GrindM m] [MonadRing m] (e : Expr) : m (Option RingExpr) := do
  let ring ← getRing
  if let some re := ring.denote.find? { expr := e } then
    return some re
@@ -76,7 +83,7 @@ then the leading coefficient of the equation must also divide `k`
 def _root_.Lean.Grind.CommRing.Mon.findSimp? (k : Int) (m : Mon) : RingM (Option EqCnstr) := do
  let checkCoeff ← checkCoeffDvd
  let noZeroDiv ← noZeroDivisors
-  for c in (← getRing).basis do
+  for c in (← getCommRing).basis do
    if !checkCoeff || noZeroDiv || (c.p.lc ∣ k) then
    if c.p.divides m then
      return some c
@@ -102,7 +109,7 @@ def PolyDerivation.simplifyWith (d : PolyDerivation) (c : EqCnstr) : RingM PolyD
  return .step r.p r.k₁ d r.k₂ r.m₂ c

 def PolyDerivation.simplifyNumEq0 (d : PolyDerivation) : RingM PolyDerivation := do
-  let some numEq0 := (← getRing).numEq0? | return d
+  let some numEq0 := (← getCommRing).numEq0? | return d
  let .num k := numEq0.p | return d
  return .normEq0 (d.p.normEq0 k.natAbs) d numEq0

@@ -140,7 +147,7 @@ partial def EqCnstr.simplifyWithExhaustively (c₁ c₂ : EqCnstr) : RingM EqCns
  c.simplifyWithExhaustively c₂

 def EqCnstr.simplifyUsingNumEq0 (c : EqCnstr) : RingM EqCnstr := do
-  let some c' := (← getRing).numEq0? | return c
+  let some c' := (← getCommRing).numEq0? | return c
  let .num k := c'.p | return c
  return { c with p := c.p.normEq0 k.natAbs, h := .numEq0 k.natAbs c' c }

@@ -171,11 +178,11 @@ def EqCnstr.checkConstant (c : EqCnstr) : RingM Bool := do
    if n < 0 then
      n := -n
      c := { c with p := .num n, h := .mul (-1) c }
-    if let some c' := (← getRing).numEq0? then
+    if let some c' := (← getCommRing).numEq0? then
      let .num m := c'.p | unreachable!
      let (g, a, b) := gcdExt n m
      c := { c with p := .num g, h := .gcd a b c c' }
-    modifyRing fun s => { s with numEq0? := some c, numEq0Updated := true }
+    modifyCommRing fun s => { s with numEq0? := some c, numEq0Updated := true }
    trace_goal[grind.ring.assert.store] "{← c.denoteExpr}"
  return true

@@ -201,7 +208,7 @@ private def addSorted (c : EqCnstr) : List EqCnstr → List EqCnstr

 def addToBasisCore (c : EqCnstr) : RingM Unit := do
  trace[grind.debug.ring.basis] "{← c.denoteExpr}"
-  modifyRing fun s => { s with
+  modifyCommRing fun s => { s with
    basis := addSorted c s.basis
    recheck := true
  }
@@ -209,12 +216,12 @@ def addToBasisCore (c : EqCnstr) : RingM Unit := do
 def EqCnstr.addToQueue (c : EqCnstr) : RingM Unit := do
  if (← checkMaxSteps) then return ()
  trace_goal[grind.ring.assert.queue] "{← c.denoteExpr}"
-  modifyRing fun s => { s with queue := s.queue.insert c }
+  modifyCommRing fun s => { s with queue := s.queue.insert c }

 def EqCnstr.superposeWith (c : EqCnstr) : RingM Unit := do
  if (← checkMaxSteps) then return ()
  let .add _ m _ := c.p | return ()
-  for c' in (← getRing).basis do
+  for c' in (← getCommRing).basis do
    let .add _ m' _ := c'.p | pure ()
    if m.sharesVar m' then
      let r ← c.p.spolM c'.p
@@ -270,8 +277,8 @@ def EqCnstr.simplifyBasis (c : EqCnstr) : RingM Unit := do
        else
          go basis (c' :: acc)
      | _ => go basis (c' :: acc)
-  let basis ← go (← getRing).basis []
-  modifyRing fun s => { s with basis }
+  let basis ← go (← getCommRing).basis []
+  modifyCommRing fun s => { s with basis }

 def EqCnstr.addToBasisAfterSimp (c : EqCnstr) : RingM Unit := do
  let c ← c.toMonic
@@ -281,10 +288,10 @@ def EqCnstr.addToBasisAfterSimp (c : EqCnstr) : RingM Unit := do
  addToBasisCore c

 private def checkNumEq0Updated : RingM Unit := do
-  if (← getRing).numEq0Updated then
+  if (← getCommRing).numEq0Updated then
    -- `numEq0?` was updated, then we must move the basis back to the queue to be simplified.
-    let basis := (← getRing).basis
-    modifyRing fun s => { s with numEq0Updated := false, basis := {} }
+    let basis := (← getCommRing).basis
+    modifyCommRing fun s => { s with numEq0Updated := false, basis := {} }
    for c in basis do
      c.addToQueue

@@ -323,7 +330,7 @@ def DiseqCnstr.simplify (c : DiseqCnstr) : RingM DiseqCnstr :=

 def saveDiseq (c : DiseqCnstr) : RingM Unit := do
  trace_goal[grind.ring.assert.store] "{← c.denoteExpr}"
-  modifyRing fun s => { s with diseqs := s.diseqs.push c }
+  modifyCommRing fun s => { s with diseqs := s.diseqs.push c }

 def addNewDiseq (c : DiseqCnstr) : RingM Unit := do
  let c ← c.simplify
@@ -360,10 +367,10 @@ private def pre (e : Expr) : GoalM Expr := do
 private def diseqToEq (a b : Expr) : RingM Unit := do
  -- Rabinowitsch transformation
  let gen := max (← getGeneration a) (← getGeneration b)
-  let ring ← getRing
+  let ring ← getCommRing
  let some fieldInst := ring.fieldInst? | unreachable!
  let e ← pre <| mkApp2 (← getSubFn) a b
-  modifyRing fun s => { s with invSet := s.invSet.insert e }
+  modifyCommRing fun s => { s with invSet := s.invSet.insert e }
  let eInv ← pre <| mkApp (← getInvFn) e
  let lhs ← pre <| mkApp2 (← getMulFn) e eInv
  internalize lhs gen none
@@ -373,69 +380,87 @@ private def diseqToEq (a b : Expr) : RingM Unit := do
 private def diseqZeroToEq (a b : Expr) : RingM Unit := do
  -- Rabinowitsch transformation for `b = 0` case
  let gen ← getGeneration a
-  let ring ← getRing
+  let ring ← getCommRing
  let some fieldInst := ring.fieldInst? | unreachable!
-  modifyRing fun s => { s with invSet := s.invSet.insert a }
+  modifyCommRing fun s => { s with invSet := s.invSet.insert a }
  let aInv ← pre <| mkApp (← getInvFn) a
  let lhs ← pre <| mkApp2 (← getMulFn) a aInv
  internalize lhs gen none
  trace[grind.debug.ring.rabinowitsch] "{lhs}"
  pushEq lhs (← getOne) <| mkApp4 (mkConst ``Grind.CommRing.diseq0_to_eq [ring.u]) ring.type fieldInst a (← mkDiseqProof a b)

+private def processNewDiseqCommRing (a b : Expr) : RingM Unit := do
+  trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
+  let some ra ← toRingExpr? a | return ()
+  let some rb ← toRingExpr? b | return ()
+  let p ← (ra.sub rb).toPolyM
+  if (← isField) then
+    if !(p matches .num _) || !(← hasChar) then
+      if rb matches .num 0 then
+        diseqZeroToEq a b
+      else
+        diseqToEq a b
+      return ()
+  addNewDiseq {
+    lhs := a, rhs := b
+    rlhs := ra, rrhs := rb
+    d := .input p
+    ofSemiring? := none
+  }
+
+private def processNewDiseqCommSemiring (a b : Expr) : SemiringM Unit := do
+  if (← getAddRightCancelInst?).isSome then
+    trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
+    let some sa ← toSemiringExpr? a | return ()
+    let some sb ← toSemiringExpr? b | return ()
+    let lhs ← sa.denoteAsRingExpr
+    let rhs ← sb.denoteAsRingExpr
+    RingM.run (← getSemiring).ringId do
+      let some ra ← reify? lhs (skipVar := false) (gen := (← getGeneration a)) | return ()
+      let some rb ← reify? rhs (skipVar := false) (gen := (← getGeneration b)) | return ()
+      let p ← (ra.sub rb).toPolyM
+      addNewDiseq {
+        lhs := a, rhs := b
+        rlhs := ra, rrhs := rb
+        d := .input p
+        ofSemiring? := some (sa, sb)
+      }
+  else
+    -- If semiring does not have `AddRightCancel`,
+    -- we may still normalize and check whether lhs and rhs are equal
+    let some sa ← toSemiringExpr? a | return ()
+    let some sb ← toSemiringExpr? b | return ()
+    if sa.toPoly == sb.toPoly then
+      setSemiringDiseqUnsat a b sa sb
+
+private def processNewDiseqNonCommRing (a b : Expr) : NonCommRingM Unit := do
+  let some ra ← toRingExpr? a | return ()
+  let some rb ← toRingExpr? b | return ()
+  if let some (_, c) := (← getRing).charInst? then
+    if ra.toPolyC_nc c == rb.toPolyC_nc c then
+      setNonCommRingDiseqUnsat a b ra rb
+  else
+    if ra.toPoly_nc == rb.toPoly_nc then
+      setNonCommRingDiseqUnsat a b ra rb
+
 def processNewDiseq (a b : Expr) : GoalM Unit := do
  if let some ringId ← inSameRing? a b then RingM.run ringId do
-    trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
-    let some ra ← toRingExpr? a | return ()
-    let some rb ← toRingExpr? b | return ()
-    let p ← (ra.sub rb).toPolyM
-    if (← isField) then
-      if !(p matches .num _) || !(← hasChar) then
-        if rb matches .num 0 then
-          diseqZeroToEq a b
-        else
-          diseqToEq a b
-        return ()
-    addNewDiseq {
-      lhs := a, rhs := b
-      rlhs := ra, rrhs := rb
-      d := .input p
-      ofSemiring? := none
-    }
+    processNewDiseqCommRing a b
  else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do
-    if (← getAddRightCancelInst?).isSome then
-      trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
-      let some sa ← toSemiringExpr? a | return ()
-      let some sb ← toSemiringExpr? b | return ()
-      let lhs ← sa.denoteAsRingExpr
-      let rhs ← sb.denoteAsRingExpr
-      RingM.run (← getSemiring).ringId do
-        let some ra ← reify? lhs (skipVar := false) (gen := (← getGeneration a)) | return ()
-        let some rb ← reify? rhs (skipVar := false) (gen := (← getGeneration b)) | return ()
-        let p ← (ra.sub rb).toPolyM
-        addNewDiseq {
-          lhs := a, rhs := b
-          rlhs := ra, rrhs := rb
-          d := .input p
-          ofSemiring? := some (sa, sb)
-        }
-    else
-      -- If semiring does not have `AddRightCancel`,
-      -- we may still normalize and check whether lhs and rhs are equal
-      let some sa ← toSemiringExpr? a | return ()
-      let some sb ← toSemiringExpr? b | return ()
-      if sa.toPoly == sb.toPoly then
-        setSemiringDiseqUnsat a b sa sb
+    processNewDiseqCommSemiring a b
+  else if let some ncRingId ← inSameNonCommRing? a b then NonCommRingM.run ncRingId do
+    processNewDiseqNonCommRing a b

 /--
 Returns `true` if the todo queue is not empty or the `recheck` flag is set to `true`
 -/
 private def needCheck : RingM Bool := do
  unless (← isQueueEmpty) do return true
-  return (← getRing).recheck
+  return (← getCommRing).recheck

 private def checkDiseqs : RingM Unit := do
-  let diseqs := (← getRing).diseqs
-  modifyRing fun s => { s with diseqs := {} }
+  let diseqs := (← getCommRing).diseqs
+  modifyCommRing fun s => { s with diseqs := {} }
  -- No indexing simple
  for diseq in diseqs do
    addNewDiseq diseq
@@ -459,7 +484,7 @@ private def propagateEqs : RingM Unit := do
    if (← checkMaxSteps) then return ()
    let some ra ← toRingExpr? a | unreachable!
    map ← process map a ra
-  for (a, ra) in (← getRing).denoteEntries do
+  for (a, ra) in (← getCommRing).denoteEntries do
    if (← checkMaxSteps) then return ()
    map ← process map a ra
 where
@@ -498,7 +523,7 @@ def checkRing : RingM Bool := do
    if (← checkMaxSteps) then return true
  checkDiseqs
  propagateEqs
-  modifyRing fun s => { s with recheck := false }
+  modifyCommRing fun s => { s with recheck := false }
  return true

 def check : GoalM Bool := do profileitM Exception "grind ring" (← getOptions) do
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Functions.lean
@@ -9,18 +9,20 @@ public import Lean.Meta.Tactic.Grind.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadRing m]
+variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m]

+section
+variable [MonadRing m]
 def mkUnaryFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : m Expr := do
-  let inst ← MonadRing.synthInstance <| mkApp (mkConst instDeclName [u]) type
+  let inst ← MonadCanon.synthInstance <| mkApp (mkConst instDeclName [u]) type
  canonExpr <| mkApp2 (mkConst declName [u]) type inst

 def mkBinHomoFn (type : Expr) (u : Level) (instDeclName : Name) (declName : Name) : m Expr := do
-  let inst ← MonadRing.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
+  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst instDeclName [u, u, u]) type type type
  canonExpr <| mkApp4 (mkConst declName [u, u, u]) type type type inst

 def mkPowFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
-  let inst ← MonadRing.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
+  let inst ← MonadCanon.synthInstance <| mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type
  let inst' := mkApp2 (mkConst ``Grind.Semiring.npow [u]) type semiringInst
  checkInst inst inst'
  canonExpr <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst
@@ -38,7 +40,7 @@ def mkNatCastFn (u : Level) (type : Expr) (semiringInst : Expr) : m Expr := do
  -- does not guarantee that an `NatCast α` will be available.
  -- When both are present we verify that they are defeq,
  -- and otherwise fall back to the field of the `Semiring α` instance that we already have.
-  let inst ← match (← MonadRing.synthInstance? instType) with
+  let inst ← match (← MonadCanon.synthInstance? instType) with
  | none => pure inst'
  | some inst => checkInst inst inst'; pure inst
  canonExpr <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst
@@ -47,8 +49,6 @@ where
    unless (← isDefEqD inst inst') do
      throwError "instance for natCast{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}"

-variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadRing m]
-
 def getAddFn : m Expr := do
  let ring ← getRing
  if let some addFn := ring.addFn? then return addFn
@@ -77,15 +77,6 @@ def getNegFn : m Expr := do
  modifyRing fun s => { s with negFn? := some negFn }
  return negFn

-def getInvFn : m Expr := do
-  let ring ← getRing
-  if ring.fieldInst?.isNone then
-    throwError "`grind` internal error, type is not a field{indentExpr ring.type}"
-  if let some invFn := ring.invFn? then return invFn
-  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv
-  modifyRing fun s => { s with invFn? := some invFn }
-  return invFn
-
 def getPowFn : m Expr := do
  let ring ← getRing
  if let some powFn := ring.powFn? then return powFn
@@ -104,7 +95,7 @@ def getIntCastFn : m Expr := do
  -- does not guarantee that an `IntCast α` will be available.
  -- When both are present we verify that they are defeq,
  -- and otherwise fall back to the field of the `Ring α` instance that we already have.
-  let inst ← match (← MonadRing.synthInstance? instType) with
+  let inst ← match (← MonadCanon.synthInstance? instType) with
    | none => pure inst'
    | some inst => checkInst inst inst'; pure inst
  let intCastFn ← canonExpr <| mkApp2 (mkConst ``IntCast.intCast [ring.u]) ring.type inst
@@ -134,5 +125,19 @@ def getOne [MonadLiftT GoalM m] : m Expr := do
  modifyRing fun s => { s with one? := some one }
  internalize one 0
  return one
+end
+
+section
+variable [MonadCommRing m]
+
+def getInvFn : m Expr := do
+  let ring ← getCommRing
+  if ring.fieldInst?.isNone then
+    throwError "`grind` internal error, type is not a field{indentExpr ring.type}"
+  if let some invFn := ring.invFn? then return invFn
+  let invFn ← mkUnaryFn ring.type ring.u ``Inv ``Inv.inv
+  modifyCommRing fun s => { s with invFn? := some invFn }
+  return invFn
+end

 end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean
@@ -69,7 +69,7 @@ private partial def toInt? (e : Expr) : RingM (Option Int) := do
  | _ => return none

 private def isInvInst (inst : Expr) : RingM Bool := do
-  if (← getRing).fieldInst?.isNone then return false
+  if (← getCommRing).fieldInst?.isNone then return false
  return isSameExpr (← getInvFn).appArg! inst

 /--
@@ -79,10 +79,10 @@ Otherwise, asserts `if a = 0 then a⁻¹ = 0 else a * a⁻¹ = 1`
 -/
 private def processInv (e inst a : Expr) : RingM Unit := do
  unless (← isInvInst inst) do return ()
-  let ring ← getRing
+  let ring ← getCommRing
  let some fieldInst := ring.fieldInst? | return ()
-  if (← getRing).invSet.contains a then return ()
-  modifyRing fun s => { s with invSet := s.invSet.insert a }
+  if (← getCommRing).invSet.contains a then return ()
+  modifyCommRing fun s => { s with invSet := s.invSet.insert a }
  if let some k ← toInt? a then
    if k == 0 then
      /-
@@ -117,7 +117,7 @@ private def processInv (e inst a : Expr) : RingM Unit := do
 private def internalizeInv (e : Expr) : GoalM Bool := do
  match_expr e with
  | Inv.inv α inst a =>
-    let some ringId ← getRingId? α | return true
+    let some ringId ← getCommRingId? α | return true
    RingM.run ringId do processInv e inst a
    return true
  | _ => return false
@@ -130,20 +130,26 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
  if (← internalizeInv e) then return ()
  let some type := getType? e | return ()
  if isForbiddenParent parent? then return ()
-  if let some ringId ← getRingId? type then RingM.run ringId do
+  if let some ringId ← getCommRingId? type then RingM.run ringId do
    let some re ← reify? e | return ()
    trace_goal[grind.ring.internalize] "[{ringId}]: {e}"
    setTermRingId e
    ringExt.markTerm e
-    modifyRing fun s => { s with
+    modifyCommRing fun s => { s with
      denote := s.denote.insert { expr := e } re
      denoteEntries := s.denoteEntries.push (e, re)
    }
-  else if let some semiringId ← getSemiringId? type then SemiringM.run semiringId do
+  else if let some semiringId ← getCommSemiringId? type then SemiringM.run semiringId do
    let some re ← sreify? e | return ()
    trace_goal[grind.ring.internalize] "semiring [{semiringId}]: {e}"
    setTermSemiringId e
    ringExt.markTerm e
    modifySemiring fun s => { s with denote := s.denote.insert { expr := e } re }
+  else if let some ncRingId ← getNonCommRingId? type then NonCommRingM.run ncRingId do
+    let some re ← ncreify? e | return ()
+    trace_goal[grind.ring.internalize] "(non-comm) ring [ncRingId}]: {e}"
+    setTermNonCommRingId e
+    ringExt.markTerm e
+    modifyRing fun s => { s with denote := s.denote.insert { expr := e } re }

 end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean
@@ -30,16 +30,16 @@ private def checkPoly (p : Poly) : RingM Unit := do

 private def checkBasis : RingM Unit := do
  let mut x := 0
-  for c in (← getRing).basis do
+  for c in (← getCommRing).basis do
    checkPoly c.p
    x := x + 1

 private def checkQueue : RingM Unit := do
-  for c in (← getRing).queue do
+  for c in (← getCommRing).queue do
    checkPoly c.p

 private def checkDiseqs : RingM Unit := do
-  for c in (← getRing).diseqs do
+  for c in (← getCommRing).diseqs do
    checkPoly c.d.p

 private def checkRingInvs : RingM Unit := do
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/MonadRing.lean
@@ -9,9 +9,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public section
 namespace Lean.Meta.Grind.Arith.CommRing

-class MonadRing (m : Type → Type) where
-  getRing : m Ring
-  modifyRing : (Ring → Ring) → m Unit
+class MonadCanon (m : Type → Type) where
  /--
  Helper function for removing dependency on `GoalM`.
  In `RingM` and `SemiringM`, this is just `sharedCommon (← canon e)`
@@ -24,18 +22,43 @@ class MonadRing (m : Type → Type) where
  -/
  synthInstance? : Expr → m (Option Expr)

-export MonadRing (getRing modifyRing canonExpr)
+export MonadCanon (canonExpr)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadCanon m] : MonadCanon n where
+  canonExpr e := liftM (canonExpr e : m Expr)
+  synthInstance? e := liftM (MonadCanon.synthInstance? e : m (Option Expr))
+
+def MonadCanon.synthInstance [Monad m] [MonadError m] [MonadCanon m] (type : Expr) : m Expr := do
+  let some inst ← synthInstance? type
+    | throwError "`grind` failed to find instance{indentExpr type}"
+  return inst
+
+class MonadRing (m : Type → Type) where
+  getRing : m Ring
+  modifyRing : (Ring → Ring) → m Unit
+
+export MonadRing (getRing modifyRing)

@[always_inline]
 instance (m n) [MonadLift m n] [MonadRing m] : MonadRing n where
  getRing    := liftM (getRing : m Ring)
  modifyRing f := liftM (modifyRing f : m Unit)
-  canonExpr e := liftM (canonExpr e : m Expr)
-  synthInstance? e := liftM (MonadRing.synthInstance? e : m (Option Expr))

-def MonadRing.synthInstance [Monad m] [MonadError m] [MonadRing m] (type : Expr) : m Expr := do
-  let some inst ← synthInstance? type
-    | throwError "`grind` failed to find instance{indentExpr type}"
-  return inst
+class MonadCommRing (m : Type → Type) where
+  getCommRing : m CommRing
+  modifyCommRing : (CommRing → CommRing) → m Unit
+
+export MonadCommRing (getCommRing modifyCommRing)
+
+@[always_inline]
+instance (m n) [MonadLift m n] [MonadCommRing m] : MonadCommRing n where
+  getCommRing      := liftM (getCommRing : m CommRing)
+  modifyCommRing f := liftM (modifyCommRing f : m Unit)
+
+@[always_inline]
+instance (m) [Monad m] [MonadCommRing m] : MonadRing m where
+  getRing := return (← getCommRing).toRing
+  modifyRing f := modifyCommRing fun s => { s with toRing := f s.toRing }

 end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/NonCommRingM.lean
@@ -0,0 +1,55 @@
+/-
+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
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
+public section
+namespace Lean.Meta.Grind.Arith.CommRing
+
+structure NonCommRingM.Context where
+  ringId : Nat
+
+/-- We don't want to keep carrying the `RingId` around. -/
+abbrev NonCommRingM := ReaderT NonCommRingM.Context GoalM
+
+abbrev NonCommRingM.run (ringId : Nat) (x : NonCommRingM α) : GoalM α :=
+  x { ringId }
+
+instance : MonadCanon NonCommRingM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
+
+protected def NonCommRingM.getRing : NonCommRingM Ring := do
+  let s ← get'
+  let ringId := (← read).ringId
+  if h : ringId < s.ncRings.size then
+    return s.ncRings[ringId]
+  else
+    throwError "`grind` internal error, invalid ringId"
+
+protected def NonCommRingM.modifyRing (f : Ring → Ring) : NonCommRingM Unit := do
+  let ringId := (← read).ringId
+  modify' fun s => { s with ncRings := s.ncRings.modify ringId f }
+
+instance : MonadRing NonCommRingM where
+  getRing := NonCommRingM.getRing
+  modifyRing := NonCommRingM.modifyRing
+
+def getTermNonCommRingId? (e : Expr) : GoalM (Option Nat) := do
+    return (← get').exprToNCRingId.find? { expr := e }
+
+def setTermNonCommRingId (e : Expr) : NonCommRingM Unit := do
+  let ringId := (← read).ringId
+  if let some ringId' ← getTermNonCommRingId? e then
+    unless ringId' == ringId do
+      reportIssue! "expression in two different rings{indentExpr e}"
+    return ()
+  modify' fun s => { s with exprToNCRingId := s.exprToNCRingId.insert { expr := e } ringId }
+
+instance : MonadSetTermId NonCommRingM where
+  setTermId e := setTermNonCommRingId e
+
+end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/PP.lean
@@ -12,14 +12,16 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public section
 namespace Lean.Meta.Grind.Arith.CommRing

-private abbrev M := StateT Ring MetaM
+private abbrev M := StateT CommRing MetaM

-private instance : MonadRing M where
-  getRing := get
-  modifyRing := modify
+private instance : MonadCanon M where
  canonExpr e := return e
  synthInstance? e := Meta.synthInstance? e none

+private instance : MonadCommRing M where
+  getCommRing := get
+  modifyCommRing := modify
+
 private def toOption (cls : Name) (header : Thunk MessageData) (msgs : Array MessageData) : Option MessageData :=
  if msgs.isEmpty then
    none
@@ -31,13 +33,13 @@ private def push (msgs : Array MessageData) (msg? : Option MessageData) : Array

 private def ppBasis? : M (Option MessageData) := do
  let mut basis := #[]
-  for c in (← getRing).basis do
+  for c in (← getCommRing).basis do
    basis := basis.push (toTraceElem (← c.denoteExpr))
  return toOption `basis "Basis" basis

 private def ppDiseqs? : M (Option MessageData) := do
  let mut diseqs := #[]
-  for d in (← getRing).diseqs do
+  for d in (← getCommRing).diseqs do
    diseqs := diseqs.push (toTraceElem (← d.denoteExpr))
  return toOption `diseqs "Disequalities" diseqs

--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.Poly
+public import Init.Grind.Ring.CommSolver
 public section
 namespace Lean.Grind.CommRing

--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
@@ -7,7 +7,8 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
-import Init.Grind.Ring.OfSemiring
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
+import Init.Grind.Ring.CommSemiringAdapter
 import Lean.Data.RArray
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.ProofUtil
@@ -23,7 +24,7 @@ namespace Lean.Meta.Grind.Arith.CommRing
 Returns a context of type `RArray α` containing the variables `vars` where
 `α` is the type of the ring.
 -/
-private def toContextExpr (vars : Array Expr) : RingM Expr := do
+private def toContextExpr [Monad m] [MonadLiftT MetaM m] [MonadCanon m] [MonadRing m] (vars : Array Expr) : m Expr := do
  let ring ← getRing
  if h : 0 < vars.size then
    RArray.toExpr ring.type id (RArray.ofFn (vars[·]) h)
@@ -116,19 +117,19 @@ private def mkMonDecl (m : Mon) : ProofM Expr := do

 private def mkStepBasicPrefix (declName : Name) : ProofM Expr := do
  let ctx ← getContext
-  let ring ← getRing
+  let ring ← getCommRing
  return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx

 private def mkStepPrefix (declName declNameC : Name) : ProofM Expr := do
  if let some (charInst, char) ← nonzeroCharInst? then
    let ctx ← getContext
-    let ring ← getRing
+    let ring ← getCommRing
    return mkApp5 (mkConst declNameC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx
  else
    mkStepBasicPrefix declName

 private def getSemiringIdOf : RingM Nat := do
-  let some semiringId := (← getRing).semiringId? | throwError "`grind` internal error, semiring is not available"
+  let some semiringId := (← getCommRing).semiringId? | throwError "`grind` internal error, semiring is not available"
  return semiringId

 private def getSemiringOf : RingM Semiring := do
@@ -256,7 +257,7 @@ private def mkContext (h : Expr) : ProofM Expr := do

 private def mkSemiringContext (h : Expr) : ProofM Expr := do
  let some sctx := (← read).sctx? | return h
-  let some semiringId := (← getRing).semiringId? | return h
+  let some semiringId := (← getCommRing).semiringId? | return h
  let semiring ← getSemiringOf
  let usedVars     := collectMapVars (← get).sexprDecls (·.collectVars) {}
  let vars'        := usedVars.toArray
@@ -273,7 +274,7 @@ private def mkSemiringContext (h : Expr) : ProofM Expr := do

 private abbrev withProofContext (x : ProofM Expr) : RingM Expr := do
  let ctx := mkFVar (← mkFreshFVarId)
-  let sctx? ← if (← getRing).semiringId?.isSome then pure <| some (mkFVar (← mkFreshFVarId)) else pure none
+  let sctx? ← if (← getCommRing).semiringId?.isSome then pure <| some (mkFVar (← mkFreshFVarId)) else pure none
  go { ctx, sctx? } |>.run' {}
 where
  go : ProofM Expr := do
@@ -284,7 +285,7 @@ where
 open Lean.Grind.CommRing in
 def EqCnstr.setUnsat  (c : EqCnstr) : RingM Unit := do
  let h ← withProofContext do
-    let ring ← getRing
+    let ring ← getCommRing
    if let some (charInst, char) := ring.charInst? then
      let mut h ← mkStepPrefix ``Stepwise.unsat_eq ``Stepwise.unsat_eqC
      if char == 0 then
@@ -335,4 +336,26 @@ def setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit :
  let h := mkApp3 h (toExpr sa) (toExpr sb) eagerReflBoolTrue
  closeGoal (mkApp hne h)

+/--
+Given `a` and `b`, such that `a ≠ b` in the core and `ra` and `rb` their reified ring
+terms s.t. `ra.toPoly_nc == rb.toPoly_nc`, close the goal.
+-/
+def setNonCommRingDiseqUnsat (a b : Expr) (ra rb : RingExpr) : NonCommRingM Unit := do
+  let ring ← getRing
+  let hne ← mkDiseqProof a b
+  let usedVars     := ra.collectVars >> rb.collectVars <| {}
+  let vars'        := usedVars.toArray
+  let varRename    := mkVarRename vars'
+  let vars         := ring.vars
+  let vars         := vars'.map fun x => vars[x]!
+  let ra           := ra.renameVars varRename
+  let rb           := rb.renameVars varRename
+  let ctx          ← toContextExpr vars
+  let h := if let some (charInst, c) := ring.charInst? then
+    mkApp5 (mkConst ``Grind.CommRing.Expr.eq_of_toPolyC_nc_eq [ring.u]) ring.type (toExpr c) ring.ringInst charInst ctx
+  else
+    mkApp3 (mkConst ``Grind.CommRing.Expr.eq_of_toPoly_nc_eq [ring.u]) ring.type ring.ringInst ctx
+  let h := mkApp3 h (toExpr ra) (toExpr rb) eagerReflBoolTrue
+  closeGoal (mkApp hne h)
+
 end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean
@@ -7,48 +7,53 @@ module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.SemiringM
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.NonCommRingM
 import Lean.Meta.Tactic.Grind.Simp
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
 namespace Lean.Meta.Grind.Arith.CommRing

-def isAddInst (inst : Expr) : RingM Bool :=
+variable [MonadLiftT MetaM m] [MonadError m] [Monad m] [MonadCanon m] [MonadRing m]
+
+def isAddInst (inst : Expr) : m Bool :=
  return isSameExpr (← getAddFn).appArg! inst
-def isMulInst (inst : Expr) : RingM Bool :=
+def isMulInst (inst : Expr) : m Bool :=
  return isSameExpr (← getMulFn).appArg! inst
-def isSubInst (inst : Expr) : RingM Bool :=
+def isSubInst (inst : Expr) : m Bool :=
  return isSameExpr (← getSubFn).appArg! inst
-def isNegInst (inst : Expr) : RingM Bool :=
+def isNegInst (inst : Expr) : m Bool :=
  return isSameExpr (← getNegFn).appArg! inst
-def isPowInst (inst : Expr) : RingM Bool :=
+def isPowInst (inst : Expr) : m Bool :=
  return isSameExpr (← getPowFn).appArg! inst
-def isIntCastInst (inst : Expr) : RingM Bool :=
+def isIntCastInst (inst : Expr) : m Bool :=
  return isSameExpr (← getIntCastFn).appArg! inst
-def isNatCastInst (inst : Expr) : RingM Bool :=
+def isNatCastInst (inst : Expr) : m Bool :=
  return isSameExpr (← getNatCastFn).appArg! inst

 private def reportAppIssue (e : Expr) : GoalM Unit := do
  reportIssue! "comm ring term with unexpected instance{indentExpr e}"

+variable [MonadLiftT GoalM m] [MonadSetTermId m]
+
 /--
 Converts a Lean expression `e` in the `CommRing` into a `CommRing.Expr` object.

 If `skipVar` is `true`, then the result is `none` if `e` is not an interpreted `CommRing` term.
 We use `skipVar := false` when processing inequalities, and `skipVar := true` for equalities and disequalities
 -/
-partial def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option RingExpr) := do
-  let mkVar (e : Expr) : RingM Var := do
+partial def reifyCore? (e : Expr) (skipVar : Bool) (gen : Nat) : m (Option RingExpr) := do
+  let mkVar (e : Expr) : m Var := do
    if (← alreadyInternalized e) then
-      mkVar e
+      mkVarCore e
    else
      internalize e gen
-      mkVar e
-  let toVar (e : Expr) : RingM RingExpr := do
+      mkVarCore e
+  let toVar (e : Expr) : m RingExpr := do
    return .var (← mkVar e)
-  let asVar (e : Expr) : RingM RingExpr := do
+  let asVar (e : Expr) : m RingExpr := do
    reportAppIssue e
    return .var (← mkVar e)
-  let rec go (e : Expr) : RingM RingExpr := do
+  let rec go (e : Expr) : m RingExpr := do
    match_expr e with
    | HAdd.hAdd _ _ _ i a b =>
      if (← isAddInst i) then return .add (← go a) (← go b) else asVar e
@@ -77,12 +82,12 @@ partial def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option
      let some k ← getNatValue? n | toVar e
      return .num k
    | _ => toVar e
-  let toTopVar (e : Expr) : RingM (Option RingExpr) := do
+  let toTopVar (e : Expr) : m (Option RingExpr) := do
    if skipVar then
      return none
    else
      return some (← toVar e)
-  let asTopVar (e : Expr) : RingM (Option RingExpr) := do
+  let asTopVar (e : Expr) : m (Option RingExpr) := do
    reportAppIssue e
    toTopVar e
  match_expr e with
@@ -114,6 +119,12 @@ partial def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option
    return some (.num k)
  | _ => toTopVar e

+partial def reify? (e : Expr) (skipVar := true) (gen : Nat := 0) : RingM (Option RingExpr) := do
+  reifyCore? e skipVar gen
+
+partial def ncreify? (e : Expr) (skipVar := true) (gen : Nat := 0) : NonCommRingM (Option RingExpr) := do
+  reifyCore? e skipVar gen
+
 private def reportSAppIssue (e : Expr) : GoalM Unit := do
  reportIssue! "comm semiring term with unexpected instance{indentExpr e}"

--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean
@@ -22,7 +22,7 @@ This function will also perform sanity-checks

 It also caches the functions representing `+`, `*`, `-`, `^`, and `intCast`.
 -/
-def getRingId? (type : Expr) : GoalM (Option Nat) := do
+def getCommRingId? (type : Expr) : GoalM (Option Nat) := do
  if let some id? := (← get').typeIdOf.find? { expr := type } then
    return id?
  else
@@ -44,17 +44,43 @@ where
    let fieldInst? ← synthInstance? <| mkApp (mkConst ``Grind.Field [u]) type
    let semiringId? := none
    let id := (← get').rings.size
-    let ring : Ring := {
+    let ring : CommRing := {
      id, semiringId?, type, u, semiringInst, ringInst, commSemiringInst,
      commRingInst, charInst?, noZeroDivInst?, fieldInst?,
    }
    modify' fun s => { s with rings := s.rings.push ring }
    return some id

-private def setSemiringId (ringId : Nat) (semiringId : Nat) : GoalM Unit := do
-  RingM.run ringId do modifyRing fun s => { s with semiringId? := some semiringId }
+/--
+Returns the ring id for the given type if there is a `Ring` instance for it.
+This function is invoked only when `getCommRingId?` returns `none`.
+-/
+def getNonCommRingId? (type : Expr) : GoalM (Option Nat) := do
+  if let some id? := (← get').nctypeIdOf.find? { expr := type } then
+    return id?
+  else
+    let id? ← go?
+    modify' fun s => { s with nctypeIdOf := s.nctypeIdOf.insert { expr := type } id? }
+    return id?
+where
+  go? : GoalM (Option Nat) := do
+    let u ← getDecLevel type
+    let ring := mkApp (mkConst ``Grind.Ring [u]) type
+    let some ringInst ← synthInstance? ring | return none
+    let semiringInst := mkApp2 (mkConst ``Grind.Ring.toSemiring [u]) type ringInst
+    trace_goal[grind.ring] "new ring: {type}"
+    let charInst? ← getIsCharInst? u type semiringInst
+    let id := (← get').ncRings.size
+    let ring : Ring := {
+      id, type, u, semiringInst, ringInst, charInst?
+    }
+    modify' fun s => { s with ncRings := s.ncRings.push ring }
+    return some id

-def getSemiringId? (type : Expr) : GoalM (Option Nat) := do
+private def setCommSemiringId (ringId : Nat) (semiringId : Nat) : GoalM Unit := do
+  RingM.run ringId do modifyCommRing fun s => { s with semiringId? := some semiringId }
+
+def getCommSemiringId? (type : Expr) : GoalM (Option Nat) := do
  if let some id? := (← get').stypeIdOf.find? { expr := type } then
    return id?
  else
@@ -68,14 +94,14 @@ where
    let some commSemiringInst ← synthInstance? commSemiring | return none
    let semiringInst := mkApp2 (mkConst ``Grind.CommSemiring.toSemiring [u]) type commSemiringInst
    let q ← shareCommon (← canon (mkApp2 (mkConst ``Grind.Ring.OfSemiring.Q [u]) type semiringInst))
-    let some ringId ← getRingId? q
+    let some ringId ← getCommRingId? q
      | throwError "`grind` unexpected failure, failure to initialize ring{indentExpr q}"
    let id := (← get').semirings.size
    let semiring : Semiring := {
      id, type, ringId, u, semiringInst, commSemiringInst
    }
    modify' fun s => { s with semirings := s.semirings.push semiring }
-    setSemiringId ringId id
+    setCommSemiringId ringId id
    return some id

 end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingM.lean
@@ -43,7 +43,11 @@ abbrev RingM.run (ringId : Nat) (x : RingM α) : GoalM α :=
 abbrev getRingId : RingM Nat :=
  return (← read).ringId

-protected def RingM.getRing : RingM Ring := do
+instance : MonadCanon RingM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
+
+protected def RingM.getCommRing : RingM CommRing := do
  let s ← get'
  let ringId ← getRingId
  if h : ringId < s.rings.size then
@@ -51,15 +55,13 @@ protected def RingM.getRing : RingM Ring := do
  else
    throwError "`grind` internal error, invalid ringId"

-protected def modifyRing (f : Ring → Ring) : RingM Unit := do
+protected def RingM.modifyCommRing (f : CommRing → CommRing) : RingM Unit := do
  let ringId ← getRingId
  modify' fun s => { s with rings := s.rings.modify ringId f }

-instance : MonadRing RingM where
-  getRing := RingM.getRing
-  modifyRing := CommRing.modifyRing
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
+instance : MonadCommRing RingM where
+  getCommRing := RingM.getCommRing
+  modifyCommRing := RingM.modifyCommRing

 abbrev withCheckCoeffDvd (x : RingM α) : RingM α :=
  withReader (fun ctx => { ctx with checkCoeffDvd := true }) x
@@ -70,14 +72,6 @@ def checkCoeffDvd : RingM Bool :=
 def getTermRingId? (e : Expr) : GoalM (Option Nat) := do
  return (← get').exprToRingId.find? { expr := e }

-def setTermRingId (e : Expr) : RingM Unit := do
-  let ringId ← getRingId
-  if let some ringId' ← getTermRingId? e then
-    unless ringId' == ringId do
-      reportIssue! "expression in two different rings{indentExpr e}"
-    return ()
-  modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
-
 /-- Returns `some c` if the current ring has a nonzero characteristic `c`. -/
 def nonzeroChar? [Monad m] [MonadRing m] : m (Option Nat) := do
  if let some (_, c) := (← getRing).charInst? then
@@ -93,7 +87,7 @@ def nonzeroCharInst? [Monad m] [MonadRing m] : m (Option (Expr × Nat)) := do
  return none

 def noZeroDivisorsInst? : RingM (Option Expr) := do
-  return (← getRing).noZeroDivInst?
+  return (← getCommRing).noZeroDivInst?

 /--
 Returns `true` if the current ring satisfies the property
@@ -102,7 +96,7 @@ Returns `true` if the current ring satisfies the property
 ```
 -/
 def noZeroDivisors : RingM Bool := do
-  return (← getRing).noZeroDivInst?.isSome
+  return (← getCommRing).noZeroDivInst?.isSome

 /-- Returns `true` if the current ring has a `IsCharP` instance. -/
 def hasChar  : RingM Bool := do
@@ -117,18 +111,29 @@ def getCharInst : RingM (Expr × Nat) := do
  return c

 def isField : RingM Bool :=
-  return (← getRing).fieldInst?.isSome
+  return (← getCommRing).fieldInst?.isSome

 def isQueueEmpty : RingM Bool :=
-  return (← getRing).queue.isEmpty
+  return (← getCommRing).queue.isEmpty

 def getNext? : RingM (Option EqCnstr) := do
-  let some c := (← getRing).queue.min? | return none
-  modifyRing fun s => { s with queue := s.queue.erase c }
+  let some c := (← getCommRing).queue.min? | return none
+  modifyCommRing fun s => { s with queue := s.queue.erase c }
  incSteps
  return some c

-def mkVar (e : Expr) : RingM Var := do
+class MonadSetTermId (m : Type → Type) where
+  setTermId : Expr → m Unit
+
+def setTermRingId (e : Expr) : RingM Unit := do
+  let ringId ← getRingId
+  if let some ringId' ← getTermRingId? e then
+    unless ringId' == ringId do
+      reportIssue! "expression in two different rings{indentExpr e}"
+    return ()
+  modify' fun s => { s with exprToRingId := s.exprToRingId.insert { expr := e } ringId }
+
+def mkVarCore [MonadLiftT GoalM m] [Monad m] [MonadRing m] [MonadSetTermId m] (e : Expr) : m Var := do
  let s ← getRing
  if let some var := s.varMap.find? { expr := e } then
    return var
@@ -137,8 +142,14 @@ def mkVar (e : Expr) : RingM Var := do
    vars       := s.vars.push e
    varMap     := s.varMap.insert { expr := e } var
  }
-  setTermRingId e
+  MonadSetTermId.setTermId e
  ringExt.markTerm e
  return var

+instance : MonadSetTermId RingM where
+  setTermId e := setTermRingId e
+
+def mkVar (e : Expr) : RingM Var :=
+  mkVarCore e
+
 end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SemiringM.lean
@@ -8,7 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.SynthInstance
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
-import Init.Grind.Ring.OfSemiring
+import Init.Grind.Ring.CommSemiringAdapter
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Functions
 public section
@@ -33,7 +33,15 @@ def getSemiring : SemiringM Semiring := do
  else
    throwError "`grind` internal error, invalid semiringId"

-protected def SemiringM.getRing : SemiringM Ring := do
+@[inline] def modifySemiring (f : Semiring → Semiring) : SemiringM Unit := do
+  let semiringId ← getSemiringId
+  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
+
+instance : MonadCanon SemiringM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
+
+protected def SemiringM.getCommRing : SemiringM CommRing := do
  let s ← get'
  let ringId := (← getSemiring).ringId
  if h : ringId < s.rings.size then
@@ -41,17 +49,13 @@ protected def SemiringM.getRing : SemiringM Ring := do
  else
    throwError "`grind` internal error, invalid ringId"

-instance : MonadRing SemiringM where
-  getRing := SemiringM.getRing
-  modifyRing f := do
-    let ringId := (← getSemiring).ringId
-    modify' fun s => { s with rings := s.rings.modify ringId f }
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e
+protected def SemiringM.modifyCommRing (f : CommRing → CommRing) : SemiringM Unit := do
+  let ringId := (← getSemiring).ringId
+  modify' fun s => { s with rings := s.rings.modify ringId f }

-@[inline] def modifySemiring (f : Semiring → Semiring) : SemiringM Unit := do
-  let semiringId ← getSemiringId
-  modify' fun s => { s with semirings := s.semirings.modify semiringId f }
+instance : MonadCommRing SemiringM where
+ getCommRing := SemiringM.getCommRing
+ modifyCommRing := SemiringM.modifyCommRing

 def getAddFn' : SemiringM Expr := do
  let s ← getSemiring
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/ToExpr.lean
@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.Poly
-public import Init.Grind.Ring.OfSemiring
+public import Init.Grind.Ring.CommSolver
+public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.ToExpr
 public section
 namespace Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.OfSemiring
+public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 import Lean.Data.PersistentArray
@@ -140,31 +140,18 @@ structure DiseqCnstr where
  -/
  ofSemiring? : Option (SemiringExpr × SemiringExpr)

-/-- State for each `CommRing` processed by this module. -/
+/-- Shared state for non-commutative and commutative rings. -/
 structure Ring where
  id             : Nat
-  /--
-  If this is a `OfSemiring.Q α` ring, this field contain the
-  `semiringId` for `α`.
-  -/
-  semiringId?    : Option Nat
  type           : Expr
  /-- Cached `getDecLevel type` -/
  u              : Level
-  /-- `Semiring` instance for `type` -/
-  semiringInst   : Expr
  /-- `Ring` instance for `type` -/
  ringInst       : Expr
-  /-- `CommSemiring` instance for `type` -/
-  commSemiringInst   : Expr
-  /-- `CommRing` instance for `type` -/
-  commRingInst   : Expr
+  /-- `Semiring` instance for `type` -/
+  semiringInst   : Expr
  /-- `IsCharP` instance for `type` if available. -/
  charInst?      : Option (Expr × Nat)
-  /-- `NoNatZeroDivisors` instance for `type` if available. -/
-  noZeroDivInst? : Option Expr
-  /-- `Field` instance for `type` if available. -/
-  fieldInst?     : Option Expr
  addFn?         : Option Expr := none
  mulFn?         : Option Expr := none
  subFn?         : Option Expr := none
@@ -172,8 +159,6 @@ structure Ring where
  powFn?         : Option Expr := none
  intCastFn?     : Option Expr := none
  natCastFn?     : Option Expr := none
-  /-- Inverse if `fieldInst?` is `some inst` -/
-  invFn?         : Option Expr := none
  one?           : Option Expr := none
  /--
  Mapping from variables to their denotations.
@@ -184,6 +169,25 @@ structure Ring where
  varMap         : PHashMap ExprPtr Var := {}
  /-- Mapping from Lean expressions to their representations as `RingExpr` -/
  denote         : PHashMap ExprPtr RingExpr := {}
+  deriving Inhabited
+
+/-- State for each `CommRing` processed by this module. -/
+structure CommRing extends Ring where
+  /-- Inverse if `fieldInst?` is `some inst` -/
+  invFn?         : Option Expr := none
+  /--
+  If this is a `OfSemiring.Q α` ring, this field contain the
+  `semiringId` for `α`.
+  -/
+  semiringId?    : Option Nat
+  /-- `CommSemiring` instance for `type` -/
+  commSemiringInst   : Expr
+  /-- `CommRing` instance for `type` -/
+  commRingInst   : Expr
+  /-- `NoNatZeroDivisors` instance for `type` if available. -/
+  noZeroDivInst? : Option Expr
+  /-- `Field` instance for `type` if available. -/
+  fieldInst?     : Option Expr
  /-- `denoteEntries` is `denote` as a `PArray` for deterministic traversal. -/
  denoteEntries  : PArray (Expr × RingExpr) := {}
  /-- Next unique id for `EqCnstr`s. -/
@@ -255,7 +259,7 @@ structure State where
  Commutative rings.
  We expect to find a small number of rings in a given goal. Thus, using `Array` is fine here.
  -/
-  rings : Array Ring := {}
+  rings : Array CommRing := {}
  /--
  Mapping from types to its "ring id". We cache failures using `none`.
  `typeIdOf[type]` is `some id`, then `id < rings.size`. -/
@@ -275,6 +279,16 @@ structure State where
  If an expression is in this map, it is not in `exprToRingId`.
  -/
  exprToSemiringId : PHashMap ExprPtr Nat := {}
+  /--
+  Non commutative rings.
+  -/
+  ncRings : Array Ring := {}
+  /- Mapping from expressions/terms to their (non-commutative) ring ids. -/
+  exprToNCRingId : PHashMap ExprPtr Nat := {}
+  /--
+  Mapping from types to its "ring id". We cache failures using `none`.
+  `nctypeIdOf[type]` is `some id`, then `id < ncRings.size`. -/
+  nctypeIdOf : PHashMap ExprPtr (Option Nat) := {}
  steps := 0
  deriving Inhabited

--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.lean
@@ -5,8 +5,8 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.Poly
-public import Init.Grind.Ring.OfSemiring
+public import Init.Grind.Ring.CommSolver
+public import Init.Grind.Ring.CommSemiringAdapter
 public import Lean.Meta.Tactic.Grind.VarRename
 namespace Lean.Grind.CommRing
 open Lean.Meta.Grind
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean
@@ -34,7 +34,7 @@ where
  | .add _ x p, gen => do go p (max (← Grind.getGeneration (← getVar x)) gen)

 def getIntRingId? : GoalM (Option Nat) := do
-  CommRing.getRingId? (← getIntExpr)
+  CommRing.getCommRingId? (← getIntExpr)

 /-- Normalize the polynomial using `CommRing`-/
 def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.RingExpr × CommRing.Poly × Poly)) := do
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.Poly
+public import Init.Grind.Ring.CommSolver
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
 import Init.Data.Int.OfNat
 import Lean.Data.RArray
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
-import Init.Grind.Ring.Poly
+import Init.Grind.Ring.CommSolver
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/LinearM.lean
@@ -63,18 +63,20 @@ def throwNotCommRing : LinearM α :=
 def getRing? : LinearM (Option Ring) := do
  getRingCore? (← getStruct).ringId?

-def getRing : LinearM Ring := do
+instance : MonadCanon LinearM where
+  canonExpr e := do shareCommon (← canon e)
+  synthInstance? e := Grind.synthInstance? e
+
+def LinearM.getRing : LinearM Ring := do
  let some ring ← getRing?
    | throwNotCommRing
  return ring

 instance : MonadRing LinearM where
-  getRing := Linear.getRing
+  getRing := LinearM.getRing
  modifyRing f := do
    let some ringId := (← getStruct).ringId? | throwNotCommRing
    RingM.run ringId do modifyRing f
-  canonExpr e := do shareCommon (← canon e)
-  synthInstance? e := Grind.synthInstance? e

 def withRingM (x : RingM α) : LinearM α := do
  let some ringId := (← getStruct).ringId?
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
-import Init.Grind.Ring.Poly
+import Init.Grind.Ring.CommSolver
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean
@@ -42,14 +42,14 @@ We use `skipVar := false` when processing inequalities, and `skipVar := true` fo
 partial def reify? (e : Expr) (skipVar : Bool) (generation : Nat := 0) : LinearM (Option LinExpr) := do
  match_expr e with
  | HAdd.hAdd _ _ _ i a b =>
-    if isAddInst (← getStruct  ) i then return some (.add (← go a) (← go b)) else asTopVar e
+    if isAddInst (← getStruct) i then return some (.add (← go a) (← go b)) else asTopVar e
  | HSub.hSub _ _ _ i a b =>
-    if isSubInst (← getStruct  ) i then return some (.sub (← go a) (← go b)) else asTopVar e
+    if isSubInst (← getStruct) i then return some (.sub (← go a) (← go b)) else asTopVar e
  | HSMul.hSMul _ _ _ i a b =>
    let some r ← processSMul i a b | asTopVar e
    return some r
  | Neg.neg _ i a =>
-    if isNegInst (← getStruct  ) i then return some (.neg (← go a)) else asTopVar e
+    if isNegInst (← getStruct) i then return some (.neg (← go a)) else asTopVar e
  | Zero.zero _ i =>
    if isZeroInst (← getStruct) i then return some .zero else asTopVar e
  | OfNat.ofNat _ _ _ =>
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean
@@ -70,7 +70,7 @@ private def isCutsatType (type : Expr) : GoalM Bool := do

 private def getCommRingInst? (ringId? : Option Nat) : GoalM (Option Expr) := do
  let some ringId := ringId? | return none
-  return some (← CommRing.RingM.run ringId do return (← CommRing.getRing).commRingInst)
+  return some (← CommRing.RingM.run ringId do return (← CommRing.getCommRing).commRingInst)

 private def mkRingInst? (u : Level) (type : Expr) (commRingInst? : Option Expr) : GoalM (Option Expr) := do
  if let some commRingInst := commRingInst? then
@@ -206,7 +206,7 @@ def getStructId? (type : Expr) : GoalM (Option Nat) := do
 where
  go? : GoalM (Option Nat) := do
    let u ← getDecLevel type
-    let ringId? ← CommRing.getRingId? type
+    let ringId? ← CommRing.getCommRingId? type
    let leInst? ← getInst? ``LE u type
    let ltInst? ← getInst? ``LT u type
    let lawfulOrderLTInst? ← mkLawfulOrderLTInst? u type ltInst? leInst?
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 module
 prelude
-public import Init.Grind.Ring.Poly
+public import Init.Grind.Ring.CommSolver
 public import Init.Grind.Ordered.Linarith
 public import Lean.Meta.Tactic.Grind.Types
 public import Init.Data.Rat.Basic
--- a/tests/lean/run/grind_mon_order.lean
+++ b/tests/lean/run/grind_mon_order.lean
@@ -1,5 +1,5 @@
 module
-public import Init.Grind.Ring.Poly
+public import Init.Grind.Ring.CommSolver
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 open Lean.Grind.CommRing

--- a/tests/lean/run/grind_noncomm_ring.lean
+++ b/tests/lean/run/grind_noncomm_ring.lean
@@ -0,0 +1,12 @@
+open Lean Grind
+
+variable (R : Type u) [Ring R]
+example (a b c : R) : a * (b - c) = - a * c + a * b := by grind
+example (a b : R) : (a - b)^2 = a^2 - a * b - b * a + b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 + 2 * a * b + 2 * b * a + 4 * b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 + 2 * a * b + -b * (-2) * a + 4 * b^2 := by grind
+example (a b : R) : (a + 2 * b)^2 = a^2 + 2 * a * b + -b * (-4) * a - 2*b*a + 4 * b^2 := by grind
+
+variable [IsCharP R 4]
+example (a b : R) : (a - b)^2 = a^2 - a * b - b * 5 * a + b^2 := by grind
+example (a b : R) : (a - b)^2 = 13*a^2 - a * b - b * 5 * a + b*3*b*3 := by grind
Author	SHA1	Message	Date
Leonardo de Moura	f070d7ed4d	test:	2025-09-14 00:16:05 -07:00
Leonardo de Moura	2c6241956b	feat: `IsCharP` support for non commutative rings	2025-09-14 00:15:28 -07:00
Leonardo de Moura	7220d09b52	fix: `Poly.mulMonC_nc`	2025-09-14 00:09:05 -07:00
Leonardo de Moura	ff24bbdc06	test:	2025-09-14 00:00:01 -07:00
Leonardo de Moura	fea53a856b	fix: `Poly.mulMon_nc`	2025-09-13 23:59:47 -07:00
Leonardo de Moura	f226a6428c	feat: add processNewDiseqNonCommRing	2025-09-13 22:07:15 -07:00
Leonardo de Moura	4db8458a09	feat: internalizer for noncomm ring	2025-09-13 21:45:54 -07:00
Leonardo de Moura	8277c2c8e1	feat: add `NonCommRingM`	2025-09-13 21:22:24 -07:00
Leonardo de Moura	7a36cd4bad	refactor: generalize `reify?`	2025-09-13 21:05:27 -07:00
Leonardo de Moura	d346484339	refactor: split `Ring` & `CommRing`	2025-09-13 20:50:00 -07:00
Leonardo de Moura	70460c542e	chore: leftover spaces	2025-09-13 20:06:14 -07:00
Leonardo de Moura	1390e9e600	refactor: rename `getRingId?` => `getCommRingId?`	2025-09-13 20:00:41 -07:00
Leonardo de Moura	096df48b1c	feat: helper theorem for normalizing non commutative rings with a known characteristic	2025-09-13 19:52:53 -07:00
Leonardo de Moura	bc02c93f14	feat: helper theorem for normalizing non commutative rings	2025-09-13 19:45:11 -07:00
Leonardo de Moura	5298b5dbcc	feat: some functions for normalizing non commutative rings	2025-09-13 19:33:19 -07:00
Leonardo de Moura	be067f0a56	feat: add `natCast_mul_left_comm` and `intCast_mul_left_comm`	2025-09-13 19:14:04 -07:00
Leonardo de Moura	e1484b5820	chore: remove unnecessary `[expose]`s	2025-09-13 18:43:33 -07:00
Leonardo de Moura	26baca6a12	fix: some tests	2025-09-13 18:35:46 -07:00
Leonardo de Moura	09228588aa	feat: generalize some results	2025-09-13 18:35:11 -07:00
Leonardo de Moura	bd718e28d4	feat: add `natCast_mul_comm` and `intCast_mul_comm`	2025-09-13 18:22:47 -07:00
Leonardo de Moura	a4b01f16ac	refactor: rename `Ring/OfSemiring.lean` to `Ring/CommSemiringAdapter.lean`	2025-09-13 10:38:00 -07:00
Leonardo de Moura	4443eaae9c	refactor: rename `Ring/Poly.lean` to `Ring/CommSolver.lean`	2025-09-13 10:35:47 -07:00