fix: 0 divides constraint in grind (#14373)

This PR fixes nontermination in `grind` triggered by constraints of the
form `0 ∣ p`.

Author: leodemoura

src/Init/Data/Int/Linear.lean

@@ -980,6 +980,10 @@ theorem dvd_norm (ctx : Context) (d : Int) (p₁ p₂ : Poly) : p₁.norm.beq' p
   intro h₁
   simp [Poly.denote_norm ctx p₁, h₁]
 
+theorem eq_of_zero_dvd (ctx : Context) (p : Poly) : 0 ∣ p.denote' ctx → p.denote' ctx = 0 := by
+  intro ⟨k, h⟩
+  rw [h, Int.zero_mul]
+
 theorem le_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm.beq' p₂) : p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 := by
   simp at h
   replace h := congrArg (Poly.denote ctx) h

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

@@ -62,6 +62,12 @@ partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
   if c.isTrivial then
     trace[grind.lia.assert.trivial] "{← c.pp}"
     return ()
+  if c.d == 0 then
+    -- `0 ∣ p` is equivalent to `p = 0`. The model search assumes `d ≠ 0` for
+    -- stored divisibility constraints (it computes `_ % d` and `_ / d`).
+    let c' : EqCnstr := { p := c.p, h := .ofZeroDvd c }
+    c'.assert
+    return ()
   let d₁ := c.d
   let .add a₁ x p₁ := c.p | c.throwUnexpected
   if (← c.satisfied) == .false then

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

@@ -360,6 +360,9 @@ private partial def EqCnstr.toExprProofImpl (c' : EqCnstr) : ProofM Expr := cach
     return mkApp6 (mkConst ``Int.Internal.Linear.eq_of_le_ge)
       (← getContext) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p)
       eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
+  | .ofZeroDvd c =>
+    return mkApp3 (mkConst ``Int.Internal.Linear.eq_of_zero_dvd)
+      (← getContext) (← mkPolyDecl c.p) (← c.toExprProof)
   | .reorder c => withUnordered <| c.toExprProof
   | .commRingNorm c e p =>
     let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) eagerReflBoolTrue
@@ -635,6 +638,7 @@ partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do u
   | .core0 .. | .core .. | .defn .. | .defnNat ..
   | .defnCommRing .. | .defnNatCommRing .. | .coreToInt .. => return () -- Equalities coming from the core never contain cutsat decision variables
   | .commRingNorm c .. | .reorder c | .norm c | .divCoeffs c | .div _ _ c | .mod _ _ c => c.collectDecVars
+  | .ofZeroDvd c => c.collectDecVars
   | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
   | .mul _ cs => cs.forM fun (_, _, c) => c.collectDecVars
   | .pow _ ca? _ cb? => ca?.forM (·.collectDecVars); cb?.forM (·.collectDecVars)

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

@@ -90,6 +90,8 @@ inductive EqCnstrProof where
   | divCoeffs (c : EqCnstr)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | ofLeGe (c₁ : LeCnstr) (c₂ : LeCnstr)
+  | /-- `p = 0` derived from the divisibility constraint `c` of the form `0 ∣ p`. -/
+    ofZeroDvd (c : DvdCnstr)
   | reorder (c : EqCnstr)
   | commRingNorm (c : EqCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
   | defnCommRing (e : Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly)

tests/elab/grind_cutsat_loop.lean

@@ -0,0 +1,22 @@
+/-!
+Tests for divisibility constraints with divisor `0` in `grind`'s cutsat procedure.
+Cutsat used to store `0 ∣ p` constraints, but the model search assumes a nonzero
+divisor: it could loop forever in `DvdSolution.geAvoiding` (the original example
+below), or weaken bounds via `tightUsingDvd` and miss refutations. `0 ∣ p` is now
+converted into the equality `p = 0` when asserted.
+-/
+
+-- Used to hang: `0 ∣ b` with `b ≠ 0` excludes the single solution of the
+-- divisibility constraint, and the model search looped bumping the candidate.
+theorem mwe {b : Nat} (p : Nat) (x1 x2 : Nat) (hb0 : b ≠ 0) (hab : 0 ∣ b) :
+    0 / p ^ x1 ∣ b / p ^ x2 := by
+  grind
+
+-- Used to fail: the diseq was folded into the bound `b ≥ 1`, which `tightUsingDvd`
+-- then weakened back to `b ≥ 0` using the `0 ∣ b` constraint, producing the bogus
+-- model `b := 0`.
+example (b : Nat) (h1 : b ≠ 0) (h2 : 0 ∣ b) : False := by
+  grind
+
+example (a b : Nat) (h : 0 ∣ a + b) (h1 : a + b ≠ 0) : False := by
+  grind