Theory Greedy_Submodular_Construct

theory Greedy_Submodular_Construct
  imports "../Core/Submodular_Base"
begin

section ‹Greedy construction›

text ‹
  This theory sets up the greedy construction for monotone submodular
  maximization under a cardinality constraint. The locale ‹Greedy_Setup›
  fixes a finite ground set ‹V›, a budget ‹k›, and a normalized monotone
  submodular set function ‹f›. The greedy sequence starts from the empty set
  and repeatedly adds an element of maximum marginal gain, with ties broken
  by the abstract oracle.
›

subsection ‹Preliminaries on finite maximizers›

text ‹Finite arg-max via the standard maximality predicate.›

(* We rely on the standard predicate is_arg_max from the library.
   The following lemma establishes existence on finite domains. *)
lemma finite_is_arg_max_in:
  fixes g :: "'a ⇒ 'b::linorder"
  assumes fin: "finite A" and ne: "A ≠ {}"
  shows "∃x∈A. is_arg_max g (λx. x ∈ A) x"
proof -
  have img_fin: "finite (g ` A)"
    using fin by simp
  have img_ne: "g ` A ≠ {}"
    using ne by auto

  let ?M = "Max (g ` A)"
  have M_in: "?M ∈ g ` A"
    using Max_in[OF img_fin img_ne] .
  then obtain x where xA: "x ∈ A" and gx: "g x = ?M"
    by auto

    have no_better: "¬ (∃y. y ∈ A ∧ g y > g x)"
    proof
      assume ex: "∃y. y ∈ A ∧ g y > g x"
      then obtain y where yA: "y ∈ A" and gy: "g y > g x" by auto

      have "g y ≤ Max (g ` A)"
        using Max_ge_iff[OF img_fin img_ne] yA by auto
      hence gy_le_gx: "g y ≤ g x"
        by (simp add: gx)

      have gx_lt_gy: "g x < g y" using gy by simp
      show False
        using gx_lt_gy gy_le_gx by (meson less_le_not_le)
    qed

  have "is_arg_max g (λz. z ∈ A) x"
    unfolding is_arg_max_def
    using xA no_better by auto
  thus ?thesis
    using xA by blast
qed

lemma is_arg_maxD_le:
  fixes f :: "'b ⇒ 'a::linorder"
  assumes "is_arg_max f P x" "P y"
  shows "f y ≤ f x"
  using assms
  by (simp add: is_arg_max_linorder)

text ‹
  Abstract setup for the greedy algorithm:
  a finite ground set V, a budget k, and a non-negative monotone
  submodular function f with f {} = 0.

  This theory focuses on the greedy construction and basic structural
  properties, without yet proving approximation guarantees.
›

subsection ‹Hilbert-choice arg-max oracle for marginal gain›

context Submodular_Func
begin

definition argmax_gain_some :: "'a set ⇒ 'a set ⇒ 'a" where
  "argmax_gain_some S A =
     (SOME x. x ∈ A ∧ is_arg_max (gain S) (λy. y ∈ A) x)"

lemma argmax_gain_some_mem:
  assumes fin: "finite A" and ne: "A ≠ {}"
  shows "argmax_gain_some S A ∈ A"
proof -
  have exB: "∃x∈A. is_arg_max (gain S) (λy. y ∈ A) x"
    using finite_is_arg_max_in[OF fin ne] .

  have ex: "∃x. x ∈ A ∧ is_arg_max (gain S) (λy. y ∈ A) x"
    using exB by auto

  show ?thesis
    unfolding argmax_gain_some_def
    using someI_ex[OF ex] by blast
qed

lemma argmax_gain_some_max:
  assumes fin: "finite A" and ne: "A ≠ {}" and yA: "y ∈ A"
  shows "gain S y ≤ gain S (argmax_gain_some S A)"
proof -
  have exB: "∃x∈A. is_arg_max (gain S) (λz. z ∈ A) x"
    using finite_is_arg_max_in[OF fin ne] .

  have ex: "∃x. x ∈ A ∧ is_arg_max (gain S) (λz. z ∈ A) x"
    using exB by auto

  have chosen:
    "is_arg_max (gain S) (λz. z ∈ A) (argmax_gain_some S A)"
    unfolding argmax_gain_some_def
    using someI_ex[OF ex] by blast

  show ?thesis
    using is_arg_maxD_le[OF chosen yA] .
qed

end

locale Greedy_Setup = Cardinality_Constraint V f k
  for V :: "'a set" and f :: "'a set ⇒ real" and k :: nat +
  fixes argmax_gain :: "'a set ⇒ 'a set ⇒ 'a"
  assumes argmax_gain_mem:
    "finite A ⟹ A ≠ {} ⟹ argmax_gain S A ∈ A"
  assumes argmax_gain_max:
    "finite A ⟹ A ≠ {} ⟹ ∀y∈A. gain S y ≤ gain S (argmax_gain S A)"
begin

text ‹
  Greedy construction: start from ‹{}› and, as long as there are remaining
  elements, add one with maximum marginal gain.
›
fun greedy_set :: "nat ⇒ 'a set" where
  "greedy_set 0 = {}"
| "greedy_set (Suc i) =
     (let S = greedy_set i in
      if V - S = {} then S else insert (argmax_gain S (V - S)) S)"

text ‹Greedy sets are always subsets of the ground set ‹V›.›
lemma greedy_subset_V: "greedy_set i ⊆ V"
proof (induction i)
  case 0
  show ?case by simp
next
  case (Suc i)
  have IH: "greedy_set i ⊆ V" by fact
  show ?case
  proof (cases "V - greedy_set i = {}")
    case True
    have "greedy_set (Suc i) = greedy_set i"
      using True by (simp add: Let_def)
    thus ?thesis
      using IH by simp

  next
    case False
    have finA: "finite (V - greedy_set i)"
      using finite_V by simp
    have inA:
      "argmax_gain (greedy_set i) (V - greedy_set i) ∈ V - greedy_set i"
      using argmax_gain_mem[OF finA False] .

    hence inV: "argmax_gain (greedy_set i) (V - greedy_set i) ∈ V"
      by simp

    from IH inV
    have "greedy_set i ∪ {argmax_gain (greedy_set i) (V - greedy_set i)} ⊆ V"
      by auto
    with False show ?thesis
      by (simp add: Let_def)
  qed
qed


text ‹If a genuinely new element is inserted, the cardinality increases by one.›
lemma greedy_card_step:
  assumes ne: "V - greedy_set i ≠ {}"
  shows   "card (greedy_set (Suc i)) = card (greedy_set i) + 1"
proof -
  let ?S = "greedy_set i"
  let ?A = "V - ?S"
  let ?x = "argmax_gain ?S ?A"

  have finS: "finite ?S"
    using greedy_subset_V finite_V
    by (meson finite_subset)

  have finA: "finite ?A"
    using finite_V by simp

  have x_in_A: "?x ∈ ?A"
    using argmax_gain_mem[OF finA ne] .
  hence x_notin_S: "?x ∉ ?S"
    by simp

  have suc_def:
    "greedy_set (Suc i) =
       (let S = ?S in
        if V ⊆ S then S else insert (argmax_gain S (V - S)) S)"
    by simp

  from ne have "greedy_set (Suc i) = ?S ∪ {?x}"
    unfolding suc_def by (simp add: Let_def)
  hence "greedy_set (Suc i) = insert ?x ?S"
    by simp

  thus ?thesis
    using finS x_notin_S by simp
qed


text ‹If the remainder is empty, the greedy set stays unchanged.›
lemma greedy_card_idle:
  assumes "V - greedy_set i = {}"
  shows   "card (greedy_set (Suc i)) = card (greedy_set i)"
  using assms by (simp add: Let_def)

text ‹
  State transition: when the remainder is non-empty, ‹Sᵢ› evolves by adding
  the arg-max element.
›
lemma state_transition_nonempty:
  assumes "0 < i" and "V - greedy_set (i - 1) ≠ {}"
  shows   "greedy_set i =
           greedy_set (i - 1)
           ∪ {argmax_gain (greedy_set (i - 1)) (V - greedy_set (i - 1))}"
proof -
  obtain j where ij: "i = Suc j"
    using assms(1) by (cases i) auto

  from assms(2) ij have rem_ne: "V - greedy_set j ≠ {}"
    by simp

  have def_suc:
    "greedy_set (Suc j) =
       (let S = greedy_set j in
        if V ⊆ S then S else insert (argmax_gain S (V - S)) S)"
    by simp

  from rem_ne have
    "greedy_set (Suc j) =
       greedy_set j ∪ {argmax_gain (greedy_set j) (V - greedy_set j)}"
    by (simp add: def_suc Let_def)

  with ij show ?thesis
    by simp
qed


text ‹At most one new element is added in each greedy step.›
lemma card_greedy_le_i: "card (greedy_set i) ≤ i"
proof (induction i)
  case 0
  show ?case by simp
next
  case (Suc i)
  show ?case
  proof (cases "V - greedy_set i = {}")
    case True
    have "card (greedy_set (Suc i)) = card (greedy_set i)"
      using True by (rule greedy_card_idle)
    with Suc.IH show ?thesis by simp
  next
    case False
    have "card (greedy_set (Suc i)) = card (greedy_set i) + 1"
      using False by (rule greedy_card_step)
    with Suc.IH show ?thesis by simp
  qed
qed

text ‹If ‹i ≤ k› then ‹card (greedy_set i) ≤ k› (used later in the gap bound).›
lemma card_greedy_le_k:
  assumes "i ≤ k"
  shows   "card (greedy_set i) ≤ k"
  using card_greedy_le_i assms by (meson le_trans)

text ‹
  If ‹card (greedy_set t) < card V›, then the remainder ‹V - greedy_set t›
  is non-empty.
›
lemma remainder_nonempty_if_card_ltV:
  assumes "card (greedy_set t) < card V"
  shows   "V - greedy_set t ≠ {}"
proof
  assume "V - greedy_set t = {}"
  then have vsub: "V ⊆ greedy_set t" by auto
  have ssub: "greedy_set t ⊆ V" by (rule greedy_subset_V)
  from ssub vsub have "greedy_set t = V" by (rule subset_antisym)
  with assms show False by simp
qed

text ‹
  Under ‹k ≤ card V›, the greedy transition up to step ‹k› always adds a new
  element.
›
lemma state_transition_upto_k:
  assumes "0 < i" "i ≤ k"
  shows   "greedy_set i =
           greedy_set (i - 1)
           ∪ {argmax_gain (greedy_set (i - 1)) (V - greedy_set (i - 1))}"
proof -
  have "card (greedy_set (i - 1)) ≤ i - 1"
    using card_greedy_le_i by simp
  also have "... < k"
    using assms(1,2) by simp
  also have "... ≤ card V"
    using k_le_cardV by simp
  finally have ltV: "card (greedy_set (i - 1)) < card V" .

  have rem_ne: "V - greedy_set (i - 1) ≠ {}"
    using remainder_nonempty_if_card_ltV[OF ltV] .

  show ?thesis
    by (rule state_transition_nonempty[OF assms(1) rem_ne])
qed

text ‹Intermediate greedy states as a list ‹[S₀,…,Sₙ]›.›
definition greedy_sequence :: "nat ⇒ 'a set list" where
  "greedy_sequence n = map greedy_set [0..<Suc n]"

text ‹Indexing lemma for the sequence representation.›
lemma greedy_sequence_nth[simp]:
  assumes "i ≤ n"
  shows   "greedy_sequence n ! i = greedy_set i"
proof -
  have i_lt: "i < Suc n" using assms by simp
  have "(map greedy_set [0..<Suc n]) ! i = greedy_set ([0..<Suc n] ! i)"
    using i_lt by (simp only: nth_map length_upt)
  also have "... = greedy_set i"
    using i_lt by (simp only: nth_upt add_0_left)
  finally show ?thesis
    by (simp only: greedy_sequence_def)
qed

text ‹Every greedy state is finite.›
lemma greedy_set_finite [simp]: "finite (greedy_set i)"
  using greedy_subset_V finite_V by (meson finite_subset)

text ‹One-step monotonicity: ‹Sᵢ ⊆ Sᵢ₊₁›.›
lemma greedy_mono_Suc: "greedy_set i ⊆ greedy_set (Suc i)"
proof (cases "V - greedy_set i = {}")
  case True
  then show ?thesis by (simp add: Let_def)
next
  case False
  then show ?thesis by (auto simp: Let_def)
qed

text ‹Chain monotonicity: if ‹i ≤ j› then ‹Sᵢ ⊆ Sⱼ›.›
lemma greedy_chain_mono:
  assumes "i ≤ j"
  shows   "greedy_set i ⊆ greedy_set j"
using assms
proof (induction j arbitrary: i)
  case 0
  then show ?case
    by simp
next
  case (Suc j i)
  show ?case
  proof (cases "i ≤ j")
    case True
    with Suc.IH have "greedy_set i ⊆ greedy_set j" .
    also have "... ⊆ greedy_set (Suc j)"
      by (rule greedy_mono_Suc)
    finally show ?thesis .
  next
    case False
    hence "i = Suc j" using Suc.prems by simp
    thus ?thesis by simp
  qed
qed

text ‹Cardinality is non-decreasing along the greedy sequence.›
lemma greedy_card_mono:
  "i ≤ j ⟹ card (greedy_set i) ≤ card (greedy_set j)"
  by (meson greedy_chain_mono greedy_set_finite finite_subset card_mono)

text ‹
  A compact cardinality bound: ‹card Sᵢ ≤ min i (card V)› for all ‹i›.
›
lemma greedy_card_min:
  "card (greedy_set i) ≤ min i (card V)"
proof -
  have A1: "card (greedy_set i) ≤ i"
    by (rule card_greedy_le_i)
  have A2: "card (greedy_set i) ≤ card V"
  proof -
    have fin: "finite V" using finite_V .
    have sub: "greedy_set i ⊆ V" by (rule greedy_subset_V)
    from fin sub show ?thesis by (rule card_mono)
  qed
  show ?thesis
  proof (cases "i ≤ card V")
    case True
    then show ?thesis using A1 by (simp add: min_def)
  next
    case False
    then show ?thesis using A2 by (simp add: min_def)
  qed
qed

text ‹Length and endpoints of the intermediate sequence.›
lemma greedy_sequence_length [simp]:
  "length (greedy_sequence n) = Suc n"
  by (simp add: greedy_sequence_def)

lemma greedy_sequence_0 [simp]:
  "greedy_sequence n ! 0 = {}"
  using greedy_sequence_nth[of 0 n] by simp

lemma greedy_sequence_last [simp]:
  "greedy_sequence n ! n = greedy_set n"
  using greedy_sequence_nth by simp

text ‹
  At a non-empty remainder, the chosen element is new and lies in ‹V - S›.
›
lemma chosen_in_remainder_nonempty:
  assumes rem_ne: "V - greedy_set i ≠ {}"
  defines x_def:  "x ≡ argmax_gain (greedy_set i) (V - greedy_set i)"
  shows   "x ∈ V - greedy_set i" "x ∉ greedy_set i"
proof -
  have finA: "finite (V - greedy_set i)"
    using finite_V by simp
  have xinA:
    "argmax_gain (greedy_set i) (V - greedy_set i) ∈ V - greedy_set i"
    using argmax_gain_mem[OF finA rem_ne] .
  show "x ∈ V - greedy_set i"
    unfolding x_def by (rule xinA)
  then show "x ∉ greedy_set i" by simp
qed

text ‹
  At a non-empty step, ‹greedy_set (Suc i)› is obtained by inserting the
  arg-max element into ‹greedy_set i›. This is often useful in counting
  arguments.
›

lemma greedy_increment_nonempty[simp]:
  assumes rem_ne: "V - greedy_set i ≠ {}"
  shows   "greedy_set (Suc i) =
           insert (argmax_gain (greedy_set i) (V - greedy_set i)) (greedy_set i)"
proof -
  have not_subset: "¬ V ⊆ greedy_set i"
    using rem_ne by (simp add: Diff_eq_empty_iff)

  have def:
    "greedy_set (Suc i) =
       (let S = greedy_set i in
        if V ⊆ S then S else insert (argmax_gain S (V - S)) S)"
    by simp

  show ?thesis
    unfolding def
    using not_subset
    by (simp add: Let_def)
qed

text ‹
  One-step update of the objective value along the greedy sequence.
›
lemma greedy_step_f_eq:
  assumes "V - greedy_set i ≠ {}"
  shows
    "f (greedy_set (Suc i)) =
       f (greedy_set i) +
       gain (greedy_set i)
         (argmax_gain (greedy_set i) (V - greedy_set i))"
proof -
  let ?S = "greedy_set i"
  let ?x = "argmax_gain ?S (V - ?S)"

  have gs_Suc:
    "greedy_set (Suc i) =
       insert (argmax_gain (greedy_set i) (V - greedy_set i)) (greedy_set i)"
    using assms by (rule greedy_increment_nonempty)

  hence "greedy_set (Suc i) = ?S ∪ {?x}"
    by simp

  hence "f (greedy_set (Suc i)) = f (?S ∪ {?x})"
    by simp
  also have "… = f ?S + gain ?S ?x"
    by (simp add: gain_def)
  finally show ?thesis
    by simp
qed

end

context Cardinality_Constraint
begin

interpretation Greedy_Concrete: Greedy_Setup V f k argmax_gain_some
proof
  fix S :: "'a set" and A :: "'a set"
  assume fin: "finite A" and ne: "A ≠ {}"
  show "argmax_gain_some S A ∈ A"
    using argmax_gain_some_mem[OF fin ne] .
next
  fix S :: "'a set" and A :: "'a set"
  assume fin: "finite A" and ne: "A ≠ {}"
  show "∀y∈A. gain S y ≤ gain S (argmax_gain_some S A)"
  proof
    fix y
    assume yA: "y ∈ A"
    show "gain S y ≤ gain S (argmax_gain_some S A)"
      using argmax_gain_some_max[OF fin ne yA] .
  qed
qed

end

end