feat: helper theorems for cooper_dvd_right (#7292)

This PR adds support theorems for the **Cooper-Dvd-Right** conflict
resolution rule used in the cutsat procedure. During model construction,
when attempting to extend the model to a variable `x`, cutsat may find a
conflict that involves two inequalities (the lower and upper bounds for
`x`) and a divisibility constraint.

src/Init/Data/Int/Linear.lean

@@ -1116,6 +1116,7 @@ private theorem orOver_of_exists {n p} : (∃ k, k < n ∧ p k) → OrOver n p :
   apply orOver_of_p h₁ h₂
 
 private theorem ofNat_toNat {a : Int} : a ≥ 0 → Int.ofNat a.toNat = a := by cases a <;> simp
+private theorem cast_toNat {a : Int} : a ≥ 0 → a.toNat = a := by cases a <;> simp
 private theorem ofNat_lt {a : Int} {n : Nat} : a ≥ 0 → a < Int.ofNat n → a.toNat < n := by cases a <;> simp
 @[local simp] private theorem lcm_neg_left (a b : Int) : Int.lcm (-a) b = Int.lcm a b := by simp [Int.lcm]
 @[local simp] private theorem lcm_neg_right (a b : Int) : Int.lcm a (-b) = Int.lcm a b := by simp [Int.lcm]
@@ -1200,7 +1201,6 @@ theorem cooper_dvd_left (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : N
  intro; subst n
  simp only [Poly.denote'_add, Poly.leadCoeff]
  intro h₁ h₂ h₃
- have := cooper_dvd_left_core ha hb hd h₁ h₂ h₃
  simp only [denote'_mul_combine_mul_addConst_eq]
  simp only [denote'_addConst_eq]
  exact cooper_dvd_left_core ha hb hd h₁ h₂ h₃
@@ -1307,6 +1307,104 @@ theorem cooper_left_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (a :
   simp [cooper_left_split_dvd_cert, cooper_left_split]
   intros; subst a p'; simp; assumption
 
+private theorem cooper_dvd_right_core
+    {a b c d s p q x : Int} (a_neg : a < 0) (b_pos : 0 < b) (d_pos : 0 < d)
+    (h₁ : a * x + p ≤ 0)
+    (h₂ : b * x + q ≤ 0)
+    (h₃ : d ∣ c * x + s)
+    : OrOver (Int.lcm b (b * d / Int.gcd (b * d) c)) fun k =>
+      b * p + (-a) * q + (-a) * k ≤ 0 ∧
+      b ∣ q + k ∧
+      b * d ∣ (-c) * q + b * s + (-c) * k := by
+  have a_pos' : 0 < -a := by apply Int.neg_pos_of_neg; assumption
+  have h₁'    : p ≤ (-a)*x := by rw [Int.neg_mul, ← Lean.Omega.Int.add_le_zero_iff_le_neg']; assumption
+  have h₂'    : b * x ≤ -q := by rw [← Lean.Omega.Int.add_le_zero_iff_le_neg', Int.add_comm]; assumption
+  have ⟨k, h₁, h₂, h₃, h₄, h₅⟩ := Int.cooper_resolution_dvd_right a_pos' b_pos d_pos |>.mp ⟨x, h₁', h₂', h₃⟩
+  simp only [Int.neg_mul, neg_gcd, lcm_neg_left, Int.mul_neg, Int.neg_neg, Int.neg_dvd] at *
+  apply orOver_of_exists
+  have hlt := ofNat_lt h₁ h₂
+  replace h₃ := Int.add_le_add_right h₃ (-(a*q)); rw [Int.add_right_neg] at h₃
+  have : -(a * k) + b * p + -(a * q) = b * p + -(a * q) + -(a * k) := by ac_rfl
+  rw [this] at h₃; clear this
+  rw [Int.sub_neg, Int.add_comm] at h₄
+  have : -(c * k) + -(c * q) + b * s = -(c * q) + b * s + -(c * k) := by ac_rfl
+  rw [this] at h₅; clear this
+  exists k.toNat
+  simp only [hlt, true_and, and_true, cast_toNat h₁, h₃, h₄, h₅]
+
+def cooper_dvd_right_cert (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat) : Bool :=
+  p₁.casesOn (fun _ => false) fun a x _ =>
+  p₂.casesOn (fun _ => false) fun b y _ =>
+  p₃.casesOn (fun _ => false) fun c z _ =>
+   .and (x == y) <| .and (x == z) <|
+   .and (a < 0)  <| .and (b > 0)  <|
+   .and (d > 0)  <| n == Int.lcm b (b * d / Int.gcd (b * d) c)
+
+def cooper_dvd_right_split (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) : Prop :=
+  let p  := p₁.tail
+  let q  := p₂.tail
+  let s  := p₃.tail
+  let a  := p₁.leadCoeff
+  let b  := p₂.leadCoeff
+  let c  := p₃.leadCoeff
+  let p₁ := p.mul b |>.combine (q.mul (-a))
+  let p₂ := q.mul (-c) |>.combine (s.mul b)
+  (p₁.addConst ((-a)*k)).denote' ctx ≤ 0
+  ∧ b ∣ (q.addConst k).denote' ctx
+  ∧ b*d ∣ (p₂.addConst ((-c)*k)).denote' ctx
+
+theorem cooper_dvd_right (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (n : Nat)
+    : cooper_dvd_right_cert p₁ p₂ p₃ d n
+      → p₁.denote' ctx ≤ 0
+      → p₂.denote' ctx ≤ 0
+      → d ∣ p₃.denote' ctx
+      → OrOver n (cooper_dvd_right_split ctx p₁ p₂ p₃ d) := by
+ unfold cooper_dvd_right_split
+ cases p₁ <;> cases p₂ <;> cases p₃ <;> simp [cooper_dvd_right_cert, Poly.tail, -Poly.denote'_eq_denote]
+ next a x p b y q c z s =>
+ intro _ _; subst y z
+ intro ha hb hd
+ intro; subst n
+ simp only [Poly.denote'_add, Poly.leadCoeff]
+ intro h₁ h₂ h₃
+ have := cooper_dvd_right_core ha hb hd h₁ h₂ h₃
+ simp only [denote'_mul_combine_mul_addConst_eq]
+ simp only [denote'_addConst_eq, ←Int.neg_mul]
+ exact cooper_dvd_right_core ha hb hd h₁ h₂ h₃
+
+def cooper_dvd_right_split_ineq_cert (p₁ p₂ : Poly) (k : Int) (a : Int) (p' : Poly) : Bool :=
+  let p  := p₁.tail
+  let q  := p₂.tail
+  let b  := p₂.leadCoeff
+  let p₂ := p.mul b |>.combine (q.mul (-a))
+  p₁.leadCoeff == a && p' == p₂.addConst ((-a)*k)
+
+theorem cooper_dvd_right_split_ineq (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (a : Int) (p' : Poly)
+    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_ineq_cert p₁ p₂ k a p' → p'.denote ctx ≤ 0 := by
+  simp [cooper_dvd_right_split_ineq_cert, cooper_dvd_right_split]
+  intros; subst a p'; simp [denote'_mul_combine_mul_addConst_eq]; assumption
+
+def cooper_dvd_right_split_dvd1_cert (p₂ p' : Poly) (b : Int) (k : Int) : Bool :=
+  b == p₂.leadCoeff && p' == p₂.tail.addConst k
+
+theorem cooper_dvd_right_split_dvd1 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (b : Int) (p' : Poly)
+    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd1_cert p₂ p' b k → b ∣ p'.denote ctx := by
+  simp [cooper_dvd_right_split_dvd1_cert, cooper_dvd_right_split]
+  intros; subst b p'; simp; assumption
+
+def cooper_dvd_right_split_dvd2_cert (p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly): Bool :=
+  let q  := p₂.tail
+  let s  := p₃.tail
+  let b  := p₂.leadCoeff
+  let c  := p₃.leadCoeff
+  let p₂ := q.mul (-c) |>.combine (s.mul b)
+  d' == b*d && p' == p₂.addConst ((-c)*k)
+
+theorem cooper_dvd_right_split_dvd2 (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (k : Nat) (d' : Int) (p' : Poly)
+    : cooper_dvd_right_split ctx p₁ p₂ p₃ d k → cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' → d' ∣ p'.denote ctx := by
+  simp [cooper_dvd_right_split_dvd2_cert, cooper_dvd_right_split]
+  intros; subst d' p'; simp; assumption
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by