Require Export Basic.

Section Trees.

Variable T : Type.

Inductive BinaryTree : Type :=
  nought : BinaryTree
  | node : T -> BinaryTree -> BinaryTree -> BinaryTree.

Fixpoint BT_In (t:T) (Tree:BinaryTree) : Prop :=
  match Tree with
  | nought => False
  | node t' L R => BT_In t L \/ t = t' \/ BT_In t R
  end.

Fixpoint BT_wf (T_compare : T -> T -> comparison) (Tree:BinaryTree) :=
  match Tree with
  | nought => True
  | node t L R => BT_wf T_compare L /\ BT_wf T_compare R /\
                 (forall t', BT_In t' L -> T_compare t' t = Lt) /\
                 (forall t', BT_In t' R -> T_compare t' t = Gt)
  end.

Variable T_compare : T -> T -> comparison.

Hypothesis eq_T_compare : forall t t', T_compare t t' = Eq -> t = t'.
Hypothesis T_compare_eq : forall t, T_compare t t = Eq.
Hypothesis T_compare_trans : forall t t' t'', T_compare t t' = Lt -> T_compare t' t'' = Lt ->
                                              T_compare t t'' = Lt.
Hypothesis T_compare_sym_Gt : forall t t', T_compare t t' = Gt -> T_compare t' t = Lt.
Hypothesis T_compare_sym_Lt : forall t t', T_compare t t' = Lt -> T_compare t' t = Gt.

Let BT_Wf := BT_wf T_compare.

Lemma BT_nought_char : forall Tree, (forall (t:T), ~(BT_In t Tree)) -> Tree = nought.

Lemma BT_singleton_char : forall Tree t, BT_Wf Tree -> (BT_In t Tree) ->
     (forall (t':T), (BT_In t' Tree) -> t=t') -> Tree = (node t nought nought).

Section Balancing.

Open Scope Z_scope.

Fixpoint height (Tree:BinaryTree) : Z :=
  match Tree with
  | nought => 0
  | node _ L R => 1 + (Z.max (height L) (height R))
  end.

Fixpoint balanced (Tree:BinaryTree) :=
  match Tree with
  | nought => True
  | node _ L R => balanced L /\ balanced R /\ Z.abs (height L - height R) <= 1
  end.

Definition BT_rot_L (Tree:BinaryTree) :=
  match Tree with
  | nought => nought
  | node n L nought => node n L nought
  | node n L (node n' RL RR) => node n' (node n L RL) RR
  end.

Lemma BT_rot_L_wf : forall Tree, BT_Wf Tree -> BT_Wf (BT_rot_L Tree).

Lemma BT_rot_L_in : forall t Tree, BT_In t Tree -> BT_In t (BT_rot_L Tree).

Lemma BT_in_rot_L : forall t Tree, BT_In t (BT_rot_L Tree) -> BT_In t Tree.

Lemma BT_rot_L_wf_rev : forall Tree, BT_Wf (BT_rot_L Tree) -> BT_Wf Tree.

Definition BT_rot_R (Tree:BinaryTree) :=
  match Tree with
  | nought => nought
  | node n nought R => node n nought R
  | node n (node n' LL LR) R => node n' LL (node n LR R)
  end.

Lemma BT_rot_R_wf : forall Tree, BT_Wf Tree -> BT_Wf (BT_rot_R Tree).

Lemma BT_rot_R_in : forall t Tree, BT_In t Tree -> BT_In t (BT_rot_R Tree).

Lemma BT_in_rot_R : forall t Tree, BT_In t (BT_rot_R Tree) -> BT_In t Tree.

Lemma BT_rot_R_wf_rev : forall Tree, BT_Wf (BT_rot_R Tree) -> BT_Wf Tree.

Definition BT_rot_LL (Tree:BinaryTree) :=
  match Tree with
  | nought => nought
  | node n L R => BT_rot_L (node n L (BT_rot_R R))
  end.

Lemma BT_rot_LL_wf : forall Tree, BT_Wf Tree -> BT_Wf (BT_rot_LL Tree).

Lemma BT_rot_LL_in : forall t Tree, BT_In t Tree -> BT_In t (BT_rot_LL Tree).

Lemma BT_in_rot_LL : forall t Tree, BT_In t (BT_rot_LL Tree) -> BT_In t Tree.

Definition BT_rot_RR (Tree:BinaryTree) :=
  match Tree with
  | nought => nought
  | node n L R => BT_rot_R (node n (BT_rot_L L) R)
  end.

Lemma BT_rot_RR_wf : forall Tree, BT_Wf Tree -> BT_Wf (BT_rot_RR Tree).

Lemma BT_rot_RR_in : forall t Tree, BT_In t Tree -> BT_In t (BT_rot_RR Tree).

Lemma BT_in_rot_RR : forall t Tree, BT_In t (BT_rot_RR Tree) -> BT_In t Tree.

Definition BT_balance (Tree:BinaryTree) :=
  match Tree with
  | nought => nought
  | node n L R => if (Z.eq_dec ((height L)-(height R)) 2)
                  then match L with
                       | nought => node n L R
                       | node n' LL LR => if (compare_Gt_dec (Z.compare (height LL) (height LR)))
                                          then BT_rot_R Tree
                                          else BT_rot_RR Tree
                       end
                  else if (Z.eq_dec ((height R)-(height L)) 2)
                  then match R with
                       | nought => node n L R
                       | node n' RL RR => if (compare_Lt_dec (Z.compare (height RL) (height RR)))
                                          then BT_rot_L Tree
                                          else BT_rot_LL Tree
                       end
                  else Tree
  end.

Lemma BT_balance_wf : forall Tree, BT_Wf Tree -> BT_Wf (BT_balance Tree).

Lemma BT_balance_in : forall t Tree, BT_In t Tree -> BT_In t (BT_balance Tree).

Lemma BT_in_balance : forall t Tree, BT_In t (BT_balance Tree) -> BT_In t Tree.

End Balancing.

Opaque BT_balance.

Fixpoint BT_add (t:T) (Tree:BinaryTree) :=
  match Tree with
  | nought => node t nought nought
  | node t' L R => match T_compare t t' with
         | Lt => node t' (BT_add t L) R
         | Gt => node t' L (BT_add t R)
         | Eq => Tree
         end
  end.

Lemma BT_add_in : forall t Tree, BT_In t (BT_add t Tree).

Lemma BT_in_add : forall t t' Tree, BT_In t (BT_add t' Tree) ->
                  BT_In t Tree \/ t=t'.

Lemma BT_wf_add : forall t Tree, BT_Wf Tree -> BT_Wf (BT_add t Tree).

Lemma BT_add_mon : forall t t' Tree, BT_In t' Tree -> BT_In t' (BT_add t Tree).

Lemma BT_add_wf_rev : forall t Tree, BT_Wf (BT_add t Tree) -> BT_Wf Tree.

Fixpoint BT_split (Tree:BinaryTree) (default:T) : T * BinaryTree :=
  match Tree with
  | nought => (default,nought)
  | node t nought R => (t,R)
  | node t L R => let (t',L') := BT_split L default in
                  (t',node t L' R)
  end.

Lemma BT_split_in_r : forall t t' x Tree Tree', BT_split Tree x = (t,Tree') ->
                      BT_In t' Tree' -> BT_In t' Tree.

Lemma BT_split_wf : forall Tree x, BT_Wf Tree -> forall t Tree', BT_split Tree x = (t,Tree') -> BT_Wf Tree'.

Lemma BT_split_in_l : forall t x Tree, Tree <> nought ->
                      forall Tree', BT_split Tree x = (t,Tree') -> BT_In t Tree.

Lemma BT_split_in : forall t t' x Tree Tree', BT_split Tree x = (t',Tree') ->
                    BT_In t Tree -> t = t' \/ BT_In t Tree'.

Lemma BT_split_compare : forall Tree x, BT_Wf Tree -> forall t Tree', BT_split Tree x = (t,Tree') ->
                         forall t', BT_In t' Tree' -> T_compare t t' = Lt.

Hypothesis T_dec : forall t t':T, {t=t'} + {t<>t'}.

Lemma BT_in_dec : forall t Tree, BT_Wf Tree -> {BT_In t Tree} + {~BT_In t Tree}.

Lemma BT_all_in_dec : forall f:T->T, forall Tree Tree',
     BT_Wf Tree' ->
     {forall t, BT_In t Tree -> BT_In (f t) Tree'} +
     {~forall t, BT_In t Tree -> BT_In (f t) Tree'}.

Fixpoint BT_remove (t:T) (Tree:BinaryTree) : BinaryTree :=
  match Tree with
  | nought => nought
  | node t' L R => match T_compare t t' with
                   | Eq => match R with
                           | nought => L
                           | R => let (min,R') := BT_split R t in node min L R'
                           end
                   | Lt => node t' (BT_remove t L) R
                   | Gt => node t' L (BT_remove t R)
  end end.

Lemma BT_remove_in : forall t t' Tree Tree', BT_remove t Tree = Tree' ->
                     BT_In t' Tree' -> BT_In t' Tree.

Lemma BT_remove_wf : forall Tree, BT_Wf Tree -> forall t Tree', BT_remove t Tree = Tree' -> BT_Wf Tree'.

Lemma BT_remove_in_rev : forall t' Tree Tree', BT_remove t' Tree = Tree' ->
                    forall t, BT_In t Tree -> t = t' \/ BT_In t Tree'.

Lemma BT_in_remove : forall Tree t t', (BT_Wf Tree) -> (BT_In t Tree) ->
     (t <> t') -> BT_In t (BT_remove t' Tree).

Lemma BT_remove_out : forall t Tree, (BT_Wf Tree) -> ~(BT_In t (BT_remove t Tree)).

Fixpoint BT_diff (Tree Tree':BinaryTree) : BinaryTree :=
  match Tree' with
  | nought => Tree
  | node t' L R => BT_remove t' (BT_diff (BT_diff Tree L) R)
  end.

Lemma BT_diff_wf : forall Tree Tree', BT_Wf Tree -> forall Tree'', BT_diff Tree Tree' = Tree'' -> BT_Wf Tree''.

Lemma BT_diff_in : forall t Tree Tree' Tree'', BT_diff Tree Tree' = Tree'' ->
                     BT_In t Tree'' -> BT_In t Tree.

Lemma BT_diff_in_rev : forall Tree Tree' Tree'', BT_diff Tree Tree' = Tree'' ->
                       forall t, BT_In t Tree -> BT_In t Tree' \/ BT_In t Tree''.

Lemma BT_diff_out : forall Tree Tree', (BT_Wf Tree) ->
                    forall t, BT_In t Tree' -> ~(BT_In t (BT_diff Tree Tree')).

Lemma BT_diff_out' : forall Tree Tree', (BT_Wf Tree) ->
                    forall t, BT_In t (BT_diff Tree Tree') -> ~(BT_In t Tree').

Lemma BT_diff_nought : forall Tree Tree', BT_Wf Tree ->
     (forall t:T, BT_In t Tree -> BT_In t Tree') -> BT_diff Tree Tree' = nought.

Lemma BT_nought_diff : forall Tree Tree', BT_Wf Tree ->
  BT_diff Tree Tree' = nought -> forall t:T, BT_In t Tree -> BT_In t Tree'.

Fixpoint list_to_BTree (l:list T) :=
  match l with
  | nil => nought
  | (x::l') => BT_add x (list_to_BTree l')
  end.

Lemma in_list_BTree : forall l t, In t l -> BT_In t (list_to_BTree l).

Lemma in_BTree_list : forall l t, BT_In t (list_to_BTree l) -> In t l.

Lemma list_to_BTree_wf : forall l, BT_Wf (list_to_BTree l).

Fixpoint BT_size (Tree:BinaryTree) : nat :=
  match Tree with
  | nought => 0
  | node _ L R => (BT_size L) + (BT_size R) + 1
  end.

Lemma BT_size_split : forall Tree x t Tree', BT_split Tree x = (t,Tree') ->
                      BT_size (Tree') = pred (BT_size Tree).

Fixpoint BT_add_all (Tree Tree':BinaryTree) :=
  match Tree with
  | nought => Tree'
  | node t L R => BT_add_all R (BT_add_all L (BT_add t Tree'))
  end.

Lemma BT_wf_add_all : forall Tree Tree', BT_Wf Tree' -> BT_Wf (BT_add_all Tree Tree').

Lemma BT_add_all_wf_rev : forall Tree Tree', BT_Wf (BT_add_all Tree Tree') -> BT_Wf Tree'.

Lemma BT_add_all_mon : forall Tree Tree' t, BT_In t Tree' -> BT_In t (BT_add_all Tree Tree').

Lemma BT_add_all_in : forall Tree Tree' t, BT_In t Tree -> BT_In t (BT_add_all Tree Tree').

Lemma BT_in_add_all : forall Tree Tree' t, BT_In t (BT_add_all Tree Tree') ->
                      BT_In t Tree \/ BT_In t Tree'.

Section Map.

Variable f:T->T.

Fixpoint BT_map (Tree:BinaryTree) : BinaryTree :=
  match Tree with
  | nought => nought
  | node t L R => BT_add_all (BT_map L) (BT_add (f t) (BT_map R))
  end.

Lemma BT_map_in : forall t Tree, BT_In t Tree -> BT_In (f t) (BT_map Tree).

End Map.

End Trees.