Theory Submodular_Base

theory Submodular_Base
  imports Complex_Main
begin

lemma finite_has_maximal_on:
  fixes g :: "'a ⇒ 'b::linorder"
  assumes fin: "finite A"
    and nonempty: "A ≠ {}"
  shows "∃x∈A. ∀y∈A. g y ≤ g x" using arg_max_on_def[of g A]
proof -
  have fin_image: "finite (g ` A)"
    using fin by simp
  have nonempty_image: "g ` A ≠ {}"
    using nonempty by auto

  have max_in_image: "Max (g ` A) ∈ g ` A"
    using Max_in[OF fin_image nonempty_image] .

  then obtain x where xA: "x ∈ A" and x_eq: "g x = Max (g ` A)"
    by auto

  have "∀y∈A. g y ≤ g x"
    by (simp add: fin_image x_eq)

  then show ?thesis
    using xA by blast
qed

text ‹
  The main development is carried out in a single locale for normalized
  monotone submodular functions, which is the setting needed for the
  cardinality-constrained greedy approximation guarantees below. Some
  auxiliary facts hold under weaker assumptions; for this entry we keep them
  in the same locale to maintain a compact and uniform development.
›

locale Submodular_Func =
  fixes V :: "'a set" and f :: "'a set ⇒ real"
  assumes finite_V: "finite V"
      and monotone_f: "⋀S T. S ⊆ T ⟹ T ⊆ V ⟹ f S ≤ f T"
      and submodular_f:
        "⋀S T. S ⊆ V ⟹ T ⊆ V ⟹ f (S ∪ T) + f (S ∩ T) ≤ f S + f T"
      and f_empty: "f {} = 0"
begin

text ‹Marginal gain of adding a single element to a set.›
definition gain :: "'a set ⇒ 'a ⇒ real" where
  "gain S e = f (S ∪ {e}) - f S"

lemma f_nonneg:
  assumes "S ⊆ V"
  shows "0 ≤ f S"
proof -
  have "{} ⊆ S" by auto
  from monotone_f[OF this assms] have "f {} ≤ f S" .
  thus ?thesis by (simp add: f_empty)
qed

lemma monotone_on_PowV:
  shows "monotone_on (Pow V) (⊆) (≤) f"
  unfolding monotone_on_def
  using monotone_f by auto

lemma gain_nonneg:
  assumes "S ⊆ V" and "x ∈ V - S"
  shows "0 ≤ gain S x"
proof -
  have "S ⊆ S ∪ {x}" by auto
  moreover from assms have "S ∪ {x} ⊆ V" by auto
  ultimately have "f S ≤ f (S ∪ {x})" using monotone_f by auto
  thus ?thesis by (simp add: gain_def)
qed

text ‹Diminishing returns for single-element marginal gains.›
lemma gain_decreasing:
  assumes "S ⊆ T" "T ⊆ V" "x ∈ V" "x ∉ T"
  shows "gain S x ≥ gain T x"
proof -
  have Sx_sub_V: "insert x S ⊆ V"
    using assms by auto

  have subm:
    "f (insert x (S ∪ T)) + f (insert x S ∩ T) ≤ f (insert x S) + f T"
    using submodular_f[OF Sx_sub_V assms(2)]
    by simp

  have inter_eq: "insert x S ∩ T = S"
    using assms by auto

  have union_eq: "insert x (S ∪ T) = insert x T"
    using assms by auto

  from subm have "f S + f (insert x T) ≤ f T + f (insert x S)"
    by (simp add: inter_eq union_eq)

  hence "f (insert x S) - f S ≥ f (insert x T) - f T"
    by linarith

  thus ?thesis
    by (simp add: gain_def)
qed

text ‹Set-valued diminishing returns.›
lemma gain_decreasing_set:
  assumes "S ⊆ T" "T ⊆ V" "A ⊆ V"
  shows "f (S ∪ A) - f S ≥ f (T ∪ A) - f T"
proof -
  have SUA_subV: "S ∪ A ⊆ V"
    using assms by auto

  have subm:
    "f ((S ∪ A) ∪ T) + f ((S ∪ A) ∩ T) ≤ f (S ∪ A) + f T"
    using submodular_f[OF SUA_subV assms(2)] .

  have union_eq: "(S ∪ A) ∪ T = T ∪ A"
    using assms by auto

  have S_sub_inter: "S ⊆ (S ∪ A) ∩ T"
    using assms by auto

  have inter_subV: "(S ∪ A) ∩ T ⊆ V"
    using assms by auto

  have mono_inter: "f S ≤ f ((S ∪ A) ∩ T)"
    using monotone_f[OF S_sub_inter inter_subV] .

  have "f (T ∪ A) + f ((S ∪ A) ∩ T) ≤ f (S ∪ A) + f T"
    using subm by (simp add: union_eq)
  then have "f (T ∪ A) + f S ≤ f (S ∪ A) + f T"
    using mono_inter by linarith
  then show ?thesis
    by linarith
qed

end

text ‹
  This entry treats cardinality-constrained monotone submodular maximization.
  Other constraint systems, such as matroid or knapsack constraints, are
  outside the scope of the present development.
›

locale Cardinality_Constraint = Submodular_Func +
  fixes k :: nat
  assumes k_le_cardV: "k ≤ card V"
begin

definition feasible :: "'a set ⇒ bool" where
  "feasible S ⟷ S ⊆ V ∧ card S ≤ k"

lemma feasibleI:
  assumes "S ⊆ V" "card S ≤ k"
  shows "feasible S"
  using assms unfolding feasible_def by auto

lemma feasibleD:
  assumes "feasible S"
  shows "S ⊆ V" "card S ≤ k"
  using assms unfolding feasible_def by auto

lemma feasible_empty[simp]: "feasible {}"
  unfolding feasible_def by auto

lemma feasible_family_nonempty: "Collect feasible ≠ {}"
proof -
  have "∃S. feasible S"
  proof
    show "feasible {}" by (rule feasible_empty)
  qed
  then show ?thesis by auto
qed

lemma finite_feasible_family: "finite {S. feasible S}"
proof -
  have "{S. feasible S} ⊆ Pow V"
    by (auto simp: feasible_def)
  moreover have "finite (Pow V)"
    using finite_V by simp
  ultimately show ?thesis
    by (rule finite_subset)
qed

subsection ‹Optimal feasible sets›

text ‹
  We select a canonical optimal feasible set ‹OPT_set› using Hilbert choice
  and define ‹OPT_k› as its value. These are problem-level objects for the
  cardinality-constrained maximization problem, independent of any particular
  greedy implementation.
›

definition OPT_set :: "'a set" where
  "OPT_set =
     (SOME X. feasible X ∧ (∀Y. feasible Y ⟶ f Y ≤ f X))"

lemma exists_max_feasible:
  "∃X. feasible X ∧ (∀Y. feasible Y ⟶ f Y ≤ f X)"
proof -
  from finite_has_maximal_on[OF finite_feasible_family feasible_family_nonempty]
  obtain X where X_feas: "X ∈ Collect feasible"
    and X_max: "∀Y ∈ Collect feasible. f Y ≤ f X"
    by blast
  have "feasible X ∧ (∀Y. feasible Y ⟶ f Y ≤ f X)"
    using X_feas X_max by auto
  thus ?thesis ..
qed

lemma OPT_set_props:
  shows OPT_set_in: "feasible OPT_set"
    and OPT_set_max: "∀Y. feasible Y ⟶ f Y ≤ f OPT_set"
proof -
  from exists_max_feasible
  obtain X where X_in: "feasible X"
    and X_max: "∀Y. feasible Y ⟶ f Y ≤ f X"
    by blast
  then have ex_spec:
    "∃X. feasible X ∧ (∀Y. feasible Y ⟶ f Y ≤ f X)"
    by blast
  from someI_ex[OF ex_spec]
  have "feasible OPT_set ∧ (∀Y. feasible Y ⟶ f Y ≤ f OPT_set)"
    unfolding OPT_set_def by simp
  then show "feasible OPT_set"
    and "∀Y. feasible Y ⟶ f Y ≤ f OPT_set"
    by auto
qed

definition OPT_k :: real where
  "OPT_k = f OPT_set"

lemma exists_opt_set:
  "∃X. feasible X ∧ f X = OPT_k"
proof -
  have "feasible OPT_set"
    by (rule OPT_set_in)
  moreover have "f OPT_set = OPT_k"
    unfolding OPT_k_def by simp
  ultimately show ?thesis
    by blast
qed

lemma OPT_k_upper_bound:
  assumes "feasible S"
  shows "f S ≤ OPT_k"
proof -
  have "∀Y. feasible Y ⟶ f Y ≤ f OPT_set"
    by (rule OPT_set_max)
  with assms have "f S ≤ f OPT_set"
    by auto
  thus ?thesis
    unfolding OPT_k_def by simp
qed

subsection ‹Basic non-emptiness facts›

lemma nonempty_candidates:
  assumes "S ⊆ V" "card S < k"
  shows "V - S ≠ {}"
proof
  assume "V - S = {}"
  hence "V ⊆ S" by auto
  with assms(1) have "V = S" by auto
  with assms(2) k_le_cardV show False by simp
qed

lemma nonempty_gap:
  assumes "S ⊆ V" "Opt ⊆ V" "f S < f Opt"
  shows "Opt - S ≠ {}"
proof
  assume "Opt - S = {}"
  hence "Opt ⊆ S" by auto
  with assms(1,2) have "f Opt ≤ f S"
    using monotone_f by auto
  with assms(3) show False by linarith
qed

lemma OPT_k_nonneg: "0 ≤ OPT_k"
proof -
  have "feasible {}"
    by (rule feasible_empty)
  then have "f {} ≤ OPT_k"
    by (rule OPT_k_upper_bound)
  thus ?thesis
    by (simp add: f_empty)
qed

text ‹Submodular telescoping: sum of marginals upper-bounds the joint gain.›
lemma submod_sum_upper:
  assumes "finite A" "A ⊆ V" "S ⊆ V" "A ∩ S = {}"
  shows "f (S ∪ A) - f S ≤ (∑x∈A. gain S x)"
  using assms
proof (induction rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert a A)
  from insert.hyps have a_notin: "a ∉ A" and finA: "finite A" by auto

  from insert.prems have S_sub: "S ⊆ V" by auto
  from insert.prems have ins_subV: "insert a A ⊆ V" by auto
  from insert.prems have ins_disj: "insert a A ∩ S = {}" by auto

  have A_sub: "A ⊆ V" using ins_subV by auto
  have aV   : "a ∈ V"  using ins_subV by auto
  have disjA: "A ∩ S = {}" using ins_disj by auto
  have a_notS: "a ∉ S" using ins_disj by auto

  have step:
    "f (S ∪ insert a A) - f S
     = (f ((S ∪ A) ∪ {a}) - f (S ∪ A)) + (f (S ∪ A) - f S)"
    by (simp add: insert_commute Un_assoc)

  have SSUA: "S ⊆ S ∪ A" by auto
  have SUA_subV: "S ∪ A ⊆ V" using S_sub A_sub by auto
  have a_notin_SUA: "a ∉ S ∪ A" using a_notS a_notin by auto
  have dec:
    "f ((S ∪ A) ∪ {a}) - f (S ∪ A) ≤ gain S a"
    using gain_decreasing[OF SSUA SUA_subV aV a_notin_SUA]
    by (simp add: gain_def)

  from insert.IH[OF A_sub S_sub disjA]
  have IH: "f (S ∪ A) - f S ≤ (∑x∈A. gain S x)" .

  have "(f ((S ∪ A) ∪ {a}) - f (S ∪ A)) + (f (S ∪ A) - f S)
        ≤ gain S a + (∑x∈A. gain S x)"
    using dec IH by linarith
  thus ?case
    by (simp add: step insert_commute finA a_notin)
qed

text ‹
  Average marginal bound against any candidate set ‹Opt ⊆ V› with
  ‹card Opt ≤ k›: if ‹S ⊆ V› and ‹card S < k›, then there exists an
  element ‹e ∈ V - S› such that
  ‹gain S e ≥ (f Opt - f S) / real k›.
›
lemma marginal_gain_lower_bound:
  fixes Opt S :: "'a set"
  assumes S_sub: "S ⊆ V"
    and O_sub: "Opt ⊆ V"
    and cardS_lt_k: "card S < k"
    and cardO_le_k: "card Opt ≤ k"
  shows "∃e∈V - S. gain S e ≥ (f Opt - f S) / real k"
proof -
  have finV: "finite V" by (rule finite_V)
  have k_pos: "0 < k" using cardS_lt_k by (simp add: not_less)

  consider (le) "f Opt ≤ f S" | (gt) "f S < f Opt" by linarith
  then show ?thesis
  proof cases
    case le
    have VS_ne: "V - S ≠ {}"
      using nonempty_candidates[OF S_sub cardS_lt_k] .

    then obtain e where eVS: "e ∈ V - S" by blast
    hence ge0: "0 ≤ gain S e" using S_sub gain_nonneg by auto

    moreover have "(f Opt - f S) / real k ≤ 0"
    proof -
      have "f Opt - f S ≤ 0" using le by linarith
      thus ?thesis
        using k_pos by (simp add: divide_nonpos_pos)
    qed

    ultimately have "(f Opt - f S) / real k ≤ gain S e"
      by linarith

    thus ?thesis
      using eVS by (intro bexI[of _ e]) auto
  next
    case gt
    have OS_ne: "Opt - S ≠ {}"
      using nonempty_gap[OF S_sub O_sub gt] .

    have finOS: "finite (Opt - S)"
      using finV O_sub by (meson Diff_subset finite_subset)
    have OS_subV: "Opt - S ⊆ V" using O_sub by auto
    have disj: "(Opt - S) ∩ S = {}" by auto
    have finO: "finite Opt" using finV O_sub finite_subset by blast

    have step_sum:
      "f (S ∪ (Opt - S)) - f S ≤ (∑x∈Opt - S. gain S x)"
      using submod_sum_upper[OF finOS OS_subV S_sub disj] .

    have SUO_subV: "S ∪ Opt ⊆ V" using S_sub O_sub by auto
    have sum_upper: "f Opt - f S ≤ (∑x∈Opt - S. gain S x)"
    proof -
      have "f Opt ≤ f (S ∪ Opt)"
        using monotone_f[rule_format, of Opt "S ∪ Opt"] SUO_subV by auto
      then have "f Opt - f S ≤ f (S ∪ Opt) - f S" by linarith
      also have "S ∪ Opt = S ∪ (Opt - S)" by auto
      also have "f (S ∪ (Opt - S)) - f S
                   ≤ (∑x∈Opt - S. gain S x)"
        using step_sum .
      finally show ?thesis .
    qed

    obtain e where e_in: "e ∈ Opt - S"
      and e_max: "∀y∈Opt - S. gain S y ≤ gain S e"
      using finite_has_maximal_on[OF finOS OS_ne, of "gain S"]
      by blast

    have "(∑x∈Opt - S. gain S x) ≤ (∑x∈Opt - S. gain S e)"
      using e_max by (intro sum_mono) simp_all
    also have "... = real (card (Opt - S)) * gain S e"
      by simp
    finally have sum_le_card_max:
      "(∑x∈Opt - S. gain S x) ≤ real (card (Opt - S)) * gain S e" .

    have base: "f Opt - f S ≤ real (card (Opt - S)) * gain S e"
      using sum_upper sum_le_card_max by linarith

    have cardOS_le_k: "card (Opt - S) ≤ k"
    proof -
      have "card (Opt - S) ≤ card Opt"
        using finO Diff_subset by (rule card_mono)
      also have "... ≤ k" using cardO_le_k .
      finally show ?thesis .
    qed

    have eVS: "e ∈ V - S" using e_in O_sub by auto
    have ge0: "0 ≤ gain S e" using S_sub eVS gain_nonneg by auto

    have "real (card (Opt - S)) * gain S e ≤ real k * gain S e"
      using cardOS_le_k ge0 by (simp add: mult_right_mono)
    hence main_ineq: "f Opt - f S ≤ real k * gain S e"
      using base by linarith

    have "gain S e ≥ (f Opt - f S) / real k"
      using main_ineq k_pos by (simp add: mult.commute pos_divide_le_eq)
    thus ?thesis using eVS by blast
  qed
qed

end

end