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 ≥ 0v nr ∧ A *v x = b) ⟷ (∀ y. y ∈ carrier_vec n ⟶ AT *v y ≥ 0v 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 ≥ 0v nr ∧ A *v x = b) = (b ∈ cone ?C)"
    using cone_of_cols[OF A b] by simp
  also have "… = (∄y. y ∈ carrier_vec n ∧ (∀ai∈?C. 0 ≤ y ∙ ai) ∧ 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 ⟶ (∀ai∈?C. 0 ≤ y ∙ ai) ⟶ y ∙ b ≥ 0)"
    by auto
  also have "… = (∀ y. y ∈ carrier_vec n ⟶ AT *v y ≥ 0v nr ⟶ y ∙ b ≥ 0)"
  proof (intro all_cong imp_cong refl)
    fix y :: "'a vec"
    assume y: "y ∈ carrier_vec n"
    have "(∀ai∈ ?C. 0 ≤ y ∙ ai) = (∀ai∈ ?C. 0 ≤ ai ∙ y)"
      by (intro ball_cong[OF refl], subst comm_scalar_prod[OF y], insert C, auto)
    also have "… = (0v nr ≤ AT *v y)"
      unfolding less_eq_vec_def using C A y by (auto simp: cols_def)
    finally show "(∀ai∈set (cols A). 0 ≤ y ∙ ai) = (0v nr ≤ AT *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 ≥ 0v nr ∧ AT *v y = 0v nc ⟶ y ∙ b ≥ 0)"
proof -
  define B where "B = (1m nr) @c (A @c -A)"   
  define b' where "b' = 0v nc @v (b @v -b)" 
  define n where "n = nr + (nc + nc)" 
  have id0: "0v (nr + (nc + nc)) = 0v nr @v (0v nc @v 0v nc)" by (intro eq_vecI, auto)
  have idcarr: "(1m 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 ≥ 0v nr ∧ x2 ≥ 0v nc ∧ x3 ≥ 0v 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 ≤ 0v nr" using vec_le_iff_diff_le_0 b
      by (metis A Axb carrier_matD(1) dim_mult_mat_vec)
    hence x1lez: "x1 ≥ 0v 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 ≥ 0v nc" using x2 less_eq_vec_def unfolding x2_def by fastforce
    have x3lez: "x3 ≥ 0v nc" using x3 less_eq_vec_def unfolding x3_def by fastforce
    have B1: "(1m 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)) = (1m 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.
          0v nr ≤ x1 ∧ 0v nc ≤ x2 ∧ 0v 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 ≥ 0v nr ∧ x2 ≥ 0v nc ∧ x3 ≥ 0v nc ∧ B *v (x1 @v (x2 @v x3)) = b"
    from this obtain x1 x2 x3 where x1: "x1 ∈ carrier_vec nr" and x1lez: "x1 ≥ 0v nr" 
      and x2: "x2 ∈ carrier_vec nc" and x2lez: "x2 ≥ 0v nc"
      and x3: "x3 ∈ carrier_vec nc" and x3lez: "x3 ≥ 0v 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 "… = (1m 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 = (1m 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 ≥ 0v 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.
          0v nr ≤ x1 ∧ 0v nc ≤ x2 ∧ 0v 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)) ≥ 0v 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 ≥ 0v n  ∧ B *v x = b)"
    unfolding n_def exists_vec_append by auto
  also have "… = (∃x ≥ 0v n. B *v x = b)" unfolding less_eq_vec_def by fastforce
  also have "… = (∀ y. y ∈ carrier_vec nr ⟶ BT *v y ≥ 0v n ⟶ y ∙ b ≥ 0)"
    by (rule gram_schmidt.Farkas_Lemma[OF B b])
  also have "… = (∀ y. y ∈ carrier_vec nr ⟶ (y ≥ 0v nr ∧ AT *v y = 0v nc) ⟶ y ∙ b ≥ 0)" 
  proof (intro all_cong imp_cong refl)
    fix y :: "'a vec"
    assume y: "y ∈ carrier_vec nr"
    have idtcarr: "(1m nr)T ∈ carrier_mat nr nr" by auto
    have Atcarr: "AT ∈ carrier_mat nc nr" using A by auto
    have mAtcarr: "(-A)T ∈ carrier_mat nc nr" using A by auto
    have AtAtcarr: "AT @r (-A)T ∈ carrier_mat (nc + nc) nr" using A by auto
    have "BT *v y = ((1m nr)T @r AT @r (-A)T) *v y" unfolding B_def
      by (simp add: append_cols_def)
    also have "… = ((1m nr)T *v y) @v (AT *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: "BT *v y = ((1m nr)T *v y) @v (AT *v y) @v ((-A)T *v y)" by auto
    have "(BT *v y ≥ 0v n) = (0v n ≤ (1m nr)T *v y @v AT *v y @v (- A)T *v y)" unfolding eq by simp
    also have "… = (((1m nr)T *v y) @v (AT *v y) @v ((-A)T *v y) ≥ 0v nr @v 0v nc @v 0v nc)"
      using id0 by (metis eq n_def)
    also have "… = (y ≥ 0v nr ∧ AT *v y ≥ 0v nc ∧ ((-A)T *v y) ≥ 0v nc)"
      by (metis Atcarr append_vec_le mult_mat_vec_carrier one_mult_mat_vec transpose_one y zero_carrier_vec)
    also have "… = (y ≥ 0v nr ∧AT *v y ≥ 0v nc ∧ -(AT *v y) ≥ 0v nc)"
      by (metis A Atcarr carrier_matD(2) carrier_vecD transpose_uminus uminus_mult_mat_vec y)
    also have "… = (y ≥ 0v nr ∧AT *v y ≥ 0v nc ∧ (AT *v y) ≤ 0v 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 ≥ 0v nr ∧ AT *v y = 0v nc)" by auto
    finally show "(BT *v y ≥ 0v n) = (y ≥ 0v nr ∧ AT *v y = 0v nc)" .
  qed
  finally show ?thesis by (auto simp: less_eq_vec_def)
qed

end
end