Library ordered_main
The ordered_main library contains all the main lemmas concerned with the
orderedness of AVL trees. These lemmas build on those define in ordered_helper
Require Import Hbt.Lemmas.Ordered.Helper.ordered_helper.
Require Export Hbt.Lemmas.Ordered.Helper.ordered_helper.
Maximum and Minimum Elements After Insertion
- the maximum element is either x or the maximum element of the original tree
- the minimum element is either x or the minimum element of the original tree
Lemma insertion_in_node_min_max:
forall (A : Type)
(compare : A -> A -> element_comparison),
(forall (hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A)
(x min min' max max' : A),
is_sound_hbt A hbt = true ->
is_balanced_hbt A hbt = true ->
insert_hbt_helper A compare x hbt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TSome (A * A) (min', max') ->
traverse_to_check_ordered_hbt A hbt compare = TSome (A * A) (min, max) ->
(max' = x \/ max' = max) /\ (min' = x \/ min' = min))
/\
(forall (bt : binary_tree A)
(h : nat)
(hbt' : heightened_binary_tree A)
(x min min' max max' : A),
is_sound_hbt A (HNode A h bt) = true ->
is_balanced_hbt A (HNode A h bt) = true ->
insert_bt_helper A compare x h bt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TSome (A * A) (min', max') ->
traverse_to_check_ordered_bt A bt compare = TSome (A * A) (min, max) ->
(max' = x \/ max' = max) /\ (min' = x \/ min' = min))
/\
(forall (t : triple A)
(h : nat)
(hbt' : heightened_binary_tree A)
(x min min' max max' : A),
is_sound_hbt A (HNode A h (Node A t)) = true ->
is_balanced_hbt A (HNode A h (Node A t)) = true ->
insert_t_helper A compare x h t = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TSome (A * A) (min', max') ->
traverse_to_check_ordered_t A t compare = TSome (A * A) (min, max) ->
(max' = x \/ max' = max) /\ (min' = x \/ min' = min)).
forall (A : Type)
(compare : A -> A -> element_comparison),
(forall (hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A)
(x min min' max max' : A),
is_sound_hbt A hbt = true ->
is_balanced_hbt A hbt = true ->
insert_hbt_helper A compare x hbt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TSome (A * A) (min', max') ->
traverse_to_check_ordered_hbt A hbt compare = TSome (A * A) (min, max) ->
(max' = x \/ max' = max) /\ (min' = x \/ min' = min))
/\
(forall (bt : binary_tree A)
(h : nat)
(hbt' : heightened_binary_tree A)
(x min min' max max' : A),
is_sound_hbt A (HNode A h bt) = true ->
is_balanced_hbt A (HNode A h bt) = true ->
insert_bt_helper A compare x h bt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TSome (A * A) (min', max') ->
traverse_to_check_ordered_bt A bt compare = TSome (A * A) (min, max) ->
(max' = x \/ max' = max) /\ (min' = x \/ min' = min))
/\
(forall (t : triple A)
(h : nat)
(hbt' : heightened_binary_tree A)
(x min min' max max' : A),
is_sound_hbt A (HNode A h (Node A t)) = true ->
is_balanced_hbt A (HNode A h (Node A t)) = true ->
insert_t_helper A compare x h t = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TSome (A * A) (min', max') ->
traverse_to_check_ordered_t A t compare = TSome (A * A) (min, max) ->
(max' = x \/ max' = max) /\ (min' = x \/ min' = min)).
Rotations Preserves Order
- rotate_right_2 and rotate_left_2 correspond to the elementary rotate right and rotate left opertations
- The double rotation rotate_right_1 results from composing an elementery rotate left operation on a sub-tree followed by an elementary rotate right operation on the entire tree
- The double rotation rotate_left_1 results from composing an elementery rotate right operation on a sub-tree followed by an elementary rotate left operation on the entire tree.
Helper Lemmas for Rotations
- hbt1 is ordered and has a minimum and maximum payload
- the maximum payload of hbt1 is less than e
- hbt2 is ordered
- if hbt2 has a minimum and a maximum, then e is less than this minimum,
Lemma rotate_right_intermediate_tree_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(min1 max1 : A),
traverse_to_check_ordered_hbt A (HNode A h1 bt1) compare =
TSome (A * A) (min1, max1) ->
compare max1 e = Lt ->
is_ordered_hbt A (HNode A h2 bt2) compare = true ->
(forall min2 max2 : A,
traverse_to_check_ordered_hbt A (HNode A h2 bt2) compare =
TSome (A * A) (min2, max2) -> compare e min2 = Lt) ->
exists max2,
traverse_to_check_ordered_hbt
A
(HNode A (1 + max h1 h2)
(Node A
(Triple A
(HNode A h1 bt1)
e
(HNode A h2 bt2))))
compare = TSome (A * A) (min1, max2).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(min1 max1 : A),
traverse_to_check_ordered_hbt A (HNode A h1 bt1) compare =
TSome (A * A) (min1, max1) ->
compare max1 e = Lt ->
is_ordered_hbt A (HNode A h2 bt2) compare = true ->
(forall min2 max2 : A,
traverse_to_check_ordered_hbt A (HNode A h2 bt2) compare =
TSome (A * A) (min2, max2) -> compare e min2 = Lt) ->
exists max2,
traverse_to_check_ordered_hbt
A
(HNode A (1 + max h1 h2)
(Node A
(Triple A
(HNode A h1 bt1)
e
(HNode A h2 bt2))))
compare = TSome (A * A) (min1, max2).
Lemma to show that given two sub-trees hbt1, hbt2 and a payload e such that:
- hbt2 is ordered and has a minimum and maximum payload
- the minimum payload of hbt2 is less than e
- hbt1 is ordered
- if hbt1 has a minimum and a maximum, then this maximum is less than e,
Lemma rotate_left_intermediate_tree_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(min2 max2 : A),
is_ordered_hbt A (HNode A h1 bt1) compare = true ->
(forall min1 max1 : A,
traverse_to_check_ordered_hbt A (HNode A h1 bt1) compare =
TSome (A * A) (min1, max1) -> compare max1 e = Lt) ->
traverse_to_check_ordered_hbt A (HNode A h2 bt2) compare =
TSome (A * A) (min2, max2) ->
compare e min2 = Lt ->
exists min1,
traverse_to_check_ordered_hbt
A
(HNode A (1 + max h1 h2)
(Node A
(Triple A
(HNode A h1 bt1)
e
(HNode A h2 bt2))))
compare = TSome (A * A) (min1, max2).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(min2 max2 : A),
is_ordered_hbt A (HNode A h1 bt1) compare = true ->
(forall min1 max1 : A,
traverse_to_check_ordered_hbt A (HNode A h1 bt1) compare =
TSome (A * A) (min1, max1) -> compare max1 e = Lt) ->
traverse_to_check_ordered_hbt A (HNode A h2 bt2) compare =
TSome (A * A) (min2, max2) ->
compare e min2 = Lt ->
exists min1,
traverse_to_check_ordered_hbt
A
(HNode A (1 + max h1 h2)
(Node A
(Triple A
(HNode A h1 bt1)
e
(HNode A h2 bt2))))
compare = TSome (A * A) (min1, max2).
Lemma to show that an elementary right rotation operation preserves order
Lemma rotate_right_preserves_order:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11 : nat)
(bt11 : binary_tree A)
(e1 : A)
(h12 : nat)
(bt12 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(t_min t_max : A),
traverse_to_check_ordered_hbt
A (HNode A (1 + max (1 + max h11 h12) h2)
(Node A (Triple A
(HNode A (1 + max h11 h12)
(Node A (Triple A
(HNode A h11 bt11)
e1
(HNode A h12 bt12))))
e
(HNode A h2 bt2)))) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt
A (HNode A (1 + max h11 (1 + max h12 h2))
(Node A (Triple A
(HNode A h11 bt11)
e1
(HNode A (1 + max h12 h2)
(Node A (Triple A
(HNode A h12 bt12)
e
(HNode A h2 bt2)))))))
compare = TSome (A * A) (t_min, t_max).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11 : nat)
(bt11 : binary_tree A)
(e1 : A)
(h12 : nat)
(bt12 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(t_min t_max : A),
traverse_to_check_ordered_hbt
A (HNode A (1 + max (1 + max h11 h12) h2)
(Node A (Triple A
(HNode A (1 + max h11 h12)
(Node A (Triple A
(HNode A h11 bt11)
e1
(HNode A h12 bt12))))
e
(HNode A h2 bt2)))) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt
A (HNode A (1 + max h11 (1 + max h12 h2))
(Node A (Triple A
(HNode A h11 bt11)
e1
(HNode A (1 + max h12 h2)
(Node A (Triple A
(HNode A h12 bt12)
e
(HNode A h2 bt2)))))))
compare = TSome (A * A) (t_min, t_max).
Lemma to show that an elementary left rotation operation preserves order
Lemma rotate_left_preserves_order:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h21 : nat)
(bt21 : binary_tree A)
(e2 : A)
(h22 : nat)
(bt22 : binary_tree A)
(t_min t_max : A),
traverse_to_check_ordered_hbt
A (HNode A (1 + max h1 (1 + max h21 h22))
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A (1 + max h21 h22)
(Node A (Triple A
(HNode A h21 bt21)
e2
(HNode A h22 bt22)))))))
compare = TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt
A (HNode A (1 + max (1 + max h1 h21) h22)
(Node A (Triple A
(HNode A (1 + max h1 h21)
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A h21 bt21))))
e2
(HNode A h22 bt22)))) compare =
TSome (A * A) (t_min, t_max).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h21 : nat)
(bt21 : binary_tree A)
(e2 : A)
(h22 : nat)
(bt22 : binary_tree A)
(t_min t_max : A),
traverse_to_check_ordered_hbt
A (HNode A (1 + max h1 (1 + max h21 h22))
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A (1 + max h21 h22)
(Node A (Triple A
(HNode A h21 bt21)
e2
(HNode A h22 bt22)))))))
compare = TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt
A (HNode A (1 + max (1 + max h1 h21) h22)
(Node A (Triple A
(HNode A (1 + max h1 h21)
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A h21 bt21))))
e2
(HNode A h22 bt22)))) compare =
TSome (A * A) (t_min, t_max).
Main Lemmas for Rotations
- the modified left sub-tree hbt_ret is sound, ordered, and not a leaf,
- the maximum payload of hbt_ret sub-tree is less than the root payload,
- the right sub-tree is ordered
- if the right sub-tree were a node with a maximum and minimum value, then the root payload would be less than the minimum value,
Lemma insertion_rotate_right_preserves_order:
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt_ret : heightened_binary_tree A)
(hbt2 : heightened_binary_tree A)
(min_ret max_ret : A)
(e : A)
(hbt' : heightened_binary_tree A),
traverse_to_check_ordered_hbt A hbt_ret compare =
TSome (A * A) (min_ret, max_ret) ->
is_ordered_hbt A hbt2 compare = true ->
is_sound_hbt A hbt_ret = true ->
compare max_ret e = Lt ->
(forall (min2 max2 : A),
traverse_to_check_ordered_hbt A hbt2 compare =
TSome (A * A) (min2, max2) ->
compare e min2 = Lt) ->
rotate_right_hbt A hbt_ret e hbt2 = Some hbt' ->
is_ordered_hbt A hbt' compare = true.
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt_ret : heightened_binary_tree A)
(hbt2 : heightened_binary_tree A)
(min_ret max_ret : A)
(e : A)
(hbt' : heightened_binary_tree A),
traverse_to_check_ordered_hbt A hbt_ret compare =
TSome (A * A) (min_ret, max_ret) ->
is_ordered_hbt A hbt2 compare = true ->
is_sound_hbt A hbt_ret = true ->
compare max_ret e = Lt ->
(forall (min2 max2 : A),
traverse_to_check_ordered_hbt A hbt2 compare =
TSome (A * A) (min2, max2) ->
compare e min2 = Lt) ->
rotate_right_hbt A hbt_ret e hbt2 = Some hbt' ->
is_ordered_hbt A hbt' compare = true.
Lemma to show that post an insertion operation on the right sub-tree of a given tree such that the resultant tree is unbalanced, and assuming:
applying rotate_left_hbt on this unbalanced tree returns a tree which is ordered
- the modified right sub-tree hbt_ret is sound, ordered, and not a leaf,
- the root payload is less than the minimum payload of hbt_ret
- the left sub-tree is ordered
- if the left sub-tree were a node with a maximum and minimum value, then maximum value would be less than the root payload,
Lemma insertion_rotate_left_preserves_order:
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt1 : heightened_binary_tree A)
(hbt_ret : heightened_binary_tree A)
(min_ret max_ret : A)
(e : A)
(hbt' : heightened_binary_tree A),
is_ordered_hbt A hbt1 compare = true ->
traverse_to_check_ordered_hbt A hbt_ret compare =
TSome (A * A) (min_ret, max_ret) ->
is_sound_hbt A hbt_ret = true ->
(forall (min1 max1 : A),
traverse_to_check_ordered_hbt A hbt1 compare =
TSome (A * A) (min1, max1) ->
compare max1 e = Lt) ->
compare e min_ret = Lt ->
rotate_left_hbt A hbt1 e hbt_ret = Some hbt' ->
is_ordered_hbt A hbt' compare = true.
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt1 : heightened_binary_tree A)
(hbt_ret : heightened_binary_tree A)
(min_ret max_ret : A)
(e : A)
(hbt' : heightened_binary_tree A),
is_ordered_hbt A hbt1 compare = true ->
traverse_to_check_ordered_hbt A hbt_ret compare =
TSome (A * A) (min_ret, max_ret) ->
is_sound_hbt A hbt_ret = true ->
(forall (min1 max1 : A),
traverse_to_check_ordered_hbt A hbt1 compare =
TSome (A * A) (min1, max1) ->
compare max1 e = Lt) ->
compare e min_ret = Lt ->
rotate_left_hbt A hbt1 e hbt_ret = Some hbt' ->
is_ordered_hbt A hbt' compare = true.
Insertion Preserves Order
- the crucial insertion_in_node_min_max lemma (defined in this library) show the relationship between a payload and the maximum/minimum values of the sub-trees
- the lemmas concerning the preservation of orderedness post rotation operations
Lemma insertion_preserves_order:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A),
specification_of_compare_defining_total_order A compare ->
(forall (hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A),
is_sound_hbt A hbt = true ->
is_balanced_hbt A hbt = true ->
is_ordered_hbt A hbt compare = true ->
insert_hbt_helper A compare x hbt = Some hbt' ->
is_ordered_hbt A hbt' compare = true)
/\
(forall (bt : binary_tree A)
(h_hbt : nat)
(hbt' : heightened_binary_tree A),
is_sound_hbt A (HNode A h_hbt bt) = true ->
is_balanced_hbt A (HNode A h_hbt bt) = true ->
is_ordered_hbt A (HNode A h_hbt bt) compare = true ->
insert_bt_helper A compare x h_hbt bt = Some hbt' ->
is_ordered_hbt A hbt' compare = true)
/\
(forall (t : triple A)
(h_hbt : nat)
(hbt' : heightened_binary_tree A),
is_sound_hbt A (HNode A h_hbt (Node A t)) = true ->
is_balanced_hbt A (HNode A h_hbt (Node A t)) = true ->
is_ordered_hbt A (HNode A h_hbt (Node A t)) compare = true ->
insert_t_helper A compare x h_hbt t = Some hbt' ->
is_ordered_hbt A hbt' compare = true).
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A),
specification_of_compare_defining_total_order A compare ->
(forall (hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A),
is_sound_hbt A hbt = true ->
is_balanced_hbt A hbt = true ->
is_ordered_hbt A hbt compare = true ->
insert_hbt_helper A compare x hbt = Some hbt' ->
is_ordered_hbt A hbt' compare = true)
/\
(forall (bt : binary_tree A)
(h_hbt : nat)
(hbt' : heightened_binary_tree A),
is_sound_hbt A (HNode A h_hbt bt) = true ->
is_balanced_hbt A (HNode A h_hbt bt) = true ->
is_ordered_hbt A (HNode A h_hbt bt) compare = true ->
insert_bt_helper A compare x h_hbt bt = Some hbt' ->
is_ordered_hbt A hbt' compare = true)
/\
(forall (t : triple A)
(h_hbt : nat)
(hbt' : heightened_binary_tree A),
is_sound_hbt A (HNode A h_hbt (Node A t)) = true ->
is_balanced_hbt A (HNode A h_hbt (Node A t)) = true ->
is_ordered_hbt A (HNode A h_hbt (Node A t)) compare = true ->
insert_t_helper A compare x h_hbt t = Some hbt' ->
is_ordered_hbt A hbt' compare = true).