Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

We are given an array `a` of integers with `n` elments and are interested in the *maximum sum subsequence* of `a`: the maximum value of any contiguous subsequence of values in `a`. [Kadane's algorithm](https://en.wikipedia.org/wiki/Maximum_subarray_problem) provides a simple solution to compute this value in just one pass over `a`. Here is the algorithm formulated in Isabelle/HOL: ``` f i s m = ( if i ≥ n then m else let s' = (if s > 0 then s + a i else a i) in f (i + 1) s' (max s' m) ) ``` Your task is to prove this algorithm correct. **Hint**: The key to understanding the algorithm is to consider the following definition: ``` s j = Max {∑k=i..j. a k | i ≤ j} ``` The maximum sum subsequence is just the maximum of all `s j` for `j ≤ n`. Try to prove a recursion for `s`! NB: no partial credits given for this problem.

Resources

Definitions File

theory Defs
imports Main
begin

context
fixes a :: "nat \<Rightarrow> int" \<comment> \<open>The input array\<close>
fixes n :: nat \<comment> \<open>The length of @{term a}\<close>
assumes n_gt_0: "n > 0"
begin

definition
"max_sum_subseq = Max {\<Sum>k=i..j. a k | i j. i \<le> j \<and> j < n}"

function f where
"f i s m = (
if i \<ge> n then m
else
let s' = (if s > 0 then s + a i else a i) in
f (i + 1) s' (max s' m)
)
"
by auto
termination
by (relation "measure (\<lambda>(i, _, _). n - i)"; simp)

definition
"sum_upto j = Max {\<Sum>k=i..j. a k | i. i \<le> j}"

end

end

Template File

theory Submission
imports Defs
begin

context
fixes a :: "nat \<Rightarrow> int" \<comment> \<open>The input array\<close>
fixes n :: nat \<comment> \<open>The length of @{term a}\<close>
assumes n_gt_0: "n > 0"
begin

definition max_sum_subseq where
"max_sum_subseq = Max {\<Sum>k=i..j. a k | i j. i \<le> j \<and> j < n}"

function f where
"f i s m = (
if i \<ge> n then m
else
let s' = (if s > 0 then s + a i else a i) in
f (i + 1) s' (max s' m)
)
"
by auto
termination
by (relation "measure (\<lambda>(i, _, _). n - i)"; simp)

theorem max_sum_subseq_compute':
"max_sum_subseq = f 1 (a 0) (a 0)"
sorry

lemma f_eq:
"Defs.f a n i x y = Submission.f a n i x y" if "n > 0"
by (induction i x y rule: f.induct) (simp add: f.simps that)

end

theorem max_sum_subseq_compute:
"n > 0 \<Longrightarrow> Defs.max_sum_subseq a n = Defs.f a n 1 (a 0) (a 0)"
using max_sum_subseq_compute' by (simp only: Defs.max_sum_subseq_def max_sum_subseq_def f_eq)

end

Check File

theory Check
imports Submission
begin

theorem max_sum_subseq_compute:
"n > 0 \<Longrightarrow> Defs.max_sum_subseq a n = Defs.f a n 1 (a 0) (a 0)"
by (rule max_sum_subseq_compute)

end

Definitions File

import data.finset.intervals
import order.conditionally_complete_lattice
import data.real.basic
/-!
Maximum Sum Subsequence

Given a finite sequence of real numbers.
The goal is to show that the given algorithm below computes the maximal sum of any (consecutive)
subsequence.
-/

open_locale big_operators

variables
(a : ℕ → ℝ) -- the input array
(n : ℕ) -- the length of the array
(h : 0 < n)

/-- The function `∑ k in Ico i j, a k` maximized over all `i < j < n+1` -/
noncomputable def max_sum_subseq : ℝ :=
Sup \$ (λ p : ℕ × ℕ, ∑ k in finset.Ico p.1 p.2, a k) '' { p : ℕ × ℕ | p.1 < p.2 ∧ p.2 ≤ n }

/-- The algorithm to compute the maximum. -/
noncomputable def find_max : ℕ → ℝ → ℝ → ℝ
| i s m :=
if hi : i < n then
let s' := if 0 < s then s + a i else a i in
have hi : n - (i + 1) < n - i, from (nat.sub_lt_sub_left_iff \$ by linarith).mpr \$ by linarith,
find_max (i+1) s' (max s' m)
else
m
using_well_founded { rel_tac := λ _ _,
`[exact ⟨ _, measure_wf \$ λ ⟨arg1, arg2, arg3⟩, n - arg1⟩] }

Template File

import .defs

noncomputable theory

open_locale big_operators

section

parameters
(a : ℕ → ℝ) -- the input array
(n : ℕ) -- the length of the array
(h : 0 < n)

include h

/-- Now prove the final theorem: -/
lemma max_sum_subseq_compute : max_sum_subseq a n = find_max a n 1 (a 0) (a 0) :=
sorry

end

Check File

import .submission

lemma check : ∀ (a : ℕ → ℝ) (n : ℕ) (h : 0 < n),
max_sum_subseq a n = find_max a n 1 (a 0) (a 0) :=
max_sum_subseq_compute

Definitions File

From Coq Require Export List ZArith.
Import ListNotations.

(* Maximum Sum Subsequence

Given a finite sequence of integer numbers, the goal is to show that the given
algorithm below (`mss`) computes the maximal sum of any (consecutive)
subsequence. *)

Fixpoint mss' (xs : list Z) (s m : Z) : Z :=
match xs with
| [] => m
| x :: xs' =>
let s' := Z.max x (s + x) in
mss' xs' s' (Z.max s' m)
end.

Definition mss (xs : list Z) : Z :=
match xs with
| [] => 0%Z
| x :: xs' => mss' xs' x x
end.

(* Unit test *)
Check eq_refl : mss [-2; 1; -3; 4; -1; 2; 1; -5; 4]%Z = 6%Z.
(*                              ^^^^^^^^^^^                  *)
(*                              maximal subsequence          *)

(* The definition of subsequence `sub` of a list `xs`. *)
Definition subseq {A} (sub xs : list A) : Prop :=
exists (prefix suffix : list A), xs = prefix ++ sub ++ suffix.

(* The sum of the elements of a list `xs` *)
Definition sum (xs : list Z) : Z :=

Template File

From Coq Require Import List ZArith.
Import ListNotations.
Require Import Defs.

(* Maximum Sum Subsequence

Given a finite sequence of integer numbers, the goal is to show that the given
algorithm `mss` computes the maximal sum of any (consecutive) subsequence. *)

(* The `mss` algorithm finds the sum of a subsequence and its the largest one *)
Theorem mss_correct (xs : list Z) :
0 < length xs ->
(exists s, subseq s xs /\ mss xs = sum s)
/\
(forall s, subseq s xs -> 0 < length s -> (sum s <= mss xs)%Z).
Proof.