Homework 5

Fill in the proofs in Perm.v, SearchTree.v (only those exercises noted below), and Sort.v at each place marked "Exercise". You don't have to do exercises marked "optional" except:

In SearchTree.v do only the following:

replace the proof of lookup_insert_neq with one that does not use bdall or bdestruct_guard
prove bound_default without using bdall or bdestruct_guard
prove lookup_insert_same, following the instructions in the Hint just above it
Add a README comment describing who you helped (or got help from), and what kind of help.
Upload your assignment at right.