Theory Farkas_Minkowsky_Weyl
section ‹The Theorem of Farkas, Minkowsky and Weyl›
text ‹We prove the theorem of Farkas, Minkowsky and Weyl that a cone is finitely generated
iff it is polyhedral. Moreover, we provide quantative bounds via determinant bounds.›
theory Farkas_Minkowsky_Weyl
imports Fundamental_Theorem_Linear_Inequalities
begin
context gram_schmidt
begin
text ‹We first prove the one direction of the theorem
for the case that the span of the vectors is the full n-dimensional space.›
lemma farkas_minkowsky_weyl_theorem_1_full_dim:
assumes X: "X ⊆ carrier_vec n"
and fin: "finite X"
and span: "span X = carrier_vec n"
shows "∃ nr A. A ∈ carrier_mat nr n ∧ cone X = polyhedral_cone A
∧ (is_det_bound db ⟶ X ⊆ ℤ⇩v ∩ Bounded_vec (of_int Bnd) ⟶ A ∈ ℤ⇩m ∩ Bounded_mat (of_int (db (n-1) Bnd)))"
proof -
define cond where "cond = (λ W. Suc (card W) = n ∧ lin_indpt W ∧ W ⊆ X)"
let ?oi = "of_int :: int ⇒ 'a"
{
fix W
assume "cond W"
hence *: "finite W" "Suc (card W) = n" "lin_indpt W" "W ⊆ carrier_vec n" and WX: "W ⊆ X" unfolding cond_def
using finite_subset[OF _ fin] X by auto
note nv = normal_vector[OF *]
hence "normal_vector W ∈ carrier_vec n" "⋀ w. w ∈ W ⟹ normal_vector W ∙ w = 0"
"normal_vector W ≠ 0⇩v n" "is_det_bound db ⟹ X ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd) ⟹ normal_vector W ∈ ℤ⇩v ∩ Bounded_vec (?oi (db (n - 1) Bnd))"
using WX by blast+
} note condD = this
define Ns where "Ns = { normal_vector W | W. cond W ∧ (∀ w ∈ X. normal_vector W ∙ w ≥ 0) }
∪ { - normal_vector W | W. cond W ∧ (∀ w ∈ X. (- normal_vector W) ∙ w ≥ 0)}"
have "Ns ⊆ normal_vector ` {W . W ⊆ X} ∪ (λ W. - normal_vector W) ` {W. W ⊆ X}" unfolding Ns_def cond_def by blast
moreover have "finite …" using ‹finite X› by auto
ultimately have "finite Ns" by (metis finite_subset)
from finite_list[OF this] obtain ns where ns: "set ns = Ns" by auto
have Ns: "Ns ⊆ carrier_vec n" unfolding Ns_def using condD by auto
define A where "A = mat_of_rows n ns"
define nr where "nr = length ns"
have A: "- A ∈ carrier_mat nr n" unfolding A_def nr_def by auto
show ?thesis
proof (intro exI conjI impI, rule A)
have not_conj: "¬ (a ∧ b) ⟷ (a ⟶ ¬ b)" for a b by auto
have id: "Ns = { nv . ∃ W. W ⊆ X ∧ nv ∈ {normal_vector W, - normal_vector W} ∧
Suc (card W) = n ∧ lin_indpt W ∧ (∀a⇩i∈X. 0 ≤ nv ∙ a⇩i)}"
unfolding Ns_def cond_def by auto
have "polyhedral_cone (- A) = { b. b ∈ carrier_vec n ∧ (- A) *⇩v b ≤ 0⇩v nr}" unfolding polyhedral_cone_def
using A by auto
also have "… = {b. b ∈ carrier_vec n ∧ (∀ i < nr. row (- A) i ∙ b ≤ 0)}"
unfolding less_eq_vec_def using A by auto
also have "… = {b. b ∈ carrier_vec n ∧ (∀ i < nr. - (ns ! i) ∙ b ≤ 0)}" using A Ns[folded ns]
by (intro Collect_cong conj_cong refl all_cong arg_cong[of _ _ "λ x. x ∙ _ ≤ _"],
force simp: A_def mat_of_rows_def nr_def set_conv_nth)
also have "… = {b. b ∈ carrier_vec n ∧ (∀ n ∈ Ns. - n ∙ b ≤ 0)}"
unfolding ns[symmetric] nr_def by (auto simp: set_conv_nth)
also have "… = {b. b ∈ carrier_vec n ∧ (∀ n ∈ Ns. n ∙ b ≥ 0)}"
by (intro Collect_cong conj_cong refl ball_cong, insert Ns, auto)
also have "… = cone X"
unfolding fundamental_theorem_of_linear_inequalities_full_dim(2)[OF X fin span]
by (intro Collect_cong conj_cong refl, unfold not_le[symmetric] not_ex not_conj not_not id, blast)
finally show "cone X = polyhedral_cone (- A)" ..
{
assume XI: "X ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd)" and db: "is_det_bound db"
{
fix v
assume "v ∈ set (rows (- A))"
hence "-v ∈ set (rows A)" unfolding rows_def by auto
hence "-v ∈ Ns" unfolding A_def using ns Ns by auto
from this[unfolded Ns_def] obtain W where cW: "cond W"
and v: "-v = normal_vector W ∨ v = normal_vector W" by auto
from cW[unfolded cond_def] have WX: "W ⊆ X" by auto
from v have v: "v = normal_vector W ∨ v = - normal_vector W"
by (metis uminus_uminus_vec)
from condD(4)[OF cW db XI]
have "normal_vector W ∈ ℤ⇩v ∩ Bounded_vec (?oi (db (n - 1) Bnd))" by auto
hence "v ∈ ℤ⇩v ∩ Bounded_vec (?oi (db (n - 1) Bnd))" using v by auto
}
hence "set (rows (- A)) ⊆ ℤ⇩v ∩ Bounded_vec (?oi (db (n - 1) Bnd))" by blast
thus "- A ∈ ℤ⇩m ∩ Bounded_mat (?oi (db (n - 1) Bnd))" by simp
}
qed
qed
text ‹We next generalize the theorem to the case where X does not span the full space.
To this end, we extend X by unit-vectors until the full space is spanned, and then
add the normal-vectors of these unit-vectors which are orthogonal to span X as additional
constraints to the resulting matrix.›
lemma farkas_minkowsky_weyl_theorem_1:
assumes X: "X ⊆ carrier_vec n"
and finX: "finite X"
shows "∃ nr A. A ∈ carrier_mat nr n ∧ cone X = polyhedral_cone A ∧
(is_det_bound db ⟶ X ⊆ ℤ⇩v ∩ Bounded_vec (of_int Bnd) ⟶ A ∈ ℤ⇩m ∩ Bounded_mat (of_int (db (n-1) (max 1 Bnd))))"
proof -
let ?oi = "of_int :: int ⇒ 'a"
from exists_lin_indpt_sublist[OF X]
obtain Ls where lin_Ls: "lin_indpt_list Ls" and
spanL: "span (set Ls) = span X" and LX: "set Ls ⊆ X" by auto
define Ns where "Ns = normal_vectors Ls"
define Bs where "Bs = basis_extension Ls"
from basis_extension[OF lin_Ls, folded Bs_def]
have BU: "set Bs ⊆ set (unit_vecs n)"
and lin_Ls_Bs: "lin_indpt_list (Ls @ Bs)"
and len_Ls_Bs: "length (Ls @ Bs) = n"
by auto
note nv = normal_vectors[OF lin_Ls, folded Ns_def]
from nv(1-6) nv(7)[of db Bnd]
have N: "set Ns ⊆ carrier_vec n"
and LN': "lin_indpt_list (Ls @ Ns)" "length (Ls @ Ns) = n"
and ortho: "⋀ l w. l ∈ set Ls ⟹ w ∈ set Ns ⟹ w ∙ l = 0"
and Ns_bnd: "is_det_bound db ⟹ set Ls ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd)
⟹ set Ns ⊆ ℤ⇩v ∩ Bounded_vec (?oi (db (n-1) (max 1 Bnd)))"
by auto
from lin_indpt_list_length_eq_n[OF LN']
have spanLN: "span (set Ls ∪ set Ns) = carrier_vec n" by auto
let ?Bnd = "Bounded_vec (?oi (db (n-1) (max 1 Bnd)))"
let ?Bndm = "Bounded_mat (?oi (db (n-1) (max 1 Bnd)))"
define Y where "Y = X ∪ set Bs"
from lin_Ls_Bs[unfolded lin_indpt_list_def] have
Ls: "set Ls ⊆ carrier_vec n" and
Bs: "set Bs ⊆ carrier_vec n" and
distLsBs: "distinct (Ls @ Bs)" and
lin': "lin_indpt (set (Ls @ Bs))" by auto
have LN: "set Ls ∩ set Ns = {}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain x where xX: "x ∈ set Ls" and xW: "x ∈ set Ns" by auto
from ortho[OF xX xW] have "x ∙ x = 0" by auto
hence "sq_norm x = 0" by (auto simp: sq_norm_vec_as_cscalar_prod)
with xX LX X have "x = 0⇩v n" by auto
with vs_zero_lin_dep[OF _ lin'] Ls Bs xX show False by auto
qed
have Y: "Y ⊆ carrier_vec n" using X Bs unfolding Y_def by auto
have CLB: "carrier_vec n = span (set (Ls @ Bs))"
using lin_Ls_Bs len_Ls_Bs lin_indpt_list_length_eq_n by blast
also have "… ⊆ span Y"
by (rule span_is_monotone, insert LX, auto simp: Y_def)
finally have span: "span Y = carrier_vec n" using Y by auto
have finY: "finite Y" using finX unfolding Y_def by auto
from farkas_minkowsky_weyl_theorem_1_full_dim[OF Y finY span]
obtain A nr where A: "A ∈ carrier_mat nr n" and YA: "cone Y = polyhedral_cone A"
and Y_Ints: "is_det_bound db ⟹ Y ⊆ ℤ⇩v ∩ Bounded_vec (?oi (max 1 Bnd)) ⟹ A ∈ ℤ⇩m ∩ ?Bndm" by blast
have fin: "finite ({row A i | i. i < nr} ∪ set Ns ∪ uminus ` set Ns)" by auto
from finite_list[OF this] obtain rs where rs_def: "set rs = {row A i |i. i < nr} ∪ set Ns ∪ uminus ` set Ns" by auto
from A N have rs: "set rs ⊆ carrier_vec n" unfolding rs_def by auto
let ?m = "length rs"
define B where "B = mat_of_rows n rs"
have B: "B ∈ carrier_mat ?m n" unfolding B_def by auto
show ?thesis
proof (intro exI conjI impI, rule B)
have id: "(∀r∈{rs ! i |i. i < ?m}. P r) = (∀ r < ?m. P (rs ! r))" for P by auto
have "polyhedral_cone B = { x ∈ carrier_vec n. B *⇩v x ≤ 0⇩v ?m}" unfolding polyhedral_cone_def
using B by auto
also have "… = { x ∈ carrier_vec n. ∀ i < ?m. row B i ∙ x ≤ 0}"
unfolding less_eq_vec_def using B by auto
also have "… = { x ∈ carrier_vec n. ∀ r ∈ set rs. r ∙ x ≤ 0}" using rs unfolding set_conv_nth id
by (intro Collect_cong conj_cong refl all_cong arg_cong[of _ _ "λ x. x ∙ _ ≤ 0"], auto simp: B_def)
also have "… = {x ∈ carrier_vec n. ∀ i < nr. row A i ∙ x ≤ 0}
∩ {x ∈ carrier_vec n. ∀ w ∈ set Ns ∪ uminus ` set Ns. w ∙ x ≤ 0}"
unfolding rs_def by blast
also have "{x ∈ carrier_vec n. ∀ i < nr. row A i ∙ x ≤ 0} = polyhedral_cone A"
unfolding polyhedral_cone_def using A by (auto simp: less_eq_vec_def)
also have "… = cone Y" unfolding YA ..
also have "{x ∈ carrier_vec n. ∀ w ∈ set Ns ∪ uminus ` set Ns. w ∙ x ≤ 0}
= {x ∈ carrier_vec n. ∀ w ∈ set Ns. w ∙ x = 0}"
(is "?l = ?r")
proof
show "?r ⊆ ?l" using N by auto
{
fix x w
assume "x ∈ ?l" "w ∈ set Ns"
with N have x: "x ∈ carrier_vec n" and w: "w ∈ carrier_vec n"
and one: "w ∙ x ≤ 0" and two: "(-w) ∙ x ≤ 0" by auto
from two have "w ∙ x ≥ 0"
by (subst (asm) scalar_prod_uminus_left, insert w x, auto)
with one have "w ∙ x = 0" by auto
}
thus "?l ⊆ ?r" by blast
qed
finally have "polyhedral_cone B = cone Y ∩ {x ∈ carrier_vec n. ∀w∈set Ns. w ∙ x = 0}" .
also have "… = cone X" unfolding Y_def
by (rule orthogonal_cone(1)[OF X N finX spanLN ortho refl spanL LX lin_Ls_Bs len_Ls_Bs])
finally show "cone X = polyhedral_cone B" ..
assume X_I: "X ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd)" and db: "is_det_bound db"
with LX have "set Ls ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd)" by auto
from Ns_bnd[OF db this] have N_I_Bnd: "set Ns ⊆ ℤ⇩v ∩ ?Bnd" by auto
from lin_Ls_Bs have linLs: "lin_indpt_list Ls" unfolding lin_indpt_list_def
using subset_li_is_li[of _ "set Ls"] by auto
from X_I LX have L_I: "set Ls ⊆ ℤ⇩v" by auto
have Y_I: "Y ⊆ ℤ⇩v ∩ Bounded_vec (?oi (max 1 Bnd))" unfolding Y_def using X_I order.trans[OF BU unit_vec_int_bounds, of Bnd]
Bounded_vec_mono[of "?oi Bnd" "?oi (max 1 Bnd)"] by auto
from Y_Ints[OF db Y_I]
have A_I_Bnd: "set (rows A) ⊆ ℤ⇩v ∩ ?Bnd" by auto
have "set (rows B) = set (rows (mat_of_rows n rs))" unfolding B_def by auto
also have "… = set rs" using rs by auto
also have "… = set (rows A) ∪ set Ns ∪ uminus ` set Ns" unfolding rs_def rows_def using A by auto
also have "… ⊆ ℤ⇩v ∩ ?Bnd" using A_I_Bnd N_I_Bnd by auto
finally show "B ∈ ℤ⇩m ∩ ?Bndm" by simp
qed
qed
text ‹Now for the other direction.›
lemma farkas_minkowsky_weyl_theorem_2:
assumes A: "A ∈ carrier_mat nr n"
shows "∃ X. X ⊆ carrier_vec n ∧ finite X ∧ polyhedral_cone A = cone X
∧ (is_det_bound db ⟶ A ∈ ℤ⇩m ∩ Bounded_mat (of_int Bnd) ⟶ X ⊆ ℤ⇩v ∩ Bounded_vec (of_int (db (n-1) (max 1 Bnd))))"
proof -
let ?oi = "of_int :: int ⇒ 'a"
let ?rows_A = "{row A i | i. i < nr}"
let ?Bnd = "Bounded_vec (?oi (db (n-1) (max 1 Bnd)))"
have rows_A_n: "?rows_A ⊆ carrier_vec n" using row_carrier_vec A by auto
hence "∃ mr B. B ∈ carrier_mat mr n ∧ cone ?rows_A = polyhedral_cone B
∧ (is_det_bound db ⟶ ?rows_A ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd) ⟶ set (rows B) ⊆ ℤ⇩v ∩ ?Bnd)"
using farkas_minkowsky_weyl_theorem_1[of ?rows_A] by auto
then obtain mr B
where mr: "B ∈ carrier_mat mr n" and B: "cone ?rows_A = polyhedral_cone B"
and Bnd: "is_det_bound db ⟹ ?rows_A ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd) ⟹ set (rows B) ⊆ ℤ⇩v ∩ ?Bnd"
by blast
let ?rows_B = "{row B i | i. i < mr}"
have rows_B: "?rows_B ⊆ carrier_vec n" using mr by auto
have "cone ?rows_B = polyhedral_cone A"
proof
have "?rows_B ⊆ polyhedral_cone A"
proof
fix r
assume "r ∈ ?rows_B"
then obtain j where r: "r = row B j" and j: "j < mr" by auto
then have rn: "r ∈ carrier_vec n" using mr row_carrier by auto
moreover have "A *⇩v r ≤ 0⇩v nr" unfolding less_eq_vec_def
proof (standard, unfold index_zero_vec)
show "dim_vec (A *⇩v r) = nr" using A by auto
next
show "∀i< nr. (A *⇩v r) $ i ≤ 0⇩v nr $ i"
proof (standard, rule impI)
fix i
assume i: "i < nr"
then have "row A i ∈ ?rows_A" by auto
then have "row A i ∈ cone ?rows_A"
using set_in_cone rows_A_n by blast
then have "row A i ∈ polyhedral_cone B" using B by auto
then have Br: "B *⇩v (row A i) ≤ 0⇩v mr"
unfolding polyhedral_cone_def using rows_A_n mr by auto
then have "(A *⇩v r) $ i = (row A i) ∙ r" using A i index_mult_mat_vec by auto
also have "… = r ∙ (row A i)"
using comm_scalar_prod[OF _ rn] row_carrier A by auto
also have "… = (row B j) ∙ (row A i)" using r by auto
also have "… = (B *⇩v (row A i)) $ j" using index_mult_mat_vec mr j by auto
also have "… ≤ 0" using Br j unfolding less_eq_vec_def by auto
also have "… = 0⇩v nr $ i" using i by auto
finally show "(A *⇩v r) $ i ≤ 0⇩v nr $ i" by auto
qed
qed
then show "r ∈ polyhedral_cone A"
unfolding polyhedral_cone_def
using A rn by auto
qed
then show "cone ?rows_B ⊆ polyhedral_cone A"
using cone_in_polyhedral_cone A by auto
next
show "polyhedral_cone A ⊆ cone ?rows_B"
proof (rule ccontr)
assume "¬ polyhedral_cone A ⊆ cone ?rows_B"
then obtain y where yA: "y ∈ polyhedral_cone A"
and yB: "y ∉ cone ?rows_B" by auto
then have yn: "y ∈ carrier_vec n" unfolding polyhedral_cone_def by auto
have finRB: "finite ?rows_B" by auto
from farkas_minkowsky_weyl_theorem_1[OF rows_B finRB]
obtain nr' A' where A': "A' ∈ carrier_mat nr' n" and cone: "cone ?rows_B = polyhedral_cone A'"
by blast
from yB[unfolded cone polyhedral_cone_def] yn A'
have "¬ (A' *⇩v y ≤ 0⇩v nr')" by auto
then obtain i where i: "i < nr'" and "row A' i ∙ y > 0"
unfolding less_eq_vec_def using A' yn by auto
define w where "w = row A' i"
have w: "w ∈ carrier_vec n" using i A' yn unfolding w_def by auto
from ‹row A' i ∙ y > 0› comm_scalar_prod[OF w yn] have wy: "w ∙ y > 0" "y ∙ w > 0" unfolding w_def by auto
{
fix b
assume "b ∈ ?rows_B"
hence "b ∈ cone ?rows_B" using set_in_cone[OF rows_B] by auto
from this[unfolded cone polyhedral_cone_def] A'
have b: "b ∈ carrier_vec n" and "A' *⇩v b ≤ 0⇩v nr'" by auto
from this(2)[unfolded less_eq_vec_def, THEN conjunct2, rule_format, of i]
have "w ∙ b ≤ 0" unfolding w_def using i A' by auto
hence "b ∙ w ≤ 0" using comm_scalar_prod[OF b w] by auto
}
hence wA: "w ∈ cone ?rows_A" unfolding B polyhedral_cone_def using mr w
by (auto simp: less_eq_vec_def)
from wy have yw: "-y ∙ w < 0"
by (subst scalar_prod_uminus_left, insert yn w, auto)
have "?rows_A ⊆ carrier_vec n" "finite ?rows_A" using assms by auto
from fundamental_theorem_of_linear_inequalities_A_imp_D[OF this wA, unfolded not_ex,
rule_format, of "-y" ] yn yw
obtain i where i: "i < nr" and "- y ∙ row A i < 0" by auto
hence "y ∙ row A i > 0" by (subst (asm) scalar_prod_uminus_left, insert i assms yn, auto)
hence "row A i ∙ y > 0" using comm_scalar_prod[OF _ yn, of "row A i"] i assms yn by auto
with yA show False unfolding polyhedral_cone_def less_eq_vec_def using i assms by auto
qed
qed
moreover have "?rows_B ⊆ carrier_vec n"
using row_carrier_vec mr by auto
moreover have "finite ?rows_B" by auto
moreover {
have rA: "set (rows A) = ?rows_A" using A unfolding rows_def by auto
have rB: "set (rows B) = ?rows_B" using mr unfolding rows_def by auto
assume "A ∈ ℤ⇩m ∩ Bounded_mat (?oi Bnd)" and db: "is_det_bound db"
hence "set (rows A) ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd)" by simp
from Bnd[OF db this[unfolded rA]]
have "?rows_B ⊆ ℤ⇩v ∩ ?Bnd" unfolding rA rB .
}
ultimately show ?thesis by blast
qed
lemma farkas_minkowsky_weyl_theorem:
"(∃ X. X ⊆ carrier_vec n ∧ finite X ∧ P = cone X)
⟷ (∃ A nr. A ∈ carrier_mat nr n ∧ P = polyhedral_cone A)"
using farkas_minkowsky_weyl_theorem_1 farkas_minkowsky_weyl_theorem_2 by metis
end
end