The deadline for this problem set was Wednesday, November 4 at 9pm.
Submit your work on Gradescope at Problem Set 7.
Problem Set 7
Red-black trees
Before you start this problem set
Please fill out a survey about the time you spent on Problem Set 6.
Download
pset07_definitions.dfypset07.dfypset07_validator.dfypset07_hints.dfy← but don’t read yet
The structure here follows that of previous psets: read pset07_definitions.dfy to see our supporting definitions on red-black trees, complete pset07.dfy with your edits of the functions we point you toward, and use pset07_validator.dfy to confirm you’re done.
This time, the validator contains a nontrivial example proof building on the data structure we ask you to verify.
See also pset07_hints.dfy for suggestions, in case you get stuck. But beware that this file may give away some of the interesting challenges.
An example of how Ins and Balance rebalance a tree
The implementation provided in the definitions file is explained in the paper Red-black trees in a functional setting by Chris Okasaki. Here is an example of how the insertion algorithm proceeds:
We’ll insert the value 
6, 8, and 12 are red, the rest are black.
Calling Insert(7, ...) results in recursive calls to Ins that eventually reach the Empty left subtree of 8.
A red 7 replaces that empty left subtree, and Balance on the resulting tree rooted at 8 does nothing.
That result is now the left subtree of 9.
The new tree rooted at 9 matches the first case in Balance, where a black node has a red left child with a red left child.
In the diagram on the right, values x, y, and z are labeled as in the match case in Balance and in Figure 1 from the paper — it’s the case on the left in that figure. Subtrees a, b, c, d are all empty.
Balance rotates and recolors the tree so it is now rooted at 8.
That tree is now the right subtree of 6.
Balance on the new tree rooted at 6 does nothing.
OK — that result is now the left subtree of 10.
Again at 10 we match a case in Balance: red left child with a red right child.
Matching values x, y, & z are labeled, along with matching subtrees a, b, c, & d.
Balance rotates and recolors that subtree, which becomes the left subtree of 12.
Balance on the tree rooted at 12 does nothing.
