feat: not divides in cutsat (#7536)

This PR implements support for `¬ d ∣ p` in the cutsat procedure.

src/Init/Data/Int/Linear.lean

@@ -1790,6 +1790,12 @@ theorem not_eq_norm_expr (ctx : Context) (lhs rhs : Expr) (p : Poly)
   intro; subst p; simp
   intro; rwa [Int.sub_eq_zero]
 
+theorem of_not_dvd (a b : Int) : a != 0 → ¬ (a ∣ b) → b % a > 0 := by
+  simp; intro h₁ h₂
+  replace h₂ := Int.emod_pos_of_not_dvd h₂
+  simp [h₁] at h₂
+  assumption
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

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

@@ -100,11 +100,7 @@ def propagateIntDvd (e : Expr) : GoalM Unit := do
     trace[grind.cutsat.assert.dvd] "{← c.pp}"
     c.assert
   else if (← isEqFalse e) then
-    /-
-    TODO: we have `¬ a ∣ b`, we should assert
-    `∃ x z, b = a*x + z ∧ 1 ≤ z < a`
-    -/
-    throwError "NIY: ¬ {e}"
+    pushNewFact <| mkApp4 (mkConst ``Int.Linear.of_not_dvd) a b reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
 
 def propagateNatDvd (e : Expr) : GoalM Unit := do
   let some (d, b, ctx) ← Int.OfNat.toIntDvd? e | return ()
@@ -115,11 +111,8 @@ def propagateNatDvd (e : Expr) : GoalM Unit := do
     let c := { d, p, h := .coreNat e ctx d b b' : DvdCnstr }
     c.assert
   else
-    /-
-    TODO: we have `¬ a ∣ b`, we should assert
-    `∃ x z, b = a*x + z ∧ 1 ≤ z < a`
-    -/
-    throwError "NIY: ¬ {e}"
+    let_expr Dvd.dvd _ _ a b ← e | return ()
+    pushNewFact <| mkApp3 (mkConst ``Nat.emod_pos_of_not_dvd) a b (mkOfEqFalseCore e (← mkEqFalseProof e))
 
 builtin_grind_propagator propagateDvd ↓Dvd.dvd := fun e => do
   let_expr Dvd.dvd α _ _ _ ← e | return ()

tests/lean/run/grind_cutsat_div_1.lean

@@ -82,3 +82,9 @@ set_option trace.grind.cutsat.conflict true in
 example (f : Int → Int) (_ : 2 ∣ f 0 + 3) (_ : 3 ∣ f 0 + f 1 - 4) (_ : f 0 ≥ 11): False := by
   fail_if_success grind
   sorry
+
+example (x : Int) (_ : 10 ∣ x) (_ : ¬ 5 ∣ x) : False := by
+  grind
+
+example (x : Nat) (_ : 10 ∣ x) (_ : ¬ 5 ∣ x) : False := by
+  grind