chore: fix build

This PR adds helper theorems for normalizing divisibility constraints.

src/Init/Data/Int/Linear.lean

@@ -9,6 +9,7 @@ import Init.Data.Prod
 import Init.Data.Int.Lemmas
 import Init.Data.Int.LemmasAux
 import Init.Data.Int.DivModLemmas
+import Init.Data.Int.Gcd
 import Init.Data.RArray
 
 namespace Int.Linear
@@ -126,7 +127,11 @@ theorem cmod_eq_zero_iff_emod_eq_zero (a b : Int) : cmod a b = 0 ↔ a%b = 0 :=
   simp at this
   simp [Int.neg_emod, ← this, Eq.comm]
 
-theorem cdiv_eq_div_of_divides {a b : Int} (h : (a/b)*b = a) : a/b = cdiv a b := by
+abbrev div_mul_cancel_of_mod_zero :=
+  @Int.ediv_mul_cancel_of_emod_eq_zero
+
+theorem cdiv_eq_div_of_divides {a b : Int} (h : a % b = 0) : a/b = cdiv a b := by
+  replace h := div_mul_cancel_of_mod_zero h
   have hz : a % b = 0 := by
     have := Int.ediv_add_emod a b
     conv at this => rhs; rw [← Int.add_zero a]
@@ -148,12 +153,12 @@ def Poly.div (k : Int) : Poly → Poly
   | .add k' x p => .add (k'/k) x (div k p)
 
 def Poly.divAll (k : Int) : Poly → Bool
-  | .num k' => (k'/k)*k == k'
-  | .add k' _ p => (k'/k)*k == k' && divAll k p
+  | .num k' => k' % k == 0
+  | .add k' _ p => k' % k == 0 && divAll k p
 
 def Poly.divCoeffs (k : Int) : Poly → Bool
   | .num _ => true
-  | .add k' _ p => (k'/k)*k == k' && divCoeffs k p
+  | .add k' _ p => k' % k == 0 && divCoeffs k p
 
 def Poly.getConst : Poly → Int
   | .num k => k
@@ -232,9 +237,10 @@ attribute [local simp] Poly.div Poly.divAll PolyCnstr.denote
 
 theorem Poly.denote_div_eq_of_divAll (ctx : Context) (p : Poly) (k : Int) : p.divAll k → (p.div k).denote ctx * k = p.denote ctx := by
   induction p with
-  | num _ => simp; intro h; rw [← cdiv_eq_div_of_divides h]; assumption
+  | num _ => simp; intro h; rw [← cdiv_eq_div_of_divides h]; exact div_mul_cancel_of_mod_zero h
   | add k' v p ih =>
     simp; intro h₁ h₂
+    replace h₁ := div_mul_cancel_of_mod_zero h₁
     have ih := ih h₂
     simp [ih]
     apply congrArg (denote ctx p + ·)
@@ -247,6 +253,7 @@ theorem Poly.denote_div_eq_of_divCoeffs (ctx : Context) (p : Poly) (k : Int) : p
   | num k' => simp; rw [Int.mul_comm, cdiv_add_cmod]
   | add k' v p ih =>
     simp; intro h₁ h₂
+    replace h₁ := div_mul_cancel_of_mod_zero h₁
     rw [← ih h₂]
     rw [Int.mul_right_comm, h₁, Int.add_assoc]
 
@@ -373,7 +380,6 @@ theorem ExprCnstr.eq_of_toPoly_eq_of_divBy' (ctx : Context) (e e' : ExprCnstr) (
     rw [denote_toPoly, denote_toPoly] at this
     exact this
   next p =>
-    -- TODO: this is correct but we can simplify `p ≤ 0` if `p.divCoeffs k` and `p.getConst % k > 0`. Here, we are simplifying only the case `p.getConst % k = 0`
     replace h₁ := Poly.denote_div_eq_of_divAll ctx p k h₁
     replace h₂ := congrArg (PolyCnstr.denote ctx) h₂
     simp only [PolyCnstr.denote.eq_2, ← h₁] at h₂
@@ -526,6 +532,109 @@ theorem ExprCnstr.eq_true_of_isValid (ctx : Context) (c : ExprCnstr) (h : c.toPo
   rw [ExprCnstr.denote_toPoly] at this
   assumption
 
+private def gcd (a b : Int) : Int :=
+  Int.ofNat <| Int.gcd a b
+
+private theorem gcd_dvd_left (a b : Int) : gcd a b ∣ a := by
+  simp [gcd, Int.gcd_dvd_left]
+
+private theorem gcd_dvd_right (a b : Int) : gcd a b ∣ b := by
+  simp [gcd, Int.gcd_dvd_right]
+
+private theorem gcd_dvd_step {k a b x : Int} (h : k ∣ a*x + b) : gcd a k ∣ b := by
+  have h₁ : gcd a k ∣ a*x + b := Int.dvd_trans (gcd_dvd_right a k) h
+  have h₂ : gcd a k ∣ a*x := Int.dvd_trans (gcd_dvd_left a k) (Int.dvd_mul_right a x)
+  exact Int.dvd_iff_dvd_of_dvd_add h₁ |>.mp h₂
+
+def Poly.gcdCoeffs : Poly → Int → Int
+  | .num _, k => k
+  | .add k' _ p, k => gcdCoeffs p (gcd k' k)
+
+theorem Poly.gcd_dvd_const {ctx : Context} {p : Poly} {k : Int} (h : k ∣ p.denote ctx) : p.gcdCoeffs k ∣ p.getConst := by
+  induction p generalizing k <;> simp_all [gcdCoeffs]
+  next k' x p ih =>
+    rw [Int.add_comm] at h
+    exact ih (gcd_dvd_step h)
+
+def Poly.mul (p : Poly) (k : Int) : Poly :=
+  match p with
+  | .num k' => .num (k*k')
+  | .add k' v p => .add (k*k') v (mul p k)
+
+@[simp] theorem Poly.denote_mul (ctx : Context) (p : Poly) (k : Int) : (p.mul k).denote ctx = k * p.denote ctx := by
+  induction p <;> simp [mul, *]
+  rw [Int.mul_assoc]
+
+structure DvdPolyCnstr where
+  a : Int
+  p : Poly
+
+def DvdPolyCnstr.denote (ctx : Context) (c : DvdPolyCnstr) : Prop :=
+  c.a ∣ c.p.denote ctx
+
+def DvdPolyCnstr.isUnsat (c : DvdPolyCnstr) : Bool :=
+  c.p.getConst % c.p.gcdCoeffs c.a != 0
+
+def DvdPolyCnstr.isEqv (c₁ c₂ : DvdPolyCnstr) (k : Int) : Bool :=
+  k != 0 && c₁.a == k*c₂.a && c₁.p == c₂.p.mul k
+
+private theorem not_dvd_of_not_mod_zero {a b : Int} (h : ¬ b % a = 0) : ¬ a ∣ b := by
+  intro h; have := Int.emod_eq_zero_of_dvd h; contradiction
+
+def DvdPolyCnstr.eq_false_of_isUnsat (ctx : Context) (c : DvdPolyCnstr) : c.isUnsat → c.denote ctx = False := by
+  rcases c with ⟨a, p⟩
+  simp [isUnsat, denote]
+  intro h₁ h₂
+  have := Poly.gcd_dvd_const h₂
+  have := not_dvd_of_not_mod_zero h₁
+  contradiction
+
+@[local simp] private theorem mul_dvd_mul_eq {a b c : Int} (hnz : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c := by
+  constructor
+  · intro h
+    rcases h with ⟨k, h⟩
+    rw [Int.mul_assoc a] at h
+    replace h := Int.eq_of_mul_eq_mul_left hnz h
+    exists k
+  · intro h
+    rcases h with ⟨k, h⟩
+    exists k
+    rw [h, Int.mul_assoc]
+
+@[local simp] theorem DvdPolyCnstr.eq_of_isEqv (ctx : Context) (c₁ c₂ : DvdPolyCnstr) (k : Int) (h : isEqv c₁ c₂ k) : c₁.denote ctx = c₂.denote ctx := by
+  rcases c₁ with ⟨a₁, e₁⟩
+  rcases c₂ with ⟨a₂, e₂⟩
+  simp [isEqv] at h
+  rcases h with ⟨⟨h₁, h₂⟩, h₃⟩
+  replace h₃ := congrArg (Poly.denote ctx) h₃
+  simp at h₃
+  simp [denote, *]
+
+structure DvdCnstr where
+  a : Int
+  e : Expr
+
+def DvdCnstr.denote (ctx : Context) (c : DvdCnstr) : Prop :=
+  c.a ∣ c.e.denote ctx
+
+def DvdCnstr.toPoly (c : DvdCnstr) : DvdPolyCnstr :=
+  { a := c.a, p := c.e.toPoly }
+
+@[simp] theorem DvdCnstr.denote_toPoly_eq (ctx : Context) (c : DvdCnstr) : c.denote ctx = c.toPoly.denote ctx := by
+  simp [toPoly, denote, DvdPolyCnstr.denote]
+
+def DvdCnstr.isEqv (c₁ c₂ : DvdCnstr) (k : Int) : Bool :=
+  c₁.toPoly.isEqv c₂.toPoly k
+
+def DvdCnstr.isUnsat (c : DvdCnstr) : Bool :=
+  c.toPoly.isUnsat
+
+theorem DvdCnstr.eq_of_isEqv (ctx : Context) (c₁ c₂ : DvdCnstr) (k : Int) (h : isEqv c₁ c₂ k) : c₁.denote ctx = c₂.denote ctx := by
+  simp [DvdPolyCnstr.eq_of_isEqv ctx c₁.toPoly c₂.toPoly k h]
+
+theorem DvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : DvdCnstr) (h : c.isUnsat) : c.denote ctx = False := by
+  simp [DvdPolyCnstr.eq_false_of_isUnsat ctx c.toPoly h]
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

src/Lean/Meta/Tactic/LinearArith/Int/Simp.lean

@@ -21,7 +21,7 @@ def Int.Linear.PolyCnstr.gcdAll : PolyCnstr → Nat
   | .eq p => p.gcdAll
   | .le p => p.gcdAll
 
-def Int.Linear.Poly.gcdCoeffs : Poly → Nat
+def Int.Linear.Poly.gcdCoeffs' : Poly → Nat
   | .num _ => 1
   | .add k _ p => go k.natAbs p
 where
@@ -32,7 +32,7 @@ where
       | .add k' _ p => go (Nat.gcd k k'.natAbs) p
 
 def Int.Linear.PolyCnstr.gcdCoeffs : PolyCnstr → Nat
-  | .eq p | .le p => p.gcdCoeffs
+  | .eq p | .le p => p.gcdCoeffs'
 
 def Int.Linear.PolyCnstr.isEq : PolyCnstr → Bool
   | .eq _ => true