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.

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  0v 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  (aiX. 0  nv  ai)}"
      unfolding Ns_def cond_def by auto
    have "polyhedral_cone (- A) = { b. b  carrier_vec n  (- A) *v b  0v 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 = 0v 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  0v ?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. wset 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  0v 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  0v 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)  0v 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 " = 0v nr $ i" using i by auto
          finally show "(A *v r) $ i  0v 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  0v 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  0v 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