refactor: add RingDiseqCnstr to grind linarith

src/Init/Grind/Ring/CommSolver.lean

@@ -1393,15 +1393,19 @@ theorem simp {α} [CommRing α] (ctx : Context α) (k₁ : Int) (p₁ : Poly) (k
 noncomputable def mul_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
   p₁.mulConst_k k |>.beq' p
 
-def mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
+theorem 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]
 
+theorem inv {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (p : Poly)
+    : mul_cert p₁ (-1) p → p₁.denote ctx = 0 → p.denote ctx = 0 :=
+  mul ctx p₁ (-1) p
+
 noncomputable def div_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
   !Int.beq' k 0 |>.and' (p.mulConst_k k |>.beq' p₁)
 
-def div {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly)
+theorem 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
@@ -1575,60 +1579,62 @@ theorem Poly.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) (
 open Stepwise
 
 theorem eq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denoteAsIntModule ctx = 0 := by
-  rw [Poly.denoteAsIntModule_eq_denote]; apply core
+    : core_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote ctx = 0 := by
+  apply core
+
+theorem eq_int_module {α} [CommRing α] (ctx : Context α) (p : Poly)
+    : p.denote ctx = 0 → p.denoteAsIntModule ctx = 0 := by
+  simp [Poly.denoteAsIntModule_eq_denote]
 
 theorem diseq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denoteAsIntModule ctx ≠ 0 := by
-  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
+    : core_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denote ctx ≠ 0 := by
+  simp [core_cert]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
   intro h; rw [sub_eq_zero_iff] at h; contradiction
 
+theorem diseq_int_module {α} [CommRing α] (ctx : Context α) (p : Poly)
+    : p.denote ctx ≠ 0 → p.denoteAsIntModule ctx ≠ 0 := by
+  simp [Poly.denoteAsIntModule_eq_denote]
+
 open OrderedAdd
 
 theorem le_norm {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by
-  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
+    : core_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx ≤ 0 := by
+  simp [core_cert]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h := add_le_left h ((-1) * rhs.denote ctx)
   rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h
   assumption
 
+theorem le_int_module {α} [CommRing α] [LE α] (ctx : Context α) (p : Poly)
+    : p.denote ctx ≤ 0 → p.denoteAsIntModule ctx ≤ 0 := by
+  simp [Poly.denoteAsIntModule_eq_denote]
+
 theorem lt_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by
-  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
+    : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote ctx < 0 := by
+  simp [core_cert]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h := add_lt_left h ((-1) * rhs.denote ctx)
   rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h
   assumption
 
+theorem lt_int_module {α} [CommRing α] [LT α] (ctx : Context α) (p : Poly)
+    : p.denote ctx < 0 → p.denoteAsIntModule ctx < 0 := by
+  simp [Poly.denoteAsIntModule_eq_denote]
+
 theorem not_le_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx < 0 := by
-  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
+    : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx < 0 := by
+  simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h₁ := LinearOrder.lt_of_not_le h₁
   replace h₁ := add_lt_left h₁ (-lhs.denote ctx)
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
 theorem not_lt_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by
-  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
+    : core_cert rhs lhs p → ¬ lhs.denote ctx < rhs.denote ctx → p.denote ctx ≤ 0 := by
+  simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
   replace h₁ := LinearOrder.le_of_not_lt h₁
   replace h₁ := add_le_left h₁ (-lhs.denote ctx)
   simp [← sub_eq_add_neg, sub_self] at h₁
   assumption
 
-theorem not_le_norm' {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by
-  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
-  replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) ≤ _ := add_le_right (rhs.denote ctx) h
-  rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
-  contradiction
-
-theorem not_lt_norm' {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
-    : core_cert lhs rhs p → ¬ lhs.denote ctx < rhs.denote ctx → ¬ p.denoteAsIntModule ctx < 0 := by
-  simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h
-  replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) < _ := add_lt_right (rhs.denote ctx) h
-  rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h
-  contradiction
-
 theorem inv_int_eq [Field α] [IsCharP α 0] (b : Int) : b != 0 → (denoteInt b : α) * (denoteInt b)⁻¹ = 1 := by
   simp; intro h
   have : (denoteInt b : α) ≠ 0 := by

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

@@ -46,19 +46,21 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue :
   let some rhs ← withRingM <| CommRing.reify? rhs (skipVar := false) | return ()
   let generation ← getGeneration e
   if eqTrue then
-    let p' := (lhs.sub rhs).toPoly
-    let lhs' ← p'.toIntModuleExpr generation
-    let some lhs' ← reify? lhs' (skipVar := false) generation | return ()
-    let p := lhs'.norm
-    let c : IneqCnstr := { p, strict, h := .coreCommRing e lhs rhs p' lhs' }
+    let p := (lhs.sub rhs).toPoly
+    let c : RingIneqCnstr := { p, strict, h := .core e lhs rhs }
+    let lhs ← p.toIntModuleExpr generation
+    let some lhs ← reify? lhs (skipVar := false) generation | return ()
+    let p := lhs.norm
+    let c : IneqCnstr := { p, strict, h := .ring c lhs }
     c.assert
   else if (← isLinearOrder) then
-    let p' := (rhs.sub lhs).toPoly
+    let p := (rhs.sub lhs).toPoly
     let strict := !strict
-    let lhs' ← p'.toIntModuleExpr generation
-    let some lhs' ← reify? lhs' (skipVar := false) generation | return ()
-    let p := lhs'.norm
-    let c : IneqCnstr := { p, strict, h := .notCoreCommRing e lhs rhs p' lhs' }
+    let c : RingIneqCnstr := { p, strict, h := .notCore e lhs rhs }
+    let lhs ← p.toIntModuleExpr generation
+    let some lhs ← reify? lhs (skipVar := false) generation | return ()
+    let p := lhs.norm
+    let c : IneqCnstr := { p, strict, h := .ring c lhs }
     c.assert
   else
     -- Negation for preorders is not supported

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

@@ -204,6 +204,22 @@ private def mkCommRingThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
   return mkApp3 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getRingContext)
 
+/--
+Returns the prefix of a theorem with name `declName` where the first four arguments are
+`{α} [CommRing α] [LE α] (rctx : Context α)`
+-/
+private def mkCommRingLEThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp4 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLEInst) (← getRingContext)
+
+/--
+Returns the prefix of a theorem with name `declName` where the first four arguments are
+`{α} [CommRing α] [LT α] (rctx : Context α)`
+-/
+private def mkCommRingLTThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp4 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLTInst) (← getRingContext)
+
 /--
 Returns the prefix of a theorem with name `declName` where the first five arguments are
 `{α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (rctx : Context α)`
@@ -228,6 +244,31 @@ private def mkCommRingLinOrdThmPrefix (declName : Name) : ProofM Expr := do
   let s ← getStruct
   return mkApp8 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLEInst) (← getLTInst) (← getLawfulOrderLTInst) (← getIsLinearOrderInst) (← getOrderedRingInst) (← getRingContext)
 
+partial def RingIneqCnstr.toExprProof (c' : RingIneqCnstr) : ProofM Expr := do
+  match c'.h with
+  | .core e lhs rhs =>
+    let h' ← if c'.strict then mkCommRingLawfulPreOrdThmPrefix ``Grind.CommRing.lt_norm else mkCommRingPreOrdThmPrefix ``Grind.CommRing.le_norm
+    return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e))
+  | .notCore e lhs rhs =>
+    let h' ← mkCommRingLinOrdThmPrefix (if c'.strict then ``Grind.CommRing.not_le_norm else ``Grind.CommRing.not_lt_norm)
+    return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
+
+partial def RingEqCnstr.toExprProof (c' : RingEqCnstr) : ProofM Expr := do
+  match c'.h with
+  | .core a b la lb =>
+    let h' ← mkCommRingThmPrefix ``Grind.CommRing.eq_norm
+    return mkApp5 h' (← mkRingExprDecl la) (← mkRingExprDecl lb) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (← mkEqProof a b)
+  | .symm c =>
+    let h ← c.toExprProof
+    let h' ← mkCommRingThmPrefix ``Grind.CommRing.Stepwise.inv
+    return mkApp4 h' (← mkRingPolyDecl c.p) (← mkRingPolyDecl c'.p) eagerReflBoolTrue h
+
+partial def RingDiseqCnstr.toExprProof (c' : RingDiseqCnstr) : ProofM Expr := do
+  match c'.h with
+  | .core a b lhs rhs =>
+    let h' ← mkCommRingThmPrefix ``Grind.CommRing.diseq_norm
+    return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (← mkDiseqProof a b)
+
 mutual
 partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' do
   match c'.h with
@@ -237,14 +278,10 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d
   | .notCore e lhs rhs =>
     let h ← mkIntModLinOrdThmPrefix (if c'.strict then ``Grind.Linarith.not_le_norm else ``Grind.Linarith.not_lt_norm)
     return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) eagerReflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
-  | .coreCommRing e lhs rhs p' lhs' =>
-    let h' ← if c'.strict then mkCommRingLawfulPreOrdThmPrefix ``Grind.CommRing.lt_norm else mkCommRingPreOrdThmPrefix ``Grind.CommRing.le_norm
-    let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') eagerReflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e))
-    let h ← if c'.strict then mkIntModLawfulPreOrdThmPrefix ``Grind.Linarith.lt_norm else mkIntModPreOrdThmPrefix ``Grind.Linarith.le_norm
-    return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h'
-  | .notCoreCommRing e lhs rhs p' lhs' =>
-    let h' ← mkCommRingLinOrdThmPrefix (if c'.strict then ``Grind.CommRing.not_le_norm else ``Grind.CommRing.not_lt_norm)
-    let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') eagerReflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
+  | .ring c lhs' =>
+    let h ← c.toExprProof
+    let h' ← if c'.strict then mkCommRingLTThmPrefix ``Grind.CommRing.lt_int_module else mkCommRingLEThmPrefix ``Grind.CommRing.le_int_module
+    let h' := mkApp2 h' (← mkRingPolyDecl c.p) h
     let h ← if c'.strict then mkIntModLawfulPreOrdThmPrefix ``Grind.Linarith.lt_norm else mkIntModPreOrdThmPrefix ``Grind.Linarith.le_norm
     return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h'
   | .coreOfNat e natStructId lhs rhs =>
@@ -304,11 +341,11 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d
         a b a' b' ha hb (← mkEqProof a b)
     let h ← mkIntModPreOrdThmPrefix ``Grind.Linarith.le_of_eq
     return mkApp5 h (← mkExprDecl la) (← mkExprDecl lb) (← mkPolyDecl c'.p) eagerReflBoolTrue h'
-  | .ofCommRingEq a b la lb p' lhs' =>
-    let h' ← mkCommRingThmPrefix ``Grind.CommRing.eq_norm
-    let h' := mkApp5 h' (← mkRingExprDecl la) (← mkRingExprDecl lb) (← mkRingPolyDecl p') eagerReflBoolTrue (← mkEqProof a b)
+  | .ringEq c lhs =>
+    let h' ← c.toExprProof
+    let h' := mkApp2 (← mkCommRingThmPrefix ``Grind.CommRing.eq_int_module) (← mkRingPolyDecl c.p) h'
     let h ← mkIntModPreOrdThmPrefix ``Grind.Linarith.le_of_eq
-    return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h'
+    return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h'
   | .dec h => return mkFVar h
   | .ofDiseqSplit c₁ fvarId h _ =>
     let hFalse ← h.toExprProofCore
@@ -323,11 +360,11 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c'
   | .core a b lhs rhs =>
     let h ← mkIntModThmPrefix ``Grind.Linarith.diseq_norm
     return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) eagerReflBoolTrue (← mkDiseqProof a b)
-  | .coreCommRing a b lhs rhs p' lhs' =>
-    let h' ← mkCommRingThmPrefix ``Grind.CommRing.diseq_norm
-    let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') eagerReflBoolTrue (← mkDiseqProof a b)
+  | .ring c lhs =>
+    let h' ← c.toExprProof
+    let h' := mkApp2 (← mkCommRingThmPrefix ``Grind.CommRing.diseq_int_module) (← mkRingPolyDecl c.p) h'
     let h ← mkIntModThmPrefix ``Grind.Linarith.diseq_norm
-    return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h'
+    return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h'
   | .coreOfNat a b natStructId lhs rhs =>
     let h ← OfNatModuleM.run natStructId do
       let ns ← getNatStruct
@@ -403,8 +440,8 @@ mutual
 
 partial def IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
-  | .core .. | .notCore .. | .coreCommRing .. | .notCoreCommRing .. | .coreOfNat .. | .notCoreOfNat ..
-  | .oneGtZero | .ofEq .. | .ofEqOfNat .. | .ofCommRingEq .. => return ()
+  | .core .. | .notCore .. | .coreOfNat .. | .notCoreOfNat .. | .ring .. | .ringEq ..
+  | .oneGtZero | .ofEq .. | .ofEqOfNat .. => return ()
   | .combine c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
   | .norm c₁ _ => c₁.collectDecVars
   | .dec h => markAsFound h
@@ -415,7 +452,7 @@ partial def IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit :=
 -- Actually, it cannot even contain decision variables in the current implementation.
 partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
-  | .core .. | .coreCommRing .. | .coreOfNat .. | .oneNeZero => return ()
+  | .core .. | .coreOfNat .. | .oneNeZero | .ring .. => return ()
   | .neg c => c.collectDecVars
   | .subst _ _ c₁ c₂ | .subst1 _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 

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

@@ -54,18 +54,19 @@ private def processNewCommRingEq' (a b : Expr) : LinearM Unit := do
   let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
   let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
   let generation := max (← getGeneration a) (← getGeneration b)
-  let p' := (lhs.sub rhs).toPoly
-  let lhs' ← p'.toIntModuleExpr generation
-  let some lhs' ← reify? lhs' (skipVar := false) generation | return ()
-  let p := lhs'.norm
+  let p := (lhs.sub rhs).toPoly
+  let c : RingEqCnstr := { p, h := .core a b lhs rhs }
+  let lhs ← p.toIntModuleExpr generation
+  let some lhs ← reify? lhs (skipVar := false) generation | return ()
+  let p := lhs.norm
   if p == .nil then return ()
-  let c₁ : IneqCnstr := { p, strict := false, h := .ofCommRingEq a b lhs rhs p' lhs' }
+  let c₁ : IneqCnstr := { p, strict := false, h := .ringEq c lhs }
   c₁.assert
+  let c := { c with p := c.p.mulConst (-1), h := .symm c }
   let p := p.mul (-1)
-  let p' := p'.mulConst (-1)
-  let lhs' ← p'.toIntModuleExpr generation
-  let some lhs' ← reify? lhs' (skipVar := false) generation | return ()
-  let c₂ : IneqCnstr := { p, strict := false, h := .ofCommRingEq b a rhs lhs p' lhs' }
+  let lhs ← c.p.toIntModuleExpr generation
+  let some lhs ← reify? lhs (skipVar := false) generation | return ()
+  let c₂ : IneqCnstr := { p, strict := false, h := .ringEq c lhs }
   c₂.assert
 
 private def processNewIntModuleEq' (a b : Expr) : LinearM Unit := do
@@ -271,12 +272,13 @@ def processNewEq (a b : Expr) : GoalM Unit := do
 private def processNewCommRingDiseq (a b : Expr) : LinearM Unit := do
   let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return ()
   let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
+  let p := (lhs.sub rhs).toPoly
+  let c : RingDiseqCnstr := { p, h := .core a b lhs rhs }
   let generation := max (← getGeneration a) (← getGeneration b)
-  let p' := (lhs.sub rhs).toPoly
-  let lhs' ← p'.toIntModuleExpr generation
-  let some lhs' ← reify? lhs' (skipVar := false) generation | return ()
-  let p := lhs'.norm
-  let c : DiseqCnstr := { p, h := .coreCommRing a b lhs rhs p' lhs' }
+  let lhs ← p.toIntModuleExpr generation
+  let some lhs ← reify? lhs (skipVar := false) generation | return ()
+  let p := lhs.norm
+  let c : DiseqCnstr := { p, h := .ring c lhs }
   c.assert
 
 private def processNewIntModuleDiseq (a b : Expr) : LinearM Unit := do

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

@@ -18,6 +18,42 @@ abbrev LinExpr := Lean.Grind.Linarith.Expr
 deriving instance Hashable for Poly
 deriving instance Hashable for Grind.Linarith.Expr
 
+mutual
+/-- Auxiliary type for normalizing `Ring` and `Field` inequalities. -/
+structure RingIneqCnstr where
+  p      : Grind.CommRing.Poly
+  strict : Bool
+  h      : RingIneqCnstrProof
+
+inductive RingIneqCnstrProof where
+  | core (e : Expr) (lhs rhs : Grind.CommRing.Expr)
+  | notCore (e : Expr) (lhs rhs : Grind.CommRing.Expr)
+  -- **TODO**: cleanup denominator proof step
+end
+
+mutual
+/-- Auxiliary type for normalizing `Ring` and `Field` equalities. -/
+structure RingEqCnstr where
+  p      : Grind.CommRing.Poly
+  h      : RingEqCnstrProof
+
+inductive RingEqCnstrProof where
+  | core (a b : Expr) (ra rb : Grind.CommRing.Expr)
+  | symm (c : RingEqCnstr)
+  -- **TODO**: cleanup denominator proof step
+end
+
+mutual
+/-- Auxiliary type for normalizing `Ring` and `Field` disequalities. -/
+structure RingDiseqCnstr where
+  p      : Grind.CommRing.Poly
+  h      : RingDiseqCnstrProof
+
+inductive RingDiseqCnstrProof where
+  | core (a b : Expr) (ra rb : Grind.CommRing.Expr)
+  -- **TODO**: cleanup denominator proof step
+end
+
 mutual
 /-- An equality constraint and its justification/proof. -/
 structure EqCnstr where
@@ -41,8 +77,7 @@ structure IneqCnstr where
 inductive IneqCnstrProof where
   | core (e : Expr) (lhs rhs : LinExpr)
   | notCore (e : Expr) (lhs rhs : LinExpr)
-  | coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
-  | notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
+  | ring (c : RingIneqCnstr) (lhs : LinExpr)
   | coreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr)
   | notCoreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr)
   | combine (c₁ : IneqCnstr) (c₂ : IneqCnstr)
@@ -54,8 +89,8 @@ inductive IneqCnstrProof where
     ofEq (a b : Expr) (la lb : LinExpr)
   | /-- `a ≤ b` from an equality `a = b` coming from the core. -/
     ofEqOfNat (a b : Expr) (natStructId : Nat) (la lb : LinExpr)
-  | /-- `a ≤ b` from an equality `a = b` coming from the core. -/
-    ofCommRingEq (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
+  | /-- `p ≤ 0` from a ring equality `p = 0`. -/
+    ringEq (c : RingEqCnstr) (lhs : LinExpr)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : IneqCnstr)
 
 structure DiseqCnstr where
@@ -64,7 +99,7 @@ structure DiseqCnstr where
 
 inductive DiseqCnstrProof where
   | core (a b : Expr) (lhs rhs : LinExpr)
-  | coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr)
+  | ring (c : RingDiseqCnstr) (lhs : LinExpr)
   | coreOfNat (a b : Expr) (natStructId : Nat) (lhs rhs : LinExpr)
   | neg (c : DiseqCnstr)
   | subst (k₁ k₂ : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr)

tests/lean/run/grind_linarith_2.lean

@@ -19,7 +19,8 @@ trace: [grind.debug.proof] Classical.byContradiction fun h =>
         let re_2 := (CommRing.Expr.var 1).add (CommRing.Expr.var 0);
         diseq_unsat ctx
           (diseq_norm ctx e_2 e_1 p_1 (eagerReduce (Eq.refl true))
-            (CommRing.diseq_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h)))
+            (CommRing.diseq_int_module rctx rp_1
+              (CommRing.diseq_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h))))
 -/
 #guard_msgs in
 open Linarith in

tests/lean/run/grind_linarith_trim_context.lean

@@ -22,9 +22,11 @@ trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
           (le_lt_combine ctx p_3 p_5 p_1 (eagerReduce (Eq.refl true))
             (le_le_combine ctx p_4 p_2 p_3 (eagerReduce (Eq.refl true))
               (le_norm ctx e_3 e_2 p_4 (eagerReduce (Eq.refl true))
-                (CommRing.le_norm rctx re_3 re_2 rp_2 (eagerReduce (Eq.refl true)) h_8))
+                (CommRing.le_int_module rctx rp_2
+                  (CommRing.le_norm rctx re_3 re_2 rp_2 (eagerReduce (Eq.refl true)) h_8)))
               (le_norm ctx e_1 e_2 p_2 (eagerReduce (Eq.refl true))
-                (CommRing.le_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h_1)))
+                (CommRing.le_int_module rctx rp_1
+                  (CommRing.le_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h_1))))
             (zero_lt_one ctx p_5 (eagerReduce (Eq.refl true)) (Eq.refl One.one))))
 -/
 #guard_msgs in