section ‹Mixed Integer Solutions›
text ‹We prove that if an integral system of linear inequalities
$Ax \leq b \wedge A'x < b'$ has a (mixed)integer solution, there there is also
a small (mixed)integer solution, where the numbers are bounded by
$(n+1)! \cdot m^n$ where $n$ is the number of variables and $m$ is a bound on
the absolute values of numbers occurring in $A,A',b,b'$.›
theory Mixed_Integer_Solutions
imports Decomposition_Theorem
begin
definition less_vec :: "'a vec ⇒ ('a :: ord) vec ⇒ bool" (infix "<⇩v" 50) where
"v <⇩v w = (dim_vec v = dim_vec w ∧ (∀ i < dim_vec w. v $ i < w $ i))"
lemma less_vecD: assumes "v <⇩v w" and "w ∈ carrier_vec n"
shows "i < n ⟹ v $ i < w $ i"
using assms unfolding less_vec_def by auto
lemma less_vecI: assumes "v ∈ carrier_vec n" "w ∈ carrier_vec n"
"⋀ i. i < n ⟹ v $ i < w $ i"
shows "v <⇩v w"
using assms unfolding less_vec_def by auto
lemma less_vec_lesseq_vec: "v <⇩v (w :: 'a :: preorder vec) ⟹ v ≤ w"
unfolding less_vec_def less_eq_vec_def
by (auto simp: less_le_not_le)
lemma floor_less: "x ∉ ℤ ⟹ of_int ⌊x⌋ < x"
using le_less by fastforce
lemma floor_of_int_eq[simp]: "x ∈ ℤ ⟹ of_int ⌊x⌋ = x"
by (metis Ints_cases of_int_floor_cancel)
locale gram_schmidt_floor = gram_schmidt n f_ty
for n :: nat and f_ty :: "'a :: {floor_ceiling,
trivial_conjugatable_linordered_field} itself"
begin
lemma small_mixed_integer_solution_main: fixes A⇩1 :: "'a mat"
assumes A1: "A⇩1 ∈ carrier_mat nr⇩1 n"
and A2: "A⇩2 ∈ carrier_mat nr⇩2 n"
and b1: "b⇩1 ∈ carrier_vec nr⇩1"
and b2: "b⇩2 ∈ carrier_vec nr⇩2"
and A1Bnd: "A⇩1 ∈ ℤ⇩m ∩ Bounded_mat Bnd"
and b1Bnd: "b⇩1 ∈ ℤ⇩v ∩ Bounded_vec Bnd"
and A2Bnd: "A⇩2 ∈ ℤ⇩m ∩ Bounded_mat Bnd"
and b2Bnd: "b⇩2 ∈ ℤ⇩v ∩ Bounded_vec Bnd"
and x: "x ∈ carrier_vec n"
and xI: "x ∈ indexed_Ints_vec I"
and sol_nonstrict: "A⇩1 *⇩v x ≤ b⇩1"
and sol_strict: "A⇩2 *⇩v x <⇩v b⇩2"
shows "∃ x.
x ∈ carrier_vec n ∧
x ∈ indexed_Ints_vec I ∧
A⇩1 *⇩v x ≤ b⇩1 ∧
A⇩2 *⇩v x <⇩v b⇩2 ∧
x ∈ Bounded_vec (fact (n+1) * (max 1 Bnd)^n)"
proof -
define B where "B = det_bound n (max 1 Bnd)"
define A where "A = A⇩1 @⇩r A⇩2"
define b where "b = b⇩1 @⇩v b⇩2"
define nr where "nr = nr⇩1 + nr⇩2"
have B0: "B ≥ 0" unfolding B_def det_bound_def by auto
note defs = A_def b_def nr_def
from A1 A2 have A: "A ∈ carrier_mat nr n" unfolding defs by auto
from b1 b2 have b: "b ∈ carrier_vec nr" unfolding defs by auto
from A1Bnd A2Bnd A1 A2 have ABnd: "A ∈ ℤ⇩m ∩ Bounded_mat Bnd" unfolding defs
by (auto simp: Ints_mat_elements_mat Bounded_mat_elements_mat elements_mat_append_rows)
from b1Bnd b2Bnd b1 b2 have bBnd: "b ∈ ℤ⇩v ∩ Bounded_vec Bnd" unfolding defs
by (auto simp: Ints_vec_vec_set Bounded_vec_vec_set)
from decomposition_theorem_polyhedra_1[OF A b refl, of Bnd] ABnd bBnd
obtain Y Z where Z: "Z ⊆ carrier_vec n"
and finX: "finite Z"
and Y: "Y ⊆ carrier_vec n"
and finY: "finite Y"
and poly: "polyhedron A b = convex_hull Y + cone Z"
and ZBnd: "Z ⊆ ℤ⇩v ∩ Bounded_vec B"
and YBnd: "Y ⊆ Bounded_vec B" unfolding B_def by blast
let ?P = "{x ∈ carrier_vec n. A⇩1 *⇩v x ≤ b⇩1 ∧ A⇩2 *⇩v x ≤ b⇩2}"
let ?L = "?P ∩ {x. A⇩2 *⇩v x <⇩v b⇩2} ∩ indexed_Ints_vec I"
have "polyhedron A b = {x ∈ carrier_vec n. A *⇩v x ≤ b}" unfolding polyhedron_def by auto
also have "… = ?P" unfolding defs
by (intro Collect_cong conj_cong refl append_rows_le[OF A1 A2 b1])
finally have poly: "?P = convex_hull Y + cone Z" unfolding poly ..
have "x ∈ ?P" using x sol_nonstrict less_vec_lesseq_vec[OF sol_strict] by blast
note sol = this[unfolded poly]
from set_plus_elim[OF sol] obtain y z where xyz: "x = y + z" and
yY: "y ∈ convex_hull Y" and zZ: "z ∈ cone Z" by auto
from convex_hull_carrier[OF Y] yY have y: "y ∈ carrier_vec n" by auto
from Caratheodory_theorem[OF Z] zZ
obtain C where zC: "z ∈ finite_cone C" and CZ: "C ⊆ Z" and lin: "lin_indpt C" by auto
from subset_trans[OF CZ Z] lin have card: "card C ≤ n"
using dim_is_n li_le_dim(2) by auto
from finite_subset[OF CZ finX] have finC: "finite C" .
from zC[unfolded finite_cone_def nonneg_lincomb_def] finC obtain a
where za: "z = lincomb a C" and nonneg: "⋀ u. u ∈ C ⟹ a u ≥ 0" by auto
from CZ Z have C: "C ⊆ carrier_vec n" by auto
have z: "z ∈ carrier_vec n" using C unfolding za by auto
have yB: "y ∈ Bounded_vec B" using yY convex_hull_bound[OF YBnd Y] by auto
{
fix D
assume DC: "D ⊆ C"
from finite_subset[OF this finC] have "finite D" .
hence "∃ a. y + lincomb a C ∈ ?L ∧ (∀ c ∈ C. a c ≥ 0) ∧ (∀ c ∈ D. a c ≤ 1)"
using DC
proof (induct D)
case empty
show ?case by (intro exI[of _ a], fold za xyz, insert sol_strict x xI nonneg ‹x ∈ ?P›, auto)
next
case (insert c D)
then obtain a where sol: "y + lincomb a C ∈ ?L"
and a: "(∀ c ∈ C. a c ≥ 0)" and D: "(∀ c ∈ D. a c ≤ 1)" by auto
from insert(4) C have c: "c ∈ carrier_vec n" and cC: "c ∈ C" by auto
show ?case
proof (cases "a c > 1")
case False
thus ?thesis by (intro exI[of _ a], insert sol a D, auto)
next
case True
let ?z = "λ d. lincomb a C - d ⋅⇩v c"
let ?x = "λ d. y + ?z d"
{
fix d
have lin: "lincomb a (C - {c}) ∈ carrier_vec n" using C by auto
have id: "?z d = lincomb (λ e. if e = c then (a c - d) else a e) C"
unfolding lincomb_del2[OF finC C TrueI cC]
by (subst (2) lincomb_cong[OF refl, of _ _ a], insert C c lin, auto simp: diff_smult_distrib_vec)
{
assume le: "d ≤ a c"
have "?z d ∈ finite_cone C"
proof -
have "∀f∈C. 0 ≤ (λe. if e = c then a c - d else a e) f" using le a finC by simp
then show ?thesis unfolding id using le a finC
by (simp add: C lincomb_in_finite_cone)
qed
hence "?z d ∈ cone Z" using CZ
using finC local.cone_def by blast
hence "?x d ∈ ?P" unfolding poly
by (intro set_plus_intro[OF yY], auto)
} note sol = this
{
fix w :: "'a vec"
assume w: "w ∈ carrier_vec n"
have "w ∙ (?x d) = w ∙ y + w ∙ lincomb a C - d * (w ∙ c)"
by (subst scalar_prod_add_distrib[OF w y], (insert C c, force),
subst scalar_prod_minus_distrib[OF w], insert w c C, auto)
} note scalar = this
note id sol scalar
} note generic = this
let ?fl = "(of_int (floor (a c)) :: 'a)"
define p where "p = (if ?fl = a c then a c - 1 else ?fl)"
have p_lt_ac: "p < a c" unfolding p_def
using floor_less floor_of_int_eq by auto
have p1_ge_ac: "p + 1 ≥ a c" unfolding p_def
using floor_correct le_less by auto
have p1: "p ≥ 1" using True unfolding p_def by auto
define a' where "a' = (λe. if e = c then a c - p else a e)"
have lin_id: "lincomb a' C = lincomb a C - p ⋅⇩v c" unfolding a'_def using id
by (simp add: generic(1))
hence 1: "y + lincomb a' C ∈ {x ∈ carrier_vec n. A⇩1 *⇩v x ≤ b⇩1 ∧ A⇩2 *⇩v x ≤ b⇩2}"
using p_lt_ac generic(2)[of p] by auto
have pInt: "p ∈ ℤ" unfolding p_def using sol by auto
have "C ⊆ indexed_Ints_vec I" using CZ ZBnd
using indexed_Ints_vec_subset by force
hence "c ∈ indexed_Ints_vec I" using cC by auto
hence pvindInts: "p ⋅⇩v c ∈ indexed_Ints_vec I" unfolding indexed_Ints_vec_def using pInt by simp
have prod: "A⇩2 *⇩v (?x b) ∈ carrier_vec nr⇩2" for b using A2 C c y by auto
have 2: "y + lincomb a' C ∈ {x. A⇩2 *⇩v x <⇩v b⇩2}" unfolding lin_id
proof (intro less_vecI[OF prod b2] CollectI)
fix i
assume i: "i < nr⇩2"
from sol have "A⇩2 *⇩v (?x 0) <⇩v b⇩2" using y C c by auto
from less_vecD[OF this b2 i]
have lt: "row A⇩2 i ∙ ?x 0 < b⇩2 $ i" using A2 i by auto
from generic(2)[of "a c"] i A2
have le: "row A⇩2 i ∙ ?x (a c) ≤ b⇩2 $ i"
unfolding less_eq_vec_def by auto
from A2 i have A2icarr: "row A⇩2 i ∈ carrier_vec n" by auto
have "row A⇩2 i ∙ ?x p < b⇩2 $ i"
proof -
define lhs where "lhs = row A⇩2 i ∙ y + row A⇩2 i ∙ lincomb a C - b⇩2 $ i"
define mult where "mult = row A⇩2 i ∙ c"
have le2: "lhs ≤ a c * mult" using le unfolding generic(3)[OF A2icarr] lhs_def mult_def by auto
have lt2: "lhs < 0 * mult" using lt unfolding generic(3)[OF A2icarr] lhs_def by auto
from le2 lt2 have "lhs < p * mult" using p_lt_ac p1 True
by (smt dual_order.strict_trans linorder_neqE_linordered_idom
mult_less_cancel_right not_less zero_less_one_class.zero_less_one)
then show ?thesis unfolding generic(3)[OF A2icarr] lhs_def mult_def by auto
qed
thus "(A⇩2 *⇩v ?x p) $ i < b⇩2 $ i" using i A2 by auto
qed
have "y + lincomb a' C = y + lincomb a C - p ⋅⇩v c"
by (subst lin_id, insert y C c, auto simp: add_diff_eq_vec)
also have "… ∈ indexed_Ints_vec I" using sol
by(intro diff_indexed_Ints_vec[OF _ _ _ pvindInts, of _ n ], insert c C, auto)
finally have 3: "y + lincomb a' C ∈ indexed_Ints_vec I" by auto
have 4: "∀c∈C. 0 ≤ a' c" unfolding a'_def p_def using p_lt_ac a by auto
have 5: "∀c∈insert c D. a' c ≤ 1" unfolding a'_def using p1_ge_ac D p_def by auto
show ?thesis
by (intro exI[of _ a'], intro conjI IntI 1 2 3 4 5)
qed
qed
}
from this[of C] obtain a where
sol: "y + lincomb a C ∈ ?L" and bnds: "(∀ c ∈ C. a c ≥ 0)" "(∀ c ∈ C. a c ≤ 1)" by auto
show ?thesis
proof (intro exI[of _ "y + lincomb a C"] conjI)
from ZBnd CZ have BndC: "C ⊆ Bounded_vec B" and IntC: "C ⊆ ℤ⇩v" by auto
have "lincomb a C ∈ Bounded_vec (of_nat n * B)"
using lincomb_card_bound[OF BndC C B0 _ card] bnds by auto
from sum_in_Bounded_vecI[OF yB this y] C
have "y + lincomb a C ∈ Bounded_vec (B + of_nat n * B)" by auto
also have "B + of_nat n * B = of_nat (n+1) * B" by (auto simp: field_simps)
also have "… = fact (n + 1) * (max 1 Bnd)^n" unfolding B_def det_bound_def by simp
finally show "y + lincomb a C ∈ Bounded_vec (fact (n + 1) * max 1 Bnd ^ n)" by auto
qed (insert sol, auto)
qed
text ‹We get rid of the max-1 operation, by showing that a smaller value of Bnd
can only occur in very special cases where the theorem is trivially satisfied.›
lemma small_mixed_integer_solution: fixes A⇩1 :: "'a mat"
assumes A1: "A⇩1 ∈ carrier_mat nr⇩1 n"
and A2: "A⇩2 ∈ carrier_mat nr⇩2 n"
and b1: "b⇩1 ∈ carrier_vec nr⇩1"
and b2: "b⇩2 ∈ carrier_vec nr⇩2"
and A1Bnd: "A⇩1 ∈ ℤ⇩m ∩ Bounded_mat Bnd"
and b1Bnd: "b⇩1 ∈ ℤ⇩v ∩ Bounded_vec Bnd"
and A2Bnd: "A⇩2 ∈ ℤ⇩m ∩ Bounded_mat Bnd"
and b2Bnd: "b⇩2 ∈ ℤ⇩v ∩ Bounded_vec Bnd"
and x: "x ∈ carrier_vec n"
and xI: "x ∈ indexed_Ints_vec I"
and sol_nonstrict: "A⇩1 *⇩v x ≤ b⇩1"
and sol_strict: "A⇩2 *⇩v x <⇩v b⇩2"
and non_degenerate: "nr⇩1 ≠ 0 ∨ nr⇩2 ≠ 0 ∨ Bnd ≥ 0"
shows "∃ x.
x ∈ carrier_vec n ∧
x ∈ indexed_Ints_vec I ∧
A⇩1 *⇩v x ≤ b⇩1 ∧
A⇩2 *⇩v x <⇩v b⇩2 ∧
x ∈ Bounded_vec (fact (n+1) * Bnd^n)"
proof (cases "Bnd ≥ 1")
case True
hence "max 1 Bnd = Bnd" by auto
with small_mixed_integer_solution_main[OF assms(1-12)] True show ?thesis by auto
next
case trivial: False
show ?thesis
proof (cases "n = 0")
case True
with x have "x ∈ Bounded_vec (fact (n+1) * Bnd^n)" unfolding Bounded_vec_def by auto
with xI x sol_nonstrict sol_strict show ?thesis by blast
next
case n: False
{
fix A nr
assume A: "A ∈ carrier_mat nr n" and Bnd: "A ∈ ℤ⇩m ∩ Bounded_mat Bnd"
{
fix i j
assume "i < nr" "j < n"
with Bnd A have *: "A $$ (i,j) ∈ ℤ" "abs (A $$ (i,j)) ≤ Bnd"
unfolding Bounded_mat_def Ints_mat_def by auto
with trivial have "Bnd ≥ 0" "A $$ (i,j) = 0" by (auto simp: Ints_nonzero_abs_less1)
} note main = this
have A0: "A = 0⇩m nr n"
by (intro eq_matI, insert main A, auto)
have "nr ≠ 0 ⟹ Bnd ≥ 0" using main[of 0 0] n by auto
note A0 this
} note main = this
from main[OF A1 A1Bnd] have A1: "A⇩1 = 0⇩m nr⇩1 n" and nr1: "nr⇩1 ≠ 0 ⟹ Bnd ≥ 0"
by auto
from main[OF A2 A2Bnd] have A2: "A⇩2 = 0⇩m nr⇩2 n" and nr2: "nr⇩2 ≠ 0 ⟹ Bnd ≥ 0"
by auto
let ?x = "0⇩v n"
show ?thesis
proof (intro exI[of _ ?x] conjI)
show "A⇩1 *⇩v ?x ≤ b⇩1" using sol_nonstrict x unfolding A1 by auto
show "A⇩2 *⇩v ?x <⇩v b⇩2" using sol_strict x unfolding A2 by auto
show "?x ∈ carrier_vec n" by auto
show "?x ∈ indexed_Ints_vec I" unfolding indexed_Ints_vec_def by auto
from nr1 nr2 non_degenerate have Bnd: "Bnd ≥ 0" by auto
hence "fact (n + 1) * Bnd ^ n ≥ 0" by simp
thus "?x ∈ Bounded_vec (fact (n + 1) * Bnd ^ n)" by (auto simp: Bounded_vec_def)
qed
qed
qed
corollary small_integer_solution_nonstrict: fixes A :: "'a mat"
assumes A: "A ∈ carrier_mat nr n"
and b: "b ∈ carrier_vec nr"
and ABnd: "A ∈ ℤ⇩m ∩ Bounded_mat Bnd"
and bBnd: "b ∈ ℤ⇩v ∩ Bounded_vec Bnd"
and x: "x ∈ carrier_vec n"
and xI: "x ∈ ℤ⇩v"
and sol: "A *⇩v x ≤ b"
and non_degenerate: "nr ≠ 0 ∨ Bnd ≥ 0"
shows "∃ y.
y ∈ carrier_vec n ∧
y ∈ ℤ⇩v ∧
A *⇩v y ≤ b ∧
y ∈ Bounded_vec (fact (n+1) * Bnd^n)"
proof -
let ?A2 = "0⇩m 0 n :: 'a mat"
let ?b2 = "0⇩v 0 :: 'a vec"
from non_degenerate have degen: "nr ≠ 0 ∨ (0 :: nat) ≠ 0 ∨ Bnd ≥ 0" by auto
have "∃y. y ∈ carrier_vec n ∧ y ∈ ℤ⇩v ∧ A *⇩v y ≤ b ∧ ?A2 *⇩v y <⇩v ?b2
∧ y ∈ Bounded_vec (fact (n + 1) * Bnd ^ n)"
by (rule small_mixed_integer_solution[OF A _ b _ ABnd bBnd _ _ x _ sol, of ?A2 0 ?b2 UNIV,
folded indexed_Ints_vec_UNIV], insert xI degen,
auto simp: Ints_vec_def Ints_mat_def Bounded_mat_def Bounded_vec_def less_vec_def)
thus ?thesis by blast
qed
end
end