BST DEFINITIONS
=================================================================
type bst =
| Leaf
| Node of bst * int * bst

let empty : bst = Leaf

let singleton (n:int) : bst = Node (Leaf, n, Leaf)

let rec insert (t:bst) (n:int) : bst =
    match t with
    | Leaf -> Node (Leaf, n, Leaf)
    | Node (l,x,r) ->
      if n < x then Node((insert l n), x, r)
      else if n > x then Node (l, x, (insert r n))
      else t

let rec sub lo t hi =
        match t with
        | Leaf -> true
        | Node (l,x,r) -> (x>lo) && (x<hi) &&
                          (sub lo l x) && (sub x r hi)

let inv t = sub -inf t +inf
=================================================================


EMPTY
=================================================================
For empty, we need to prove:
inv empty == true

Proof by simple equational reasoning:
   inv empty                                LHS
== inv Leaf                                 eval empty
== sub -inf Leaf +inf                       eval inv
== true                                     eval sub 
=================================================================


SINGLETON
=================================================================
For singleton, wee need to prove:
for all x:int, inv (singleton x) == true

Proof by simple equational reasoning:
First, pick an arbitrary x.
   inv (singleton x)                        LHS
== inv (Node(Leaf,x, Leaf))                 eval singleton
== sub -inf Node(Leaf,x,Leaf)) +inf         eval inv
== (x > -inf) && (x < +inf) &&
   (sub -inf Leaf x) && (sub x Leaf +inf)   eval sub 
== true && true &&
   (sub -inf Leaf x) && (sub x Leaf +inf)   math x2
== true && true && true && true             eval sub x2
== true                                     and identity
=================================================================


INSERT
=================================================================
For insert, we need to prove:
for all t:bst, n:int, inv t => inv (insert t n)

A natural approach would be to attempt a proof by induction,
but one inductive hypothesis for t=Node(l,x,r) would be:
inv l => inv (insert l n)
when evaluated, the RHS results in
sub -inf (insert l n) +inf
... but this is weaker than what we need to maintain the bst property:
sub -inf (insert l n) x

(The same flaw arises for insertion into the right subtree)

So let us first prove the following more general lemma:

  LEMMA
  ===============================================================
  In this case, we have to use the sub invariant's Node case
  with values of hi and lo other than -inf and +inf, and on 
  So we first prove the following lemma:

  for all t:bst, n,lo,hi:int,
  (sub lo t hi) && (lo < n < hi) => (sub lo (insert t n) hi)
  
  Proof by induction on t:
  Case 1) Base case [t = Leaf]
     Assume (sub lo Leaf hi) and (lo < n < hi)
     IMS: sub lo (insert Leaf n) hi == true
     
     sub lo (insert Leaf n) hi              LHS
  == sub lo Node(Leaf, n, Leaf) hi          eval insert
  == (n>lo) && (n<hi) &&
     (sub lo Leaf n) && (sub n Leaf hi)     eval sub 
  == true && true &&
     (sub lo Leaf n) && (sub n Leaf hi)     assumption (lo < n < hi) x2
  == true && true                           eval sub x2

  Case 2) Inductive step [t = Node(l, x, r)], in 3 cases.
  IMS: for all n,lo,hi:int,
     (sub lo t hi) && (lo < n < hi) => (sub lo (insert t n) hi)
  IH1: for all n,lo,hi:int,
     (sub lo l hi) && (lo < n < hi) => (sub lo (insert l n) hi)
  IH2: for all n,lo,hi:int,
     (sub lo r hi) && (lo < n < hi) => (sub lo (insert r n) hi)

    Case 2.1 [n = x]:
       sub lo (insert Node(l, x, r) n) hi   LHS
    == sub lo t hi                          eval insert 
    == true                                 assumption (sub lo t hi)

    Case 2.2 [n < x]:
    From assumption (sub lo t hi), we know (by evaluating sub) that
    a) (x>lo)
    b) (x<hi)
    c) (sub lo l x)
    d) (sub x r hi)

    From assumption (lo < n < hi) and (n < x), we also know that
    e) lo < n < x

       sub lo (insert Node(l, x, r) n) hi        LHS
    == sub lo Node((insert l n), x, r) hi        eval insert
    == (x>lo) && (x<hi) &&
       (sub lo (insert l n) x) && (sub x r hi)   eval sub
    == true && true &&
       (sub lo (insert l n) x) && true           by (a) (b) (d)
    == (sub lo (insert l n) x)                   && identity
    == true                                      IH1 and (c) (e)

    Case 2.3 [n > x]:
    From assumption (sub lo t hi), we know (by evaluating sub) that
    a) (x>lo)
    b) (x<hi)
    c) (sub lo l x)
    d) (sub x r hi)

    From assumption (lo < n < hi) and (n > x), we also know that
    e) x < n < hi

       sub lo (insert Node(l, x, r) n) hi        LHS
    == sub lo Node(l, x, (insert r n)) hi        eval insert
    == (x>lo) && (x<hi) &&
       (sub lo l x) && (sub x (insert r n) hi)   eval sub
    == true && true &&
       true && (sub x (insert r n) hi)           by (a) (b) (c)
    == (sub x (insert r n) hi)                   && identity
    == true                                      IH2 and (d) (e)
  ===============================================================

Now, we will show that what we must prove is an instance of Lemma
 (sub lo t hi) && (lo < n < hi) => (sub lo (insert t n) hi)
where lo = -inf and hi = +inf

   (sub lo t hi) && (lo < n < hi) =>
     (sub lo (insert t n) hi)                       Lemma
== (sub -inf t +inf) && (-inf < n < +inf) =>
     sub -inf (insert t n) +inf                     substitution
== (sub -inf t +inf) && true =>
     sub -inf (insert t n) +inf                     math
== (sub -inf t +inf) => sub -inf (insert t n) +inf  && id.
== inv t => inv (insert t n)                        inv. eval inv x2

This was what we needed to prove. QED.
=================================================================