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