Library sound

The sound library contains lemmas concerning the soundness property of AVL trees

Require Import Hbt.Implementation.hbt.
Require Export Hbt.Implementation.hbt.

General Lemmas Concerning Soundness of Heightened Binary Trees

Lemma to show that if a heightened binary tree is sound, then its height is equal to 1 + max h1 h2, where h1 and h2 are the heights of its left and right subtrees respectively

Lemma relate_heights:
  forall (A : Type)
         (h_res : nat)
         (h1 : nat)
         (bt1 : binary_tree A)
         (e : A)
         (h2 : nat)
         (bt2 : binary_tree A),
    is_sound_hbt
      A
      (HNode A h_res (Node A (Triple A (HNode A h1 bt1) e (HNode A h2 bt2)))) = true ->
    h_res = 1 + max h1 h2.

Lemma to show that if a triple is sound, the heightened_binary_trees it contains should also be sound

Lemma triple_sound_implies_hbts_sound:
  forall (A : Type)
         (h_hbt : nat)
         (hbt1 : heightened_binary_tree A)
         (e : A)
         (hbt2 : heightened_binary_tree A),
    is_sound_hbt A (HNode A h_hbt (Node A (Triple A hbt1 e hbt2))) = true ->
    is_sound_hbt A hbt1 = true /\ is_sound_hbt A hbt2 = true.

Lemma to show that if the helper function to check soundness for heightened_binary_trees returns Some value, then the helper function to check soundness for binary_trees should return the same value

Lemma traverse_to_check_soundness_hbt_bt_same:
  forall (A : Type)
         (h h_hbt : nat)
         (bt : binary_tree A),
    traverse_to_check_soundness_hbt A (HNode A h bt) = Some h_hbt ->
    traverse_to_check_soundness_bt A bt = Some h_hbt.

Lemma to show that if the helper function to check soundness for binary_trees returns Some value, then the helper function to check soundness for triples should return the same value

Lemma traverse_to_check_soundness_bt_t_same:
  forall (A : Type)
         (h_hbt : nat)
         (t : triple A),
    traverse_to_check_soundness_bt A (Node A t) = Some h_hbt ->
    traverse_to_check_soundness_t A t = Some h_hbt.

Lemma to show that if a heightened_binary_tree is sound, then it should have Some height

Lemma soundness_implies_some_height:
  forall (A : Type)
         (h : nat)
         (bt : binary_tree A),
    is_sound_hbt A (HNode A h bt) = true ->
    traverse_to_check_soundness_hbt A (HNode A h bt) = Some h.

Lemma that lays the condition which must hold for the soundness of two sub-trees to imply the soundness of the tree itself. The condition is that the height stored in the heightened_binary_tree concerend should be equal to 1 + max h1 h2, where h1 is the height of the left sub-tree and h2 is the height of the right sub-tree

Lemma hbts_sound_implies_triple_sound_weak:
    forall (A : Type)
           (h_hbt : nat)
           (hbt1 : heightened_binary_tree A)
           (e : A)
           (hbt2 : heightened_binary_tree A),
      is_sound_hbt A hbt1 = true ->
      is_sound_hbt A hbt2 = true ->
      h_hbt = 1 + max (project_height_hbt A hbt1) (project_height_hbt A hbt2) ->
      is_sound_hbt A (HNode A h_hbt (Node A (Triple A hbt1 e hbt2))) = true.

Rotation Lemmas for Soundness

Lemma to show that right rotating a tree preserves soundness

Lemma rotate_right_preserves_soundness:
  forall (A : Type)
         (h_ret : nat)
         (bt_ret : binary_tree A)
         (e : A)
         (hbt2 : heightened_binary_tree A)
         (hbt' : heightened_binary_tree A),
    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' ->
    is_sound_hbt A hbt' = true.

Lemma to show that left rotating a tree preserves soundness

Lemma rotate_left_preserves_soundness:
  forall (A : Type)
         (hbt1 : heightened_binary_tree A)
         (e : A)
         (h_ret : nat)
         (bt_ret : binary_tree A)
         (hbt' : heightened_binary_tree A),
    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' ->
    is_sound_hbt A hbt' = true.

Insertion Preserves Soundness

This section contains the most important lemma concerning soundness in this project, namely, that inserting an element into a sound heightened_binary_tree using insert_hbt_helper returns a heightened_binary_tree which is also sound. The proof proceeds by unfolding the insert_hbt_helper function, and performing a sequence of case analyses.

Lemma insertion_preserves_soundness:
  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 ->
        insert_hbt_helper A compare x hbt = Some hbt' ->
        is_sound_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 ->
        insert_bt_helper A compare x h_hbt bt = Some hbt' ->
        is_sound_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 ->
        insert_t_helper A compare x h_hbt t = Some hbt' ->
        is_sound_hbt A hbt' = true).