Definition A:= nat.

Inductive tree : Set :=
  | Emp : tree (* empty *)
  | B : tree -> A -> tree -> tree.

Fixpoint member (x:A) (a: tree) := 
  match a with
  | Emp => False
  | B a y b => member x a \/ x = y \/ member x b
  end.

(* equivalent inductive definition *)
Inductive imember (x: A) : tree -> Prop :=
  | Mroot: forall a b, imember x (B a x b)
  | Mleft: forall a y b, imember x a ->  imember x (B a y b)
  | Mright: forall a y b, imember x b -> imember x (B a y b).

(* Exercises: indeed equivalent *)

Lemma member_imember: forall x a, member x a -> imember x a.
Proof.
Admitted.

Lemma imember_member: forall x a, imember x a -> member x a.
Proof.
Admitted.

Fixpoint eqb_nat (x y: A): bool. 
Admitted.

Lemma eqb_nat_correct1 : forall n m, eqb_nat n m = true -> n = m.
Admitted.

Lemma eqb_nat_correct2 : forall n m, eqb_nat n m = false -> n <> m.
Admitted.

Fixpoint test_member (x:A) (a:tree) : bool.
Admitted.

Lemma test_member_correct2 : 
  forall x a, test_member x a = true -> member x a.
Admitted.

Lemma test_member_correct1 : 
  forall x a, test_member x a = false -> ~member x a.
Admitted.

(* Adding ordering structure *)

Definition R : A -> A -> Prop := le.

Fixpoint testR (x y: A) : bool.
Admitted.

Lemma testR_correct1: forall x y, testR x y = true -> R x y.
Admitted.

Lemma testR_correct2: forall x y, testR x y = false -> R y x.
Admitted.

Lemma testR_antisym: 
  forall x y, testR x y = true -> testR y x = true -> x = y.
Proof.
Admitted.

Lemma antisym: forall x y, R x y -> R y x -> x = y.
Proof.
Admitted.

(* Exercise: reflexivity can be deduced from the above properties *)
Lemma refl : forall x, R x x.
Proof.
Admitted.

Lemma trans: forall x y z, R x y -> R y z -> R x z.
Admitted.

(* l is a lower bound of a tree *)
Inductive lower_bound (l: A) : tree -> Prop :=
  | LbE: lower_bound l Emp
  | lbB: forall a x b, 
         lower_bound l a -> R l x -> lower_bound l b ->
         lower_bound l (B a x b).

(* Exercises *)
(* Remark that sometime member is easier to use than imember,
   but it is sometmes the opposite *)
(* hint: use (sometimes only!) inversion on version with imember *) 

Lemma imember_lower_bound: 
  forall l a, (forall x, imember x a -> R l x) -> lower_bound l a.
Proof.
Admitted.

(* Longer and boring to do directly --- try or use the previous one *)
Lemma member_lower_bound: 
  forall l a, (forall x, member x a -> R l x) -> lower_bound l a.
Proof.
Admitted.

(* Conversely *)
Lemma lower_bound_member: 
  forall l a, lower_bound l a -> forall x, member x a -> R l x.
Proof.
Admitted.

Lemma lower_bound_imember: 
  forall l a, lower_bound l a -> forall x, imember x a -> R l x.
Proof.
Admitted.

(* Similar with upper bound *)
(* u is an upper bound of a tree *)

Inductive upper_bound (u: A) : tree -> Prop :=
  | UbE: upper_bound u Emp
  | ubB: forall a x b, 
         upper_bound u a -> R x u -> upper_bound u b ->
         upper_bound u (B a x b).

Lemma imember_upper_bound: 
  forall u a, (forall x, imember x a -> R x u) -> upper_bound u a.
Proof.
Admitted.

(* Longer and boring to do directly --- try or use the previous one *)
Lemma member_upper_bound: 
  forall u a, (forall x, member x a -> R x u) -> upper_bound u a.
Proof.
Admitted.

(* Conversely *)
Lemma upper_bound_member: 
  forall u a, upper_bound u a -> forall x, member x a -> R x u.
Proof.
Admitted.

Lemma upper_bound_imember: 
  forall u a, upper_bound u a -> forall x, imember x a -> R x u.
Proof.
Admitted.

(* ------------------------------------------------------------ *)
(* Binary search trees *)

Inductive ind_is_bst : tree -> Prop :=
  | Eb : ind_is_bst Emp
  | Bb : 
     forall a x b,
     upper_bound x a -> lower_bound x b ->
     ind_is_bst a -> ind_is_bst b -> 
     ind_is_bst (B a x b).

Fixpoint is_bst a: Prop :=
  match a with
  | Emp => True
  | B a x b => upper_bound x a /\ lower_bound x b /\ is_bst a /\ is_bst b
  end.

(* Exercise: the 2 previous definitions are equivalent
State and show it.
*)


(* Exercise : binary search. Some previous lemmas may be useful... *)

(* warning: use testR in order to search only in 1 branch *)

Fixpoint bsearch (x: A) (a: tree) : bool.
(* Your code *)
Admitted.
  

(* Then prove correctness: *)

Lemma bsearch_correctness1: 
  forall x a, is_bst a -> bsearch x a = true -> member x a.
Proof.
Admitted.

Lemma bsearch_correctness2: 
  forall x a, is_bst a -> member x a -> bsearch x a = true.
Proof.
Admitted.


(* ------------------------------------------------------------ *)
(* Insertion *)
Fixpoint insert (x: A) (a: tree) : tree. 
(* := your code*)
Admitted.

(* The 3 first correctness theorems can be proved even for non-bst trees *)
Theorem insert_correct_inserted :
  forall x a, member x (insert x a).
Proof.
Admitted.

Theorem insert_correct_noleak :
  forall x a z, member z a -> member z (insert x a).
Proof.
Admitted.

Theorem insert_correct_nocreation :
  forall x a z, member z (insert x a) -> z = x \/ member z a.
Proof.
Admitted.

Theorem insert_correct_bst_invar :
  forall x a, is_bst a -> is_bst (insert x a).
Proof.
Admitted.