bst_base.v

Require Import ssreflect eqtype ssrbool ssrfun ssrnat seq.
Require Import Adlibssr.btree Adlibssr.binsearch Adlibssr.order.



(* leq is total-order on nat *)
Program Canonical Structure leq: totalOrder nat := makeTotalOrder leq.
Next Obligation.
  apply anti_leq.
Qed.
Next Obligation.
  move=> x y z; apply leq_trans.
Qed.
Next Obligation.
  move=> x y; apply leq_total.
Qed.


Definition t1 := ((#-< 1 >-#)-< 2 >-(#-< 3 >-#))-< 4 >-((#-< 5 >-#)-< 6 >-#).

Eval compute in (bst leq t1).
     (* = true *)
     (* : bool *)

Eval compute in (search leq 3 t1).
     (* = true *)
     (* : bool *)

Eval compute in (search leq 7 t1).
     (* = false *)
     (* : bool *)

Eval compute in (insert leq 4 t1).
     (* = ((# -< 1 >- #) -< 2 >- (# -< 3 >- #)) -< 4 >- *)
     (*   (((# -< 4 >- #) -< 5 >- #) -< 6 >- #) *)
     (* : btree nat_eqType *)

Eval compute in (insert leq 8 t1).
     (* = ((# -< 1 >- #) -< 2 >- (# -< 3 >- #)) -< 4 >- *)
     (*   ((# -< 5 >- #) -< 6 >- (# -< 8 >- #)) *)
     (* : btree nat_eqType *)

Eval compute in (flatten t1).
     (* = [:: 1; 2; 3; 4; 5; 6] *)
     (* : seq nat *)

Eval compute in (bst leq (insert leq 4 t1)).
     (* = true *)
     (* : bool *)

Eval compute in (btsort leq [:: 3;1;4;1;5;9]).
     (* = [:: 1; 1; 3; 4; 5; 9] *)
     (* : seq nat_eqType *)