Theory Convex_Hull

theory Convex_Hull
imports Cone
section ‹Convex Hulls›

text ‹We define the notion of convex hull of a set or list of vectors and derive basic
  properties thereof.›

theory Convex_Hull
  imports Cone
begin

context gram_schmidt
begin

definition "convex_lincomb c Vs b = (nonneg_lincomb c Vs b ∧ sum c Vs = 1)"

definition "convex_lincomb_list c Vs b = (nonneg_lincomb_list c Vs b ∧ sum c {0..<length Vs} = 1)"

definition "convex_hull Vs = {x. ∃ Ws c. finite Ws ∧ Ws ⊆ Vs ∧ convex_lincomb c Ws x}"

lemma convex_hull_carrier[intro]: "Vs ⊆ carrier_vec n ⟹ convex_hull Vs ⊆ carrier_vec n"
  unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def by auto

lemma convex_hull_mono: "Vs ⊆ Ws ⟹ convex_hull Vs ⊆ convex_hull Ws"
  unfolding convex_hull_def by auto

lemma convex_lincomb_empty[simp]: "¬ (convex_lincomb c {} x)"
  unfolding convex_lincomb_def by simp

lemma set_in_convex_hull:
  assumes "A ⊆ carrier_vec n"
  shows "A ⊆ convex_hull A"
proof
  fix a
  assume "a ∈ A"
  hence acarr: "a ∈ carrier_vec n" using assms by auto
  hence "convex_lincomb (λ x. 1) {a} a " unfolding convex_lincomb_def
    by (auto simp: nonneg_lincomb_def lincomb_def)
  then show "a ∈ convex_hull A" using ‹a ∈ A› unfolding convex_hull_def by auto
qed

lemma convex_hull_empty[simp]:
  "convex_hull {} = {}"
  "A ⊆ carrier_vec n ⟹ convex_hull A = {} ⟷ A = {}"
proof -
  show "convex_hull {} = {}" unfolding convex_hull_def by auto
  then show "A ⊆ carrier_vec n ⟹ convex_hull A = {} ⟷ A = {}"
    using set_in_convex_hull[of A] by auto
qed

lemma convex_hull_bound: assumes XBnd: "X ⊆ Bounded_vec Bnd"
  and X: "X ⊆ carrier_vec n"
shows "convex_hull X ⊆ Bounded_vec Bnd"
proof
  fix x
  assume "x ∈ convex_hull X"
  from this[unfolded convex_hull_def]
  obtain Y c where fin: "finite Y" and YX: "Y ⊆ X" and cx: "convex_lincomb c Y x" by auto
  from cx[unfolded convex_lincomb_def nonneg_lincomb_def]
  have x: "x = lincomb c Y" and sum: "sum c Y = 1" and c0: "⋀ y. y ∈ Y ⟹ c y ≥ 0" by auto
  from YX X XBnd have Y: "Y ⊆ carrier_vec n" and YBnd: "Y ⊆ Bounded_vec Bnd" by auto
  from x Y have dim: "dim_vec x = n" by auto
  show "x ∈ Bounded_vec Bnd" unfolding Bounded_vec_def mem_Collect_eq dim
  proof (intro allI impI)
    fix i
    assume i: "i < n"
    have "abs (x $ i) = abs (∑x∈Y. c x * x $ i)" unfolding x
      by (subst lincomb_index[OF i Y], auto)
    also have "… ≤ (∑x∈Y. abs (c x * x $ i))" by auto
    also have "… = (∑x∈Y. abs (c x) * abs (x $ i))" by (simp add: abs_mult)
    also have "… ≤ (∑x∈Y. abs (c x) * Bnd)"
      by (intro sum_mono mult_left_mono, insert YBnd[unfolded Bounded_vec_def] i Y, force+)
    also have "… = (∑x∈Y. abs (c x)) * Bnd"
      by (simp add: sum_distrib_right)
    also have "(∑x∈Y. abs (c x)) = (∑x∈Y. c x)"
      by (rule sum.cong, insert c0, auto)
    also have "… = 1" by fact
    finally show "¦x $ i¦ ≤ Bnd" by auto
  qed
qed

definition "convex_hull_list Vs = {x. ∃ c. convex_lincomb_list c Vs x}"

lemma lincomb_list_elem:
  "set Vs ⊆ carrier_vec n ⟹
   lincomb_list (λ j. if i=j then 1 else 0) Vs = (if i < length Vs then Vs ! i else 0v n)"
proof (induction Vs rule: rev_induct)
  case (snoc x Vs)
  have x: "x ∈ carrier_vec n" and Vs: "set Vs ⊆ carrier_vec n" using snoc.prems by auto
  let ?f = "λ j. if i = j then 1 else 0"
  have "lincomb_list ?f (Vs @ [x]) = lincomb_list ?f Vs + ?f (length Vs) ⋅v x"
    using x Vs by simp
  also have "… = (if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n)" (is ?goal)
    using less_linear[of i "length Vs"]
  proof (elim disjE)
    assume i: "i < length Vs"
    have "lincomb_list (λj. if i = j then 1 else 0) Vs = Vs ! i"
      using snoc.IH[OF Vs] i by auto
    moreover have "(if i = length Vs then 1 else 0) ⋅v x = 0v n" using i x by auto
    moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n) = Vs ! i"
      using i append_Cons_nth_left by fastforce
    ultimately show ?goal using Vs i lincomb_list_carrier M.r_zero by metis
  next
    assume i: "i = length Vs"
    have "lincomb_list (λj. if i = j then 1 else 0) Vs = 0v n"
      using snoc.IH[OF Vs] i by auto
    moreover have "(if i = length Vs then 1 else 0) ⋅v x = x" using i x by auto
    moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n) = x"
      using i append_Cons_nth_left by simp
    ultimately show ?goal using x by simp
  next
    assume i: "i > length Vs"
    have "lincomb_list (λj. if i = j then 1 else 0) Vs = 0v n"
      using snoc.IH[OF Vs] i by auto
    moreover have "(if i = length Vs then 1 else 0) ⋅v x = 0v n" using i x by auto
    moreover have "(if i < length (Vs @ [x]) then (Vs @ [x]) ! i else 0v n) = 0v n"
      using i by simp
    ultimately show ?goal by simp
  qed
  finally show ?case by auto
qed simp

lemma set_in_convex_hull_list: fixes Vs :: "'a vec list"
  assumes "set Vs ⊆ carrier_vec n"
  shows "set Vs ⊆ convex_hull_list Vs"
proof
  fix x assume "x ∈ set Vs"
  then obtain i where i: "i < length Vs"
    and x: "x = Vs ! i" using set_conv_nth[of Vs] by auto
  let ?f = "λ j. if i = j then 1 else 0 :: 'a"
  have "lincomb_list ?f Vs = x" using i x lincomb_list_elem[OF assms] by auto
  moreover have "∀ j < length Vs. ?f j ≥ 0" by auto
  moreover have "sum ?f {0..<length Vs} = 1" using i by simp
  ultimately show "x ∈ convex_hull_list Vs"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
qed

lemma convex_hull_list_combination:
  assumes Vs: "set Vs ⊆ carrier_vec n"
    and x: "x ∈ convex_hull_list Vs"
    and y: "y ∈ convex_hull_list Vs"
    and l0: "0 ≤ l" and l1: "l ≤ 1"
  shows "l ⋅v x + (1 - l) ⋅v y ∈ convex_hull_list Vs"
proof -
  from x obtain cx where x: "lincomb_list cx Vs = x" and cx0: "∀ i < length Vs. cx i ≥ 0"
    and cx1: "sum cx {0..<length Vs} = 1"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
  from y obtain cy where y: "lincomb_list cy Vs = y" and cy0: "∀ i < length Vs. cy i ≥ 0"
    and cy1: "sum cy {0..<length Vs} = 1"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
  let ?c = "λ i. l * cx i + (1 - l) * cy i"
  have "set Vs ⊆ carrier_vec n ⟹
        lincomb_list ?c Vs = l ⋅v lincomb_list cx Vs + (1 - l) ⋅v lincomb_list cy Vs"
  proof (induction Vs rule: rev_induct)
    case (snoc v Vs)
    have v: "v ∈ carrier_vec n" and Vs: "set Vs ⊆ carrier_vec n"
      using snoc.prems by auto
    have "lincomb_list ?c (Vs @ [v]) = lincomb_list ?c Vs + ?c (length Vs) ⋅v v"
      using snoc.prems by auto
    also have "lincomb_list ?c Vs =
               l ⋅v lincomb_list cx Vs + (1 - l) ⋅v lincomb_list cy Vs"
      by (rule snoc.IH[OF Vs])
    also have "?c (length Vs) ⋅v v =
               l ⋅v (cx (length Vs) ⋅v v) + (1 - l) ⋅v (cy (length Vs) ⋅v v)"
      using add_smult_distrib_vec smult_smult_assoc by metis
    also have "l ⋅v lincomb_list cx Vs + (1 - l) ⋅v lincomb_list cy Vs + … =
                  l ⋅v (lincomb_list cx Vs + cx (length Vs) ⋅v v) +
                  (1 - l) ⋅v (lincomb_list cy Vs + cy (length Vs) ⋅v v)"
      using lincomb_list_carrier[OF Vs] v
      by (simp add: M.add.m_assoc M.add.m_lcomm smult_r_distr)
    finally show ?case using Vs v by simp
  qed simp
  hence "lincomb_list ?c Vs = l ⋅v x + (1 - l) ⋅v y" using Vs x y by simp
  moreover have "∀ i < length Vs. ?c i ≥ 0" using cx0 cy0 l0 l1 by simp
  moreover have "sum ?c {0..<length Vs} = 1"
  proof(simp add: sum.distrib)
    have "(∑i = 0..<length Vs. (1 - l) * cy i) = (1 - l) * sum cy {0..<length Vs}"
      using sum_distrib_left by metis
    moreover have "(∑i = 0..<length Vs. l * cx i) = l * sum cx {0..<length Vs}"
      using sum_distrib_left by metis
    ultimately show "(∑i = 0..<length Vs. l * cx i) + (∑i = 0..<length Vs. (1 - l) * cy i) = 1"
      using cx1 cy1 by simp
  qed
  ultimately show ?thesis
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
qed

lemma convex_hull_list_mono:
  assumes "set Ws ⊆ carrier_vec n"
  shows "set Vs ⊆ set Ws ⟹ convex_hull_list Vs ⊆ convex_hull_list Ws"
proof (standard, induction Vs)
  case Nil
  from Nil(2) show ?case unfolding convex_hull_list_def convex_lincomb_list_def by auto
next
  case (Cons v Vs)
  have v: "v ∈ set Ws" and Vs: "set Vs ⊆ set Ws" using Cons.prems(1) by auto
  hence v1: "v ∈ convex_hull_list Ws" using set_in_convex_hull_list[OF assms] by auto
  from Cons.prems(2) obtain c
    where x: "lincomb_list c (v # Vs) = x" and c0: "∀ i < length Vs + 1. c i ≥ 0"
      and c1: "sum c {0..<length Vs + 1} = 1"
    unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
    by auto
  have x: "x = c 0 ⋅v v + lincomb_list (c ∘ Suc) Vs" using Vs v assms x by auto

  show ?case proof (cases)
    assume P: "c 0 = 1"
    hence "sum (c ∘ Suc) {0..<length Vs} = 0"
      using sum.atLeast0_lessThan_Suc_shift c1
      by (metis One_nat_def R.show_r_zero add.right_neutral add_Suc_right)
    moreover have "⋀ i. i ∈ {0..<length Vs} ⟹ (c ∘ Suc) i ≥ 0"
      using c0 by simp
    ultimately have "∀ i ∈ {0..<length Vs}. (c ∘ Suc) i = 0"
      using sum_nonneg_eq_0_iff by blast
    hence "⋀ i. i < length Vs ⟹ (c ∘ Suc) i ⋅v Vs ! i = 0v n"
      using Vs assms by (simp add: subset_code(1))
    hence "lincomb_list (c ∘ Suc) Vs = 0v n"
      using lincomb_list_eq_0 by simp
    hence "x = v" using P x v assms by auto
    thus ?case using v1 by auto

  next

    assume P: "c 0 ≠ 1"
    have c1: "c 0 + sum (c ∘ Suc) {0..<length Vs} = 1"
      using sum.atLeast0_lessThan_Suc_shift[of c] c1 by simp
    have "sum (c ∘ Suc) {0..<length Vs} ≥ 0" by (rule sum_nonneg, insert c0, simp)
    hence "c 0 < 1" using P c1 by auto
    let ?c' = "λ i. 1 / (1 - c 0) * (c ∘ Suc) i"
    have "sum ?c' {0..<length Vs} = 1 / (1 - c 0) * sum (c ∘ Suc) {0..<length Vs}"
      using c1 P sum_distrib_left by metis
    hence "sum ?c' {0..<length Vs} = 1" using P c1 by simp
    moreover have "∀ i < length Vs. ?c' i ≥ 0" using c0 `c 0 < 1` by simp
    ultimately have c': "lincomb_list ?c' Vs ∈ convex_hull_list Ws"
      using Cons.IH[OF Vs]
        convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
      by blast
    have "lincomb_list ?c' Vs = 1 / (1 - c 0) ⋅v lincomb_list (c ∘ Suc) Vs"
      by(rule lincomb_list_smult, insert Vs assms, auto)
    hence "(1 - c 0) ⋅v lincomb_list ?c' Vs = lincomb_list (c ∘ Suc) Vs"
      using P by auto
    hence "x = c 0 ⋅v v + (1 - c 0) ⋅v lincomb_list ?c' Vs" using x by auto
    thus "x ∈ convex_hull_list Ws"
      using convex_hull_list_combination[OF assms v1 c'] c0 `c 0 < 1`
      by simp
  qed
qed

lemma convex_hull_list_eq_set:
  "set Vs ⊆ carrier_vec n ⟹ set Vs = set Ws ⟹ convex_hull_list Vs = convex_hull_list Ws"
  using convex_hull_list_mono by blast

lemma find_indices_empty: "(find_indices x Vs = []) = (x ∉ set Vs)"
proof (induction Vs rule: rev_induct)
  case (snoc v Vs)
  show ?case
  proof
    assume "find_indices x (Vs @ [v]) = []"
    hence "x ≠ v ∧ find_indices x Vs = []" by auto
    thus "x ∉ set (Vs @ [v])" using snoc by simp
  next
    assume "x ∉ set (Vs @ [v])"
    hence "x ≠ v ∧ find_indices x Vs = []" using snoc by auto
    thus "find_indices x (Vs @ [v]) = []" by simp
  qed
qed simp

lemma distinct_list_find_indices:
  shows "⟦ i < length Vs; Vs ! i = x; distinct Vs ⟧ ⟹ find_indices x Vs = [i]"
proof (induction Vs rule: rev_induct)
  case (snoc v Vs)
  have dist: "distinct Vs" and xVs: "v ∉ set Vs" using snoc.prems(3) by(simp_all)
  show ?case
  proof (cases)
    assume i: "i = length Vs"
    hence "x = v" using snoc.prems(2) by auto
    thus ?case using xVs find_indices_empty i
      by fastforce
  next
    assume "i ≠ length Vs"
    hence i: "i < length Vs" using snoc.prems(1) by simp
    hence Vsi: "Vs ! i = x" using snoc.prems(2) append_Cons_nth_left by fastforce
    hence "x ≠ v" using snoc.prems(3) i by auto
    thus ?case using snoc.IH[OF i Vsi dist] by simp
  qed
qed auto

lemma finite_convex_hull_iff_convex_hull_list: assumes Vs: "Vs ⊆ carrier_vec n"
  and id': "Vs = set Vsl'"
shows "convex_hull Vs = convex_hull_list Vsl'"
proof -
  have fin: "finite Vs" unfolding id' by auto
  from finite_distinct_list fin obtain Vsl
    where id: "Vs = set Vsl" and dist: "distinct Vsl" by auto
  from Vs id have Vsl: "set Vsl ⊆ carrier_vec n" by auto
  {
    fix c :: "nat ⇒ 'a"
    have "distinct Vsl ⟹(∑x∈set Vsl. sum_list (map c (find_indices x Vsl))) =
                          sum c {0..<length Vsl}"
    proof (induction Vsl rule: rev_induct)
      case (snoc v Vsl)
      let ?coef = "λ x. sum_list (map c (find_indices x (Vsl @ [v])))"
      let ?coef' = "λ x. sum_list (map c (find_indices x Vsl))"
      have dist: "distinct Vsl" using snoc.prems by simp
      have "sum ?coef (set (Vsl @ [v])) = sum_list (map ?coef (Vsl @ [v]))"
        by (rule sum.distinct_set_conv_list[OF snoc.prems, of ?coef])
      also have "… = sum_list (map ?coef Vsl) + ?coef v" by simp
      also have "sum_list (map ?coef Vsl) = sum ?coef (set Vsl)"
        using sum.distinct_set_conv_list[OF dist, of ?coef] by auto
      also have "… = sum ?coef' (set Vsl)"
      proof (intro R.finsum_restrict[of ?coef] restrict_ext, standard)
        fix x
        assume "x ∈ set Vsl"
        then obtain i where i: "i < length Vsl" and x: "x = Vsl ! i"
          using in_set_conv_nth[of x Vsl] by blast
        hence "(Vsl @ [v]) ! i = x" by (simp add: append_Cons_nth_left)
        hence "?coef x = c i"
          using distinct_list_find_indices[OF _ _ snoc.prems] i by fastforce
        also have  "c i = ?coef' x"
          using distinct_list_find_indices[OF i _ dist] x by simp
        finally show "?coef x = ?coef' x" by auto
      qed
      also have "… = sum c {0..<length Vsl}" by (rule snoc.IH[OF dist])
      also have "?coef v = c (length Vsl)"
        using distinct_list_find_indices[OF _ _ snoc.prems, of "length Vsl" v]
          nth_append_length by simp
      finally show ?case using sum.atLeast0_lessThan_Suc by simp
    qed simp
  } note sum_sumlist = this
  {
    fix b
    assume "b ∈ convex_hull_list Vsl"
    then obtain c where b: "lincomb_list c Vsl = b" and c: "(∀ i < length Vsl. c i ≥ 0)"
      and c1: "sum c {0..<length Vsl} = 1"
      unfolding convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def
      by auto
    have "convex_lincomb (mk_coeff Vsl c) Vs b"
      unfolding b[symmetric] convex_lincomb_def nonneg_lincomb_def
      apply (subst lincomb_list_as_lincomb[OF Vsl])
      by (insert c c1, auto simp: id mk_coeff_def dist sum_sumlist intro!: sum_list_nonneg)
    hence "b ∈ convex_hull Vs"
      unfolding convex_hull_def convex_lincomb_def using fin by blast
  }
  moreover
  {
    fix b
    assume "b ∈ convex_hull Vs"
    then obtain c Ws where Ws: "Ws ⊆ Vs" and b: "lincomb c Ws = b"
      and c: "c ` Ws ⊆ {x. x ≥ 0}" and c1: "sum c Ws = 1"
      unfolding convex_hull_def convex_lincomb_def nonneg_lincomb_def by auto
    let ?d = "λ x. if x ∈ Ws then c x else 0"
    have "lincomb ?d Vs = lincomb c Ws + lincomb (λ x. 0) (Vs - Ws)"
      using lincomb_union2[OF _ _ Diff_disjoint[of Ws Vs], of c "λ x. 0"]
        fin Vs Diff_partition[OF Ws] by metis
    also have "lincomb (λ x. 0) (Vs - Ws) = 0v n"
      using lincomb_zero[of "Vs - Ws" "λ x. 0"] Vs by auto
    finally have "lincomb ?d Vs = b" using b lincomb_closed Vs Ws by auto
    moreover have "?d ` Vs ⊆ {t. t ≥ 0}" using c by auto
    moreover have "sum ?d Vs = 1" using  c1 R.extend_sum[OF fin Ws] by auto
    ultimately have "∃ c. convex_lincomb c Vs b"
      unfolding convex_lincomb_def nonneg_lincomb_def by blast
  }
  moreover
  {
    fix b
    assume "∃ c. convex_lincomb c Vs b"
    then obtain c where b: "lincomb c Vs = b" and c: "c ` Vs ⊆ {x. x ≥ 0}"
      and c1: "sum c Vs = 1"
      unfolding convex_lincomb_def nonneg_lincomb_def by auto
    from lincomb_as_lincomb_list_distinct[OF Vsl dist, of c]
    have b: "lincomb_list (λi. c (Vsl ! i)) Vsl = b"
      unfolding b[symmetric] id by simp
    have "1 = sum c (set Vsl)" using c1 id by auto
    also have "… = sum_list (map c Vsl)" by(rule sum.distinct_set_conv_list[OF dist])
    also have "… = sum ((!) (map c Vsl)) {0..<length Vsl}"
      using sum_list_sum_nth length_map by metis
    also have "… = sum (λ i. c (Vsl ! i)) {0..<length Vsl}" by simp
    finally have sum_1: "(∑i = 0..<length Vsl. c (Vsl ! i)) = 1" by simp

    have "∃ c. convex_lincomb_list c Vsl b"
      unfolding convex_lincomb_list_def nonneg_lincomb_list_def
      by (intro exI[of _ "λi. c (Vsl ! i)"] conjI b sum_1)
        (insert c, force simp: set_conv_nth id)
    hence "b ∈ convex_hull_list Vsl" unfolding convex_hull_list_def by auto
  }
  ultimately have "convex_hull Vs = convex_hull_list Vsl" by auto
  also have "convex_hull_list Vsl = convex_hull_list Vsl'"
    using convex_hull_list_eq_set[OF Vsl, of Vsl'] id id' by simp
  finally show ?thesis by simp
qed

definition "convex S = (convex_hull S = S)"

lemma convex_convex_hull: "convex S ⟹ convex_hull S = S"
  unfolding convex_def by auto

lemma convex_hull_convex_hull_listD: assumes A: "A ⊆ carrier_vec n"
  and x: "x ∈ convex_hull A"
shows "∃ as. set as ⊆ A ∧ x ∈ convex_hull_list as"
proof -
  from x[unfolded convex_hull_def]
  obtain X c where finX: "finite X" and XA: "X ⊆ A" and "convex_lincomb c X x" by auto
  hence x: "x ∈ convex_hull X" unfolding convex_hull_def by auto
  from finite_list[OF finX] obtain xs where X: "X = set xs" by auto
  from finite_convex_hull_iff_convex_hull_list[OF _ this] x XA A have x: "x ∈ convex_hull_list xs" by auto
  thus ?thesis using XA unfolding X by auto
qed

lemma convex_hull_convex_sum: assumes A: "A ⊆ carrier_vec n"
  and x: "x ∈ convex_hull A"
  and y: "y ∈ convex_hull A"
  and a: "0 ≤ a" "a ≤ 1"
shows "a ⋅v x + (1 - a) ⋅v y ∈ convex_hull A"
proof -
  from convex_hull_convex_hull_listD[OF A x] obtain xs where xs: "set xs ⊆ A"
    and x: "x ∈ convex_hull_list xs" by auto
  from convex_hull_convex_hull_listD[OF A y] obtain ys where ys: "set ys ⊆ A"
    and y: "y ∈ convex_hull_list ys" by auto
  have fin: "finite (set (xs @ ys))" by auto
  have sub: "set (xs @ ys) ⊆ A" using xs ys by auto
  from convex_hull_list_mono[of "xs @ ys" xs] x sub A have x: "x ∈ convex_hull_list (xs @ ys)" by auto
  from convex_hull_list_mono[of "xs @ ys" ys] y sub A have y: "y ∈ convex_hull_list (xs @ ys)" by auto
  from convex_hull_list_combination[OF _ x y a]
  have "a ⋅v x + (1 - a) ⋅v y ∈ convex_hull_list (xs @ ys)" using sub A by auto
  from finite_convex_hull_iff_convex_hull_list[of _ "xs @ ys"] this sub A
  have "a ⋅v x + (1 - a) ⋅v y ∈ convex_hull (set (xs @ ys))" by auto
  with convex_hull_mono[OF sub]
  show "a ⋅v x + (1 - a) ⋅v y ∈ convex_hull A" by auto
qed

lemma convexI: assumes S: "S ⊆ carrier_vec n"
  and step: "⋀ a x y. x ∈ S ⟹ y ∈ S ⟹ 0 ≤ a ⟹ a ≤ 1 ⟹ a ⋅v x + (1 - a) ⋅v y ∈ S"
shows "convex S"
  unfolding convex_def
proof (standard, standard)
  fix z
  assume "z ∈ convex_hull S"
  from this[unfolded convex_hull_def] obtain W c where "finite W" and WS: "W ⊆ S"
    and "convex_lincomb c W z" by auto
  then show "z ∈ S"
  proof (induct W arbitrary: c z)
    case empty
    thus ?case unfolding convex_lincomb_def by auto
  next
    case (insert w W c z)
    have "convex_lincomb c (insert w W) z" by fact
    hence zl: "z = lincomb c (insert w W)" and nonneg: "⋀ w. w ∈ W ⟹ 0 ≤ c w"
      and cw: "c w ≥ 0"
      and sum: "sum c (insert w W) = 1"
      unfolding convex_lincomb_def nonneg_lincomb_def by auto
    have zl: "z = c w ⋅v w + lincomb c W" unfolding zl
      by (rule lincomb_insert2, insert insert S, auto)
    have sum: "c w + sum c W = 1" unfolding sum[symmetric]
      by (subst sum.insert, insert insert, auto)
    have W: "W ⊆ carrier_vec n" and w: "w ∈ carrier_vec n" using S insert by auto
    show ?case
    proof (cases "sum c W = 0")
      case True
      with nonneg have c0: "⋀ w. w ∈ W ⟹ c w = 0"
        using insert(1) sum_nonneg_eq_0_iff by auto
      with sum have cw: "c w = 1" by auto
      have lin0: "lincomb c W = 0v n"
        by (intro lincomb_zero W, insert c0, auto)
      have "z = w" unfolding zl cw lin0 using w by simp
      with insert(4) show ?thesis by simp
    next
      case False
      have "sum c W ≥ 0" using nonneg by (metis sum_nonneg)
      with False have pos: "sum c W > 0" by auto
      define b where "b = (λ w. inverse (sum c W) * c w)"
      have "convex_lincomb b W (lincomb b W)"
        unfolding convex_lincomb_def nonneg_lincomb_def b_def
      proof (intro conjI refl)
        show "(λw. inverse (sum c W) * c w) ` W ⊆ Collect ((≤) 0)" using nonneg pos by auto
        show "(∑w∈W. inverse (sum c W) * c w) = 1" unfolding sum_distrib_left[symmetric] using False by auto
      qed
      from insert(3)[OF _ this] insert
      have IH: "lincomb b W ∈ S" by auto
      have lin: "lincomb c W = sum c W ⋅v lincomb b W"
        unfolding b_def
        by (subst lincomb_smult[symmetric, OF W], rule lincomb_cong[OF _ W], insert False, auto)
      from sum cw pos have sum: "sum c W = 1 - c w" and cw1: "c w ≤ 1" by auto
      show ?thesis unfolding zl lin unfolding sum
        by (rule step[OF _ IH cw cw1], insert insert, auto)
    qed
  qed
next
  show "S ⊆ convex_hull S" using S by (rule set_in_convex_hull)
qed

lemma convex_hulls_are_convex: assumes "A ⊆ carrier_vec n"
  shows "convex (convex_hull A)"
  by (intro convexI convex_hull_convex_sum convex_hull_carrier assms)

lemma convex_hull_sum: assumes A: "A ⊆ carrier_vec n" and B: "B ⊆ carrier_vec n"
  shows "convex_hull (A + B) = convex_hull A + convex_hull B"
proof
  note cA = convex_hull_carrier[OF A]
  note cB = convex_hull_carrier[OF B]
  have "convex (convex_hull A + convex_hull B)"
  proof (intro convexI sum_carrier_vec convex_hull_carrier A B)
    fix a :: 'a and x1 x2
    assume "x1 ∈ convex_hull A + convex_hull B" "x2 ∈ convex_hull A + convex_hull B"
    then obtain y1 y2 z1 z2 where
      x12: "x1 = y1 + z1" "x2 = y2 + z2" and
      y12: "y1 ∈ convex_hull A" "y2 ∈ convex_hull A" and
      z12: "z1 ∈ convex_hull B" "z2 ∈ convex_hull B"
      unfolding set_plus_def by auto
    from y12 z12 cA cB have carr:
      "y1 ∈ carrier_vec n" "y2 ∈ carrier_vec n"
      "z1 ∈ carrier_vec n" "z2 ∈ carrier_vec n"
      by auto
    assume a: "0 ≤ a" "a ≤ 1"
    have A: "a ⋅v y1 + (1 - a) ⋅v y2 ∈ convex_hull A" using y12 a A by (metis convex_hull_convex_sum)
    have B: "a ⋅v z1 + (1 - a) ⋅v z2 ∈ convex_hull B" using z12 a B by (metis convex_hull_convex_sum)
    have "a ⋅v x1 + (1 - a) ⋅v x2 = (a ⋅v y1 + a ⋅v z1) + ((1 - a) ⋅v y2 + (1 - a) ⋅v z2)" unfolding x12
      using carr by (auto simp: smult_add_distrib_vec)
    also have "… = (a ⋅v y1 + (1 - a) ⋅v y2) + (a ⋅v z1 + (1 - a) ⋅v z2)" using carr
      by (intro eq_vecI, auto)
    finally show "a ⋅v x1 + (1 - a) ⋅v x2 ∈ convex_hull A + convex_hull B"
      using A B by auto
  qed
  from convex_convex_hull[OF this]
  have id: "convex_hull (convex_hull A + convex_hull B) = convex_hull A + convex_hull B" .
  show "convex_hull (A + B) ⊆ convex_hull A + convex_hull B"
    by (subst id[symmetric], rule convex_hull_mono[OF set_plus_mono2]; intro set_in_convex_hull A B)
  show "convex_hull A + convex_hull B ⊆ convex_hull (A + B)"
  proof
    fix x
    assume "x ∈ convex_hull A + convex_hull B"
    then obtain y z where x: "x = y + z" and y: "y ∈ convex_hull A" and z: "z ∈ convex_hull B"
      by (auto simp: set_plus_def)
    from convex_hull_convex_hull_listD[OF A y] obtain ys where ysA: "set ys ⊆ A" and
      y: "y ∈ convex_hull_list ys" by auto
    from convex_hull_convex_hull_listD[OF B z] obtain zs where zsB: "set zs ⊆ B" and
      z: "z ∈ convex_hull_list zs" by auto
    from y[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def]
    obtain c where yid: "y = lincomb_list c ys"
      and conv_c: "(∀i<length ys. 0 ≤ c i) ∧ sum c {0..<length ys} = 1"
      by auto
    from z[unfolded convex_hull_list_def convex_lincomb_list_def nonneg_lincomb_list_def]
    obtain d where zid: "z = lincomb_list d zs"
      and conv_d: "(∀i<length zs. 0 ≤ d i) ∧ sum d {0..<length zs} = 1"
      by auto
    from ysA A have ys: "set ys ⊆ carrier_vec n" by auto
    from zsB B have zs: "set zs ⊆ carrier_vec n" by auto
    have [intro, simp]: "lincomb_list x ys ∈ carrier_vec n" for x using lincomb_list_carrier[OF ys] .
    have [intro, simp]: "lincomb_list x zs ∈ carrier_vec n" for x using lincomb_list_carrier[OF zs] .
    have dim[simp]: "dim_vec (lincomb_list d zs) = n" by auto
    from yid have y: "y ∈ carrier_vec n" by auto
    from zid have z: "z ∈ carrier_vec n" by auto
    {
      fix x
      assume "x ∈ set (map ((+) y) zs)"
      then obtain z where "x = y + z" and "z ∈ set zs" by auto
      then obtain j where j: "j < length zs" and x: "x = y + zs ! j" unfolding set_conv_nth by auto
      hence mem: "zs ! j ∈ set zs" by auto
      hence zsj: "zs ! j ∈ carrier_vec n" using zs by auto
      let ?list = "(map (λ y. y + zs ! j) ys)"
      let ?set = "set ?list"
      have set: "?set ⊆ carrier_vec n" using ys A zsj by auto
      have lin_map: "lincomb_list c ?list ∈ carrier_vec n"
        by (intro lincomb_list_carrier[OF set])
      have "y + (zs ! j) = lincomb_list c ?list"
        unfolding yid using zsj lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ ys]
        by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_c)
      hence "convex_lincomb_list c ?list (y + (zs ! j))"
        unfolding convex_lincomb_list_def nonneg_lincomb_list_def using conv_c by auto
      hence "y + (zs ! j) ∈ convex_hull_list ?list" unfolding convex_hull_list_def by auto
      with finite_convex_hull_iff_convex_hull_list[OF set refl]
      have "(y + zs ! j) ∈ convex_hull ?set" by auto
      also have "… ⊆ convex_hull (A + B)"
        by (rule convex_hull_mono, insert mem ys ysA zsB, force simp: set_plus_def)
      finally have "x ∈ convex_hull (A + B)" unfolding x .
    } note step1 = this
    {
      let ?list = "map ((+) y) zs"
      let ?set = "set ?list"
      have set: "?set ⊆ carrier_vec n" using zs B y by auto
      have lin_map: "lincomb_list d ?list ∈ carrier_vec n"
        by (intro lincomb_list_carrier[OF set])
      have [simp]: "i < n ⟹ (∑j = 0..<length zs. d j * (y + zs ! j) $ i) =
        (∑j = 0..<length zs. d j * (y $ i + zs ! j $ i))" for i
        by (rule sum.cong, insert zs[unfolded set_conv_nth] y, auto)
      have "y + z = lincomb_list d ?list"
        unfolding zid using y zs lin_map lincomb_list_index[OF _ set] lincomb_list_index[OF _ zs]
          set lincomb_list_carrier[OF zs, of d] zs[unfolded set_conv_nth]
        by (intro eq_vecI, auto simp: field_simps sum_distrib_right[symmetric] conv_d)
      hence "convex_lincomb_list d ?list x" unfolding x
        unfolding convex_lincomb_list_def nonneg_lincomb_list_def using conv_d by auto
      hence "x ∈ convex_hull_list ?list" unfolding convex_hull_list_def by auto
      with finite_convex_hull_iff_convex_hull_list[OF set refl]
      have "x ∈ convex_hull ?set" by auto
      also have "… ⊆ convex_hull (convex_hull (A + B))"
        by (rule convex_hull_mono, insert step1, auto)
      also have "… = convex_hull (A + B)"
        by (rule convex_convex_hull[OF convex_hulls_are_convex], intro sum_carrier_vec A B)
      finally show "x ∈ convex_hull (A + B)" .
    }
  qed
qed

lemma convex_hull_in_cone:
  "convex_hull C ⊆ cone C"
  unfolding convex_hull_def cone_def convex_lincomb_def finite_cone_def by auto

lemma convex_cone:
  assumes C: "C ⊆ carrier_vec n"
  shows "convex (cone C)"
  unfolding convex_def
  using convex_hull_in_cone set_in_convex_hull[OF cone_carrier[OF C]] cone_cone[OF C]
  by blast

end
end