(**  * Programs, proofs and types (End Semester exam).

Please fill in the the following details.

Name:
Rollnumber:

Instructions:

This file has a partial implementation and proof of insertion in a
binary search tree. Do not change the definitions in the begining of
the file. Only edit the proofs. There is a space further down in the
file where you can write your own Ltac rules.  Complete the proofs,
create a document out of it using coqdoc and submit the print out to
me. Also email me the competed code.

*)


Require Import Nat.
Require Import Omega. (* For the omega tactics *)

(** The Binary tree of nats. *)

Inductive tree :=
| empty : tree
| node  : tree -> nat -> tree -> tree
.

(* Predicate that captures that a particular element is in the given tree *)
Inductive in_tree (x : nat) : tree -> Prop :=
| atRoot  : forall lt rt, in_tree x (node lt x rt)
| inLeft  : forall lt y rt, in_tree x lt -> in_tree x (node lt y rt)
| inRight : forall lt y rt, in_tree x rt -> in_tree x (node lt y rt).

Hint Constructors in_tree.


(* A binary tree with a single element *)

Definition singleton (n : nat) := node empty n empty.

(**

The [everyWhere f t] takes a predicate [f : nat -> Prop] on nats, and
asserts thatf holds on all elements of the tree.

*)

Fixpoint everyWhere (f : nat -> Prop)(t : tree) : Prop :=
  match t with
    | empty        => True
    | node lt x rt => f x /\ everyWhere f lt /\ everyWhere f rt
  end.


(** * A binary search tree.

We now build predicates for asserting a tree is a valid search
tree. We generalise the property of being a search tree to that of
being a search tree with nodes bounded appropriately.

*)



Fixpoint search_tree (t : tree) : Prop :=
  match t with
    | empty => True (* an empty tree is a search tree *)
    | node lt x rt => search_tree lt        (* the left subtree is a search tree  *)
                      /\ search_tree rt     (* the right subtree is a search tree *)
                      /\ everyWhere (fun n => n < x) lt (* elements of left sub-tree is less than [x] *)
                      /\ everyWhere (fun n => x < n) rt (* [x] is less than the elements of right sub-tree  *)
  end.

(* We define the insertion function *)
Fixpoint insert (t : tree) (n : nat) : tree :=
  match t with
    | empty      => singleton n
    | node l x r => match compare n x with
                      | Eq => t
                      | Gt => node l  x (insert r n)
                      | Lt => node (insert l n)   x r
                    end
  end.


(** Proof of correctness *)
(* In case you are writing a crush tactic please write it here *)


(* Some helpeful theorems regarding compare is given below.


nat_compare_eq.
nat_compare_lt.
nat_compare_gt.
nat_compare_Lt_lt.
nat_compare_Gt_gt.

*)

(* A helpful lemma that you can use for the proof *)

Lemma everyWhere_insert : forall f x t, f x /\ everyWhere f t -> everyWhere f (insert t x).
  (* intros. induction t; crush. *)
Abort.

Theorem insert_preserves_search_property : forall t n,  search_tree t -> search_tree (insert t n).
Proof.
  (* crush *)
Abort.

Theorem insert_actually_inserts : forall t n, in_tree n (insert t n).
  (* crush *)
Abort.