# Theory Farkas_Lemma

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
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
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)
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
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