From 2c2a3a65b256adbf3f47f470ba7ac625c2aea147 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 13 Feb 2025 20:55:58 -0800
Subject: [PATCH] feat: support theorems for cutsat `Div-Solve` rule (#7077)

This PR proves the helper theorems for justifying the "Div-Solve" rule
in the cutsat procedure.
---
 src/Init/Data/Int.lean        |  1 +
 src/Init/Data/Int/Cutsat.lean | 68 +++++++++++++++++++++++++++++++++++
 2 files changed, 69 insertions(+)
 create mode 100644 src/Init/Data/Int/Cutsat.lean

diff --git a/src/Init/Data/Int.lean b/src/Init/Data/Int.lean
index 48c60e78ce..2afc7e14aa 100644
--- a/src/Init/Data/Int.lean
+++ b/src/Init/Data/Int.lean
@@ -15,3 +15,4 @@ import Init.Data.Int.Order
 import Init.Data.Int.Pow
 import Init.Data.Int.Cooper
 import Init.Data.Int.Linear
+import Init.Data.Int.Cutsat
diff --git a/src/Init/Data/Int/Cutsat.lean b/src/Init/Data/Int/Cutsat.lean
new file mode 100644
index 0000000000..494f316afa
--- /dev/null
+++ b/src/Init/Data/Int/Cutsat.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.AC
+import Init.Data.Int.Gcd
+
+namespace Int.Linear
+
+/-!
+Helper theorems for solving divisibility constraints.
+The two theorems are used to justify the `Div-Solve` rule
+in the section "Strong Conflict Resolution" in the paper
+"Cutting to the Chase: Solving Linear Integer Arithmetic".
+-/
+
+theorem dvd_solve_1 {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂ : Int} {α β d : Int}
+   (h : α*a₁*d₂ + β*a₂*d₁ = d)
+   (h₁ : d₁ ∣ a₁*x + p₁)
+   (h₂ : d₂ ∣ a₂*x + p₂)
+   : d₁*d₂ ∣ d*x + α*d₂*p₁ + β*d₁*p₂ := by
+ rcases h₁ with ⟨k₁, h₁⟩
+ replace h₁ : α*a₁*d₂*x + α*d₂*p₁ = d₁*d₂*(α*k₁) := by
+   have ac₁ : d₁*d₂*(α*k₁) = α*d₂*(d₁*k₁) := by ac_rfl
+   have ac₂ : α * a₁ * d₂ * x = α * d₂ * (a₁ * x) := by ac_rfl
+   rw [ac₁, ← h₁, Int.mul_add, ac₂]
+ rcases h₂ with ⟨k₂, h₂⟩
+ replace h₂ : β*a₂*d₁*x + β*d₁*p₂ = d₁*d₂*(β*k₂) := by
+   have ac₁ : d₁*d₂*(β*k₂) = β*d₁*(d₂*k₂) := by ac_rfl
+   have ac₂ : β * a₂ * d₁ * x = β * d₁ * (a₂ * x) := by ac_rfl
+   rw [ac₁, ←h₂, Int.mul_add, ac₂]
+ replace h₁ : d₁*d₂ ∣ α*a₁*d₂*x + α*d₂*p₁ := ⟨α*k₁, h₁⟩
+ replace h₂ : d₁*d₂ ∣ β*a₂*d₁*x + β*d₁*p₂ := ⟨β*k₂, h₂⟩
+ have h' := Int.dvd_add h₁ h₂; clear h₁ h₂ k₁ k₂
+ replace h : d*x = α*a₁*d₂*x + β*a₂*d₁*x := by
+   rw [←h, Int.add_mul]
+ have ac :
+   α * a₁ * d₂ * x + α * d₂ * p₁ + (β * a₂ * d₁ * x + β * d₁ * p₂)
+   =
+   α * a₁ * d₂ * x + β * a₂ * d₁ * x + α * d₂ * p₁ + β * d₁ * p₂ := by ac_rfl
+ rw [h, ←ac]
+ assumption
+
+theorem dvd_solve_2 {x : Int} {d₁ a₁ p₁ : Int} {d₂ a₂ p₂ : Int} {d : Int}
+   (h : d = Int.gcd (a₁*d₂) (a₂*d₁))
+   (h₁ : d₁ ∣ a₁*x + p₁)
+   (h₂ : d₂ ∣ a₂*x + p₂)
+   : d ∣ a₂*p₁ - a₁*p₂ := by
+ rcases h₁ with ⟨k₁, h₁⟩
+ rcases h₂ with ⟨k₂, h₂⟩
+ have h₃ : d ∣ a₁*d₂ := by
+  rw [h]; apply Int.gcd_dvd_left
+ have h₄ : d ∣ a₂*d₁ := by
+  rw [h]; apply Int.gcd_dvd_right
+ rcases h₃ with ⟨k₃, h₃⟩
+ rcases h₄ with ⟨k₄, h₄⟩
+ have : a₂*p₁ - a₁*p₂ = a₂*d₁*k₁ - a₁*d₂*k₂ := by
+   have ac₁ : a₂*d₁*k₁ = a₂*(d₁*k₁) := by ac_rfl
+   have ac₂ : a₁*d₂*k₂ = a₁*(d₂*k₂) := by ac_rfl
+   have ac₃ : a₁*(a₂*x) = a₂*(a₁*x) := by ac_rfl
+   rw [ac₁, ac₂, ←h₁, ←h₂, Int.mul_add, Int.mul_add, ac₃, ←Int.sub_sub, Int.add_comm, Int.add_sub_assoc]
+   simp
+ rw [h₃, h₄, Int.mul_assoc, Int.mul_assoc, ←Int.mul_sub] at this
+ exact ⟨k₄ * k₁ - k₃ * k₂, this⟩
+
+end Int.Linear