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.› 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 ∧ (X ⊆ ℤ⇩v ∩ Bounded_vec Bnd ⟶ A ∈ ℤ⇩m ∩ Bounded_mat (det_bound (n-1) Bnd))" proof - define cond where "cond = (λ W. Suc (card W) = n ∧ lin_indpt W ∧ W ⊆ X)" { 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" "X ⊆ ℤ⇩v ∩ Bounded_vec Bnd ⟹ normal_vector W ∈ ℤ⇩v ∩ Bounded_vec (det_bound (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 Bnd" { 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 XI] have "normal_vector W ∈ ℤ⇩v ∩ Bounded_vec (det_bound (n - 1) Bnd)" by auto hence "v ∈ ℤ⇩v ∩ Bounded_vec (det_bound (n - 1) Bnd)" using v by auto } hence "set (rows (- A)) ⊆ ℤ⇩v ∩ Bounded_vec (det_bound (n - 1) Bnd)" by blast thus "- A ∈ ℤ⇩m ∩ Bounded_mat (det_bound (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 ∧ (X ⊆ ℤ⇩v ∩ Bounded_vec Bnd ⟶ A ∈ ℤ⇩m ∩ Bounded_mat (det_bound (n-1) (max 1 Bnd)))" proof - 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 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: "set Ls ⊆ ℤ⇩v ∩ Bounded_vec Bnd ⟹ set Ns ⊆ ℤ⇩v ∩ Bounded_vec (det_bound (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 (det_bound (n-1) (max 1 Bnd))" let ?Bndm = "Bounded_mat (det_bound (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: "Y ⊆ ℤ⇩v ∩ Bounded_vec (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 Bnd" with LX have "set Ls ⊆ ℤ⇩v ∩ Bounded_vec Bnd" by auto from Ns_bnd[OF 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 (max 1 Bnd)" unfolding Y_def using X_I BU Bounded_vec_mono[of Bnd "max 1 Bnd"] by (auto simp: unit_vecs_def Ints_vec_def) from Y_Ints[OF 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 ∧ (A ∈ ℤ⇩m ∩ Bounded_mat Bnd ⟶ X ⊆ ℤ⇩v ∩ Bounded_vec (det_bound (n-1) (max 1 Bnd)))" proof - let ?rows_A = "{row A i | i. i < nr}" let ?Bnd = "Bounded_vec (det_bound (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 ∧ (?rows_A ⊆ ℤ⇩v ∩ Bounded_vec 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: "?rows_A ⊆ ℤ⇩v ∩ Bounded_vec 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 Bnd" hence "set (rows A) ⊆ ℤ⇩v ∩ Bounded_vec Bnd" by simp from Bnd[OF 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