Library ordered_helper
The ordered_helper library contains all the lemmas that serve as 'helper'
lemmas to prove the main lemmas for orderedness in ordered_main. Please see how
the predicate to check orderedness is defined in the hbt library to understand the
motivation for the lemmas in this libray.
Require Import Hbt.Lemmas.Balanced.balanced.
Require Export Hbt.Lemmas.Balanced.balanced.
General Lemmas Concerning Orderedness
Lemma triple_ordered_implies_hbts_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h_hbt : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A),
is_ordered_hbt A (HNode A h_hbt (Node A (Triple A hbt1 e hbt2))) compare = true ->
is_ordered_hbt A hbt1 compare = true /\ is_ordered_hbt A hbt2 compare = true.
forall (A : Type)
(compare : A -> A -> element_comparison)
(h_hbt : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A),
is_ordered_hbt A (HNode A h_hbt (Node A (Triple A hbt1 e hbt2))) compare = true ->
is_ordered_hbt A hbt1 compare = true /\ is_ordered_hbt A hbt2 compare = true.
Lemma to show that traversing a binary_tree constructed with a Node
constructor to check orderedness can never yield a TNone value
Lemma traverse_node_impossible_case:
forall (A : Type)
(compare : A -> A -> element_comparison)
(t1 : triple A),
traverse_to_check_ordered_bt A (Node A t1) compare = TNone (A * A) -> False.
forall (A : Type)
(compare : A -> A -> element_comparison)
(t1 : triple A),
traverse_to_check_ordered_bt A (Node A t1) compare = TNone (A * A) -> False.
Lemma to show that if traversing a heightened_binary_tree to check orderedness
yields a TNone value, then the tree is a leaf
Lemma tnone_implies_leaf:
forall (A : Type)
(h : nat)
(bt : binary_tree A)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_hbt A (HNode A h bt) compare =
TNone (A * A) ->
bt = Leaf A.
forall (A : Type)
(h : nat)
(bt : binary_tree A)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_hbt A (HNode A h bt) compare =
TNone (A * A) ->
bt = Leaf A.
Lemma to show that if a heightened_binary_tree is ordered, then it is either:
- a leaf, in which case traverse_to_check_ordered_hbt returns a TNone value
- or a node, in which case traverse_to_check_ordered_hbt returns a TSome value
Lemma is_ordered_true_implies_leaf_or_ordered_node:
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt : heightened_binary_tree A),
is_ordered_hbt A hbt compare = true ->
(traverse_to_check_ordered_hbt A hbt compare =
TNone (A * A)
\/
exists (min max : A),
traverse_to_check_ordered_hbt A hbt compare =
TSome (A * A) (min, max)).
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt : heightened_binary_tree A),
is_ordered_hbt A hbt compare = true ->
(traverse_to_check_ordered_hbt A hbt compare =
TNone (A * A)
\/
exists (min max : A),
traverse_to_check_ordered_hbt A hbt compare =
TSome (A * A) (min, max)).
Lemma to show that a tree with a triple (i.e., a tree that is not a leaf) is
ordered, i.e., traversing the tree to check for orderedness returns a TSome value
with minimum and maximum payloads
Lemma single_node_tree_is_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree 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) ->
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 min1 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).
Check (is_ordered_true_implies_leaf_or_ordered_node).
Qed.
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree 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) ->
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 min1 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).
Check (is_ordered_true_implies_leaf_or_ordered_node).
Qed.
Lemma to show that a sound tree with non-zero height must be a node
Lemma non_zero_height_implies_node:
forall (A : Type)
(h_ret h1 h2 : nat)
(bt1 : binary_tree A),
(h_ret = h1) \/ (h_ret = 1 + h1) ->
(h_ret =n= 2 + h2) = true ->
is_sound_hbt A (HNode A h1 bt1) = true ->
exists (t1 : triple A),
bt1 = Node A t1.
Check (succ_eq).
Qed.
forall (A : Type)
(h_ret h1 h2 : nat)
(bt1 : binary_tree A),
(h_ret = h1) \/ (h_ret = 1 + h1) ->
(h_ret =n= 2 + h2) = true ->
is_sound_hbt A (HNode A h1 bt1) = true ->
exists (t1 : triple A),
bt1 = Node A t1.
Check (succ_eq).
Qed.
Lemma to show that if traversing a heightened_binary_tree to check its
orderedness yields a TSome value containg the minimum and maximum payload
values, then reducing the left subtree to a leaf also yields an ordered
heightened_binary_tree such that:
- the maximum value is the same as the maximum value of the original tree
- the minimum value is the payload at the root of the tree concerned
Lemma reduce_ordered_hbt_left:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(min max : A),
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A hbt1 e hbt2))) compare = TSome (A * A) (min, max) ->
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A
(HNode A 0 (Leaf A))
e
hbt2))) compare = TSome (A * A) (e, max).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(min max : A),
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A hbt1 e hbt2))) compare = TSome (A * A) (min, max) ->
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A
(HNode A 0 (Leaf A))
e
hbt2))) compare = TSome (A * A) (e, max).
Lemma to show that if traversing a heightened_binary_tree to check its
orderedness yields a TSome value containg the minimum and maximum payload
values, then reducing the right subtree to a leaf also yields an ordered
heightened_binary_tree such that:
- the minimum value is the same as the minimum value of the original tree
- the maximum value is the payload at the root of the tree concerned
Lemma reduce_ordered_hbt_right:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(min max : A),
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A hbt1 e hbt2))) compare = TSome (A * A) (min, max) ->
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A
hbt1
e
(HNode A 0 (Leaf A))))) compare = TSome (A * A) (min, e).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(min max : A),
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A hbt1 e hbt2))) compare = TSome (A * A) (min, max) ->
traverse_to_check_ordered_hbt
A (HNode A h (Node A (Triple A
hbt1
e
(HNode A 0 (Leaf A))))) compare = TSome (A * A) (min, e).
Lemma to show that if traversing a heightened_binary_tree to check its
orderedness yields a maximum and a minimum value, then it must be ordered
Lemma traverse_to_check_ordered_hbt_some_implies_is_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt : heightened_binary_tree A)
(min max : A),
traverse_to_check_ordered_hbt A hbt compare = TSome (A * A) (min, max) ->
is_ordered_hbt A hbt compare = true.
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt : heightened_binary_tree A)
(min max : A),
traverse_to_check_ordered_hbt A hbt compare = TSome (A * A) (min, max) ->
is_ordered_hbt A hbt compare = true.
This lemma is not concerned with orderedness but is required to prove orderedness
lemmas in the rotate_right_2 and rotate_left_2 cases
Lemma non_zero_height:
forall (A : Type)
(h1 h2 h h' : nat)
(bt' : binary_tree A),
h2 = h1 ->
1 + max h1 h2 = h ->
compare_int h (2 + project_height_hbt A (HNode A h' bt')) = Eq ->
exists x, h2 = S x.
forall (A : Type)
(h1 h2 h h' : nat)
(bt' : binary_tree A),
h2 = h1 ->
1 + max h1 h2 = h ->
compare_int h (2 + project_height_hbt A (HNode A h' bt')) = Eq ->
exists x, h2 = S x.
Orderedness Lemmas Concerning Insertion
Impossible Insertion Case
Lemma insertion_impossible_case:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A),
insert_hbt_helper A compare x hbt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare <> TNone (A * A).
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A),
insert_hbt_helper A compare x hbt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare <> TNone (A * A).
Lemma to show that given the (false) hypothesis that a tree modified by the
insertion operation is a leaf, any proposition will be true
Lemma insertion_impossible_case_implies_true:
forall (A : Type)
(hbt hbt' : heightened_binary_tree A)
(compare : A -> A -> element_comparison)
(x : A)
(P : Prop),
insert_hbt_helper A compare x hbt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TNone (A * A) ->
P.
forall (A : Type)
(hbt hbt' : heightened_binary_tree A)
(compare : A -> A -> element_comparison)
(x : A)
(P : Prop),
insert_hbt_helper A compare x hbt = Some hbt' ->
traverse_to_check_ordered_hbt A hbt' compare = TNone (A * A) ->
P.
General Lemmas Concerning the Minimum and Maximum Payloads in an AVL Tree
Lemma insertion_in_leaf_min_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A)
(x min' max' : A),
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 = TNone (A * A) ->
min' = x /\ max' = x.
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt : heightened_binary_tree A)
(hbt' : heightened_binary_tree A)
(x min' max' : A),
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 = TNone (A * A) ->
min' = x /\ max' = x.
Lemma ordered_node_has_min_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(hbt11 : heightened_binary_tree A)
(e1 : A)
(hbt12 : heightened_binary_tree A),
is_ordered_hbt A (HNode A h1 (Node A (Triple A hbt11 e1 hbt12))) compare = true ->
exists (some_min some_max : A),
traverse_to_check_ordered_bt A (Node A (Triple A hbt11 e1 hbt12)) compare =
TSome (A * A) (some_min, some_max).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(hbt11 : heightened_binary_tree A)
(e1 : A)
(hbt12 : heightened_binary_tree A),
is_ordered_hbt A (HNode A h1 (Node A (Triple A hbt11 e1 hbt12))) compare = true ->
exists (some_min some_max : A),
traverse_to_check_ordered_bt A (Node A (Triple A hbt11 e1 hbt12)) compare =
TSome (A * A) (some_min, some_max).
Right Rotation Lemmas
rotate_right_1and the rotate_right_2 cases
Lemma rotate_right_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h_rot_root : nat)
(e : A)
(h_rot_left : nat)
(hbt_left : heightened_binary_tree A)
(e' : A)
(hbt_right : heightened_binary_tree A)
(max' : A)
(h_org : nat)
(max : A),
traverse_to_check_ordered_hbt
A
(HNode A h_rot_root
(Node A
(Triple A
(HNode A 0 (Leaf A))
e
(HNode A h_rot_left
(Node A
(Triple A
hbt_left
e'
hbt_right))))))
compare = TSome (A * A) (e, max') ->
traverse_to_check_ordered_hbt
A (HNode A h_org
(Node A (Triple A
(HNode A 0 (Leaf A))
e'
hbt_right)))
compare = TSome (A * A) (e', max) ->
max' = max.
forall (A : Type)
(compare : A -> A -> element_comparison)
(h_rot_root : nat)
(e : A)
(h_rot_left : nat)
(hbt_left : heightened_binary_tree A)
(e' : A)
(hbt_right : heightened_binary_tree A)
(max' : A)
(h_org : nat)
(max : A),
traverse_to_check_ordered_hbt
A
(HNode A h_rot_root
(Node A
(Triple A
(HNode A 0 (Leaf A))
e
(HNode A h_rot_left
(Node A
(Triple A
hbt_left
e'
hbt_right))))))
compare = TSome (A * A) (e, max') ->
traverse_to_check_ordered_hbt
A (HNode A h_org
(Node A (Triple A
(HNode A 0 (Leaf A))
e'
hbt_right)))
compare = TSome (A * A) (e', max) ->
max' = max.
Lemma to show that post an insertion operation on a tree which necessitates a
right rotation rebalance operation, the minimum element of a right rotated tree
is either
- the element originally inserted
- or the minimum value of the subtree on which the insertion operation was
Lemma rotate_right_min:
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt1 : heightened_binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(t_min t_max min1 max1 t_min' x : A),
traverse_to_check_ordered_t A (Triple A hbt1 e (HNode A h2 bt2)) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt1 compare = TSome (A * A) (min1, max1) ->
t_min' = x \/ t_min' = min1 ->
t_min' = x \/ t_min' = t_min.
forall (A : Type)
(compare : A -> A -> element_comparison)
(hbt1 : heightened_binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A)
(t_min t_max min1 max1 t_min' x : A),
traverse_to_check_ordered_t A (Triple A hbt1 e (HNode A h2 bt2)) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt1 compare = TSome (A * A) (min1, max1) ->
t_min' = x \/ t_min' = min1 ->
t_min' = x \/ t_min' = t_min.
Lemma to show that if a tree subject to rotate_right_1 (double rotation)
is ordered, then the original subtree into which an element was inserted was also
ordered
Lemma rotate_right_1_tree_ordered_implies_returned_tree_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11' h121' h122' h2 h1' h12': nat)
(bt11' bt121' bt122' bt2 : binary_tree A)
(e1 e12 e t_min' t_max' : A),
traverse_to_check_ordered_hbt
A
(HNode A
(1 + max (1 + max h11' h121') (1 + max h122' h2))
(Node A
(Triple A
(HNode A (1 + max h11' h121')
(Node A (Triple A
(HNode A h11' bt11')
e1
(HNode A h121' bt121'))))
e12
(HNode A (1 + max h122' h2)
(Node A (Triple A
(HNode A h122' bt122')
e
(HNode A h2 bt2)))))))
compare =
TSome (A * A) (t_min', t_max') ->
exists t_max'',
traverse_to_check_ordered_hbt
A
(HNode A h1'
(Node A
(Triple A (HNode A h11' bt11') e1
(HNode A h12'
(Node A
(Triple A
(HNode A h121' bt121')
e12
(HNode A h122' bt122')))))))
compare = TSome (A * A) (t_min', t_max'').
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11' h121' h122' h2 h1' h12': nat)
(bt11' bt121' bt122' bt2 : binary_tree A)
(e1 e12 e t_min' t_max' : A),
traverse_to_check_ordered_hbt
A
(HNode A
(1 + max (1 + max h11' h121') (1 + max h122' h2))
(Node A
(Triple A
(HNode A (1 + max h11' h121')
(Node A (Triple A
(HNode A h11' bt11')
e1
(HNode A h121' bt121'))))
e12
(HNode A (1 + max h122' h2)
(Node A (Triple A
(HNode A h122' bt122')
e
(HNode A h2 bt2)))))))
compare =
TSome (A * A) (t_min', t_max') ->
exists t_max'',
traverse_to_check_ordered_hbt
A
(HNode A h1'
(Node A
(Triple A (HNode A h11' bt11') e1
(HNode A h12'
(Node A
(Triple A
(HNode A h121' bt121')
e12
(HNode A h122' bt122')))))))
compare = TSome (A * A) (t_min', t_max'').
Lemma to show that if an insertion operation led to a rotate_right_1
operation, then the subtree on which the insertion operation was performed cannot
be a leaf
Lemma rotate_right_1_impossible_case:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h1 : nat)
(bt1 : binary_tree A)
(h1' h11' h12' h121' h122' : nat)
(bt11' bt121' bt122' : binary_tree A)
(e1 e12 : A),
insert_hbt_helper A compare x (HNode A h1 bt1) =
Some
(HNode A h1'
(Node A
(Triple A (HNode A h11' bt11') e1
(HNode A h12'
(Node A
(Triple A
(HNode A h121' bt121')
e12
(HNode A h122' bt122'))))))) ->
bt1 <> (Leaf A).
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h1 : nat)
(bt1 : binary_tree A)
(h1' h11' h12' h121' h122' : nat)
(bt11' bt121' bt122' : binary_tree A)
(e1 e12 : A),
insert_hbt_helper A compare x (HNode A h1 bt1) =
Some
(HNode A h1'
(Node A
(Triple A (HNode A h11' bt11') e1
(HNode A h12'
(Node A
(Triple A
(HNode A h121' bt121')
e12
(HNode A h122' bt122'))))))) ->
bt1 <> (Leaf A).
Lemma to show that post the insertion of some element x in a tree which
unbalances the tree and necessitates a rotate_right_1 operation,
- the minimum element of a tree subjected to a rotate_right_1 operation is either x or the minimum element of the original tree
- the maximum element of a tree subjected to a rotate_right_1 operation is either x or the maximum element of the original tree
Lemma rotate_right_1_min_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11' h121' h122' h2 : nat)
(bt11' bt121' bt122' bt2 : binary_tree A)
(e1 e12 e : A)
(hbt1 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min1 max1 x : A),
traverse_to_check_ordered_t
A
(Triple A
(HNode A (1 + max h11' h121')
(Node A (Triple A
(HNode A h11' bt11')
e1
(HNode A h121' bt121'))))
e12
(HNode A (1 + max h122' h2)
(Node A (Triple A
(HNode A h122' bt122')
e
(HNode A h2 bt2))))) compare =
TSome (A * A) (t_min', t_max') ->
traverse_to_check_ordered_t A (Triple A hbt1 e (HNode A h2 bt2)) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt1 compare = TSome (A * A) (min1, max1) ->
t_min' = x \/ t_min' = min1 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11' h121' h122' h2 : nat)
(bt11' bt121' bt122' bt2 : binary_tree A)
(e1 e12 e : A)
(hbt1 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min1 max1 x : A),
traverse_to_check_ordered_t
A
(Triple A
(HNode A (1 + max h11' h121')
(Node A (Triple A
(HNode A h11' bt11')
e1
(HNode A h121' bt121'))))
e12
(HNode A (1 + max h122' h2)
(Node A (Triple A
(HNode A h122' bt122')
e
(HNode A h2 bt2))))) compare =
TSome (A * A) (t_min', t_max') ->
traverse_to_check_ordered_t A (Triple A hbt1 e (HNode A h2 bt2)) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt1 compare = TSome (A * A) (min1, max1) ->
t_min' = x \/ t_min' = min1 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).
Lemma to show that if a tree subject to rotate_right_2 (single rotation)
is ordered, then the original subtree into which an element was inserted was also
ordered
Lemma rotate_right_2_tree_ordered_implies_returned_tree_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1' h11' h12' h2 : nat)
(bt11' bt12' bt2 : binary_tree A)
(e1 e : A)
(t_min' t_max' : A),
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') ->
exists t_max'',
traverse_to_check_ordered_hbt
A
(HNode A h1'
(Node A (Triple A (HNode A h11' bt11') e1 (HNode A h12' bt12'))))
compare = TSome (A * A) (t_min', t_max'').
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1' h11' h12' h2 : nat)
(bt11' bt12' bt2 : binary_tree A)
(e1 e : A)
(t_min' t_max' : A),
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') ->
exists t_max'',
traverse_to_check_ordered_hbt
A
(HNode A h1'
(Node A (Triple A (HNode A h11' bt11') e1 (HNode A h12' bt12'))))
compare = TSome (A * A) (t_min', t_max'').
The lemmas rotate_right_2_impossible_case_1 and
rotate_right_2_impossible_case_2 concern the two sub-cases which arise in case of
the rotate_right_2 operation, and show that if an insertion operation led to
a rotate_right_2 operation, then the subtree on which the insertion operation
was performed cannot be a leaf
Lemma rotate_right_2_impossible_case_1:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h1 : nat)
(bt1 : binary_tree A)
(h1' h11' h12' : nat)
(bt11' bt12' : binary_tree A)
(e1 : A),
insert_hbt_helper A compare x (HNode A h1 bt1) =
Some
(HNode A h1'
(Node A
(Triple A
(HNode A h11' bt11')
e1
(HNode A h12' bt12')))) ->
(h12' + 1 =n= h11') = true ->
bt1 <> (Leaf A).
Lemma rotate_right_2_impossible_case_2:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h1 : nat)
(bt1 : binary_tree A)
(h1' h11' h12' : nat)
(bt11' bt12' : binary_tree A)
(e1 : A)
(h2 : nat)
(bt2 : binary_tree A),
is_sound_hbt A (HNode A h1 bt1) = true ->
is_balanced_hbt A (HNode A h1 bt1) = true ->
insert_hbt_helper A compare x (HNode A h1 bt1) =
Some
(HNode A h1' (Node A (Triple A
(HNode A h11' bt11')
e1
(HNode A h12' bt12')))) ->
(h12' =n= h11') = true ->
compare_int h1' (2 + project_height_hbt A (HNode A h2 bt2)) = Eq ->
bt1 <> (Leaf A).
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h1 : nat)
(bt1 : binary_tree A)
(h1' h11' h12' : nat)
(bt11' bt12' : binary_tree A)
(e1 : A),
insert_hbt_helper A compare x (HNode A h1 bt1) =
Some
(HNode A h1'
(Node A
(Triple A
(HNode A h11' bt11')
e1
(HNode A h12' bt12')))) ->
(h12' + 1 =n= h11') = true ->
bt1 <> (Leaf A).
Lemma rotate_right_2_impossible_case_2:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h1 : nat)
(bt1 : binary_tree A)
(h1' h11' h12' : nat)
(bt11' bt12' : binary_tree A)
(e1 : A)
(h2 : nat)
(bt2 : binary_tree A),
is_sound_hbt A (HNode A h1 bt1) = true ->
is_balanced_hbt A (HNode A h1 bt1) = true ->
insert_hbt_helper A compare x (HNode A h1 bt1) =
Some
(HNode A h1' (Node A (Triple A
(HNode A h11' bt11')
e1
(HNode A h12' bt12')))) ->
(h12' =n= h11') = true ->
compare_int h1' (2 + project_height_hbt A (HNode A h2 bt2)) = Eq ->
bt1 <> (Leaf A).
Lemma to show that post the insertion of some element x in a tree which
unbalances the tree,
- the minimum element of a tree subjected to a rotate_right_2 operation is either
x
or the minimum element of the original tree - the maximum element of a tree subjected to a rotate_right_2 operation is either
x
or the maximum element of the original tree
Lemma rotate_right_2_min_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11' h12' h2 : nat)
(bt11' bt12' bt2 : binary_tree A)
(e1 e : A)
(hbt1 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min1 max1 x : A),
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') ->
traverse_to_check_ordered_t A (Triple A hbt1 e (HNode A h2 bt2)) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt1 compare = TSome (A * A) (min1, max1) ->
t_min' = x \/ t_min' = min1 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h11' h12' h2 : nat)
(bt11' bt12' bt2 : binary_tree A)
(e1 e : A)
(hbt1 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min1 max1 x : A),
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') ->
traverse_to_check_ordered_t A (Triple A hbt1 e (HNode A h2 bt2)) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt1 compare = TSome (A * A) (min1, max1) ->
t_min' = x \/ t_min' = min1 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).
Left Rotation Lemmas
rotate_left_1and the rotate_left_2 cases
Lemma rotate_left_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(t_min t_max min2 max2 t_max' x : A),
traverse_to_check_ordered_t A (Triple A (HNode A h1 bt1) e hbt2) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt2 compare = TSome (A * A) (min2, max2) ->
t_max' = x \/ t_max' = max2 ->
(t_max' = x \/ t_max' = t_max).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(t_min t_max min2 max2 t_max' x : A),
traverse_to_check_ordered_t A (Triple A (HNode A h1 bt1) e hbt2) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt2 compare = TSome (A * A) (min2, max2) ->
t_max' = x \/ t_max' = max2 ->
(t_max' = x \/ t_max' = t_max).
Lemma to show that post an insertion operation on a tree which necessitates a
left rotation rebalance operation, the minimum element of a left rotated tree
is either
- the element originally inserted
- or the minimum value of the subtree on which the insertion operation was
Lemma rotate_left_min:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h_rot_root : nat)
(h_rot_left : nat)
(hbt_left : heightened_binary_tree A)
(e' : A)
(hbt_right : heightened_binary_tree A)
(e : A)
(min' : A)
(h_org : nat)
(min : A),
traverse_to_check_ordered_hbt
A
(HNode A h_rot_root
(Node A
(Triple A
(HNode A
h_rot_left
(Node A
(Triple A hbt_left e' hbt_right)))
e
(HNode A 0 (Leaf A))))) compare =
TSome (A * A) (min', e) ->
traverse_to_check_ordered_hbt
A (HNode A h_org
(Node A (Triple A hbt_left e' (HNode A 0 (Leaf A)))))
compare = TSome (A * A) (min, e') ->
min' = min.
forall (A : Type)
(compare : A -> A -> element_comparison)
(h_rot_root : nat)
(h_rot_left : nat)
(hbt_left : heightened_binary_tree A)
(e' : A)
(hbt_right : heightened_binary_tree A)
(e : A)
(min' : A)
(h_org : nat)
(min : A),
traverse_to_check_ordered_hbt
A
(HNode A h_rot_root
(Node A
(Triple A
(HNode A
h_rot_left
(Node A
(Triple A hbt_left e' hbt_right)))
e
(HNode A 0 (Leaf A))))) compare =
TSome (A * A) (min', e) ->
traverse_to_check_ordered_hbt
A (HNode A h_org
(Node A (Triple A hbt_left e' (HNode A 0 (Leaf A)))))
compare = TSome (A * A) (min, e') ->
min' = min.
Lemma to show that if a tree subject to rotate_left_1 (double rotation)
is ordered, then the original subtree into which an element was inserted was also
ordered
Lemma rotate_left_1_tree_ordered_implies_returned_tree_ordered:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 h211' h212' h22' h2' h21' : nat)
(bt1 bt211' bt212' bt22' : binary_tree A)
(e e21 e2 t_min' t_max' : A),
traverse_to_check_ordered_hbt
A
(HNode A (1 + max (1 + max h1 h211') (1 + max h212' h22'))
(Node A
(Triple A
(HNode A (1 + max h1 h211')
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A h211' bt211'))))
e21
(HNode A (1 + max h212' h22')
(Node A (Triple A
(HNode A h212' bt212')
e2
(HNode A h22' bt22')))))))
compare = TSome (A * A) (t_min', t_max') ->
exists t_min'',
traverse_to_check_ordered_hbt
A
(HNode A h2'
(Node A
(Triple A
(HNode A h21'
(Node A
(Triple A
(HNode A h211' bt211')
e21
(HNode A h212' bt212'))))
e2
(HNode A h22' bt22'))))
compare = TSome (A * A) (t_min'', t_max').
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 h211' h212' h22' h2' h21' : nat)
(bt1 bt211' bt212' bt22' : binary_tree A)
(e e21 e2 t_min' t_max' : A),
traverse_to_check_ordered_hbt
A
(HNode A (1 + max (1 + max h1 h211') (1 + max h212' h22'))
(Node A
(Triple A
(HNode A (1 + max h1 h211')
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A h211' bt211'))))
e21
(HNode A (1 + max h212' h22')
(Node A (Triple A
(HNode A h212' bt212')
e2
(HNode A h22' bt22')))))))
compare = TSome (A * A) (t_min', t_max') ->
exists t_min'',
traverse_to_check_ordered_hbt
A
(HNode A h2'
(Node A
(Triple A
(HNode A h21'
(Node A
(Triple A
(HNode A h211' bt211')
e21
(HNode A h212' bt212'))))
e2
(HNode A h22' bt22'))))
compare = TSome (A * A) (t_min'', t_max').
Lemma to show that if an insertion operation led to a rotate_left_1
operation, then the subtree on which the insertion operation was performed cannot
be a leaf
Lemma rotate_left_1_impossible_case:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h2 : nat)
(bt2 : binary_tree A)
(h2' h21' h211' h212' h22' : nat)
(bt211' bt212' bt22' : binary_tree A)
(e21 e2 : A),
insert_hbt_helper A compare x (HNode A h2 bt2) =
Some
(HNode A h2'
(Node A
(Triple A
(HNode A h21'
(Node A
(Triple A
(HNode A h211' bt211')
e21
(HNode A h212' bt212'))))
e2
(HNode A h22' bt22')))) -> bt2 <> Leaf A.
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h2 : nat)
(bt2 : binary_tree A)
(h2' h21' h211' h212' h22' : nat)
(bt211' bt212' bt22' : binary_tree A)
(e21 e2 : A),
insert_hbt_helper A compare x (HNode A h2 bt2) =
Some
(HNode A h2'
(Node A
(Triple A
(HNode A h21'
(Node A
(Triple A
(HNode A h211' bt211')
e21
(HNode A h212' bt212'))))
e2
(HNode A h22' bt22')))) -> bt2 <> Leaf A.
Lemma to show that post the insertion of some element x in a tree which
unbalances the tree and necessitates a rotate_right_1 operation,
- the minimum element of a tree subjected to a rotate_left_1 operation is either
x
or the minimum element of the original tree - the maximum element of a tree subjected to a rotate_left_1 operation is either
x
or the maximum element of the original tree
Lemma rotate_left_1_min_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 h211' h212' h22' : nat)
(bt1 bt211' bt212' bt22' : binary_tree A)
(e e21 e2 : A)
(hbt2 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min2 max2 x : A),
traverse_to_check_ordered_hbt
A
(HNode A (1 + max (1 + max h1 h211') (1 + max h212' h22'))
(Node A
(Triple A
(HNode A (1 + max h1 h211')
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A h211' bt211'))))
e21
(HNode A (1 + max h212' h22')
(Node A (Triple A
(HNode A h212' bt212')
e2
(HNode A h22' bt22')))))))
compare = TSome (A * A) (t_min', t_max') ->
traverse_to_check_ordered_t A (Triple A (HNode A h1 bt1) e hbt2) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt2 compare =
TSome (A * A) (min2, max2) ->
t_max' = x \/ t_max' = max2 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 h211' h212' h22' : nat)
(bt1 bt211' bt212' bt22' : binary_tree A)
(e e21 e2 : A)
(hbt2 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min2 max2 x : A),
traverse_to_check_ordered_hbt
A
(HNode A (1 + max (1 + max h1 h211') (1 + max h212' h22'))
(Node A
(Triple A
(HNode A (1 + max h1 h211')
(Node A (Triple A
(HNode A h1 bt1)
e
(HNode A h211' bt211'))))
e21
(HNode A (1 + max h212' h22')
(Node A (Triple A
(HNode A h212' bt212')
e2
(HNode A h22' bt22')))))))
compare = TSome (A * A) (t_min', t_max') ->
traverse_to_check_ordered_t A (Triple A (HNode A h1 bt1) e hbt2) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt2 compare =
TSome (A * A) (min2, max2) ->
t_max' = x \/ t_max' = max2 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).
Lemma to show that if a tree subject to rotate_left_2 (single rotation)
is ordered, then the original subtree into which an element was inserted was also
ordered
Lemma rotate_left_2_tree_ordered_implies_returned_tree_ordered:
forall (A : Type)
(compare : A -> A ->element_comparison)
(h1 h21' h22' h2' : nat)
(bt1 bt21' bt22' : binary_tree A)
(e e2 : A)
(t_min' t_max' : A),
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') ->
exists t_min'',
traverse_to_check_ordered_hbt
A
(HNode A h2'
(Node A (Triple A
(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 h21' h22' h2' : nat)
(bt1 bt21' bt22' : binary_tree A)
(e e2 : A)
(t_min' t_max' : A),
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') ->
exists t_min'',
traverse_to_check_ordered_hbt
A
(HNode A h2'
(Node A (Triple A
(HNode A h21' bt21')
e2
(HNode A h22' bt22')))) compare =
TSome (A * A) (t_min'', t_max').
The lemmas rotate_left_2_impossible_case_1 and
rotate_left_2_impossible_case_2 concern the two sub-cases which arise in case of
the rotate_left_2 operation, and show that if an insertion operation led to
a rotate_left_2 operation, then the subtree on which the insertion operation
was performed cannot be a leaf
Lemma rotate_left_2_impossible_case_1:
forall (A :Type)
(compare : A -> A -> element_comparison)
(x : A)
(h2 : nat)
(bt2 : binary_tree A)
(h2' h21' h22' : nat)
(bt21' bt22' : binary_tree A)
(e2 : A),
insert_hbt_helper A compare x (HNode A h2 bt2) =
Some
(HNode A h2'
(Node A (Triple A (HNode A h21' bt21') e2 (HNode A h22' bt22')))) ->
(h21' + 1 =n= h22') = true ->
bt2 <> Leaf A.
Lemma rotate_left_2_impossible_case_2:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h2 : nat)
(bt2 : binary_tree A)
(h2' h21' h22' : nat)
(e2 : A)
(bt21' bt22' : binary_tree A)
(h1 : nat)
(bt1 : binary_tree A),
is_sound_hbt A (HNode A h2 bt2) = true ->
is_balanced_hbt A (HNode A h2 bt2) = true ->
insert_hbt_helper A compare x (HNode A h2 bt2) =
Some
(HNode A h2'
(Node A (Triple A (HNode A h21' bt21') e2 (HNode A h22' bt22')))) ->
(h21' =n= h22') = true ->
compare_int h2' (2 + project_height_hbt A (HNode A h1 bt1)) = Eq ->
bt2 <> Leaf A.
forall (A :Type)
(compare : A -> A -> element_comparison)
(x : A)
(h2 : nat)
(bt2 : binary_tree A)
(h2' h21' h22' : nat)
(bt21' bt22' : binary_tree A)
(e2 : A),
insert_hbt_helper A compare x (HNode A h2 bt2) =
Some
(HNode A h2'
(Node A (Triple A (HNode A h21' bt21') e2 (HNode A h22' bt22')))) ->
(h21' + 1 =n= h22') = true ->
bt2 <> Leaf A.
Lemma rotate_left_2_impossible_case_2:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h2 : nat)
(bt2 : binary_tree A)
(h2' h21' h22' : nat)
(e2 : A)
(bt21' bt22' : binary_tree A)
(h1 : nat)
(bt1 : binary_tree A),
is_sound_hbt A (HNode A h2 bt2) = true ->
is_balanced_hbt A (HNode A h2 bt2) = true ->
insert_hbt_helper A compare x (HNode A h2 bt2) =
Some
(HNode A h2'
(Node A (Triple A (HNode A h21' bt21') e2 (HNode A h22' bt22')))) ->
(h21' =n= h22') = true ->
compare_int h2' (2 + project_height_hbt A (HNode A h1 bt1)) = Eq ->
bt2 <> Leaf A.
Lemma to show that post the insertion of some element x in a tree which
unbalances the tree,
- the minimum element of a tree subjected to a rotate_left_2 operation is either x or the minimum element of the original tree
- the maximum element of a tree subjected to a rotate_left_2 operation is either x or the maximum element of the original tree
Lemma rotate_left_2_min_max:
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 h21' h22' : nat)
(bt1 bt21' bt22' : binary_tree A)
(e e2 : A)
(hbt2 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min2 max2 x : A),
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') ->
traverse_to_check_ordered_t A (Triple A (HNode A h1 bt1) e hbt2) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt2 compare = TSome (A * A) (min2, max2) ->
t_max' = x \/ t_max' = max2 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).
forall (A : Type)
(compare : A -> A -> element_comparison)
(h1 h21' h22' : nat)
(bt1 bt21' bt22' : binary_tree A)
(e e2 : A)
(hbt2 : heightened_binary_tree A)
(t_min' t_max' t_min t_max min2 max2 x : A),
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') ->
traverse_to_check_ordered_t A (Triple A (HNode A h1 bt1) e hbt2) compare =
TSome (A * A) (t_min, t_max) ->
traverse_to_check_ordered_hbt A hbt2 compare = TSome (A * A) (min2, max2) ->
t_max' = x \/ t_max' = max2 ->
(t_max' = x \/ t_max' = t_max) /\ (t_min' = x \/ t_min' = t_min).