Simple Function on binary trees

Inductive Zbtree : Type :=
|  leaf 
|  bnode (r:Z)(t1 t2: Zbtree).

(** Checks whether t is a leaf *)
is_leaf (t: Zbtree) : bool :=


(** Returns the total number of nodes (binary nodes and leaves) of t *)
size (t: Zbtree) : nat :=

(** returns the heigth of t *)
height (t:Zbtree) : nat :=

(** returns the mirror of t *)
mirror (t:Zbtree) : Zbtree 

(** Checks whether n labels some node of t *)
memb (n:Z)(t: Zbtree) : bool 

(** Computes the list of t's labels (in infix order) *)
infix_list (t:Zbtree) : list Z 

(** Checks whether t is a search tree *)
is_searchtree (t:Zbtree) : bool

(** Checks whether n labels some node of t . This function is more efficient
   than memb, but is correct  only is applied to to a search tree *)
memb_in_searchtree  (n:Z)(t: Zbtree) : bool 

(** Transforms a list of integers into a searchtree *)
list_to_searchtree (l:list Z) : Zbtree 

Notes

• Max (for computing the maximum of two natural numbers)
• ZArith (for using the type Z )
• Bool (for infix notations of the boolean connectives)
• List

Comments

• The composition of functions list_to_searchtree and infix_list cannot be considered as a sorting function on lists. Why? One can fix this issue in two ways:
  • Modifying the data structure for storing the multiplicity of any element of the list, or
  • Keeping the type Zbtree but slightly modifying the notion of search-trees.
• Polymorphism : type Z will be replaced with any type provided with a decidable total order.
• Formal proof of correctness of the functions above
• Formal specification of a type associated with search-trees (using sigma-types)

Solution