Cooper resolution: small solutions to boundedness and divisibility constraints.

def Int.add_of_le {a b : Int} (h : a ≤ b) : { c : Nat // b = a + ↑c }

Equations

• Int.add_of_le h = ⟨(b - a).toNat, ⋯⟩

theorem Int.dvd_of_mul_dvd {a b c : Int} (w : a * b ∣ a * c) (h : 0 < a) : b ∣ c

theorem Int.dvd_mul_emod_add_of_dvd_mul_add {a b c d x : Int} (w : a ∣ b * x + c) (h : a / ↑(a.gcd b) ∣ d) : a ∣ b * (x % d) + c

Given a solution x to a divisibility constraint a ∣ b * x + c, then x % d is another solution as long as (a / gcd a b) | d.

See dvd_emod_add_of_dvd_add for the specialization with b = 1.

theorem Int.dvd_emod_add_of_dvd_add {a c d x : Int} (w : a ∣ x + c) (h : a ∣ d) : a ∣ x % d + c

Given a solution x to a divisibility constraint a ∣ x + c, then x % d is another solution as long as a | d.

See dvd_mul_emod_add_of_dvd_mul_add for a more general version allowing a coefficient with x.

There is an integer solution for x to the system

p ≤ a * x
    b * x ≤ q
d | c * x + s

(here a, b, d are positive integers, c and s are integers, and p and q are integers which it may be helpful to think of as evaluations of linear forms), if and only if there is an integer solution for k to the system

0 ≤ k < lcm a (a * d / gcd (a * d) c)
b * k + b * p ≤ a * q
    a | k + p
a * d | c * k + c * p + a * s

Note in the new system that k has explicit lower and upper bounds (i.e. without a coefficient for k, and in terms of a, c, and d only).

This is a statement of "Cooper resolution" with a divisibility constraint, as formulated in "Cutting to the Chase: Solving Linear Integer Arithmetic" by Dejan Jovanović and Leonardo de Moura, DOI 10.1007/s10817-013-9281-x

See cooper_resolution_left for a simpler version without the divisibility constraint.

This formulation is "biased" towards the lower bound, so it is called "left Cooper resolution". See cooper_resolution_dvd_right for the version biased towards the upper bound.

def Int.Cooper.resolve_left (a c d p x : Int) : Int

Equations

• Int.Cooper.resolve_left a c d p x = (a * x - p) % ↑(a.lcm (a * d / ↑((a * d).gcd c)))

def Int.Cooper.resolve_left' (a c d p x : Int) (h₁ : p ≤ a * x) : Nat

When p ≤ a * x, we can realize resolve_left as a natural number.

Equations

• Int.Cooper.resolve_left' a c d p x h₁ = (Int.add_of_le h₁).val % a.lcm (a * d / ↑((a * d).gcd c))

@[simp]

theorem Int.Cooper.resolve_left_eq (a c d p x : Int) (h₁ : p ≤ a * x) : resolve_left a c d p x = ↑(resolve_left' a c d p x h₁)

theorem Int.Cooper.le_zero_resolve_left (a c d p x : Int) (h₁ : p ≤ a * x) : 0 ≤ resolve_left a c d p x

resolve_left is nonnegative when p ≤ a * x.

theorem Int.Cooper.resolve_left_lt_lcm (a c d p x : Int) (a_pos : 0 < a) (d_pos : 0 < d) (h₁ : p ≤ a * x) : resolve_left a c d p x < ↑(a.lcm (a * d / ↑((a * d).gcd c)))

resolve_left is bounded above by lcm a (a * d / gcd (a * d) c).

theorem Int.Cooper.resolve_left_ineq {b q : Int} (a c d p x : Int) (a_pos : 0 < a) (b_pos : 0 < b) (h₁ : p ≤ a * x) (h₂ : b * x ≤ q) : b * resolve_left a c d p x + b * p ≤ a * q

theorem Int.Cooper.resolve_left_dvd₁ (a c d p x : Int) (h₁ : p ≤ a * x) : a ∣ resolve_left a c d p x + p

theorem Int.Cooper.resolve_left_dvd₂ {s : Int} (a c d p x : Int) (h₁ : p ≤ a * x) (h₃ : d ∣ c * x + s) : a * d ∣ c * resolve_left a c d p x + c * p + a * s

def Int.Cooper.resolve_left_inv (a p k : Int) : Int

Equations

• Int.Cooper.resolve_left_inv a p k = (k + p) / a

theorem Int.Cooper.le_mul_resolve_left_inv (a p k : Int) (h₁ : 0 ≤ k) (h₄ : a ∣ k + p) : p ≤ a * resolve_left_inv a p k

theorem Int.Cooper.mul_resolve_left_inv_le {b q : Int} (a p k : Int) (a_pos : 0 < a) (h₃ : b * k + b * p ≤ a * q) (h₄ : a ∣ k + p) : b * resolve_left_inv a p k ≤ q

theorem Int.Cooper.resolve_left_inv_dvd {s : Int} (a c d p k : Int) (a_pos : 0 < a) (h₄ : a ∣ k + p) (h₅ : a * d ∣ c * k + c * p + a * s) : d ∣ c * resolve_left_inv a p k + s

theorem Int.cooper_resolution_dvd_left {a b c d s p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) (d_pos : 0 < d) : (∃ (x : Int), p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s) ↔ ∃ (k : Int), 0 ≤ k ∧ k < ↑(a.lcm (a * d / ↑((a * d).gcd c))) ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p ∧ a * d ∣ c * k + c * p + a * s

Left Cooper resolution of an upper and lower bound with divisibility constraint.

theorem Int.cooper_resolution_dvd_right {a b c d s p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) (d_pos : 0 < d) : (∃ (x : Int), p ≤ a * x ∧ b * x ≤ q ∧ d ∣ c * x + s) ↔ ∃ (k : Int), 0 ≤ k ∧ k < ↑(b.lcm (b * d / ↑((b * d).gcd c))) ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q ∧ b * d ∣ -c * k + c * q + b * s

Right Cooper resolution of an upper and lower bound with divisibility constraint.

theorem Int.cooper_resolution_left {a b p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) : (∃ (x : Int), p ≤ a * x ∧ b * x ≤ q) ↔ ∃ (k : Int), 0 ≤ k ∧ k < a ∧ b * k + b * p ≤ a * q ∧ a ∣ k + p

Left Cooper resolution of an upper and lower bound.

theorem Int.cooper_resolution_right {a b p q : Int} (a_pos : 0 < a) (b_pos : 0 < b) : (∃ (x : Int), p ≤ a * x ∧ b * x ≤ q) ↔ ∃ (k : Int), 0 ≤ k ∧ k < b ∧ a * k + b * p ≤ a * q ∧ b ∣ k - q

Right Cooper resolution of an upper and lower bound.