Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment