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.
\<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
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
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
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⟩] }
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
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
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.
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.