Fulcrum.thy

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