Require Export Basics.

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.

Fixpoint BT_add (T_compare : T -> T -> comparison) (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_compare t L) R
         | Gt => node t' L (BT_add T_compare t R)
         | Eq => Tree
         end
  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.

Let BT_Add := BT_add T_compare.
Let BT_Wf := BT_wf T_compare.

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

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_Wf 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 -> BT_Wf Tree ->
                      forall Tree', BT_split Tree x = (t,Tree') -> BT_In t Tree.

Lemma BT_split_in : forall t t' x Tree Tree', BT_Wf 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 list_to_BTree (l:list T) :=
  match l with
  | nil => nought
  | (x::l') => BT_add T_compare 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_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.