Theory Maximum_Segment_Sum

section ‹Maximum Segment Sum›

theory Maximum_Segment_Sum
  imports Main
begin

text ‹The \emph{maximum segment sum} problem is to compute, given a list of numbers,
the largest of the sums of the contiguous segments of that list. It is also known
as the \emph{maximum sum subarray} problem and has been considered many times in the literature;
the Wikipedia article
\href{https://en.wikipedia.org/wiki/Maximum\_subarray\_problem}{Maximum subarray problem} is a good starting point.

We assume that the elements of the list are not necessarily numbers but just elements
of some linearly ordered group.›

class linordered_group_add = linorder + group_add +
assumes add_left_mono: "a ≤ b ⟹ c + a ≤ c + b"
assumes add_right_mono: "a ≤ b ⟹ a + c ≤ b + c"
begin

lemma max_add_distrib_left: "max y z + x = max (y+x) (z+x)"
by (metis add_right_mono max.absorb_iff1 max_def)

lemma max_add_distrib_right: "x + max y z = max (x+y) (x+z)"
by (metis add_left_mono max.absorb1 max.cobounded2 max_def)

subsection ‹Naive Solution›

fun mss_rec_naive_aux :: "'a list ⇒ 'a" where
  "mss_rec_naive_aux [] = 0"
| "mss_rec_naive_aux (x#xs) = max 0 (x + mss_rec_naive_aux xs)"

fun mss_rec_naive :: "'a list ⇒ 'a" where
  "mss_rec_naive [] = 0"
| "mss_rec_naive (x#xs) = max (mss_rec_naive_aux (x#xs)) (mss_rec_naive xs)"

definition fronts :: "'a list ⇒ 'a list set" where
  "fronts xs = {as. ∃bs. xs = as @ bs}"

definition "front_sums xs ≡ sum_list ` fronts xs"

lemma fronts_cons: "fronts (x#xs) = ((#) x) ` fronts xs ∪ {[]}" (is "?l = ?r")
proof
  show "?l ⊆ ?r"
  proof
    fix as assume "as ∈ ?l"
    then show "as ∈ ?r" by (cases as) (auto simp: fronts_def)
  qed
  show "?r ⊆ ?l" unfolding fronts_def by auto
qed

lemma front_sums_cons: "front_sums (x#xs) = (+) x ` front_sums xs ∪ {0}"
proof -
  have "sum_list ` ((#) x) ` fronts xs = (+) x ` front_sums xs" unfolding front_sums_def by force
  then show ?thesis by (simp add: front_sums_def fronts_cons)
qed

lemma finite_fronts: "finite (fronts xs)"
  by (induction xs) (simp add: fronts_def, simp add: fronts_cons)

lemma finite_front_sums: "finite (front_sums xs)"
  using front_sums_def finite_fronts by simp

lemma front_sums_not_empty: "front_sums xs ≠ {}"
  unfolding front_sums_def fronts_def using image_iff by fastforce

lemma max_front_sum: "Max (front_sums (x#xs)) = max 0 (x + Max (front_sums xs))"
using finite_front_sums front_sums_not_empty
by (auto simp add: front_sums_cons hom_Max_commute max_add_distrib_right)

lemma mss_rec_naive_aux_front_sums: "mss_rec_naive_aux xs = Max (front_sums xs)"
by (induction xs) (simp add: front_sums_def fronts_def, auto simp: max_front_sum)

lemma front_sums: "front_sums xs = {s. ∃as bs. xs = as @ bs ∧ s = sum_list as}"
unfolding front_sums_def fronts_def by auto

lemma mss_rec_naive_aux: "mss_rec_naive_aux xs = Max {s. ∃as bs. xs = as @ bs ∧ s = sum_list as}"
using front_sums mss_rec_naive_aux_front_sums by simp
  

definition mids :: "'a list ⇒ 'a list set" where
  "mids xs ≡ {bs. ∃as cs. xs = as @ bs @ cs}"

definition "mid_sums xs ≡ sum_list ` mids xs"

lemma fronts_mids: "bs ∈ fronts xs ⟹ bs ∈ mids xs"
unfolding fronts_def mids_def by auto

lemma mids_mids_cons: "bs ∈ mids xs ⟹ bs ∈ mids (x#xs)"
proof-
  fix bs assume "bs ∈ mids xs"
  then obtain as cs where "xs = as @ bs @ cs" unfolding mids_def by blast
  then have "x # xs = (x#as) @ bs @ cs" by simp
  then show "bs ∈ mids (x#xs)" unfolding mids_def by blast
qed

lemma mids_cons: "mids (x#xs) = fronts (x#xs) ∪ mids xs" (is "?l = ?r")
proof
  show "?l ⊆ ?r"
  proof
    fix bs assume "bs ∈ ?l"
    then obtain as cs where as_bs_cs: "(x#xs) = as @ bs @ cs" unfolding mids_def by blast
    then show "bs ∈ ?r"
    proof (cases as)
      case Nil
      then have "bs ∈ fronts (x#xs)" by (simp add: fronts_def as_bs_cs)
      then show ?thesis by simp
    next
      case (Cons a as')
      then have "xs = as' @ bs @ cs" using as_bs_cs by simp
      then show ?thesis unfolding mids_def by auto
    qed
  qed
  show "?r ⊆ ?l" using fronts_mids mids_mids_cons by auto
qed

lemma mid_sums_cons: "mid_sums (x#xs) = front_sums (x#xs) ∪ mid_sums xs"
  unfolding mid_sums_def by (auto simp: mids_cons front_sums_def)

lemma finite_mids: "finite (mids xs)"
  by (induction xs) (simp add: mids_def, simp add: mids_cons finite_fronts)

lemma finite_mid_sums: "finite (mid_sums xs)"
  by (simp add: mid_sums_def finite_mids)

lemma mid_sums_not_empty: "mid_sums xs ≠ {}"
  unfolding mid_sums_def mids_def by blast

lemma max_mid_sums_cons: "Max (mid_sums (x#xs)) = max (Max (front_sums (x#xs))) (Max (mid_sums xs))"
  by (auto simp: mid_sums_cons Max_Un finite_front_sums finite_mid_sums front_sums_not_empty mid_sums_not_empty)

lemma mss_rec_naive_max_mid_sum: "mss_rec_naive xs = Max (mid_sums xs)"
  by (induction xs) (simp add: mid_sums_def mids_def, auto simp: max_mid_sums_cons mss_rec_naive_aux front_sums)

lemma mid_sums: "mid_sums xs = {s. ∃as bs cs. xs = as @ bs @ cs ∧ s = sum_list bs}"
  by (auto simp: mid_sums_def mids_def)

theorem mss_rec_naive: "mss_rec_naive xs = Max {s. ∃as bs cs. xs = as @ bs @ cs ∧ s = sum_list bs}"
  unfolding mss_rec_naive_max_mid_sum mid_sums by simp


subsection ‹Kadane's Algorithms›

fun kadane :: "'a list ⇒ 'a ⇒ 'a ⇒ 'a" where
  "kadane [] cur m = m"
| "kadane (x#xs) cur m =
    (let cur' = max (cur + x) x in
      kadane xs cur' (max m cur'))"

definition "mss_kadane xs ≡ kadane xs 0 0"

lemma Max_front_sums_geq_0: "Max (front_sums xs) ≥ 0"
proof-
  have "[] ∈ fronts xs" unfolding fronts_def by blast
  then have "0 ∈ front_sums xs" unfolding front_sums_def by force
  then show ?thesis using finite_front_sums Max_ge by simp
qed

lemma Max_mid_sums_geq_0: "Max (mid_sums xs) ≥ 0"
proof-
  have "0 ∈ mid_sums xs" unfolding mid_sums_def mids_def by force
  then show ?thesis using finite_mid_sums Max_ge by simp
qed

lemma kadane: "m ≥ cur ⟹ m ≥ 0 ⟹ kadane xs cur m = max m (max (cur + Max (front_sums xs)) (Max (mid_sums xs)))"
proof (induction xs cur m rule: kadane.induct)
  case (1 cur m)
  then show ?case unfolding front_sums_def fronts_def mid_sums_def mids_def by auto
next
  case (2 x xs cur m)
  then show ?case
    apply (auto simp: max_front_sum max_mid_sums_cons Let_def)
    by (smt (verit, ccfv_threshold) Max_front_sums_geq_0 add_assoc add_0_right max.assoc max.coboundedI1 max.left_commute max.orderE max_add_distrib_left max_add_distrib_right)
qed

lemma Max_front_sums_leq_Max_mid_sums: "Max (front_sums xs) ≤ Max (mid_sums xs)"
proof-
  have "front_sums xs ⊆ mid_sums xs" unfolding front_sums_def mid_sums_def using fronts_mids subset_iff by blast
  then show ?thesis using front_sums_not_empty finite_mid_sums Max_mono by blast
qed

lemma mss_kadane_mid_sums: "mss_kadane xs = Max (mid_sums xs)"
  unfolding mss_kadane_def using kadane Max_mid_sums_geq_0 Max_front_sums_leq_Max_mid_sums by auto

theorem mss_kadane: "mss_kadane xs = Max {s. ∃as bs cs. xs = as @ bs @ cs ∧ s = sum_list bs}"
  using mss_kadane_mid_sums mid_sums by auto

end

end