section ‹Farkas' Lemma› text ‹We prove two variants of Farkas' lemma. Note that type here is more general than in the versions of Farkas' Lemma which are in the AFP-entry Farkas-Lemma, which is restricted to rational matrices. However, there $\delta$-rationals are supported, which are not present here.› theory Farkas_Lemma imports Fundamental_Theorem_Linear_Inequalities begin context gram_schmidt begin lemma Farkas_Lemma: fixes A :: "'a mat" and b :: "'a vec" assumes A: "A ∈ carrier_mat n nr" and b: "b ∈ carrier_vec n" shows "(∃ x. x ≥ 0⇩_{v}nr ∧ A *⇩_{v}x = b) ⟷ (∀ y. y ∈ carrier_vec n ⟶ A⇧^{T}*⇩_{v}y ≥ 0⇩_{v}nr ⟶ y ∙ b ≥ 0)" proof - let ?C = "set (cols A)" from A have C: "?C ⊆ carrier_vec n" and C': " ∀w∈set (cols A). dim_vec w = n" unfolding cols_def by auto have "(∃ x. x ≥ 0⇩_{v}nr ∧ A *⇩_{v}x = b) = (b ∈ cone ?C)" using cone_of_cols[OF A b] by simp also have "… = (∄y. y ∈ carrier_vec n ∧ (∀a⇩_{i}∈?C. 0 ≤ y ∙ a⇩_{i}) ∧ y ∙ b < 0)" unfolding fundamental_theorem_of_linear_inequalities(3)[OF C finite_set] mem_Collect_eq using b by auto also have "… = (∀y. y ∈ carrier_vec n ⟶ (∀a⇩_{i}∈?C. 0 ≤ y ∙ a⇩_{i}) ⟶ y ∙ b ≥ 0)" by auto also have "… = (∀ y. y ∈ carrier_vec n ⟶ A⇧^{T}*⇩_{v}y ≥ 0⇩_{v}nr ⟶ y ∙ b ≥ 0)" proof (intro all_cong imp_cong refl) fix y :: "'a vec" assume y: "y ∈ carrier_vec n" have "(∀a⇩_{i}∈ ?C. 0 ≤ y ∙ a⇩_{i}) = (∀a⇩_{i}∈ ?C. 0 ≤ a⇩_{i}∙ y)" by (intro ball_cong[OF refl], subst comm_scalar_prod[OF y], insert C, auto) also have "… = (0⇩_{v}nr ≤ A⇧^{T}*⇩_{v}y)" unfolding less_eq_vec_def using C A y by (auto simp: cols_def) finally show "(∀a⇩_{i}∈set (cols A). 0 ≤ y ∙ a⇩_{i}) = (0⇩_{v}nr ≤ A⇧^{T}*⇩_{v}y)" . qed finally show ?thesis . qed lemma Farkas_Lemma': fixes A :: "'a mat" and b :: "'a vec" assumes A: "A ∈ carrier_mat nr nc" and b: "b∈ carrier_vec nr" shows "(∃x. x∈ carrier_vec nc ∧ A *⇩_{v}x ≤ b) ⟷ (∀y. y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = 0⇩_{v}nc ⟶ y ∙ b ≥ 0)" proof - define B where "B = (1⇩_{m}nr) @⇩_{c}(A @⇩_{c}-A)" define b' where "b' = 0⇩_{v}nc @⇩_{v}(b @⇩_{v}-b)" define n where "n = nr + (nc + nc)" have id0: "0⇩_{v}(nr + (nc + nc)) = 0⇩_{v}nr @⇩_{v}(0⇩_{v}nc @⇩_{v}0⇩_{v}nc)" by (intro eq_vecI, auto) have idcarr: "(1⇩_{m}nr) ∈ carrier_mat nr nr" by auto have B: "B ∈ carrier_mat nr n" unfolding B_def n_def using A by auto have "(∃x ∈ carrier_vec nc. A *⇩_{v}x ≤ b) = (∃x1 ∈ carrier_vec nr. ∃x2 ∈ carrier_vec nc. ∃x3 ∈ carrier_vec nc. x1 ≥ 0⇩_{v}nr ∧ x2 ≥ 0⇩_{v}nc ∧ x3 ≥ 0⇩_{v}nc ∧ B *⇩_{v}(x1 @⇩_{v}(x2 @⇩_{v}x3)) = b)" proof assume "∃x∈carrier_vec nc. A *⇩_{v}x ≤ b" from this obtain x where Axb: "A *⇩_{v}x ≤ b" and xcarr: "x ∈ carrier_vec nc" by auto have bmAx: "b - A *⇩_{v}x ∈ carrier_vec nr" using A b xcarr by simp define x1 where "x1 = b - A *⇩_{v}x" have x1: "x1 ∈ carrier_vec nr" using bmAx unfolding x1_def by (simp add: xcarr) define x2 where "x2 = vec (dim_vec x) (λi. if x $ i ≥ 0 then x $ i else 0)" have x2: "x2 ∈ carrier_vec nc" using xcarr unfolding x2_def by simp define x3 where "x3 = vec (dim_vec x) (λi. if x $ i < 0 then -x $ i else 0)" have x3: "x3 ∈ carrier_vec nc" using xcarr unfolding x3_def by simp have x2x3carr: "x2 @⇩_{v}x3 ∈ carrier_vec (nc + nc)" using x2 x3 by simp have x2x3x: "x2 - x3 = x" unfolding x2_def x3_def by auto have "A *⇩_{v}x -b ≤ 0⇩_{v}nr" using vec_le_iff_diff_le_0 b by (metis A Axb carrier_matD(1) dim_mult_mat_vec) hence x1lez: "x1 ≥ 0⇩_{v}nr" using x1 unfolding x1_def by (smt A Axb carrier_matD(1) carrier_vecD diff_ge_0_iff_ge dim_mult_mat_vec index_minus_vec(1) index_zero_vec(1) index_zero_vec(2) less_eq_vec_def) have x2lez: "x2 ≥ 0⇩_{v}nc" using x2 less_eq_vec_def unfolding x2_def by fastforce have x3lez: "x3 ≥ 0⇩_{v}nc" using x3 less_eq_vec_def unfolding x3_def by fastforce have B1: "(1⇩_{m}nr) *⇩_{v}x1 = b - A *⇩_{v}x" using xcarr x1 unfolding x1_def by simp have "A *⇩_{v}x2 + (-A) *⇩_{v}x3 = A *⇩_{v}x2 + A *⇩_{v}(-x3)" using x2 x3 A by auto also have "… = A *⇩_{v}(x2 + (-x3))" using A x2 x3 by (metis mult_add_distrib_mat_vec uminus_carrier_vec) also have "… = A *⇩_{v}x" using x2x3x minus_add_uminus_vec x2 x3 by fastforce finally have B2:"A *⇩_{v}x2 + (-A) *⇩_{v}x3 = A *⇩_{v}x" by auto have "B *⇩_{v}(x1 @⇩_{v}(x2 @⇩_{v}x3)) = (1⇩_{m}nr) *⇩_{v}x1 + (A *⇩_{v}x2 + (-A) *⇩_{v}x3)" (is "… = ?p1 + ?p2") using x1 x2 x3 A mat_mult_append_cols unfolding B_def by (subst mat_mult_append_cols[OF _ _ x1 x2x3carr], auto simp add: mat_mult_append_cols) also have "?p1 = b - A *⇩_{v}x" using B1 unfolding x1_def by auto also have "?p2 = A *⇩_{v}x" using B2 by simp finally have res: "B *⇩_{v}(x1 @⇩_{v}(x2 @⇩_{v}x3)) = b" using A xcarr b by auto show "∃x∈carrier_vec nc. A *⇩_{v}x ≤ b ⟹ ∃x1∈carrier_vec nr. ∃x2∈carrier_vec nc. ∃x3∈carrier_vec nc. 0⇩_{v}nr ≤ x1 ∧ 0⇩_{v}nc ≤ x2 ∧ 0⇩_{v}nc ≤ x3 ∧ B *⇩_{v}(x1 @⇩_{v}x2 @⇩_{v}x3) = b" using x1 x2 x3 x1lez x2lez x3lez res by auto next assume "∃x1 ∈ carrier_vec nr. ∃x2 ∈ carrier_vec nc. ∃x3 ∈ carrier_vec nc. x1 ≥ 0⇩_{v}nr ∧ x2 ≥ 0⇩_{v}nc ∧ x3 ≥ 0⇩_{v}nc ∧ B *⇩_{v}(x1 @⇩_{v}(x2 @⇩_{v}x3)) = b" from this obtain x1 x2 x3 where x1: "x1 ∈ carrier_vec nr" and x1lez: "x1 ≥ 0⇩_{v}nr" and x2: "x2 ∈ carrier_vec nc" and x2lez: "x2 ≥ 0⇩_{v}nc" and x3: "x3 ∈ carrier_vec nc" and x3lez: "x3 ≥ 0⇩_{v}nc" and clc: "B *⇩_{v}(x1 @⇩_{v}(x2 @⇩_{v}x3)) = b" by auto have x2x3carr: "x2 @⇩_{v}x3 ∈ carrier_vec (nc + nc)" using x2 x3 by simp define x where "x = x2 - x3" have xcarr: "x ∈ carrier_vec nc" using x2 x3 unfolding x_def by simp have "A *⇩_{v}x2 + (-A) *⇩_{v}x3 = A *⇩_{v}x2 + A *⇩_{v}(-x3)" using x2 x3 A by auto also have "… = A *⇩_{v}(x2 + (-x3))" using A x2 x3 by (metis mult_add_distrib_mat_vec uminus_carrier_vec) also have "… = A *⇩_{v}x" using minus_add_uminus_vec x2 x3 unfolding x_def by fastforce finally have B2:"A *⇩_{v}x2 + (-A) *⇩_{v}x3 = A *⇩_{v}x" by auto have Axcarr: "A *⇩_{v}x ∈ carrier_vec nr" using A xcarr by auto have "b = B *⇩_{v}(x1 @⇩_{v}(x2 @⇩_{v}x3))" using clc by auto also have "… = (1⇩_{m}nr) *⇩_{v}x1 + (A *⇩_{v}x2 + (-A) *⇩_{v}x3)" (is "… = ?p1 + ?p2") using x1 x2 x3 A mat_mult_append_cols unfolding B_def by (subst mat_mult_append_cols[OF _ _ x1 x2x3carr], auto simp add: mat_mult_append_cols) also have "?p2 = A *⇩_{v}x" using B2 by simp finally have res: "b = (1⇩_{m}nr) *⇩_{v}x1 + A *⇩_{v}x" using A xcarr b by auto hence "b = x1 + A *⇩_{v}x" using x1 A b by simp hence "b - A *⇩_{v}x = x1" using x1 A b by auto hence "b - A *⇩_{v}x ≥ 0⇩_{v}nr" using x1lez by auto hence "A *⇩_{v}x ≤ b" using Axcarr by (smt ‹b - A *⇩_{v}x = x1› ‹b = x1 + A *⇩_{v}x› carrier_vecD comm_add_vec index_zero_vec(2) minus_add_minus_vec minus_cancel_vec vec_le_iff_diff_le_0 x1) then show "∃x1∈carrier_vec nr. ∃x2∈carrier_vec nc. ∃x3∈carrier_vec nc. 0⇩_{v}nr ≤ x1 ∧ 0⇩_{v}nc ≤ x2 ∧ 0⇩_{v}nc ≤ x3 ∧ B *⇩_{v}(x1 @⇩_{v}x2 @⇩_{v}x3) = b ⟹ ∃x∈carrier_vec nc. A *⇩_{v}x ≤ b" using xcarr by blast qed also have "… = (∃x1 ∈ carrier_vec nr. ∃x2 ∈ carrier_vec nc. ∃x3 ∈ carrier_vec nc. (x1 @⇩_{v}(x2 @⇩_{v}x3)) ≥ 0⇩_{v}n ∧ B *⇩_{v}(x1 @⇩_{v}(x2 @⇩_{v}x3)) = b)" by (metis append_vec_le id0 n_def zero_carrier_vec) also have "… = (∃x ∈ carrier_vec n. x ≥ 0⇩_{v}n ∧ B *⇩_{v}x = b)" unfolding n_def exists_vec_append by auto also have "… = (∃x ≥ 0⇩_{v}n. B *⇩_{v}x = b)" unfolding less_eq_vec_def by fastforce also have "… = (∀ y. y ∈ carrier_vec nr ⟶ B⇧^{T}*⇩_{v}y ≥ 0⇩_{v}n ⟶ y ∙ b ≥ 0)" by (rule gram_schmidt.Farkas_Lemma[OF B b]) also have "… = (∀ y. y ∈ carrier_vec nr ⟶ (y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = 0⇩_{v}nc) ⟶ y ∙ b ≥ 0)" proof (intro all_cong imp_cong refl) fix y :: "'a vec" assume y: "y ∈ carrier_vec nr" have idtcarr: "(1⇩_{m}nr)⇧^{T}∈ carrier_mat nr nr" by auto have Atcarr: "A⇧^{T}∈ carrier_mat nc nr" using A by auto have mAtcarr: "(-A)⇧^{T}∈ carrier_mat nc nr" using A by auto have AtAtcarr: "A⇧^{T}@⇩_{r}(-A)⇧^{T}∈ carrier_mat (nc + nc) nr" using A by auto have "B⇧^{T}*⇩_{v}y = ((1⇩_{m}nr)⇧^{T}@⇩_{r}A⇧^{T}@⇩_{r}(-A)⇧^{T}) *⇩_{v}y" unfolding B_def by (simp add: append_cols_def) also have "… = ((1⇩_{m}nr)⇧^{T}*⇩_{v}y) @⇩_{v}(A⇧^{T}*⇩_{v}y) @⇩_{v}((-A)⇧^{T}*⇩_{v}y)" using mat_mult_append[OF Atcarr mAtcarr y] mat_mult_append y Atcarr idtcarr mAtcarr by (metis AtAtcarr) finally have eq: "B⇧^{T}*⇩_{v}y = ((1⇩_{m}nr)⇧^{T}*⇩_{v}y) @⇩_{v}(A⇧^{T}*⇩_{v}y) @⇩_{v}((-A)⇧^{T}*⇩_{v}y)" by auto have "(B⇧^{T}*⇩_{v}y ≥ 0⇩_{v}n) = (0⇩_{v}n ≤ (1⇩_{m}nr)⇧^{T}*⇩_{v}y @⇩_{v}A⇧^{T}*⇩_{v}y @⇩_{v}(- A)⇧^{T}*⇩_{v}y)" unfolding eq by simp also have "… = (((1⇩_{m}nr)⇧^{T}*⇩_{v}y) @⇩_{v}(A⇧^{T}*⇩_{v}y) @⇩_{v}((-A)⇧^{T}*⇩_{v}y) ≥ 0⇩_{v}nr @⇩_{v}0⇩_{v}nc @⇩_{v}0⇩_{v}nc)" using id0 by (metis eq n_def) also have "… = (y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y ≥ 0⇩_{v}nc ∧ ((-A)⇧^{T}*⇩_{v}y) ≥ 0⇩_{v}nc)" by (metis Atcarr append_vec_le mult_mat_vec_carrier one_mult_mat_vec transpose_one y zero_carrier_vec) also have "… = (y ≥ 0⇩_{v}nr ∧A⇧^{T}*⇩_{v}y ≥ 0⇩_{v}nc ∧ -(A⇧^{T}*⇩_{v}y) ≥ 0⇩_{v}nc)" by (metis A Atcarr carrier_matD(2) carrier_vecD transpose_uminus uminus_mult_mat_vec y) also have "… = (y ≥ 0⇩_{v}nr ∧A⇧^{T}*⇩_{v}y ≥ 0⇩_{v}nc ∧ (A⇧^{T}*⇩_{v}y) ≤ 0⇩_{v}nc)" by (metis (mono_tags, lifting) A Atcarr carrier_matD(2) carrier_vecD index_zero_vec(2) mAtcarr mult_mat_vec_carrier transpose_uminus uminus_mult_mat_vec uminus_uminus_vec vec_le_iff_diff_le_0 y zero_minus_vec) also have "… = (y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = 0⇩_{v}nc)" by auto finally show "(B⇧^{T}*⇩_{v}y ≥ 0⇩_{v}n) = (y ≥ 0⇩_{v}nr ∧ A⇧^{T}*⇩_{v}y = 0⇩_{v}nc)" . qed finally show ?thesis by (auto simp: less_eq_vec_def) qed end end