feat: detect unsat comm ring equality

src/Init/Grind/CommRing/Basic.lean

@@ -125,11 +125,14 @@ theorem neg_sub (a b : α) : -(a - b) = b - a := by
 theorem sub_self (a : α) : a - a = 0 := by
   rw [sub_eq_add_neg, add_neg_cancel]
 
-theorem eq_of_sub_eq_zero {a b : α} : a - b = 0 → a = b := by
-  intro h
-  replace h := congrArg (. + b) h; simp only at h
-  rw [sub_eq_add_neg, add_assoc, neg_add_cancel, add_zero, zero_add] at h
-  assumption
+theorem sub_eq_iff {a b c : α} : a - b = c ↔ a = c + b := by
+  rw [sub_eq_add_neg]
+  constructor
+  next => intro; subst c; rw [add_assoc, neg_add_cancel, add_zero]
+  next => intro; subst a; rw [add_assoc, add_comm b, neg_add_cancel, add_zero]
+
+theorem sub_eq_zero_iff {a b : α} : a - b = 0 ↔ a = b := by
+  simp [sub_eq_iff, zero_add]
 
 instance intCastInst : IntCast α where
   intCast n := match n with

src/Init/Grind/CommRing/Poly.lean

@@ -648,8 +648,23 @@ theorem ne_unsat {α} [CommRing α] (ctx : Context α) (a b : Expr)
   simp [ne_unsat_cert]
   intro h
   replace h := congrArg (Poly.denote ctx .) h
-  simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero] at h
-  replace h := eq_of_sub_eq_zero h
+  simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_zero_iff] at h
+  assumption
+
+def eq_unsat_cert (a b : Expr) (k : Int) : Bool :=
+  k != 0 && (a.sub b).toPoly == .num k
+
+-- Remark: `[IsCharP α 0]` after `(ctx : Context α)` is not a mistake.
+-- The `grind` procedure assumes that support theorems start with `{α} [CommRing α] (ctx : Context α)`
+theorem eq_unsat {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (a b : Expr) (k : Int)
+    : eq_unsat_cert a b k → a.denote ctx = b.denote ctx → False := by
+  simp [eq_unsat_cert]
+  intro h₁ h₂
+  replace h₂ := congrArg (Poly.denote ctx .) h₂
+  simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_iff] at h₂
+  have := IsCharP.intCast_eq_zero_iff (α := α) 0 k
+  simp [h₁] at this
+  rw [h₂, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
   assumption
 
 /-!
@@ -782,8 +797,21 @@ theorem ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b :
   simp [ne_unsatC_cert]
   intro h
   replace h := congrArg (Poly.denote ctx .) h
-  simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero] at h
-  replace h := eq_of_sub_eq_zero h
+  simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_zero_iff] at h
+  assumption
+
+def eq_unsatC_cert (a b : Expr) (c : Nat) (k : Int) : Bool :=
+  k != 0 && k % c != 0 && (a.sub b).toPolyC c == .num k
+
+theorem eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr) (k : Int)
+    : eq_unsatC_cert a b c k → a.denote ctx = b.denote ctx → False := by
+  simp [eq_unsatC_cert]
+  intro h₁ h₂ h₃
+  replace h₃ := congrArg (Poly.denote ctx .) h₃
+  simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_iff] at h₃
+  have := IsCharP.intCast_eq_zero_iff (α := α) c k
+  simp [h₁, h₂] at this
+  rw [h₃, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
   assumption
 
 end CommRing

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

@@ -9,7 +9,7 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 
 namespace Lean.Meta.Grind.Arith.CommRing
 
-private def toRingExpr? (e : Expr) (ringId : Nat) : GoalM (Option RingExpr) := do
+private def toRingExpr? (ringId : Nat) (e : Expr) : GoalM (Option RingExpr) := do
   let ring ← getRing ringId
   if let some re := ring.denote.find? { expr := e } then
     return some re
@@ -19,23 +19,36 @@ private def toRingExpr? (e : Expr) (ringId : Nat) : GoalM (Option RingExpr) := d
     reportIssue! "failed to convert to ring expression{indentExpr e}"
     return none
 
+/-- Returns `some ringId` if `a` and `b` are elements of the same ring. -/
+private def inSameRing? (a b : Expr) : GoalM (Option Nat) := do
+  let some ringId ← getTermRingId? a | return none
+  let some ringId' ← getTermRingId? b | return none
+  unless ringId == ringId' do return none -- This can happen when we have heterogeneous equalities
+  return ringId
+
 @[export lean_process_ring_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
   if isSameExpr a b then return () -- TODO: check why this is needed
+  let some ringId ← inSameRing? a b | return ()
   trace[grind.ring] "{← mkEq a b}"
-  -- TODO
+  let some ra ← toRingExpr? ringId a | return ()
+  let some rb ← toRingExpr? ringId b | return ()
+  let p ← toPoly ringId (ra.sub rb)
+  if let .num k := p then
+    if k != 0 && (← hasChar ringId) then
+      setEqUnsat ringId k a b ra rb
+      return ()
+  -- TODO: save equality
 
 @[export lean_process_ring_diseq]
 def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
-  let some ringId ← getTermRingId? a | return ()
-  let some ringId' ← getTermRingId? b | return ()
-  unless ringId == ringId' do return () -- This can happen when we have heterogeneous equalities
+  let some ringId ← inSameRing? a b | return ()
   trace[grind.ring] "{mkNot (← mkEq a b)}"
-  let some e₁ ← toRingExpr? a ringId | return ()
-  let some e₂ ← toRingExpr? b ringId | return ()
-  let p ← toPoly (e₁.sub e₂) ringId
+  let some ra ← toRingExpr? ringId a | return ()
+  let some rb ← toRingExpr? ringId b | return ()
+  let p ← toPoly ringId (ra.sub rb)
   if p == .num 0 then
-    setNeUnsat ringId a b e₁ e₂
+    setNeUnsat ringId a b ra rb
     return ()
   -- TODO: save disequalitys
 

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

@@ -34,4 +34,12 @@ def setNeUnsat (ringId : Nat) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do
   let h ← mkLemmaPrefix ringId ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC
   closeGoal <| mkApp4 h (toExpr ra) (toExpr rb) reflBoolTrue (← mkDiseqProof a b)
 
+def setEqUnsat (ringId : Nat) (k : Int) (a b : Expr) (ra rb : RingExpr) : GoalM Unit := do
+  trace[grind.ring.assert] "unsat eq {a}, {b}"
+  let mut h ← mkLemmaPrefix ringId ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC
+  let (charInst, c) ← getCharInst ringId
+  if c == 0 then
+    h := mkApp h charInst
+  closeGoal <| mkApp5 h (toExpr ra) (toExpr rb) (toExpr k) reflBoolTrue (← mkEqProof a b)
+
 end Lean.Meta.Grind.Arith.CommRing

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

@@ -50,11 +50,23 @@ def nonzeroCharInst? (ringId : Nat) : GoalM (Option (Expr × Nat)) := do
       return some (inst, c)
   return none
 
+/-- Returns `true` if the ring has a `IsCharP` instance. -/
+def hasChar (ringId : Nat) : GoalM Bool := do
+  return (← getRing ringId).charInst?.isSome
+
+/--
+Returns the pair `(charInst, c)`. If the ring does not have a `IsCharP` instance, then throws internal error.
+-/
+def getCharInst (ringId : Nat) : GoalM (Expr × Nat) := do
+  let some c := (← getRing ringId).charInst?
+    | throwError "`grind` internal error, ring does not have a characteristic"
+  return c
+
 /--
 Converts the given ring expression into a multivariate polynomial.
 If the ring has a nonzero characteristic, it is used during normalization.
 -/
-def toPoly (e : RingExpr) (ringId : Nat) : GoalM Poly := do
+def toPoly (ringId : Nat) (e : RingExpr) : GoalM Poly := do
   if let some c ← nonzeroChar? ringId then
     return e.toPolyC c
   else

tests/lean/run/grind_ring_1.lean

@@ -21,3 +21,25 @@ example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
 
 example (x : BitVec 8) : (x + 1)^2 - 1 = x^2 + 2*x := by
   grind +ring
+
+example (x : Int) : (x + 1)*(x - 1) = x^2 → False := by
+  grind +ring
+
+example (x y : Int) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
+  grind +ring
+
+example (x : UInt8) : (x + 1)*(x - 1) = x^2 → False := by
+  grind +ring
+
+example (x y : BitVec 8) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
+  grind +ring
+
+example [CommRing α] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
+  fail_if_success grind +ring
+  sorry
+
+example [CommRing α] [IsCharP α 0] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
+  grind +ring
+
+example [CommRing α] [IsCharP α 8] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
+  grind +ring