fix: bug in cutsat model construction (#10951)

This PR fixes a bug in the `cutsat` incremental model construction. The
model was not being reset when new (unsatisfied) equalities were
asserted.

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

@@ -359,6 +359,8 @@ def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   trace[grind.debug.cutsat.subst] ">> {← getVar x}, {← c.pp}"
   trace[grind.cutsat.assert.store] "{← c.pp}"
   trace[grind.debug.cutsat.elimEq] "{← getVar x}, {← c.pp}"
+  if (← c.satisfied) == .false then
+    resetAssignmentFrom x
   modify' fun s => { s with
     elimEqs := s.elimEqs.set x (some c)
     elimStack := x :: s.elimStack

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

@@ -218,6 +218,14 @@ def DiseqCnstr.satisfied (c : DiseqCnstr) : GoalM LBool := do
   let some v ← c.p.eval? | return .undef
   return v != 0 |>.toLBool
 
+/--
+Returns `.true` if `c` is satisfied by the current partial model,
+`.undef` if `c` contains unassigned variables, and `.false` otherwise.
+-/
+def EqCnstr.satisfied (c : EqCnstr) : GoalM LBool := do
+  let some v ← c.p.eval? | return .undef
+  return v == 0 |>.toLBool
+
 /--
 Given a polynomial `p`, returns `some (x, k, c)` if `p` contains the monomial `k*x`,
 and `x` has been eliminated using the equality `c`.

tests/lean/run/grind_finish_trace.lean

@@ -162,3 +162,21 @@ example (f : Int → Int → Int) (x y : Int)
   grind =>
     -- We can use `have` to golf proofs using `mbtc` and `cases`
     have : x = 1
+
+example (f : Int → Int) (x y : Int)
+    : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
+  grind
+
+example (f : Int → Int) (x y : Int)
+    : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
+  grind =>
+    mbtc
+    cases #23ad <;> mbtc <;> cases #beb4 <;> mbtc <;> cases #beed
+
+example (f : Int → Int) (x y : Int)
+    : 0 ≤ x → x ≤ 2 → f 0 = y → f 1 = y → f 2 = y → f x = y := by
+  grind =>
+    -- Again, we can use `have` to golf the proof with `mbtc`
+    have : x ≠ 0
+    have : x ≠ 1
+    have : x ≠ 2