Homework #4

Due Monday, 12 Feb @ 5:00 pm

This is an ACL2 assignment. You need not turn in handwritten proofs. However, you may find that writing parts of it by hand helps you to guide ACL2.
This assignment is difficult. Start early and ask questions!

Your task is to represent binary search trees of numbers as we discussed in class and write a function insert : Number BST → BST. Your BSTs should permit duplicate values (imagine you're representing a multiset). This can be accommodated by using a BST invariant that says that all numbers in the left subtree are less or equal to the root, and numbers in the right subtree are strictly larger than the root. You must prove that insert holds up its end of the contract; that is, prove that insert delivers a BST under the assumptions that it is given a Number and a BST.

You must also prove that insert works properly. In particular, if you insert a number n into a tree tree, then the new tree has one more occurrence of n than does tree.

Hints

You will need several lemmas (= helper-theorems). A key to successful theorem proving is to know how to recognize when the proof you're doing requires a lemma. Three are necessary for this assignment.

ACL2 is unable to discover that branches are distinct from leaves without help (due to the way defstructure works):
```
(defstructure leaf)
(defstructure branch value left right)

(defthm leaf-p-branch=nil&branch-p-leaf=nil
  (and (equal (leaf-p (branch X Y Z)) nil)
       (equal (branch-p (leaf)) nil))
  :hints (("Goal" :in-theory (enable leaf leaf-p weak-leaf-p
                                     branch branch-p weak-branch-p))))
```
That theorem above instructs ACL2 to prove that leaves are distinct from branches. The hint allows ACL2 to see inside the representation of the structures for the duration of the proof. You should *not* use any hints anywhere else; letting ACL2 see through the structures often causes it to get confused outside of corner cases like this.
Your definition of bst? : Any -> Boolean will involve helper predicates all-<= : BST Number -> Boolean and all-> : BST Number -> Boolean. To show that insert obeys its contract, you will first need to prove the following:
Suppose that all the numbers in tree are less than or equal to num, and (<= x num). Then all the numbers in (insert x tree) are less than or equal to num.
To see why, try writing out some of the inductive step of the proof that insert obeys its contract. You will also need an analogous theorem to cover the case when you insert a large number into the tree.

If ACL2 does not stop on a proof attempt, use Dracula's Stop Prover button. Unfortunately, this closes the proof window and causes you to lose the checkpoints that you'll need to look at. To get around this, use with-prover-time-limit:

;; Attempt to prove my-theorem, but automatically fail after 10 seconds

(with-prover-time-limit 10
  (defthm my-theorem
    (implies foo bar)))

Then you can examine the checkpoints as usual. Note that 10 seconds should be plenty for the theorems on this assignment.