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 to show that an ordered triple must have ordered subtrees
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.

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.

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.

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

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.

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.

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

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

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.

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.



Orderedness Lemmas Concerning Insertion

This section contains the orderedness lemmas directly related to the insertion operation. It is divided into 3 subsections, all 3 of which are concerned with the maximum and minimum elements in an AVL tree after insertion. These lemmas are required since the predicate to check orderedness relies on finding the maximum and minimum payloads for sub-trees and comparing them to payloads.


Impossible Insertion Case

Lemma to show that a tree cannot be a leaf if an element is inserted into it
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).

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.



General Lemmas Concerning the Minimum and Maximum Payloads in an AVL Tree

Lemma to show that an element inserted into a leaf will be both its minimum and its maximum element
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.

Lemma to show that a tree that is not a leaf and is ordered has a maximum and a

minimum element

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



Right Rotation Lemmas

Lemma to show that the maximum element of a right rotated tree is the same as the maximum element of the left reduced form of the original sub-tree into which the insertion was performed. Note that because the lemma can be used in both the 
rotate_right_1
and 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.

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

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

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

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

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

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

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



Left Rotation Lemmas

Lemma to show that the maximum element of a left rotated tree is the same as the maximum element of the left reduced form of the original sub-tree into which the insertion was performed. Note that because the lemma can be used in both the 
rotate_left_1
and 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).

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

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

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.

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

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

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.

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