Maximum subarray problem

DefinitionBeing the maximum subarray sum#✓fully proved

For a list \(L\) over an additive monoid \(\alpha\) with a linear order, an element \(m \in \alpha\) is the maximum subarray sum of \(L\) when some nonempty contiguous sublist of \(L\) has sum \(m\) and every nonempty contiguous sublist of \(L\) has sum at most \(m\).

def IsMaxSubarraySum (xs : List α) (m : α) : Prop :=
  (∃ ys, ys <:+: xs ∧ ys ≠ [] ∧ ys.sum = m) ∧ ∀ ys, ys <:+: xs → ys ≠ [] → ys.sum ≤ m

Used by 10

Used byMaximum subarray sum of a concatenation · Maximum subarray sum after appending an element · Kadane's algorithm returns an attained sum · Invariant of Kadane's scan · Divide and conquer agrees with Kadane's algorithm · Correctness of divide-and-conquer maximum subarray · Correctness of Kadane's algorithm · A list with a maximum subarray sum is nonempty · Kadane's algorithm bounds every nonempty run · Uniqueness of the maximum subarray sum

DefinitionBeing the maximum suffix sum#✓fully proved

For a list \(L\) over an additive monoid \(\alpha\) with a linear order, an element \(e \in \alpha\) is the maximum suffix sum of \(L\) when some nonempty suffix of \(L\) has sum \(e\) and every nonempty suffix of \(L\) has sum at most \(e\). A nonempty suffix is a contiguous run ending at the last element of \(L\).

Kadane's scan maintains its first accumulator as the maximum suffix sum of the elements read so far.

def IsMaxSuffixSum (xs : List α) (e : α) : Prop :=
  (∃ ys, ys <:+ xs ∧ ys ≠ [] ∧ ys.sum = e) ∧ ∀ ys, ys <:+ xs → ys ≠ [] → ys.sum ≤ e

Used by 7

Used byMaximum subarray sum of a concatenation · Maximum suffix sum after appending an element · Maximum subarray sum after appending an element · Invariant of Kadane's scan · Correctness of divide-and-conquer maximum subarray · Correctness of Kadane's algorithm · Correctness of the suffix scan

DefinitionKadane's scan#✓fully proved

Given accumulators \(e, b\) in an additive monoid \(\alpha\) with a linear order, the scan over the empty list returns \(b\) at cost \(0\). Over a list with first element \(x\) and remaining elements \(L\), it sets \(e' = \max(x, e + x)\) and returns the result of the scan of \(L\) from the accumulators \(e'\) and \(\max(b, e')\), at cost \(3\) plus the cost of that scan.

Here \(e\) is the best sum of a nonempty run ending at the last element read and \(b\) is the best sum of any nonempty run read so far.

def kadaneScan (ending best : α) : List α → TimeM ℕ α
  | [] => pure best
  | x :: xs => do
      ✓[3]
      let ending' := max x (ending + x)
      kadaneScan ending' (max best ending') xs

Used by 5

Used byInvariant of Kadane's scan · Cost of Kadane's scan · Kadane's algorithm · Divide and conquer agrees with Kadane's algorithm · Correctness of Kadane's algorithm

DefinitionKadane's algorithm#✓fully proved

Let \(\alpha\) be a linearly ordered type with an additive monoid structure. On the empty list, Kadane's algorithm returns no value. On a list \(x_1, x_2, \dots, x_n\) of elements of \(\alpha\) with \(n \ge 1\), it sets \(e = b = x_1\); then for \(i = 2, \dots, n\) in turn it replaces \(e\) by \(\max(x_i, e + x_i)\) and then \(b\) by \(\max(b, e)\); finally it returns \(b\). Each of the steps \(i = 2, \dots, n\) is charged three operations, and nothing else is charged.

When \(u \le v\) implies \(u + w \le v + w\) for all \(u, v, w \in \alpha\), after each step \(e\) is the largest sum of a nonempty contiguous run ending at the element just read, and \(b\) is the largest sum of a nonempty contiguous run among the elements read so far.

def maxSubarraySum : List α → TimeM ℕ (Option α)
  | [] => pure none
  | x :: xs => some <$> kadaneScan x x xs

Uses 1 · Used by 5

Statement usesKadane's scan

Used byKadane's algorithm returns an attained sum · Divide and conquer agrees with Kadane's algorithm · Correctness of Kadane's algorithm · Cost of Kadane's algorithm · Kadane's algorithm bounds every nonempty run

TheoremCost of Kadane's scan#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order. For all accumulators \(e, b \in \alpha\) and every list \(L\) over \(\alpha\) of length \(n\), Kadane's scan of \(L\) from the accumulators \(e\) and \(b\) costs exactly \(3n\).

@[simp]
theorem kadaneScan_time (ending best : α) (xs : List α) :
    (kadaneScan ending best xs).time = 3 * xs.length

Uses 1 · Used by 1

Statement usesKadane's scan

Used byCost of Kadane's algorithm

TheoremCost of Kadane's algorithm#✓fully proved

Over an additive monoid \(\alpha\) with a linear order, Kadane's algorithm on a list of length \(n \ge 1\) costs exactly \(3(n - 1)\) operations, and on the empty list it costs \(0\).

@[simp]
theorem maxSubarraySum_time (xs : List α) :
    (maxSubarraySum xs).time = 3 * (xs.length - 1)

Uses 2

Statement usesKadane's algorithm

Proof usesCost of Kadane's scan

TheoremA list with a maximum subarray sum is nonempty#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order. If an element \(m \in \alpha\) is the maximum subarray sum of a list \(L\) over \(\alpha\), then \(L\) is nonempty.

theorem IsMaxSubarraySum.ne_nil {xs : List α} {m : α} (h : IsMaxSubarraySum xs m) :
    xs ≠ []

Uses 1 · Used by 2

Statement usesBeing the maximum subarray sum

Used byCorrectness of divide-and-conquer maximum subarray · Correctness of Kadane's algorithm

TheoremUniqueness of the maximum subarray sum#✓fully proved

Let \(\alpha\) be a linearly ordered type with an additive monoid structure, and let \(L\) be a list over \(\alpha\). If \(m, m' \in \alpha\) are both maximum subarray sums of \(L\), meaning that each is the sum of some nonempty contiguous run of \(L\) and bounds the sum of every nonempty contiguous run of \(L\), then \(m = m'\).

theorem IsMaxSubarraySum.unique {xs : List α} {m m' : α} (h : IsMaxSubarraySum xs m)
    (h' : IsMaxSubarraySum xs m') : m = m'

Uses 1 · Used by 2

Statement usesBeing the maximum subarray sum

Used byCorrectness of divide-and-conquer maximum subarray · Correctness of Kadane's algorithm

TheoremMaximum suffix sum after appending an element#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(a \le b\) implies \(a + c \le b + c\). If \(e\) is the maximum sum of a nonempty suffix of a list \(p\) over \(\alpha\), then for every \(x \in \alpha\) the maximum sum of a nonempty suffix of the list obtained by appending \(x\) to \(p\) is \(\max(x, e + x)\).

Such a suffix is either \([x]\) alone or a nonempty suffix of \(p\) followed by \(x\).

theorem IsMaxSuffixSum.concat [AddRightMono α] {pre : List α} {e : α}
    (h : IsMaxSuffixSum pre e) (x : α) : IsMaxSuffixSum (pre ++ [x]) (max x (e + x))

Uses 1 · Used by 2

Statement usesBeing the maximum suffix sum

Used byMaximum subarray sum after appending an element · Invariant of Kadane's scan

TheoremMaximum subarray sum after appending an element#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(a \le b\) implies \(a + c \le b + c\). Let \(p\) be a list over \(\alpha\), let \(e\) be the maximum sum of a nonempty suffix of \(p\), and let \(b\) be the maximum sum of a nonempty contiguous sublist of \(p\). Then for every \(x \in \alpha\), the maximum sum of a nonempty contiguous sublist of the list obtained by appending \(x\) to \(p\) is \(\max(b, \max(x, e + x))\).

theorem IsMaxSubarraySum.concat [AddRightMono α] {pre : List α} {e b : α}
    (he : IsMaxSuffixSum pre e) (hb : IsMaxSubarraySum pre b) (x : α) :
    IsMaxSubarraySum (pre ++ [x]) (max b (max x (e + x)))

Uses 3 · Used by 1

Statement usesBeing the maximum subarray sum · Being the maximum suffix sum

Proof usesMaximum suffix sum after appending an element

Used byInvariant of Kadane's scan

TheoremInvariant of Kadane's scan#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(a \le b\) implies \(a + c \le b + c\). Let \(p\) be a list over \(\alpha\), let \(e\) be the maximum sum of a nonempty suffix of \(p\), and let \(b\) be the maximum sum of a nonempty contiguous sublist of \(p\). Then for every list \(r\) over \(\alpha\), the value that Kadane's scan from the accumulators \(e\) and \(b\) returns on \(r\) is the maximum sum of a nonempty contiguous sublist of the list \(p\) followed by \(r\).

theorem kadaneScan_ret [AddRightMono α] {pre : List α} {ending best : α}
    (he : IsMaxSuffixSum pre ending) (hb : IsMaxSubarraySum pre best) (rest : List α) :
    IsMaxSubarraySum (pre ++ rest) (kadaneScan ending best rest).ret

Uses 5 · Used by 1

Statement usesBeing the maximum subarray sum · Being the maximum suffix sum · Kadane's scan

Proof usesMaximum subarray sum after appending an element · Maximum suffix sum after appending an element

Used byCorrectness of Kadane's algorithm

TheoremCorrectness of Kadane's algorithm#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(a \le b\) implies \(a + c \le b + c\). For every list \(L\) over \(\alpha\) and every \(m \in \alpha\), Kadane's algorithm returns \(m\) on \(L\) if and only if \(m\) is the maximum sum of a nonempty contiguous sublist of \(L\): some nonempty contiguous sublist of \(L\) has sum \(m\), and every nonempty contiguous sublist of \(L\) has sum at most \(m\).

theorem maxSubarraySum_ret_eq_some_iff [AddRightMono α] (xs : List α) (m : α) :
    (maxSubarraySum xs).ret = some m ↔ IsMaxSubarraySum xs m

Uses 7 · Used by 3

Statement usesBeing the maximum subarray sum · Kadane's algorithm

Proof usesA list with a maximum subarray sum is nonempty · Uniqueness of the maximum subarray sum · Being the maximum suffix sum · Kadane's scan · Invariant of Kadane's scan

Used byKadane's algorithm returns an attained sum · Divide and conquer agrees with Kadane's algorithm · Kadane's algorithm bounds every nonempty run

TheoremKadane's algorithm bounds every nonempty run#✓fully proved

Let \(\alpha\) be a linearly ordered type with an additive monoid structure in which \(b \le c\) implies \(b + a \le c + a\). If Kadane's algorithm returns the value \(m\) on a list \(L\) over \(\alpha\), then every nonempty contiguous run of \(L\) has sum at most \(m\).

theorem sum_le_of_maxSubarraySum [AddRightMono α] {xs ys : List α} {m : α}
    (hm : (maxSubarraySum xs).ret = some m) (hys : ys <:+: xs) (hne : ys ≠ []) :
    ys.sum ≤ m

Uses 3

Statement usesKadane's algorithm

Proof usesBeing the maximum subarray sum · Correctness of Kadane's algorithm

TheoremKadane's algorithm returns an attained sum#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(a \le b\) implies \(a + c \le b + c\). If Kadane's algorithm returns a value \(m\) on a list \(L\) over \(\alpha\), then some nonempty contiguous sublist of \(L\) has sum \(m\).

theorem exists_sum_eq_of_maxSubarraySum [AddRightMono α] {xs : List α} {m : α}
    (hm : (maxSubarraySum xs).ret = some m) :
    ∃ ys, ys <:+: xs ∧ ys ≠ [] ∧ ys.sum = m

Uses 3

Statement usesKadane's algorithm

Proof usesBeing the maximum subarray sum · Correctness of Kadane's algorithm

DefinitionMaximum prefix sum#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order. For a list \(xs\) over \(\alpha\) and \(p \in \alpha\), \(p\) is the maximum prefix sum of \(xs\) when some nonempty prefix of \(xs\) has sum \(p\) and every nonempty prefix of \(xs\) has sum at most \(p\).

def IsMaxPrefixSum (xs : List α) (p : α) : Prop :=
  (∃ ys, ys <+: xs ∧ ys ≠ [] ∧ ys.sum = p) ∧ ∀ ys, ys <+: xs → ys ≠ [] → ys.sum ≤ p

Used by 2

Used byMaximum subarray sum of a concatenation · Correctness of divide-and-conquer maximum subarray

DefinitionRight-to-left suffix scan#✓fully proved

Let \(\alpha\) be an additive monoid carrying a linear order. For a nonempty list \(x_1, \dots, x_n\) in \(\alpha\), this timed computation returns the pair \((x_1 + \dots + x_n, s)\), where \(s\) is the maximum of the suffix sums \(x_i + \dots + x_n\) over \(1 \le i \le n\). It scans from the right: the step for \(x_i\) forms \(x_i + (x_{i+1} + \dots + x_n)\) and takes its maximum with the best suffix sum found so far, at a cost of \(2\) time units per element, \(2n\) in total. On the empty list it returns \((0, 0)\) at no cost.

def suffixScan : List α → TimeM ℕ (α × α)
  | [] => pure (0, 0)
  | [x] => do
      ✓[2]
      pure (x, x)
  | x :: y :: rest => do
      let r ← suffixScan (y :: rest)
      ✓[2]
      let total := x + r.1
      pure (total, max r.2 total)

Used by 4

Used byDivide-and-conquer core of maximum subarray · Correctness of divide-and-conquer maximum subarray · Running time of divide-and-conquer maximum subarray · Correctness of the suffix scan

DefinitionPrefix scan#✓fully proved

For lists over an additive monoid with a linear order, the prefix scan returns \(0\) on the empty list at no cost, and \(x\) on a one-element list \([x]\) at cost \(2\). On a list with first element \(x\) and nonempty tail \(t\) it returns \(\max(x, x + b)\), where \(b\) is the prefix scan of \(t\), at the cost of the scan of \(t\) plus \(2\).

When \(u \le v\) implies \(a + u \le a + v\), the value on a nonempty list is the maximum sum of a nonempty prefix of the list.

def prefixScan : List α → TimeM ℕ α
  | [] => pure 0
  | [x] => do
      ✓[2]
      pure x
  | x :: y :: rest => do
      let b ← prefixScan (y :: rest)
      ✓[2]
      pure (max x (x + b))

Used by 3

Used byDivide-and-conquer core of maximum subarray · Correctness of divide-and-conquer maximum subarray · Running time of divide-and-conquer maximum subarray

DefinitionDivide-and-conquer core of maximum subarray#✓fully proved

For lists over an additive monoid with a linear order: on the empty list it returns \(0\) and on a one-element list \([x]\) it returns \(x\), both at no cost. On a list of length \(n \ge 2\), let \(m = \lfloor n/2 \rfloor\), let \(l\) and \(r\) be its results on the first \(m\) elements and on the remaining \(n - m\) elements, let \(s\) be the best nonempty suffix sum of the first \(m\) elements as computed by the suffix scan, and let \(p\) be the prefix scan of the remaining elements. It returns \(\max(\max(l, r), s + p)\), at the cost of these four computations plus \(3\).

Cslib.Algorithms.Lean.TimeM.maxSubarrayDC · 16 lines

def maxSubarrayDC : List α → TimeM ℕ α
  | [] => pure 0
  | [x] => pure x
  | x :: y :: rest => do
      let xs := x :: y :: rest
      let m := xs.length / 2
      let l ← maxSubarrayDC (xs.take m)
      let r ← maxSubarrayDC (xs.drop m)
      let s ← suffixScan (xs.take m)
      let p ← prefixScan (xs.drop m)
      ✓[3]
      pure (max (max l r) (s.2 + p))
termination_by xs => xs.length
decreasing_by
  all_goals simp only [List.length_take, List.length_drop, List.length_cons]
  all_goals omega

Uses 2 · Used by 3

Statement usesPrefix scan · Right-to-left suffix scan

Used byDivide-and-conquer maximum subarray · Correctness of divide-and-conquer maximum subarray · Running time of divide-and-conquer maximum subarray

DefinitionDivide-and-conquer maximum subarray#✓fully proved

The CLRS algorithm FIND-MAXIMUM-SUBARRAY over an additive monoid with a linear order, returning only the sum. On the empty list it returns no value, at no cost. On a nonempty list it returns the value of the divide-and-conquer core on that list, at the same cost; the core splits a list of length \(n \ge 2\) after its first \(\lfloor n/2 \rfloor\) elements and returns the largest of its results on the two parts and the best nonempty suffix sum of the first part plus the prefix scan of the second part.

When \(b \le c\) implies \(a + b \le a + c\) and \(b + a \le c + a\), the value returned on a nonempty list is the maximum sum of a nonempty contiguous run of the list.

def maxSubarraySumDC (xs : List α) : TimeM ℕ (Option α) :=
  match xs with
  | [] => pure none
  | _ :: _ => some <$> maxSubarrayDC xs

Uses 1 · Used by 3

Statement usesDivide-and-conquer core of maximum subarray

Used byDivide and conquer agrees with Kadane's algorithm · Correctness of divide-and-conquer maximum subarray · Running time of divide-and-conquer maximum subarray

DefinitionCost recurrence of divide-and-conquer maximum subarray#✓fully proved

The function \(T : \mathbb{N} \to \mathbb{N}\) given by \(T(n) = 0\) for \(n \le 1\) and \(T(n) = T(\lfloor n/2 \rfloor) + T(n - \lfloor n/2 \rfloor) + 2n + 3\) for \(n \ge 2\).

def maxSubarrayDCCost (n : ℕ) : ℕ :=
  if n ≤ 1 then 0 else maxSubarrayDCCost (n / 2) + maxSubarrayDCCost (n - n / 2) + 2 * n + 3
termination_by n
decreasing_by all_goals omega

Used by 1

Used byRunning time of divide-and-conquer maximum subarray

TheoremRunning time of divide-and-conquer maximum subarray#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order. On a nonempty list over \(\alpha\) of length \(n\), the cost \(T\) of the divide-and-conquer maximum subarray algorithm satisfies \(T + 3 \le 2n\lceil \log_2 n \rceil + 3n\), that is, \(T \le 2n\lceil \log_2 n \rceil + 3(n - 1)\).

theorem maxSubarraySumDC_time_le (xs : List α) (hxs : xs ≠ []) :
    (maxSubarraySumDC xs).time + 3 ≤ 2 * xs.length * Nat.clog 2 xs.length + 3 * xs.length

Uses 5

Statement usesDivide-and-conquer maximum subarray

Proof usesDivide-and-conquer core of maximum subarray · Cost recurrence of divide-and-conquer maximum subarray · Prefix scan · Right-to-left suffix scan

TheoremCorrectness of the suffix scan#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order. For every nonempty list \(xs\) over \(\alpha\), the suffix scan of \(xs\) returns a pair whose first component is the sum of \(xs\) and whose second component is the maximum sum of a nonempty suffix of \(xs\).

theorem suffixScan_spec : ∀ xs : List α, xs ≠ [] →
    (suffixScan xs).ret.1 = xs.sum ∧ IsMaxSuffixSum xs (suffixScan xs).ret.2

Uses 2 · Used by 1

Statement usesBeing the maximum suffix sum · Right-to-left suffix scan

Used byCorrectness of divide-and-conquer maximum subarray

TheoremMaximum subarray sum of a concatenation#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(b \le c\) implies \(a + b \le a + c\) and \(b + a \le c + a\), and let \(L\) and \(R\) be lists over \(\alpha\). Suppose that \(l\) is the maximum sum of a nonempty contiguous run of \(L\), \(r\) is the maximum sum of a nonempty contiguous run of \(R\), \(s\) is the maximum sum of a nonempty suffix of \(L\), and \(p\) is the maximum sum of a nonempty prefix of \(R\). Then \(\max(\max(l, r), s + p)\) is the maximum sum of a nonempty contiguous run of the concatenation of \(L\) followed by \(R\).

theorem IsMaxSubarraySum.append [AddLeftMono α] [AddRightMono α] {L R : List α} {l r s p : α}
    (hl : IsMaxSubarraySum L l) (hr : IsMaxSubarraySum R r) (hs : IsMaxSuffixSum L s)
    (hp : IsMaxPrefixSum R p) : IsMaxSubarraySum (L ++ R) (max (max l r) (s + p))

Uses 3 · Used by 1

Statement usesMaximum prefix sum · Being the maximum subarray sum · Being the maximum suffix sum

Used byCorrectness of divide-and-conquer maximum subarray

TheoremCorrectness of divide-and-conquer maximum subarray#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(b \le c\) implies \(a + b \le a + c\) and \(b + a \le c + a\). For every list \(xs\) over \(\alpha\) and every \(m \in \alpha\), the divide-and-conquer algorithm returns \(m\) on \(xs\) if and only if \(m\) is the maximum sum of a nonempty contiguous run of \(xs\).

theorem maxSubarraySumDC_ret_eq_some_iff [AddLeftMono α] [AddRightMono α] (xs : List α)
    (m : α) : (maxSubarraySumDC xs).ret = some m ↔ IsMaxSubarraySum xs m

Uses 11 · Used by 1

Statement usesBeing the maximum subarray sum · Divide-and-conquer maximum subarray

Proof usesMaximum prefix sum · Maximum subarray sum of a concatenation · A list with a maximum subarray sum is nonempty · Uniqueness of the maximum subarray sum · Being the maximum suffix sum · Divide-and-conquer core of maximum subarray · Prefix scan · Right-to-left suffix scan · Correctness of the suffix scan

Used byDivide and conquer agrees with Kadane's algorithm

TheoremDivide and conquer agrees with Kadane's algorithm#✓fully proved

Let \(\alpha\) be an additive monoid with a linear order such that \(b \le c\) implies \(a + b \le a + c\) and \(b + a \le c + a\). For every list \(xs\) over \(\alpha\), the divide-and-conquer maximum subarray algorithm and Kadane's algorithm return the same result on \(xs\).

theorem maxSubarraySumDC_eq_maxSubarraySum [AddLeftMono α] [AddRightMono α] (xs : List α) :
    (maxSubarraySumDC xs).ret = (maxSubarraySum xs).ret

Uses 6

Statement usesKadane's algorithm · Divide-and-conquer maximum subarray

Proof usesBeing the maximum subarray sum · Kadane's scan · Correctness of divide-and-conquer maximum subarray · Correctness of Kadane's algorithm

25 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.