-*- coding: utf-8 -*-

In precept, we worked with the minimal
binary search tree ADT from bst.ml

We (exhaustively) worked through the
representation invariant proofs (see inv.txt).

We can define a relation between the bst
implementation and an abstract concept of
using set notation:

let empty = {}
let singleton n = {n}
let member s n = n ε s
let insert s n = {n} U s
let rec abs t =
   match t with
   | Leaf -> {}
   | Node (l,x,r) -> (abs l) U {x} U (abs r)

Your first exercise is to determine the
proof obligation for this abstraction
relationship.



=============================================
Stop. Answer for this first exercise is below
=============================================



The proof obligation is as follows:

(1) inv empty => abs empty = {}
(2) Forall x:int,
    inv (singleton x) => abs (singleton x) = {x}
(3) Forall x:int,t:bst,
    inv t => (x ε abs t <==> member t x)
(4) Forall x,y:int,t:bst,
    inv t => (x ε abs (insert t y) <==> ((x=y) V (x ε abs t)))

This week's second exercise is to complete these proofs, several of
which are quite intense, but serve as great practice for the exam!

Recall that to prove an implication (x=>y), we assume x
and then prove that y = true. It follows, then, that to
prove x<==>y, we can split it:
   * assume x, then prove that y = true
   * assume y, then prove that x = true

Here's a useful lemma: x ε (a U b) <==> (x ε a) V (x ε b)