Cookies disclaimer

I agree 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.

[Proof Ground 2021] Kadane's Algorithm

Resources

Download Files

Definitions File

\<comment> \<open>Task description\<close>
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
Download Files

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
Download Files

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 :=
  fold_right Z.add 0%Z xs.

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.
Admitted.

Terms and Conditions