Library hbt
This library contains the Gallina implementation of AVL trees, and the predicates
that check if the insertion operation on AVL trees preserves the AVL trees invariants.
Note that we use the terms 'heightened binary tree' (abbreviated as 'hbt') and
AVL trees interchangeably in this project
Require Import Hbt.Paraphernalia.paraphernalia.
Require Export Hbt.Paraphernalia.paraphernalia.
Require Extraction.
Tactic to prove simple unfold lemmas
Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
Inductive Type for Heightened Binary Trees
Inductive heightened_binary_tree (A : Type) : Type :=
HNode : nat -> binary_tree A -> heightened_binary_tree A
with binary_tree (A : Type) : Type :=
| Leaf : binary_tree A
| Node : triple A -> binary_tree A
with triple (A : Type) : Type :=
| Triple : heightened_binary_tree A -> A -> heightened_binary_tree A -> triple A.
HNode : nat -> binary_tree A -> heightened_binary_tree A
with binary_tree (A : Type) : Type :=
| Leaf : binary_tree A
| Node : triple A -> binary_tree A
with triple (A : Type) : Type :=
| Triple : heightened_binary_tree A -> A -> heightened_binary_tree A -> triple A.
Induction principle for the three mutually recursive types
heightened_binary_tree, binary_tree, and triple. See
https://coq.inria.fr/refman/user-extensions/proof-schemes.html
Scheme heightened_binary_tree_induction := Induction for heightened_binary_tree Sort Prop
with binary_tree_induction := Induction for binary_tree Sort Prop
with triple_induction := Induction for triple Sort Prop.
with binary_tree_induction := Induction for binary_tree Sort Prop
with triple_induction := Induction for triple Sort Prop.
Soundness of Heightened Binary Trees
Fixpoint traverse_to_check_soundness_hbt
(A : Type)
(hbt : heightened_binary_tree A) : option nat :=
match hbt with
| HNode _ h bt =>
match traverse_to_check_soundness_bt A bt with
| None =>
None
| Some h' =>
if h' =n= h
then Some h
else None
end
end
with traverse_to_check_soundness_bt
(A : Type)
(bt : binary_tree A) : option nat :=
match bt with
| Leaf _ =>
Some 0
| Node _ t =>
traverse_to_check_soundness_t A t
end
with traverse_to_check_soundness_t
(A : Type)
(t : triple A) : option nat :=
match t with
| Triple _ hbt1 _ hbt2 =>
match traverse_to_check_soundness_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_soundness_hbt A hbt2 with
| None =>
None
| Some h2 =>
Some (1 + max h1 h2)
end
end
end.
(A : Type)
(hbt : heightened_binary_tree A) : option nat :=
match hbt with
| HNode _ h bt =>
match traverse_to_check_soundness_bt A bt with
| None =>
None
| Some h' =>
if h' =n= h
then Some h
else None
end
end
with traverse_to_check_soundness_bt
(A : Type)
(bt : binary_tree A) : option nat :=
match bt with
| Leaf _ =>
Some 0
| Node _ t =>
traverse_to_check_soundness_t A t
end
with traverse_to_check_soundness_t
(A : Type)
(t : triple A) : option nat :=
match t with
| Triple _ hbt1 _ hbt2 =>
match traverse_to_check_soundness_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_soundness_hbt A hbt2 with
| None =>
None
| Some h2 =>
Some (1 + max h1 h2)
end
end
end.
Fold unfold lemma for traverse_to_check_soundness_hbt
Lemma fold_unfold_traverse_to_check_soundness_hbt:
forall (A : Type)
(h : nat)
(bt : binary_tree A),
traverse_to_check_soundness_hbt A (HNode A h bt) =
match traverse_to_check_soundness_bt A bt with
| None =>
None
| Some h' =>
if h' =n= h
then Some h
else None
end.
forall (A : Type)
(h : nat)
(bt : binary_tree A),
traverse_to_check_soundness_hbt A (HNode A h bt) =
match traverse_to_check_soundness_bt A bt with
| None =>
None
| Some h' =>
if h' =n= h
then Some h
else None
end.
Fold unfold lemma for traverse_to_check_soundness_bt when the tree is a Leaf
Lemma fold_unfold_traverse_to_check_soundness_bt_leaf:
forall (A : Type),
traverse_to_check_soundness_bt A (Leaf A) = Some 0.
forall (A : Type),
traverse_to_check_soundness_bt A (Leaf A) = Some 0.
Fold unfold lemma for traverse_to_check_soundness_bt when the tree is a Node
Lemma fold_unfold_traverse_to_check_soundness_bt_node:
forall (A : Type)
(t : triple A),
traverse_to_check_soundness_bt A (Node A t) = traverse_to_check_soundness_t A t.
forall (A : Type)
(t : triple A),
traverse_to_check_soundness_bt A (Node A t) = traverse_to_check_soundness_t A t.
Fold unfold lemma for traverse_to_check_soundness_t
Lemma fold_unfold_traverse_to_check_soundness_t:
forall (A : Type)
(hbt1 hbt2 : heightened_binary_tree A)
(e : A),
traverse_to_check_soundness_t A (Triple A hbt1 e hbt2) =
match traverse_to_check_soundness_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_soundness_hbt A hbt2 with
| None =>
None
| Some h2 =>
Some (1 + max h1 h2)
end
end.
forall (A : Type)
(hbt1 hbt2 : heightened_binary_tree A)
(e : A),
traverse_to_check_soundness_t A (Triple A hbt1 e hbt2) =
match traverse_to_check_soundness_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_soundness_hbt A hbt2 with
| None =>
None
| Some h2 =>
Some (1 + max h1 h2)
end
end.
Predicate to check the soundness of a heightened_binary_tree
Definition is_sound_hbt (A : Type) (hbt : heightened_binary_tree A) :=
match traverse_to_check_soundness_hbt A hbt with
| None =>
false
| Some _ =>
true
end.
match traverse_to_check_soundness_hbt A hbt with
| None =>
false
| Some _ =>
true
end.
Balancedness of Heightened Binary Trees
Definition differ_by_one (h1 h2 : nat) : bool :=
(h1 =n= h2 + 1) || (h2 =n= h1 + 1) || (h2 =n= h1).
(h1 =n= h2 + 1) || (h2 =n= h1 + 1) || (h2 =n= h1).
Structurally recursive helper function to traverse a heightened binary tree
and check for balancedness
Fixpoint traverse_to_check_balanced_hbt
(A : Type) (hbt : heightened_binary_tree A) : option nat :=
match hbt with
| HNode _ _ bt =>
traverse_to_check_balanced_bt A bt
end
with traverse_to_check_balanced_bt
(A : Type) (bt : binary_tree A) : option nat :=
match bt with
| Leaf _ =>
Some 0
| Node _ t =>
traverse_to_check_balanced_t A t
end
with traverse_to_check_balanced_t
(A : Type) (t : triple A) : option nat :=
match t with
| Triple _ hbt1 _ hbt2 =>
match traverse_to_check_balanced_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_balanced_hbt A hbt2 with
| None =>
None
| Some h2 =>
if differ_by_one h1 h2
then Some (1 + max h1 h2)
else None
end
end
end.
(A : Type) (hbt : heightened_binary_tree A) : option nat :=
match hbt with
| HNode _ _ bt =>
traverse_to_check_balanced_bt A bt
end
with traverse_to_check_balanced_bt
(A : Type) (bt : binary_tree A) : option nat :=
match bt with
| Leaf _ =>
Some 0
| Node _ t =>
traverse_to_check_balanced_t A t
end
with traverse_to_check_balanced_t
(A : Type) (t : triple A) : option nat :=
match t with
| Triple _ hbt1 _ hbt2 =>
match traverse_to_check_balanced_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_balanced_hbt A hbt2 with
| None =>
None
| Some h2 =>
if differ_by_one h1 h2
then Some (1 + max h1 h2)
else None
end
end
end.
Fold unfold lemma for traverse_to_check_balanced_hbt
Lemma fold_unfold_traverse_to_check_balanced_hbt:
forall (A : Type)
(h : nat)
(bt : binary_tree A),
traverse_to_check_balanced_hbt A (HNode A h bt) = traverse_to_check_balanced_bt A bt.
forall (A : Type)
(h : nat)
(bt : binary_tree A),
traverse_to_check_balanced_hbt A (HNode A h bt) = traverse_to_check_balanced_bt A bt.
Fold unfold lemma for traverse_to_check_balanced_bt, when the tree is a Leaf
Lemma fold_unfold_traverse_to_check_balanced_bt_leaf:
forall (A : Type),
traverse_to_check_balanced_bt A (Leaf A) = Some 0.
forall (A : Type),
traverse_to_check_balanced_bt A (Leaf A) = Some 0.
Fold unfold lemma for traverse_to_check_balanced_bt, when the tree is a Node
Lemma fold_unfold_traverse_to_check_balanced_bt_node:
forall (A : Type)
(t : triple A),
traverse_to_check_balanced_bt A (Node A t) = traverse_to_check_balanced_t A t.
forall (A : Type)
(t : triple A),
traverse_to_check_balanced_bt A (Node A t) = traverse_to_check_balanced_t A t.
Fold unfold lemma for traverse_to_check_balanced_t
Lemma fold_unfold_traverse_to_check_balanced_t:
forall (A : Type)
(hbt1 hbt2 : heightened_binary_tree A)
(e : A),
traverse_to_check_balanced_t A (Triple A hbt1 e hbt2) =
match traverse_to_check_balanced_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_balanced_hbt A hbt2 with
| None =>
None
| Some h2 =>
if differ_by_one h1 h2
then Some (1 + max h1 h2)
else None
end
end.
forall (A : Type)
(hbt1 hbt2 : heightened_binary_tree A)
(e : A),
traverse_to_check_balanced_t A (Triple A hbt1 e hbt2) =
match traverse_to_check_balanced_hbt A hbt1 with
| None =>
None
| Some h1 =>
match traverse_to_check_balanced_hbt A hbt2 with
| None =>
None
| Some h2 =>
if differ_by_one h1 h2
then Some (1 + max h1 h2)
else None
end
end.
Predicate to check the balancedness of a heightened_binary_tree
Definition is_balanced_hbt (A : Type) (hbt : heightened_binary_tree A) :=
match traverse_to_check_balanced_hbt A hbt with
| None =>
false
| Some h =>
true
end.
match traverse_to_check_balanced_hbt A hbt with
| None =>
false
| Some h =>
true
end.
Orderedness of Heightened Binary Trees
Inductive triple_option (A : Type) : Type :=
| TError : triple_option A
| TNone : triple_option A
| TSome : A -> triple_option A.
| TError : triple_option A
| TNone : triple_option A
| TSome : A -> triple_option A.
Lemma to show that the equality values constructed with the TSome constructor
is equivalent to the equality of the values contained by the TSome] constructor
Lemma tsome_x_equal_tsome_y:
forall (A : Type)
(x y : A),
TSome A x = TSome A y <-> x = y.
forall (A : Type)
(x y : A),
TSome A x = TSome A y <-> x = y.
Structurally recursive helper function to check if a heightened binary tree is
ordered. The algorithm is non-trivial and warrants discussion. The function
traverses a heightened binary tree structurally, and does the following:
- Base case: When a Leaf is encountered, the function returns a TNone value which captures the notion that a Leaf has no maximum or minimum values
- Inductive case: When a triple of the form hbt1 e hbt2 is encountered, then the function recursively traverses hbt1 and hbt2, returning either a TNone (if the sub-tree is a Leaf), or a TSome value containing a pair with the maximum and minimum payloads. The function then checks if compare max1 e = Lt and compare e min2 = Lt, where compare is comparison function that defines an ordering on the type of the payloads, and max1 is the maximum value of hbt1. If the two comparisons are true, then the function returns TSome (min1, max2) as the minimum and maximum values of the node. Note that if one of the sub-trees is a Leaf, then the payload e itself becomes the minimum/maximum value
Fixpoint traverse_to_check_ordered_hbt
(A : Type)
(hbt : heightened_binary_tree A)
(compare : A -> A -> element_comparison) : triple_option (A * A) :=
match hbt with
| HNode _ h bt =>
traverse_to_check_ordered_bt A bt compare
end
with traverse_to_check_ordered_bt
(A : Type)
(bt : binary_tree A)
(compare : A -> A -> element_comparison) : triple_option (A * A) :=
match bt with
| Leaf _ =>
TNone (A * A)
| Node _ t =>
traverse_to_check_ordered_t A t compare
end
with traverse_to_check_ordered_t
(A : Type)
(t : triple A)
(compare : A -> A -> element_comparison) : triple_option (A * A) :=
match t with
| Triple _ hbt1 e hbt2 =>
match traverse_to_check_ordered_hbt A hbt1 compare with
| TError _ =>
TError (A * A)
| TNone _ =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ =>
TError (A * A)
| TNone _ =>
TSome (A * A) (e, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt =>
TSome (A * A) (e, max2)
| Eq =>
TError (A * A)
| Gt =>
TError (A * A)
end
end
| TSome _ (min1, max1) =>
match compare max1 e with
| Lt =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ =>
TError (A * A)
| TNone _ =>
TSome (A * A) (min1, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt =>
TSome (A * A) (min1, max2)
| Eq =>
TError (A * A)
| Gt =>
TError (A * A)
end
end
| Eq =>
TError (A * A)
| Gt =>
TError (A * A)
end
end
end.
(A : Type)
(hbt : heightened_binary_tree A)
(compare : A -> A -> element_comparison) : triple_option (A * A) :=
match hbt with
| HNode _ h bt =>
traverse_to_check_ordered_bt A bt compare
end
with traverse_to_check_ordered_bt
(A : Type)
(bt : binary_tree A)
(compare : A -> A -> element_comparison) : triple_option (A * A) :=
match bt with
| Leaf _ =>
TNone (A * A)
| Node _ t =>
traverse_to_check_ordered_t A t compare
end
with traverse_to_check_ordered_t
(A : Type)
(t : triple A)
(compare : A -> A -> element_comparison) : triple_option (A * A) :=
match t with
| Triple _ hbt1 e hbt2 =>
match traverse_to_check_ordered_hbt A hbt1 compare with
| TError _ =>
TError (A * A)
| TNone _ =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ =>
TError (A * A)
| TNone _ =>
TSome (A * A) (e, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt =>
TSome (A * A) (e, max2)
| Eq =>
TError (A * A)
| Gt =>
TError (A * A)
end
end
| TSome _ (min1, max1) =>
match compare max1 e with
| Lt =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ =>
TError (A * A)
| TNone _ =>
TSome (A * A) (min1, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt =>
TSome (A * A) (min1, max2)
| Eq =>
TError (A * A)
| Gt =>
TError (A * A)
end
end
| Eq =>
TError (A * A)
| Gt =>
TError (A * A)
end
end
end.
Fold unfold lemma for traverse_to_check_ordered_hbt
Lemma fold_unfold_traverse_to_check_ordered_hbt:
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 =
traverse_to_check_ordered_bt A bt compare.
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 =
traverse_to_check_ordered_bt A bt compare.
Fold unfold lemma for traverse_to_check_ordered_bt, when the tree is a Leaf
Lemma fold_unfold_traverse_to_check_ordered_bt_leaf:
forall (A : Type)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_bt A (Leaf A) compare =
TNone (A * A).
forall (A : Type)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_bt A (Leaf A) compare =
TNone (A * A).
Fold unfold lemma for traverse_to_check_ordered_bt, when the tree is a Node
Lemma fold_unfold_traverse_to_check_ordered_bt_node:
forall (A : Type)
(t : triple A)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_bt A (Node A t) compare =
traverse_to_check_ordered_t A t compare.
forall (A : Type)
(t : triple A)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_bt A (Node A t) compare =
traverse_to_check_ordered_t A t compare.
Fold unfold lemma for traverse_to_check_ordered_t
Lemma fold_unfold_traverse_to_check_ordered_t:
forall (A : Type)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_t A (Triple A hbt1 e hbt2) compare =
match traverse_to_check_ordered_hbt A hbt1 compare with
| TError _ => TError (A * A)
| TNone _ =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ => TError (A * A)
| TNone _ => TSome (A * A) (e, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt => TSome (A * A) (e, max2)
| Eq => TError (A * A)
| Gt => TError (A * A)
end
end
| TSome _ (min1, max1) =>
match compare max1 e with
| Lt =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ => TError (A * A)
| TNone _ => TSome (A * A) (min1, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt => TSome (A * A) (min1, max2)
| Eq => TError (A * A)
| Gt => TError (A * A)
end
end
| Eq => TError (A * A)
| Gt => TError (A * A)
end
end.
forall (A : Type)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A)
(compare : A -> A -> element_comparison),
traverse_to_check_ordered_t A (Triple A hbt1 e hbt2) compare =
match traverse_to_check_ordered_hbt A hbt1 compare with
| TError _ => TError (A * A)
| TNone _ =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ => TError (A * A)
| TNone _ => TSome (A * A) (e, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt => TSome (A * A) (e, max2)
| Eq => TError (A * A)
| Gt => TError (A * A)
end
end
| TSome _ (min1, max1) =>
match compare max1 e with
| Lt =>
match traverse_to_check_ordered_hbt A hbt2 compare with
| TError _ => TError (A * A)
| TNone _ => TSome (A * A) (min1, e)
| TSome _ (min2, max2) =>
match compare e min2 with
| Lt => TSome (A * A) (min1, max2)
| Eq => TError (A * A)
| Gt => TError (A * A)
end
end
| Eq => TError (A * A)
| Gt => TError (A * A)
end
end.
Predicate to check if a heightened_binary_tree is ordered
Definition is_ordered_hbt
(A : Type)
(hbt : heightened_binary_tree A)
(compare : A -> A -> element_comparison) : bool :=
match traverse_to_check_ordered_hbt A hbt compare with
| TError _ =>
false
| _ =>
true
end.
(A : Type)
(hbt : heightened_binary_tree A)
(compare : A -> A -> element_comparison) : bool :=
match traverse_to_check_ordered_hbt A hbt compare with
| TError _ =>
false
| _ =>
true
end.
Lookup Operation on Heightened Binary Trees
Fixpoint occurs_hbt
(A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(hbt : heightened_binary_tree A) : bool :=
match hbt with
| HNode _ h bt =>
occurs_bt A compare e bt
end
with occurs_bt
(A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(bt : binary_tree A) : bool :=
match bt with
| Leaf _ =>
false
| Node _ t =>
occurs_t A compare e t
end
with occurs_t
(A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(t : triple A) : bool :=
match t with
| Triple _ hbt1 e' hbt2 =>
match compare e e' with
| Lt =>
occurs_hbt A compare e hbt1
| Eq =>
true
| Gt =>
occurs_hbt A compare e hbt2
end
end.
(A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(hbt : heightened_binary_tree A) : bool :=
match hbt with
| HNode _ h bt =>
occurs_bt A compare e bt
end
with occurs_bt
(A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(bt : binary_tree A) : bool :=
match bt with
| Leaf _ =>
false
| Node _ t =>
occurs_t A compare e t
end
with occurs_t
(A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(t : triple A) : bool :=
match t with
| Triple _ hbt1 e' hbt2 =>
match compare e e' with
| Lt =>
occurs_hbt A compare e hbt1
| Eq =>
true
| Gt =>
occurs_hbt A compare e hbt2
end
end.
Fold unfold lemma for occurs_hbt
Lemma fold_unfold_occurs_hbt:
forall (A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(h : nat)
(bt : binary_tree A),
occurs_hbt A compare e (HNode A h bt) = occurs_bt A compare e bt.
forall (A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(h : nat)
(bt : binary_tree A),
occurs_hbt A compare e (HNode A h bt) = occurs_bt A compare e bt.
Fold unfold lemma for occurs_bt, when the tree is a Leaf
Lemma fold_unfold_occurs_bt_leaf:
forall (A : Type)
(compare : A -> A -> element_comparison)
(e : A),
occurs_bt A compare e (Leaf A) = false.
forall (A : Type)
(compare : A -> A -> element_comparison)
(e : A),
occurs_bt A compare e (Leaf A) = false.
Fold unfold lemma for occurs_bt, when the tree is a Node
Lemma fold_unfold_occurs_bt_node:
forall (A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(t : triple A),
occurs_bt A compare e (Node A t) = occurs_t A compare e t.
forall (A : Type)
(compare : A -> A -> element_comparison)
(e : A)
(t : triple A),
occurs_bt A compare e (Node A t) = occurs_t A compare e t.
Fold unfold lemma for occurs_t
Lemma fold_unfold_occurs_t:
forall (A : Type)
(compare : A -> A -> element_comparison)
(e e' : A)
(hbt1 hbt2 : heightened_binary_tree A),
occurs_t A compare e (Triple A hbt1 e' hbt2) =
match compare e e' with
| Lt =>
occurs_hbt A compare e hbt1
| Eq =>
true
| Gt =>
occurs_hbt A compare e hbt2
end.
forall (A : Type)
(compare : A -> A -> element_comparison)
(e e' : A)
(hbt1 hbt2 : heightened_binary_tree A),
occurs_t A compare e (Triple A hbt1 e' hbt2) =
match compare e e' with
| Lt =>
occurs_hbt A compare e hbt1
| Eq =>
true
| Gt =>
occurs_hbt A compare e hbt2
end.
Insertion in Heightened Binary Trees
Unit tests for the Insertion Function
Fixpoint equal_lists
(A : Type)
(compare : A -> A -> element_comparison)
(xs ys : list A) : bool :=
match xs with
| nil =>
match ys with
| nil =>
true
| _ =>
false
end
| x :: xs' =>
match ys with
| nil =>
false
| y :: ys' =>
match compare x y with
| Eq =>
equal_lists A compare xs' ys'
| _ =>
false
end
end
end.
(A : Type)
(compare : A -> A -> element_comparison)
(xs ys : list A) : bool :=
match xs with
| nil =>
match ys with
| nil =>
true
| _ =>
false
end
| x :: xs' =>
match ys with
| nil =>
false
| y :: ys' =>
match compare x y with
| Eq =>
equal_lists A compare xs' ys'
| _ =>
false
end
end
end.
Function to map a heightened_binary_tree into the in-order list of its elements
Fixpoint hbt_to_list (A : Type) (hbt : heightened_binary_tree A) : list A :=
match hbt with
| HNode _ _ bt =>
bt_to_list A bt
end
with bt_to_list (A : Type) (bt : binary_tree A) : list A :=
match bt with
| Leaf _ =>
nil
| Node _ t =>
t_to_list A t
end
with t_to_list (A : Type) (t : triple A) : list A :=
match t with
| Triple _ hbt1 e hbt2 =>
(hbt_to_list A hbt1) ++ e :: (hbt_to_list A hbt2)
end.
match hbt with
| HNode _ _ bt =>
bt_to_list A bt
end
with bt_to_list (A : Type) (bt : binary_tree A) : list A :=
match bt with
| Leaf _ =>
nil
| Node _ t =>
t_to_list A t
end
with t_to_list (A : Type) (t : triple A) : list A :=
match t with
| Triple _ hbt1 e hbt2 =>
(hbt_to_list A hbt1) ++ e :: (hbt_to_list A hbt2)
end.
Function to check equality of heightened_binary_tree s
Definition equal_hbt
(A : Type)
(compare : A -> A -> element_comparison)
(hbt1 hbt2 : heightened_binary_tree A) : bool :=
equal_lists A compare (hbt_to_list A hbt1) (hbt_to_list A hbt2).
(A : Type)
(compare : A -> A -> element_comparison)
(hbt1 hbt2 : heightened_binary_tree A) : bool :=
equal_lists A compare (hbt_to_list A hbt1) (hbt_to_list A hbt2).
Function to insert a list of values into a heightened_binary_tree
Fixpoint insert_list
(A : Type)
(insert : forall (A' : Type),
(A' -> A' -> element_comparison)
-> A'
-> heightened_binary_tree A'
-> heightened_binary_tree A')
(compare : A -> A -> element_comparison)
(xs : list A)
(hbt : heightened_binary_tree A) :=
match xs with
| nil =>
hbt
| x :: xs' =>
insert_list A insert compare xs' (insert A compare x hbt)
end.
(A : Type)
(insert : forall (A' : Type),
(A' -> A' -> element_comparison)
-> A'
-> heightened_binary_tree A'
-> heightened_binary_tree A')
(compare : A -> A -> element_comparison)
(xs : list A)
(hbt : heightened_binary_tree A) :=
match xs with
| nil =>
hbt
| x :: xs' =>
insert_list A insert compare xs' (insert A compare x hbt)
end.
Function to generate values between 1 and n
Fixpoint atoi (n : nat) :=
match n with
| 0 =>
nil
| S n' =>
(S n') :: (atoi n')
end.
match n with
| 0 =>
nil
| S n' =>
(S n') :: (atoi n')
end.
Function to generate values between n and 1
Fixpoint traverse (n : nat) (acc : list nat) :=
match n with
| 0 =>
acc
| S n' =>
traverse n' ((S n') :: acc)
end.
match n with
| 0 =>
acc
| S n' =>
traverse n' ((S n') :: acc)
end.
Function to generate a list of the first n natural numbers
Definition iota (n : nat) :=
traverse n nil.
traverse n nil.
Empty heightened_binary_tree for testing
Definition hbt_empty := HNode nat 0 (Leaf nat).
Non-empty heightened_binary_tree for testing
Definition hbt_1 :=
HNode nat 2 (Node nat (Triple nat
(HNode nat 0 (Leaf nat))
1
(HNode nat 1 (Node nat (Triple nat
(HNode nat 0 (Leaf nat))
2
(HNode nat 0 (Leaf nat))))))).
HNode nat 2 (Node nat (Triple nat
(HNode nat 0 (Leaf nat))
1
(HNode nat 1 (Node nat (Triple nat
(HNode nat 0 (Leaf nat))
2
(HNode nat 0 (Leaf nat))))))).
Unit tests for an insert function: an insertion should preserve the invariant
properties of heightened binary trees
Definition test_insert_hbt
(candidate : forall (A' : Type),
(A' -> A' -> element_comparison)
-> A'
-> heightened_binary_tree A'
-> heightened_binary_tree A') :=
(is_sound_hbt
nat
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty)))
&& (is_balanced_hbt
nat
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty)))
&& (is_ordered_hbt
nat
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty))
compare_int)
&& (is_sound_hbt
nat
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty)))
&& (is_balanced_hbt
nat
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty)))
&& (is_ordered_hbt
nat
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty))
compare_int)
&& (equal_hbt
nat
compare_int
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty))
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty)))
&& (is_sound_hbt
nat
(candidate nat compare_int 15 hbt_1))
&& (is_balanced_hbt
nat
(candidate nat compare_int 15 hbt_1))
&& (is_ordered_hbt
nat
(candidate nat compare_int 15 hbt_1)
compare_int)
&& (is_sound_hbt
nat
(insert_list nat candidate compare_int (atoi 50) hbt_empty))
&& (is_ordered_hbt
nat
(insert_list nat candidate compare_int (atoi 50) hbt_empty)
compare_int)
&& (is_balanced_hbt
nat
(insert_list nat candidate compare_int (atoi 50) hbt_empty))
&& (is_sound_hbt
nat
(insert_list nat candidate compare_int (iota 50) hbt_empty))
&& (is_ordered_hbt
nat
(insert_list nat candidate compare_int (iota 50) hbt_empty)
compare_int)
&& (is_balanced_hbt
nat
(insert_list nat candidate compare_int (iota 50) hbt_empty)).
(candidate : forall (A' : Type),
(A' -> A' -> element_comparison)
-> A'
-> heightened_binary_tree A'
-> heightened_binary_tree A') :=
(is_sound_hbt
nat
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty)))
&& (is_balanced_hbt
nat
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty)))
&& (is_ordered_hbt
nat
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty))
compare_int)
&& (is_sound_hbt
nat
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty)))
&& (is_balanced_hbt
nat
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty)))
&& (is_ordered_hbt
nat
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty))
compare_int)
&& (equal_hbt
nat
compare_int
(candidate nat compare_int 1 (candidate nat compare_int 2 hbt_empty))
(candidate nat compare_int 2 (candidate nat compare_int 1 hbt_empty)))
&& (is_sound_hbt
nat
(candidate nat compare_int 15 hbt_1))
&& (is_balanced_hbt
nat
(candidate nat compare_int 15 hbt_1))
&& (is_ordered_hbt
nat
(candidate nat compare_int 15 hbt_1)
compare_int)
&& (is_sound_hbt
nat
(insert_list nat candidate compare_int (atoi 50) hbt_empty))
&& (is_ordered_hbt
nat
(insert_list nat candidate compare_int (atoi 50) hbt_empty)
compare_int)
&& (is_balanced_hbt
nat
(insert_list nat candidate compare_int (atoi 50) hbt_empty))
&& (is_sound_hbt
nat
(insert_list nat candidate compare_int (iota 50) hbt_empty))
&& (is_ordered_hbt
nat
(insert_list nat candidate compare_int (iota 50) hbt_empty)
compare_int)
&& (is_balanced_hbt
nat
(insert_list nat candidate compare_int (iota 50) hbt_empty)).
Implementation of Insertion Opertaion
Definition rotate_right_bt
(A : Type)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A) :=
match bt1 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h11 bt11) e1 (HNode _ h12 bt12)) =>
if h11 + 1 =n= h12
then
match bt12 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h121 bt121) e12 (HNode _ h122 bt122)) =>
Some (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)))))))
end
else
if (h12 + 1 =n= h11) || (h12 =n= h11)
then Some (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)))))))
else None
end.
Definition rotate_right_hbt
(A : Type)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A) :=
match hbt1 with
| HNode _ _ bt1 =>
match hbt2 with
| HNode _ h2 bt2 =>
rotate_right_bt A bt1 e h2 bt2
end
end.
(A : Type)
(bt1 : binary_tree A)
(e : A)
(h2 : nat)
(bt2 : binary_tree A) :=
match bt1 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h11 bt11) e1 (HNode _ h12 bt12)) =>
if h11 + 1 =n= h12
then
match bt12 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h121 bt121) e12 (HNode _ h122 bt122)) =>
Some (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)))))))
end
else
if (h12 + 1 =n= h11) || (h12 =n= h11)
then Some (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)))))))
else None
end.
Definition rotate_right_hbt
(A : Type)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A) :=
match hbt1 with
| HNode _ _ bt1 =>
match hbt2 with
| HNode _ h2 bt2 =>
rotate_right_bt A bt1 e h2 bt2
end
end.
Implementation of a left rotation. Note that this implementation implements the
double rotation directly, rather than making transparent the left and left rotations
which were composed. As a result, the project refers to the standard left rotation
as rotate_left_1, and the double rotation as rotate_left_2.
Definition rotate_left_bt
(A : Type)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(bt2 : binary_tree A) :=
match bt2 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h21 bt21) e2 (HNode _ h22 bt22)) =>
if h22 + 1 =n= h21
then
match bt21 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h211 bt211) e21 (HNode _ h212 bt212)) =>
Some (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)))))))
end
else
if (h21 + 1 =n= h22) || (h21 =n= h22)
then Some (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))))
else None
end.
Definition rotate_left_hbt
(A : Type)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A) :=
match hbt1 with
| HNode _ h1 bt1 =>
match hbt2 with
| HNode _ _ bt2 =>
rotate_left_bt A h1 bt1 e bt2
end
end.
(A : Type)
(h1 : nat)
(bt1 : binary_tree A)
(e : A)
(bt2 : binary_tree A) :=
match bt2 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h21 bt21) e2 (HNode _ h22 bt22)) =>
if h22 + 1 =n= h21
then
match bt21 with
| Leaf _ =>
None
| Node _ (Triple _ (HNode _ h211 bt211) e21 (HNode _ h212 bt212)) =>
Some (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)))))))
end
else
if (h21 + 1 =n= h22) || (h21 =n= h22)
then Some (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))))
else None
end.
Definition rotate_left_hbt
(A : Type)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A) :=
match hbt1 with
| HNode _ h1 bt1 =>
match hbt2 with
| HNode _ _ bt2 =>
rotate_left_bt A h1 bt1 e bt2
end
end.
Function to project the height stored in a heightened_binary_tree
Definition project_height_hbt
(A : Type)
(hbt : heightened_binary_tree A) : nat :=
match hbt with
| HNode _ h _ => h
end.
(A : Type)
(hbt : heightened_binary_tree A) : nat :=
match hbt with
| HNode _ h _ => h
end.
Function to project the binary_tree stored in a heightened_binary_tree
Definition project_bt_hbt
(A : Type)
(hbt : heightened_binary_tree A) : binary_tree A :=
match hbt with
| HNode _ _ bt => bt
end.
(A : Type)
(hbt : heightened_binary_tree A) : binary_tree A :=
match hbt with
| HNode _ _ bt => bt
end.
Function to project the height of a binary_tree
Definition project_height_bt
(A : Type)
(bt : binary_tree A) :=
match bt with
| Leaf _ =>
0
| Node _ (Triple _ hbt1 _ hbt2) =>
1 + max (project_height_hbt A hbt1) (project_height_hbt A hbt2)
end.
(A : Type)
(bt : binary_tree A) :=
match bt with
| Leaf _ =>
0
| Node _ (Triple _ hbt1 _ hbt2) =>
1 + max (project_height_hbt A hbt1) (project_height_hbt A hbt2)
end.
Function to project the height of a triple
Definition project_height_t
(A : Type)
(t : triple A) :=
match t with
| Triple _ hbt1 _ hbt2 =>
1 + max (project_height_hbt A hbt1) (project_height_hbt A hbt2)
end.
(A : Type)
(t : triple A) :=
match t with
| Triple _ hbt1 _ hbt2 =>
1 + max (project_height_hbt A hbt1) (project_height_hbt A hbt2)
end.
Structurally recursive function to insert a given value into a
heightened_binary_tree
Fixpoint insert_hbt_helper
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(hbt : heightened_binary_tree A) :=
match hbt with
| HNode _ h bt =>
insert_bt_helper A compare x h bt
end
with insert_bt_helper
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(bt : binary_tree A) :=
match bt with
| Leaf _ =>
Some (HNode A
1
(Node A (Triple A
(HNode A 0 (Leaf A))
x
(HNode A 0 (Leaf A)))))
| Node _ t =>
insert_t_helper A compare x h_hbt t
end
with insert_t_helper
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(t : triple A) :=
match t with
| Triple _ hbt1 e hbt2 =>
match compare x e with
| Lt =>
match insert_hbt_helper A compare x hbt1 with
| None =>
None
| Some (HNode _ h1' bt1') =>
match compare_int h1' (2 + (project_height_hbt A hbt2)) with
| Lt =>
Some (HNode A
(1 + max h1' (project_height_hbt A hbt2))
(Node A (Triple A (HNode A h1' bt1') e hbt2)))
| Eq =>
rotate_right_hbt A (HNode A h1' bt1') e hbt2
| Gt =>
None
end
end
| Eq =>
None
| Gt =>
match insert_hbt_helper A compare x hbt2 with
| None =>
None
| Some (HNode _ h2' bt2') =>
match compare_int h2' (2 + (project_height_hbt A hbt1)) with
| Lt =>
Some (HNode A
(1 + max (project_height_hbt A hbt1) h2')
(Node A (Triple A hbt1 e (HNode A h2' bt2'))))
| Eq =>
rotate_left_hbt A hbt1 e (HNode A h2' bt2')
| Gt =>
None
end
end
end
end.
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(hbt : heightened_binary_tree A) :=
match hbt with
| HNode _ h bt =>
insert_bt_helper A compare x h bt
end
with insert_bt_helper
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(bt : binary_tree A) :=
match bt with
| Leaf _ =>
Some (HNode A
1
(Node A (Triple A
(HNode A 0 (Leaf A))
x
(HNode A 0 (Leaf A)))))
| Node _ t =>
insert_t_helper A compare x h_hbt t
end
with insert_t_helper
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(t : triple A) :=
match t with
| Triple _ hbt1 e hbt2 =>
match compare x e with
| Lt =>
match insert_hbt_helper A compare x hbt1 with
| None =>
None
| Some (HNode _ h1' bt1') =>
match compare_int h1' (2 + (project_height_hbt A hbt2)) with
| Lt =>
Some (HNode A
(1 + max h1' (project_height_hbt A hbt2))
(Node A (Triple A (HNode A h1' bt1') e hbt2)))
| Eq =>
rotate_right_hbt A (HNode A h1' bt1') e hbt2
| Gt =>
None
end
end
| Eq =>
None
| Gt =>
match insert_hbt_helper A compare x hbt2 with
| None =>
None
| Some (HNode _ h2' bt2') =>
match compare_int h2' (2 + (project_height_hbt A hbt1)) with
| Lt =>
Some (HNode A
(1 + max (project_height_hbt A hbt1) h2')
(Node A (Triple A hbt1 e (HNode A h2' bt2'))))
| Eq =>
rotate_left_hbt A hbt1 e (HNode A h2' bt2')
| Gt =>
None
end
end
end
end.
Fold unfold lemma for insert_hbt_helper
Lemma fold_unfold_insert_hbt_helper:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h : nat)
(bt : binary_tree A),
insert_hbt_helper A compare x (HNode A h bt) = insert_bt_helper A compare x h bt.
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h : nat)
(bt : binary_tree A),
insert_hbt_helper A compare x (HNode A h bt) = insert_bt_helper A compare x h bt.
Fold unfold lemma for insert_bt_helper, when the tree is a Leaf
Lemma fold_unfold_insert_bt_helper_leaf:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat),
insert_bt_helper A compare x h_hbt (Leaf A) =
Some (HNode A
1
(Node A (Triple A
(HNode A 0 (Leaf A))
x
(HNode A 0 (Leaf A))))).
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat),
insert_bt_helper A compare x h_hbt (Leaf A) =
Some (HNode A
1
(Node A (Triple A
(HNode A 0 (Leaf A))
x
(HNode A 0 (Leaf A))))).
Fold unfold lemma for insert_bt_helper, when the tree is a Node
Lemma fold_unfold_insert_bt_helper_node:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(t : triple A),
insert_bt_helper A compare x h_hbt (Node A t) =
insert_t_helper A compare x h_hbt t.
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(t : triple A),
insert_bt_helper A compare x h_hbt (Node A t) =
insert_t_helper A compare x h_hbt t.
Fold unfold lemma for insert_t_helper
Lemma fold_unfold_insert_t_helper:
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A),
insert_t_helper A compare x h_hbt (Triple A hbt1 e hbt2) =
match compare x e with
| Lt =>
match insert_hbt_helper A compare x hbt1 with
| None =>
None
| Some (HNode _ h1' bt1') =>
match compare_int h1' (2 + (project_height_hbt A hbt2)) with
| Lt =>
Some (HNode A
(1 + max h1' (project_height_hbt A hbt2))
(Node A (Triple A (HNode A h1' bt1') e hbt2)))
| Eq =>
rotate_right_hbt A (HNode A h1' bt1') e hbt2
| Gt =>
None
end
end
| Eq =>
None
| Gt =>
match insert_hbt_helper A compare x hbt2 with
| None =>
None
| Some (HNode _ h2' bt2') =>
match compare_int h2' (2 + (project_height_hbt A hbt1)) with
| Lt =>
Some (HNode A
(1 + max (project_height_hbt A hbt1) h2')
(Node A (Triple A hbt1 e (HNode A h2' bt2'))))
| Eq =>
rotate_left_hbt A hbt1 e (HNode A h2' bt2')
| Gt =>
None
end
end
end.
forall (A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(h_hbt : nat)
(hbt1 : heightened_binary_tree A)
(e : A)
(hbt2 : heightened_binary_tree A),
insert_t_helper A compare x h_hbt (Triple A hbt1 e hbt2) =
match compare x e with
| Lt =>
match insert_hbt_helper A compare x hbt1 with
| None =>
None
| Some (HNode _ h1' bt1') =>
match compare_int h1' (2 + (project_height_hbt A hbt2)) with
| Lt =>
Some (HNode A
(1 + max h1' (project_height_hbt A hbt2))
(Node A (Triple A (HNode A h1' bt1') e hbt2)))
| Eq =>
rotate_right_hbt A (HNode A h1' bt1') e hbt2
| Gt =>
None
end
end
| Eq =>
None
| Gt =>
match insert_hbt_helper A compare x hbt2 with
| None =>
None
| Some (HNode _ h2' bt2') =>
match compare_int h2' (2 + (project_height_hbt A hbt1)) with
| Lt =>
Some (HNode A
(1 + max (project_height_hbt A hbt1) h2')
(Node A (Triple A hbt1 e (HNode A h2' bt2'))))
| Eq =>
rotate_left_hbt A hbt1 e (HNode A h2' bt2')
| Gt =>
None
end
end
end.
Main insertion function, which calls the insert_hbt_helper helper. Note that
if the helper function returns a None value (indicating an error), then this
function simply returns the original tree
Definition insert_hbt
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(hbt : heightened_binary_tree A) :=
match insert_hbt_helper A compare x hbt with
| None =>
hbt
| Some hbt' =>
hbt'
end.
Extraction occurs_hbt.
(A : Type)
(compare : A -> A -> element_comparison)
(x : A)
(hbt : heightened_binary_tree A) :=
match insert_hbt_helper A compare x hbt with
| None =>
hbt
| Some hbt' =>
hbt'
end.
Extraction occurs_hbt.