Skip to content

Instantly share code, notes, and snippets.

@DaveCTurner
Last active Mar 6, 2021
Embed
What would you like to do?
theory Fulcrum
imports Main
begin
(* https://twitter.com/Hillelogram/status/987432184217731073:
Fulcrum. Given a sequence of integers, returns the index i that minimizes |sum(seq[..i]) - sum(seq[i..])|. Does this in O(n) time and O(n) memory. https://rise4fun.com/Dafny/S1WMn *)
(* The following merely asserts the time and space bounds. *)
(* Tail-recursive-modulo-cons calculation of running total - O(n) time and space *)
fun runningTotalWorker :: "int ⇒ int list ⇒ int list" where
"runningTotalWorker accr [] = []"
| "runningTotalWorker accr (x#xs) = (let accr' = accr + x in accr' # runningTotalWorker accr' xs)"
definition runningTotal :: "int list ⇒ int list" where
"runningTotal ≡ runningTotalWorker 0"
(* Tail-recursive calculation of index of minimum element of a list - O(n) time, O(1) space *)
fun minimumIndexWorker :: "int ⇒ nat ⇒ nat ⇒ int list ⇒ nat" where
"minimumIndexWorker best bestIndex currentIndex [] = bestIndex"
| "minimumIndexWorker best bestIndex currentIndex (x#xs)
= (if x < best then minimumIndexWorker x currentIndex (Suc currentIndex) xs
else minimumIndexWorker best bestIndex (Suc currentIndex) xs)"
fun minimumIndex :: "int list ⇒ nat" where
"minimumIndex [] = undefined"
| "minimumIndex (x#xs) = minimumIndexWorker x 0 1 xs"
(* Fulcrum function - O(n) time and space since reversing and zipping lists are O(n) *)
definition fulcrum :: "int list ⇒ nat" where
"fulcrum xs ≡ let
acc = 0 # runningTotal xs;
rev = rev (runningTotal (rev xs))
in minimumIndex (map (λ(a,r). abs (r - a)) (zip acc rev))"
(* Try it out *)
lemma "fulcrum [1,2,3,4,5,-7] = 2" by (simp add: fulcrum_def runningTotal_def)
(* properties of runningTotal - show equivalence with non-tail-recursive version *)
lemma runningTotal_Nil_simp[simp]: "runningTotal [] = []" by (simp add: runningTotal_def)
lemma runningTotalWorker_accr: "runningTotalWorker accr xs = map (op + accr) (runningTotal xs)"
proof (induct xs arbitrary: accr)
case (Cons x xs)
have "runningTotalWorker (accr + x) xs = map (op + accr) (runningTotalWorker x xs)" by (simp add: Cons)
thus ?case by (simp add: runningTotal_def)
qed simp
lemma runningTotal_Cons_simp[simp]: "runningTotal (x0#xs) = x0 # map (op + x0) (runningTotal xs)"
by (simp add: runningTotal_def, simp add: runningTotalWorker_accr)
(* properties of minimumIndexWorker *)
lemma minimumIndexWorker_bound:
assumes index_lt: "bestIndex < currentIndex"
shows "minimumIndexWorker best bestIndex currentIndex xs < currentIndex + length xs"
using index_lt by (induct xs arbitrary: best bestIndex currentIndex, auto, force, metis add_Suc less_SucI)
lemma minimumIndexWorker_result:
shows "minimumIndexWorker best bestIndex currentIndex xs = bestIndex ∨ currentIndex ≤ minimumIndexWorker best bestIndex currentIndex xs"
apply (induct xs arbitrary: best bestIndex currentIndex, auto)
apply (metis Suc_leD order_refl)
by (meson Suc_le_lessD dual_order.strict_implies_order dual_order.strict_trans lessI)
lemma minimumIndexWorker_notFound:
assumes "bestIndex < currentIndex"
assumes "minimumIndexWorker best bestIndex currentIndex xs = bestIndex"
assumes "x : set xs"
shows "best ≤ x"
using assms
proof (induct xs arbitrary: x best bestIndex currentIndex)
case Nil thus ?case by simp
next
case (Cons x xs x0)
show ?case
proof (cases "x < best")
case True
from Cons have "bestIndex = minimumIndexWorker best bestIndex currentIndex (x # xs)" by simp
also have "minimumIndexWorker best bestIndex currentIndex (x # xs) = minimumIndexWorker x currentIndex (Suc currentIndex) xs" by (simp add: True)
also have "... ≥ currentIndex"
using minimumIndexWorker_result [where best = x and bestIndex = currentIndex and currentIndex = "Suc currentIndex" and xs = xs]
by auto
also from Cons have "currentIndex > bestIndex" by simp
finally show ?thesis by simp
next
case False with Cons show ?thesis apply auto using less_SucI by blast
qed
qed
lemma minimumIndexWorker_found:
assumes "bestIndex < currentIndex"
assumes "currentIndex ≤ minimumIndexWorker best bestIndex currentIndex xs"
assumes "x : insert best (set xs)"
shows "xs ! (minimumIndexWorker best bestIndex currentIndex xs - currentIndex) ≤ x"
using assms
proof (induct xs arbitrary: x best bestIndex currentIndex)
case Nil thus ?case by simp
next
case (Cons x xs x0)
show ?case
proof (cases "x < best")
case True
from minimumIndexWorker_result [where best = x and bestIndex = currentIndex and currentIndex = "Suc currentIndex" and xs = xs]
show ?thesis
proof (elim disjE)
assume 1: "minimumIndexWorker x currentIndex (Suc currentIndex) xs = currentIndex"
hence "(x # xs) ! (minimumIndexWorker best bestIndex currentIndex (x # xs) - currentIndex) = x" by (simp add: True)
also have "x ≤ x0"
proof -
from Cons have "x0 = best ∨ x0 = x ∨ x0 ∈ set xs" by auto
thus ?thesis
proof (elim disjE)
assume "x0 = best" with True show ?thesis by simp
next
assume "x0 = x" thus ?thesis by simp
next
assume mem: "x0 ∈ set xs"
thus ?thesis
proof (intro minimumIndexWorker_notFound)
from 1 show "minimumIndexWorker x currentIndex (Suc currentIndex) xs = currentIndex" .
qed auto
qed
qed
finally show ?thesis .
next
assume 1: "Suc currentIndex ≤ minimumIndexWorker x currentIndex (Suc currentIndex) xs"
hence "(x # xs) ! (minimumIndexWorker best bestIndex currentIndex (x # xs) - currentIndex)
= xs ! (minimumIndexWorker x currentIndex (Suc currentIndex) xs - Suc currentIndex)"
by (auto simp add: True)
also have "... ≤ min x x0"
proof (intro Cons.hyps [where bestIndex = currentIndex and currentIndex = "Suc currentIndex" and best = x] 1)
from Cons have "x0 = best ∨ x0 = x ∨ x0 ∈ set xs" by auto
thus "min x x0 ∈ insert x (set xs)"
proof (elim disjE)
assume "x0 = best" with True have "min x x0 = x" by simp thus ?thesis by simp
qed (auto, linarith)
qed simp
also have "... ≤ x0" by simp
finally show ?thesis by simp
qed
next
case False
have "minimumIndexWorker best bestIndex currentIndex (x # xs) = minimumIndexWorker best bestIndex (Suc currentIndex) xs"
by (simp add: False)
from minimumIndexWorker_result [where best = best and bestIndex = bestIndex and currentIndex = "Suc currentIndex" and xs = xs]
show ?thesis
proof (elim disjE)
assume "minimumIndexWorker best bestIndex (Suc currentIndex) xs = bestIndex"
with Cons.prems False show ?thesis by auto
next
assume 1: "Suc currentIndex ≤ minimumIndexWorker best bestIndex (Suc currentIndex) xs"
hence index_eq: "minimumIndexWorker best bestIndex currentIndex (x # xs) - currentIndex
= Suc (minimumIndexWorker best bestIndex (Suc currentIndex) xs - Suc currentIndex)"
by (simp add: False)
have "(x # xs) ! (minimumIndexWorker best bestIndex currentIndex (x # xs) - currentIndex)
= xs ! (minimumIndexWorker best bestIndex (Suc currentIndex) xs - Suc currentIndex)"
unfolding index_eq nth_Cons_Suc by simp
also have "... ≤ min best x0"
proof (intro Cons.hyps 1)
from Cons.prems show "bestIndex < Suc currentIndex" by simp
from Cons have "x0 = best ∨ x0 = x ∨ x0 ∈ set xs" by auto
thus "min best x0 ∈ insert best (set xs)"
proof (elim disjE)
assume "x0 = x" with False have "min best x0 = best" by simp thus ?thesis by simp
qed (auto, linarith)
qed
also have "... ≤ x0" by simp
finally show ?thesis .
qed
qed
qed
(* Properties of minimumIndex *)
lemma minimumIndex_index:
assumes nonempty: "xs ≠ []"
shows "minimumIndex xs < length xs"
proof (cases xs)
case Nil with nonempty show ?thesis by simp
next
case (Cons x xss)
have "minimumIndex xs = minimumIndexWorker x 0 1 xss" by (simp add: Cons)
also have "... < 1 + length xss" by (intro minimumIndexWorker_bound, simp)
also have "... = length xs" by (simp add: Cons)
finally show ?thesis .
qed
lemma minimumIndex_minimum:
assumes nonempty: "xs ≠ []"
assumes mem: "x0 ∈ set xs"
shows "xs ! (minimumIndex xs) ≤ x0"
proof (cases xs)
case Nil with nonempty show ?thesis by simp
next
case (Cons x xss)
have "xs ! minimumIndex xs = (x # xss) ! minimumIndexWorker x 0 (Suc 0) xss"
by (simp add: Cons)
also
from minimumIndexWorker_result [where best = x and bestIndex = 0 and currentIndex = "Suc 0" and xs = xss]
have "... ≤ x0"
proof (elim disjE)
assume 1: "minimumIndexWorker x 0 (Suc 0) xss = 0"
hence "(x # xss) ! minimumIndexWorker x 0 (Suc 0) xss = x" by simp
also from mem have "x0 = x ∨ x0 ∈ set xss" by (auto simp add: Cons)
hence "x ≤ x0"
proof (elim disjE)
assume mem: "x0 ∈ set xss"
thus ?thesis
proof (intro minimumIndexWorker_notFound)
from 1 show "minimumIndexWorker x 0 (Suc 0) xss = 0" by simp
qed simp_all
qed simp
finally show ?thesis .
next
assume 1: "Suc 0 ≤ minimumIndexWorker x 0 (Suc 0) xss"
hence index_eq: "Suc (minimumIndexWorker x 0 (Suc 0) xss - Suc 0) = minimumIndexWorker x 0 (Suc 0) xss" by simp
have "(x # xss) ! minimumIndexWorker x 0 (Suc 0) xss = (x # xss) ! (Suc (minimumIndexWorker x 0 (Suc 0) xss - Suc 0))"
by (simp add: index_eq)
also have "... = xss ! (minimumIndexWorker x 0 (Suc 0) xss - Suc 0)" by simp
also from mem have "... ≤ x0" by (intro minimumIndexWorker_found 1, auto simp add: Cons)
finally show ?thesis .
qed
finally show ?thesis .
qed
(* Sum of a list *)
fun listSum :: "int list ⇒ int" where
"listSum [] = 0"
| "listSum (x#xs) = x + listSum xs"
lemma listSum_snoc[simp]: "listSum (xs @ [x]) = x + listSum xs"
by (induct xs, auto)
lemma listSum_rev[simp]: "listSum (rev xs) = listSum xs"
by (induct xs, auto)
lemma length_runningTotal[simp]: "length (runningTotal xs) = length xs"
by (induct xs, auto)
lemma runningTotal_snoc[simp]: "runningTotal (xs @ [x]) = runningTotal xs @ [x + listSum xs]"
by (induct xs, auto)
lemma listSum_runningTotal: "n ≤ length xs ⟹ (0 # runningTotal xs) ! n = listSum (take n xs)"
proof (induct xs arbitrary: n rule: rev_induct)
case Nil thus ?case by simp
next
case (snoc x xs)
show ?case
proof (cases "n ≤ length xs")
case True
hence "(0 # runningTotal (xs @ [x])) ! n = ((0 # runningTotal xs) @ [x + listSum xs]) ! n" by simp
also have "... = (0 # runningTotal xs) ! n" unfolding nth_append using True by auto
also have "... = listSum (take n xs)" by (intro snoc True)
also have "... = listSum (take n (xs @ [x]))" unfolding take_append using True by auto
finally show ?thesis .
next
case False
with snoc have n: "n = Suc (length xs)" by simp
hence "(0 # runningTotal (xs @ [x])) ! n = ((0 # runningTotal xs) @ [x + listSum xs]) ! Suc (length xs)" by simp
also have "... = x + listSum xs" unfolding nth_append by simp
also have "... = listSum (xs @ [x])" by (induct xs, auto)
also have "... = listSum (take n (xs @ [x]))" unfolding n by auto
finally show ?thesis .
qed
qed
lemma listSum_runningTotal_rev:
assumes n: "n < length xs"
shows "rev (runningTotal (rev xs)) ! n = listSum (drop n xs)"
proof -
have "rev (runningTotal (rev xs)) ! n = runningTotal (rev xs) ! (length (runningTotal (rev xs)) - Suc n)" using n by (intro rev_nth, simp)
also have "... = (0 # runningTotal (rev xs)) ! (Suc (length (runningTotal (rev xs)) - Suc n))" by simp
also have "... = (0 # runningTotal (rev xs)) ! (length xs - n)" using n by (intro cong [OF refl, where f = "op ! (0 # runningTotal (rev xs))"], auto)
also have "... = listSum (take (length xs - n) (rev xs))" by (intro listSum_runningTotal, auto)
also have "... = listSum (drop (length xs - (length xs - n)) xs)" unfolding take_rev by simp
also have "... = listSum (drop n xs)" using n by auto
finally show ?thesis .
qed
(* Main correctness theorem *)
theorem
assumes nonempty: "xs ≠ []"
fixes fv :: "nat ⇒ int"
defines "fv n ≡ abs (listSum (take n xs) - listSum (drop n xs))"
shows "fulcrum xs < length xs"
and "∀n < length xs. fv (fulcrum xs) ≤ fv n"
proof -
define acc_totals :: "int list" where "acc_totals = 0 # runningTotal xs"
define rev_totals :: "int list" where "rev_totals = rev (runningTotal (rev xs))"
define zipped :: "(int × int) list" where "zipped = zip acc_totals rev_totals"
define diffs :: "int list" where "diffs = map (λ(a,r). abs (r - a)) zipped"
have fulcrum_minimumIndex: "fulcrum xs = minimumIndex diffs" by (simp add: fulcrum_def diffs_def zipped_def acc_totals_def rev_totals_def)
note fulcrum_minimumIndex
also have "minimumIndex diffs < length diffs"
using nonempty unfolding diffs_def zipped_def acc_totals_def rev_totals_def
by (intro minimumIndex_index, cases xs, auto)
also have "... = length xs"
unfolding diffs_def zipped_def acc_totals_def rev_totals_def by auto
finally show "fulcrum xs < length xs" by simp
{
fix n assume n: "n < length xs"
have "fv n = diffs ! n"
proof -
from n have acc_totals_nth[simp]: "acc_totals ! n = listSum (take n xs)"
unfolding acc_totals_def by (intro listSum_runningTotal, simp)
from n have rev_totals_nth[simp]: "rev_totals ! n = listSum (drop n xs)"
unfolding rev_totals_def by (intro listSum_runningTotal_rev, simp)
have "zipped ! n = (acc_totals ! n, rev_totals ! n)"
unfolding zipped_def using n by (intro nth_zip, auto simp add: acc_totals_def rev_totals_def)
hence zipped_nth[simp]: "zipped ! n = (listSum (take n xs), listSum (drop n xs))" by simp
have "diffs ! n = (λ(a, r). ¦r - a¦) (zipped ! n)"
unfolding diffs_def using n by (intro nth_map, auto simp add: zipped_def acc_totals_def rev_totals_def)
thus ?thesis unfolding fv_def by simp
qed
}
note fv_diffs = this
show "∀n < length xs. fv (fulcrum xs) ≤ fv n"
proof (intro allI impI)
fix n assume n: "n < length xs"
have "fv (fulcrum xs) = diffs ! (minimumIndex diffs)"
unfolding fulcrum_minimumIndex using `minimumIndex diffs < length diffs` `length diffs = length xs`
by (intro fv_diffs, auto)
also have "... ≤ fv n"
proof (intro minimumIndex_minimum)
from `length diffs = length xs` nonempty show "diffs ≠ []" by auto
from n have "fv n = diffs ! n" by (intro fv_diffs)
also from n `length diffs = length xs` have "... ∈ set diffs" by (intro nth_mem, simp)
finally show "fv n ∈ ..." .
qed
finally show "fv (fulcrum xs) ≤ fv n" by simp
qed
qed
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment