Create a gist now

Instantly share code, notes, and snippets.

What would you like to do?
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 *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment