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