MinimumIndex.thy

theory MinimumIndex
  imports Main
begin

(* A theory about functions that return the index of a minimum element in a list *)

(* Correctness properties: any valid implementation instantiates this locale: *)

locale minimumIndex =
  fixes minimumIndex :: "int list ⇒ nat"
    (* returns a valid index: *)
  assumes minimumIndex_index: "⋀xs. xs ≠ [] ⟹ minimumIndex xs < length xs"
    (* the entry at the returned index is minimal: *)
  assumes minimumIndex_minimum: "⋀x xs. xs ≠ [] ⟹ x ∈ set xs ⟹ xs ! (minimumIndex xs) ≤ x"

(* Tail-recursive implementation, easily translated to imperative style *)

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_tailrec :: "int list ⇒ nat" where
  "minimumIndex_tailrec [] = undefined"
| "minimumIndex_tailrec (x#xs) = minimumIndexWorker x 0 1 xs"

(* Implementation that's perhaps more representative of functional style. Not tail-recursive. *)

fun minimumIndexBelow :: "int ⇒ int list ⇒ nat option" where
  "minimumIndexBelow lb [] = None"
| "minimumIndexBelow lb (x#xs) =
  (case minimumIndexBelow (min x lb) xs of None ⇒ if lb < x then None else Some 0 | Some n ⇒ Some (Suc n))"

definition minimumIndex_functional :: "int list ⇒ nat" where
  "minimumIndex_functional xs ≡ case xs of x#xs' ⇒ (case minimumIndexBelow x xs' of None ⇒ 0 | Some n ⇒ Suc n)"

(* Declarative implementation *)

definition minimumIndex_declarative :: "int list ⇒ nat" where
  "minimumIndex_declarative xs ≡ SOME n. n < length xs ∧ xs ! n = Min (set xs)"

(* Correctness of tail-recursive implementation *)

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 (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
        with True show ?thesis
        proof (elim disjE)
          assume mem: "x0 ∈ set xs"
          thus ?thesis
          proof (intro minimumIndexWorker_notFound)
            from 1 show "minimumIndexWorker x currentIndex (Suc currentIndex) xs = currentIndex" .
          qed auto
        qed simp_all
      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]
      Cons.prems False
    show ?thesis
    proof (elim disjE)
      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 auto
  qed
qed simp

interpretation tailrec: minimumIndex minimumIndex_tailrec
proof
  fix xs :: "int list" assume "xs ≠ []"
  then obtain x xs' where Cons: "xs = x#xs'" by (cases xs, auto)

  have "minimumIndex_tailrec xs = minimumIndexWorker x 0 1 xs'" by (simp add: Cons)
  also have "... < 1 + length xs'" by (intro minimumIndexWorker_bound, simp)
  also have "... = length xs" by (simp add: Cons)
  finally show "minimumIndex_tailrec xs < length xs" .

  fix x0 assume x0: "x0 ∈ set xs"
  have "xs ! minimumIndex_tailrec xs = (x # xs') ! minimumIndexWorker x 0 (Suc 0) xs'" by (simp add: Cons)
  also from minimumIndexWorker_result [where best = x and bestIndex = 0 and currentIndex = "Suc 0" and xs = xs']
  have "... ≤ x0"
  proof (elim disjE)
    assume 1: "minimumIndexWorker x 0 (Suc 0) xs' = 0"
    hence "(x # xs') ! minimumIndexWorker x 0 (Suc 0) xs' = x" by simp
    also from x0 have "x0 = x ∨ x0 ∈ set xs'" by (auto simp add: Cons)
    hence "x ≤ x0"
    proof (elim disjE)
      assume mem: "x0 ∈ set xs'"
      thus ?thesis
      proof (intro minimumIndexWorker_notFound)
        from 1 show "minimumIndexWorker x 0 (Suc 0) xs' = 0" by simp
      qed simp_all
    qed simp
    finally show ?thesis .
  next
    assume 1: "Suc 0 ≤ minimumIndexWorker x 0 (Suc 0) xs'"
    hence index_eq: "Suc (minimumIndexWorker x 0 (Suc 0) xs' - Suc 0) = minimumIndexWorker x 0 (Suc 0) xs'" by simp

    have "(x # xs') ! minimumIndexWorker x 0 (Suc 0) xs' = (x # xs') ! (Suc (minimumIndexWorker x 0 (Suc 0) xs' - Suc 0))"
      by (simp add: index_eq)
    also have "... = xs' ! (minimumIndexWorker x 0 (Suc 0) xs' - Suc 0)" by simp
    also from x0 have "... ≤ x0" by (intro minimumIndexWorker_found 1, auto simp add: Cons)
    finally show ?thesis .
  qed
  finally show "xs ! (minimumIndex_tailrec xs) ≤ x0" .
qed

(* Correctness of "functional" implementation *)

lemma minimumIndexBelow_bound: "minimumIndexBelow lb xs = Some n ⟹ n < length xs"
proof (induct xs arbitrary: n lb)
  case (Cons x xs)
  thus ?case
  proof (cases "minimumIndexBelow (min x lb) xs")
    case (Some n') with Cons have "n' < length xs" by simp
    with Cons Some show ?thesis by auto
  qed (cases "lb < x", auto)
qed simp

lemma minimumIndexBelow_notFound: "minimumIndexBelow lb xs = None ⟹ x0 ∈ set xs ⟹ lb < x0"
proof (induct xs arbitrary: lb)
  case (Cons x xs)
  thus ?case
  proof (cases "minimumIndexBelow (min x lb) xs")
    case None
    with Cons have lb_x: "lb < x" by (cases "lb < x", auto)
    from Cons have "x0 = x ∨ x0 ∈ set xs" by auto
    with lb_x show ?thesis
    proof (elim disjE)
      assume "x0 ∈ set xs"
      hence "min x lb < x0" by (intro Cons None)
      with lb_x show ?thesis by simp
    qed simp
  qed simp
qed simp

lemma minimumIndexBelow_found: "minimumIndexBelow lb xs = Some n ⟹ x0 ∈ insert lb (set xs) ⟹ xs ! n ≤ x0"
proof (induct xs arbitrary: n lb x0)
  case (Cons x xs)
  thus ?case
  proof (cases "minimumIndexBelow (min x lb) xs")
    case None
    with Cons have x_lb: "x ≤ lb" by (cases "lb < x", auto)
    from Cons consider (lb) "x0 = lb" | (x) "x0 = x" | (xs) "x0 ∈ set xs" by auto
    from this Cons None x_lb have "min x lb ≤ x0"
    proof cases
      case xs
      with None minimumIndexBelow_notFound have "min x lb < x0" by simp
      thus ?thesis by simp
    qed auto
    with x_lb None Cons show ?thesis by auto
  next
    case (Some n')
    {
      fix x1 assume "x1 ∈ insert (min x lb) (set xs)"
      with Some Cons.hyps have "xs ! n' ≤ x1" by simp
      with Some Cons have "(x#xs) ! n ≤ x1" by auto
    }
    note hyp = this

    from Cons consider (lb) "x0 = lb ∨ x0 = x" | (xs) "x0 ∈ set xs" by auto
    thus ?thesis
    proof cases
      case lb
      have "(x#xs) ! n ≤ min x lb" by (intro hyp, simp)
      also from lb have "... ≤ x0" by auto
      finally show ?thesis.
    qed (intro hyp, auto)
  qed
qed simp

interpretation functional: minimumIndex minimumIndex_functional
proof
  fix xs :: "int list" assume "xs ≠ []"
  then obtain x xs' where Cons: "xs = x#xs'" by (cases xs, auto)

  show "minimumIndex_functional xs < length xs"
    using minimumIndexBelow_bound unfolding minimumIndex_functional_def Cons
    by (cases "minimumIndexBelow x xs'", auto)

  fix x0 assume x0: "x0 ∈ set xs"
  show "xs ! minimumIndex_functional xs ≤ x0"
  proof (cases "minimumIndexBelow x xs'")
    case None
    from minimumIndexBelow_notFound [OF this, of x0] x0 show ?thesis
      by (auto simp add: Cons minimumIndex_functional_def None)
  next
    case (Some n)
    from minimumIndexBelow_found [OF this, of x0] x0 show ?thesis
      by (auto simp add: Cons minimumIndex_functional_def Some)
  qed
qed

(* Correctness of "declarative" implementation *)

interpretation declarative: minimumIndex minimumIndex_declarative
proof
  fix xs :: "int list" assume nonempty: "xs ≠ []"

  define x0 where "x0 ≡ Min (set xs)"
  have "x0 ∈ set xs" unfolding x0_def using nonempty by (intro Min_in, auto)
  also note in_set_conv_nth
  finally obtain n where n: "n < length xs" "xs ! n = x0" by auto

  define P where "P ≡ λn. n < length xs ∧ xs ! n = Min (set xs)"
  have "P (Eps P)"
  proof (intro someI, unfold P_def, intro conjI ballI n)
    from n show "n < length xs" by simp
    from n show "xs ! n = Min (set xs)" by (simp add: x0_def)
  qed
  hence "P (minimumIndex_declarative xs)" unfolding minimumIndex_declarative_def P_def by simp
  thus "minimumIndex_declarative xs < length xs" "⋀x. x ∈ set xs ⟹ xs ! minimumIndex_declarative xs ≤ x"
    by (auto simp add: P_def)
qed

end