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

Lemma to show that post an operation on a tree to insert some element x:
  • 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)).



Rotations Preserves Order

When dealing with rotations in ordered_helper, the notions of a first rotation and a second rotation were used to refer to the double and single rotations. While this corresponds to the way rotations are treated in the implementation of rotations in hbt, the resulting proofs were repetitive and long. Thus, in this section, we instead develop our proofs with the following ideas in mind:
  • 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

Lemma to show that given two sub-trees hbt1, hbt2 and a payload e such that:
  • 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,
    then the tree with e as root, hbt1 as left sub-tree and hbt2 as right sub-tree is ordered, i.e., traversing the tree to check if it is ordered returns a minimum and maximum
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).

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,
    then the tree with e as root, hbt1 as left sub-tree and hbt2 as right sub-tree is ordered, i.e., traversing the tree to check if it is ordered returns a minimum and maximum
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).

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).

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).



Main Lemmas for Rotations

Lemma to show that post an insertion operation on the left sub-tree of a given tree such that the resultant tree is unbalanced, and assuming:
  • 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,
applying rotate_right_hbt on this unbalanced tree returns a tree which is ordered
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.

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:
  • 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,
applying rotate_left_hbt on this unbalanced tree returns a tree which is ordered
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.




Insertion Preserves Order

This lemma is the most important in this library, and shows that inserting an element into an ordered AVL tree gives results in an AVL tree which is ordered. The proof makes use of:
  • 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).