Skip to content

Instantly share code, notes, and snippets.

@iamwilhelm
Created January 22, 2024 02:33
Show Gist options
  • Save iamwilhelm/2ed1ea08bd352d4ca273e4894e08593d to your computer and use it in GitHub Desktop.
Save iamwilhelm/2ed1ea08bd352d4ca273e4894e08593d to your computer and use it in GitHub Desktop.
Incomplete proof of balancing node sizes after insert
theory balancing
imports Main
begin
type_synonym nodesizes = "nat list"
fun insert :: "nodesizes ⇒ nat ⇒ nodesizes" where
"insert [] _ = []" |
"insert (x#xs) 0 = (x+1)#xs" |
"insert (x#xs) n = x # insert xs (n-1)"
fun lend_left_helper :: "nat option ⇒ nodesizes ⇒ nat ⇒ nodesizes" where
"lend_left_helper _ [] _ = []" |
"lend_left_helper _ [x] _ = [x]" |
"lend_left_helper (Some p) (x # xs) 0 = (p + 1) # (x - 1) # xs" |
"lend_left_helper None (x # xs) 0 = x # xs" |
"lend_left_helper prev (x # xs) (Suc n) =
(case prev of
Some p ⇒ p # lend_left_helper (Some x) xs n
| None ⇒ lend_left_helper (Some x) xs n)"
definition lend_left :: "nodesizes ⇒ nat ⇒ nodesizes" where
"lend_left xs n = lend_left_helper None xs n"
fun lend_right :: "nodesizes ⇒ nat ⇒ nodesizes" where
"lend_right [] _ = []" |
"lend_right [x] _ = [x]" |
"lend_right (x # y # zs) 0 = (x-1) # (y+1) # zs" |
"lend_right (x # xs) n = x # lend_right xs (n - 1)"
definition even_div_left :: "nat ⇒ nat" where
"even_div_left x = x div 2"
definition even_div_right :: "nat ⇒ nat" where
"even_div_right x = (if x mod 2 = 0 then x div 2 else (x div 2) + 1)"
lemma left_and_right_division_sums_to_x:
shows "even_div_left x + even_div_right x = x"
proof (cases "x mod 2 = 0")
case True
then show ?thesis
using even_div_left_def even_div_right_def by auto
next
case False
then show ?thesis
using even_div_left_def even_div_right_def by presburger
qed
lemma left_and_right_division_balanced_when_even:
assumes "x mod 2 = 0"
shows "even_div_left x = even_div_right x"
using assms(1)
using even_div_left_def even_div_right_def by presburger
lemma left_and_right_division_balanced_when_odd:
assumes "x mod 2 = 1"
shows "even_div_left x + 1 = even_div_right x"
using assms(1)
using even_div_left_def even_div_right_def by presburger
fun split :: "nodesizes ⇒ nat ⇒ nodesizes" where
"split [] _ = []" |
"split (x # xs) 0 = [even_div_left x, even_div_right x] @ xs" |
"split (x # xs) (Suc n) = split xs n"
definition "N ≡ 4"
fun balance_metric :: "nat list ⇒ nat" where
"balance_metric [] = 0" |
"balance_metric (x # xs) = (x - N) ^ 2 + balance_metric xs"
definition balance :: "nodesizes ⇒ nat ⇒ nodesizes" where
"balance sizes n =
(let metric_ops = [(balance_metric sizes, sizes),
(balance_metric (lend_left sizes n), lend_left sizes n),
(balance_metric (lend_right sizes n), lend_right sizes n),
(balance_metric (split sizes n), split sizes n)];
min_metric_op =
(List.fold
(λacc tup. if (fst acc < fst tup) then acc else tup)
metric_ops
(hd metric_ops))
in
snd min_metric_op)"
definition balanced_insert :: "nodesizes ⇒ nat ⇒ nodesizes" where
"balanced_insert sizes n = balance (insert sizes n) n"
lemma insert_commutative:
assumes "∀x ∈ set sizes. x > 0 ∧ x < N"
shows "insert (insert sizes x) y = insert (insert sizes y) x"
unfolding insert.simps
proof (cases "x = y")
case True
then show ?thesis
by auto
next
case False
then show ?thesis
proof (cases "x < y")
case True
then show ?thesis sorry
next
case False
then show ?thesis sorry
qed
qed
lemma balanced_insert_commutative:
assumes "∀x ∈ set sizes. x > 0 ∧ x < N"
shows "balanced_insert (balanced_insert sizes x) y = balanced_insert (balanced_insert sizes y) x"
quickcheck
sorry
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment