Library balanced


The balanced library contains lemmas concerning the balancedness property of AVL trees

Require Import Hbt.Lemmas.Sound.sound.
Require Export Hbt.Lemmas.Sound.sound.


General Lemmas Concerning Balancedness

Lemma to show that given a balanced triple, its constituent heightened_binary_trees should also be balanced
Lemma triple_balanced_implies_hbts_balanced:
  forall (A : Type)
         (h_hbt : nat)
         (hbt1 : heightened_binary_tree A)
         (e : A)
         (hbt2 : heightened_binary_tree A),
    is_balanced_hbt A (HNode A h_hbt (Node A (Triple A hbt1 e hbt2))) = true ->
    is_balanced_hbt A hbt1 = true /\ is_balanced_hbt A hbt2 = true.

Lemma to show that if the helper function to check the balancedness of a heightened_binary_tree returns Some value, then the helper function to check the balancedness of the binary_tree returns the same value
Lemma traverse_to_check_balanced_hbt_bt_same:
  forall (A : Type)
         (h h_hbt : nat)
         (bt : binary_tree A),
    traverse_to_check_balanced_hbt A (HNode A h bt) = Some h_hbt ->
    traverse_to_check_balanced_bt A bt = Some h_hbt.

Lemma to show that if the helper function to check the balancedness of a binary_tree returns Some value, then the helper function to check the balancedness of the triple returns the same value
Lemma traverse_to_check_balanced_bt_t_same:
  forall (A : Type)
         (h_hbt : nat)
         (t : triple A),
    traverse_to_check_balanced_bt A (Node A t) = Some h_hbt ->
    traverse_to_check_balanced_t A t = Some h_hbt.



Relating Balancedness to Other Properties

Lemma to show that the heights returned by the helper functions to check for soundness and balancedness are the same
Lemma relating_soundness_and_balancedness:
  forall (A : Type),
    (forall (hbt : heightened_binary_tree A)
            (h_sound h_bal : nat),
        traverse_to_check_soundness_hbt A hbt = Some h_sound ->
        traverse_to_check_balanced_hbt A hbt = Some h_bal ->
        h_sound = h_bal)
    /\
    (forall (bt : binary_tree A)
            (h_sound h_bal : nat),
        traverse_to_check_soundness_bt A bt = Some h_sound ->
        traverse_to_check_balanced_bt A bt = Some h_bal ->
        h_sound = h_bal)
    /\
    (forall (t : triple A)
            (h_sound h_bal : nat),
        traverse_to_check_soundness_t A t = Some h_sound ->
        traverse_to_check_balanced_t A t = Some h_bal ->
        h_sound = h_bal).

Lemma to show that if an AVL tree is sound and balanced, then it must have Some height
Lemma balanced_implies_some_height:
  forall (A : Type)
         (h : nat)
         (bt : binary_tree A),
    is_sound_hbt A (HNode A h bt) = true ->
    is_balanced_hbt A (HNode A h bt) = true ->
    traverse_to_check_balanced_hbt A (HNode A h bt) = Some h.

Lemma to relate the projected height of a heightened_binary_tree to that returned by the helper function to check for soundness
Lemma relating_soundness_and_projection:
  forall (A : Type)
         (hbt : heightened_binary_tree A)
         (h_ret : nat),
    traverse_to_check_soundness_hbt A hbt = Some h_ret ->
    project_height_hbt A hbt = h_ret.



Lemmas Concerning the differ_by_one Predicate

Lemma to show that a nat value differs from itself by one
Lemma same_nat_differs_by_one:
  forall (n : nat),
    differ_by_one n n = true.

Lemma to show the a nat value and its successor differ by one
Lemma nat_and_succ_nat_differ_by_one:
  forall (n : nat),
    differ_by_one (1 + n) n = true.

Lemma to show the differ_by_one predicate is symmetric
Lemma differ_by_one_symm:
  forall (x y : nat),
    differ_by_one x y = differ_by_one y x.

Lemma to show that if a tree is sound and balanced, then its sub-trees should differ by one in height
Lemma sound_and_balanced_imply_differ_by_one:
  forall (A : Type)
         (h_hbt : nat)
         (h1 : nat)
         (bt1 : binary_tree A)
         (e : A)
         (h2 : nat)
         (bt2 : binary_tree A),
    is_sound_hbt A (HNode A h_hbt (Node A (Triple A
                                                  (HNode A h1 bt1)
                                                  e
                                                  (HNode A h2 bt2)))) = true ->
    is_balanced_hbt A (HNode A h_hbt (Node A (Triple A
                                                     (HNode A h1 bt1)
                                                     e
                                                     (HNode A h2 bt2)))) = true ->
    differ_by_one h1 h2 = true.

Lemma to show that a height and two more than the height cannot differ by one
Lemma differ_by_one_false:
  forall (h : nat),
    differ_by_one (2 + h) h = false.



Balancedness Lemmas Concerning Insertion

This section contains the lemmas directly concerned with our implementation of insertion. They build up to the main lemma concerning the preservation of balance after insertion (dealt with in the next section


Lemmas Not Involving Rotations


Lemma right_insert_differ_by_one:
  forall (h1 h2 h_ret : nat),
    differ_by_one h1 h2 = true ->
    (h_ret = h2) \/ (h_ret = 1 + h2) ->
    compare_int h_ret (2 + h1) = Lt ->
    differ_by_one h1 h_ret = true.

Lemma left_insert_differ_by_one:
  forall (h1 : nat)
         (h2 : nat)
         (h_ret : nat),
    differ_by_one h1 h2 = true ->
    h_ret = h1 \/ h_ret = 1 + h1 ->
    compare_int h_ret (2 + h2) = Lt ->
    differ_by_one h_ret h2 = true.



Lemmas Concerning Rotate Right

The following 4 lemmas, rotate_right_differ_by_one_1, rotate_right_differ_by_one_2, rotate_right_differ_by_one_3, and rotate_right_differ_by_one_4, are helper lemmas to prove that right rotations preserve balance. They deal with very specific propositions that must be proved to prove the main balanced preservation theorem, and as such involve tedious but routine arithmetic rewrites
Lemma rotate_right_differ_by_one_1:
  forall (h121 h122 h11 h12: nat),
    h12 = 1 + max h121 h122 ->
    h11 + 1 = h12 ->
    differ_by_one h121 h122 = true ->
    differ_by_one h11 (1 + max h121 h122) = true ->
    differ_by_one h11 h121 = true.

Lemma rotate_right_differ_by_one_2:
  forall (h121 h122 h12 h11 h_ret h2: nat),
    differ_by_one h121 h122 = true ->
    h12 = 1 + max h121 h122 ->
    h11 + 1 = h12 ->
    h_ret = 1 + max h11 h12 ->
    h_ret = 2 + h2 ->
    differ_by_one h122 h2 = true.

Lemma rotate_right_differ_by_one_3:
  forall (h121 h122 h12 h11 h_ret h2 : nat),
    differ_by_one h121 h122 = true ->
    h12 = 1 + max h121 h122 ->
    h11 + 1 = h12 ->
    h_ret = 1 + max h11 h12 ->
    h_ret = 2 + h2 ->
    differ_by_one (1 + max h11 h121) (1 + max h122 h2) = true.

Lemma rotate_right_differ_by_one_4:
  forall (h12 h11 h2 h_ret : nat),
    (h12 + 1 =n= h11) || (h12 =n= h11) = true ->
    h_ret = 2 + h2 ->
    h_ret = 1 + max h11 h12 ->
    differ_by_one h12 h2 = true /\ differ_by_one h11 (1 + max h12 h2) = true.

Lemma to show that right rotating a tree preserves balanced. The lemma assumes the soundness and balancedness of the sub-trees of the tree returned after rotation.
Lemma rotate_right_preserves_balance:
  forall (A : Type)
         (h_ret : nat)
         (bt_ret : binary_tree A)
         (e : A)
         (hbt2 : heightened_binary_tree A)
         (hbt' : heightened_binary_tree A),
    is_balanced_hbt A (HNode A h_ret bt_ret) = true ->
    is_balanced_hbt A hbt2 = true ->
    is_sound_hbt A (HNode A h_ret bt_ret) = true ->
    is_sound_hbt A hbt2 = true ->
    rotate_right_hbt A (HNode A h_ret bt_ret) e hbt2 = Some hbt' ->
    compare_int h_ret (2 + project_height_hbt A hbt2) = Eq ->
    is_balanced_hbt A hbt' = true.



Lemmas Concerning Rotate Left

The following 4 lemmas, rotate_left_differ_by_one_1, rotate_left_differ_by_one_2, rotate_left_differ_by_one_3, and rotate_left_differ_by_one_4, are helper lemmas to prove that left rotations preserve balance. They deal with very specific propositions that must be proved to prove the main balanced preservation theorem, and as such involve tedious but routine arithmetic rewrites
Lemma rotate_left_differ_by_one_1:
  forall (h1 h211 h212 : nat),
    h1 = max h211 h212 ->
    differ_by_one h211 h212 = true ->
    differ_by_one h1 h211 = true.

Lemma rotate_left_differ_by_one_2:
  forall (h211 h212 h22 : nat),
    differ_by_one h211 h212 = true ->
    h22 = max h211 h212 ->
    differ_by_one h212 h22 = true.

Lemma rotate_left_differ_by_one_3:
  forall (h1 h211 h212 h22 : nat),
    h1 = max h211 h212 ->
    h22 = max h211 h212 ->
    differ_by_one h211 h212 = true ->
    differ_by_one (1 + max h1 h211) (1 + max h212 h22) = true.

Lemma rotate_left_differ_by_one_4:
  forall (h1 h21 h22 h_ret : nat),
    (h21 + 1 =n= h22) || (h21 =n= h22) = true ->
    h_ret = 1 + max h21 h22 ->
    h_ret = 2 + h1 ->
    differ_by_one h1 h21 = true /\ differ_by_one (1 + max h1 h21) h22 = true.

Lemma to show that left rotating a tree preserves balanced. The lemma assumes the soundness and balancedness of the sub-trees of the tree returned after rotation.
Lemma rotate_left_preserves_balance:
  forall (A : Type)
         (hbt1 : heightened_binary_tree A)
         (e : A)
         (h_ret : nat)
         (bt_ret : binary_tree A)
         (hbt' : heightened_binary_tree A),
    is_balanced_hbt A hbt1 = true ->
    is_balanced_hbt A (HNode A h_ret bt_ret) = true ->
    is_sound_hbt A hbt1 = true ->
    is_sound_hbt A (HNode A h_ret bt_ret) = true ->
    rotate_left_hbt A hbt1 e (HNode A h_ret bt_ret) = Some hbt' ->
    compare_int h_ret (2 + project_height_hbt A hbt1) = Eq ->
    is_balanced_hbt A hbt' = true.



Main Lemmas

Lemma to show that if a value is inserted into a sub-tree, and the resultant tree is balanced, then the height of the new sub-tree is either the same or one more than the height of the original sub-tree
Lemma relating_insertion_and_original_height:
  forall (A : Type)
         (compare : A -> A -> element_comparison)
         (x : A),
    (forall (hbt : heightened_binary_tree A)
            (hbt' : heightened_binary_tree A),
        insert_hbt_helper A compare x hbt = Some hbt' ->
        is_sound_hbt A hbt = true ->
        is_balanced_hbt A hbt = true ->
        is_sound_hbt A hbt' = true ->
        (project_height_hbt A hbt' = project_height_hbt A hbt)
        \/
        (project_height_hbt A hbt' = 1 + project_height_hbt A hbt))
    /\
    (forall (bt : binary_tree A)
            (h_hbt : nat)
            (hbt' : heightened_binary_tree A),
        insert_bt_helper A compare x h_hbt bt = Some hbt' ->
        is_sound_hbt A (HNode A h_hbt bt) = true ->
        is_balanced_hbt A (HNode A h_hbt bt) = true ->
        is_sound_hbt A hbt' = true ->
        (project_height_hbt A hbt' = h_hbt)
        \/
        (project_height_hbt A hbt' = 1 + h_hbt))
    /\
    (forall (t : triple A)
            (h_hbt : nat)
            (hbt' : heightened_binary_tree A),
        insert_t_helper A compare x h_hbt t = Some hbt' ->
        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_sound_hbt A hbt' = true ->
        (project_height_hbt A hbt' = h_hbt)
        \/
        (project_height_hbt A hbt' = 1 + h_hbt)).

This is the most important lemma concerning balanced in this project. It claims that inserting an element into a sound and balanced heightened_binary_tree using insert_hbt_helper returns a heightened_binary_tree which is also balanced. The proof proceeds by unfolding the insert_hbt_helper function, and performing a sequence of case analyses.
Lemma insertion_preserves_balance:
  forall (A : Type)
         (compare : A -> A -> element_comparison)
         (x : A),
    (forall (hbt : heightened_binary_tree A)
            (hbt' : heightened_binary_tree A),
        is_sound_hbt A hbt = true ->
        is_balanced_hbt A hbt = true ->
        insert_hbt_helper A compare x hbt = Some hbt' ->
        is_balanced_hbt A hbt' = 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 ->
        insert_bt_helper A compare x h_hbt bt = Some hbt' ->
        is_balanced_hbt A hbt' = 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 ->
        insert_t_helper A compare x h_hbt t = Some hbt' ->
        is_balanced_hbt A hbt' = true).