From a0acbd77ea784d43d8daab052567da0087b3783c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 17 Mar 2025 15:29:42 -0700
Subject: [PATCH] feat: not divides in cutsat (#7536)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR implements support for `¬ d ∣ p` in the cutsat procedure.
---
 src/Init/Data/Int/Linear.lean                       |  6 ++++++
 .../Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean    | 13 +++----------
 tests/lean/run/grind_cutsat_div_1.lean              |  6 ++++++
 3 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 994d7fa700..90c9f25ac2 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/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
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean
index bdc2933429..72df15a262 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean
+++ b/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 ()
diff --git a/tests/lean/run/grind_cutsat_div_1.lean b/tests/lean/run/grind_cutsat_div_1.lean
index d95c22bb1c..bb35017683 100644
--- a/tests/lean/run/grind_cutsat_div_1.lean
+++ b/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