Lab 3 is a lot less guided than lab 1 and 2: you will need to prove multiple lemmas for each of the BST theorems, and we do not give the exact statement of each lemma. Think about the proofs on paper, take each proof slowly, and do not hesitate to prove useful intermediate results as separate lemmas.

There are lemmas on BSTs in lab 2 that could be useful for this lab.

Definition rotR (t : tree) :=
  match t with
  | Node v lt rt =>
      match lt with
      | Node v' llt lrt => Node v' llt (Node v lrt rt)
      | _ => t
      end
  | _ => t
  end.

Definition rotL (t : tree) :=
  match t with
  | Node v lt rt =>
      match rt with
      | Node v' lrt rrt => Node v' (Node v lt lrt) rrt
      | _ => t
      end
  | _ => t
  end.

It may also be useful to know that you can switch to proving False by calling exfalso. This, for example, enables you to apply lemmas that end in -> False or neg. Of course, only do this if the hypotheses are contradictory.

Consider destruct (rightmost tr2) or destruct (is_leaf tr2) instead of destruct tr2. Not breaking apart the tree itself can avoid a mess.

A convenient way to specify "the largest element in this set" is to say that all elements in this set are no larger than the given element.

merge_ordered needs a rather strong precondition. It does not work correctly for merging just any two trees. However, it is called in a rather specific scenario. (And it is feasible to prove its use by inlining it, but we found a separate specification helpful.)

Why is it bad to call merge_ordered on trees representing the sets {3, 4} and {1, 2}?

Our proofs, contains a couple of long apply … with invocations, such as this:

apply bst_iff with (P:=let S' := (fun x : t => S x /\ d < x) in (fun x : t => S' x /\ x < rm)).