Proving correctness of an AVL-Tree colouring algorithm

Question

I came up with the following recursive algorithm to colour the nodes of an AVL tree so that the resulting tree is red-black. The logic is that the algorithm first colours the root and, recursively, the left and right subtrees black. Since it is an AVL tree, if the root has height h, one path to a leaf takes distance h, and another is h-1. If h is odd the two subtrees from the root have heights h-1 (even) and h-2 (odd), with the even subtree having an extra black node, hence to be coloured red.

(pseudocode)
colour_tree(root(T)):
r <- root(T)
if r = null:
    return
colour(r) = "black"

colour_tree(right(r))
colour_tree(left(r))

if isodd(height(r)):
    if right(r) != null and iseven(right(r)):
        colour(right(r)) = "red"
    if left(r) != null and iseven(left(r)):
        colour(left(r)) = "red"

I am having trouble starting on a proof of correctness for this algorithm. I know that for any tree with height h, there are at least $\lceil (h+1)/2 \rceil$ blacknodes, and intuitively it seems like I'd have to perform induction on the height, but I am not sure where to start. Thanks.

Answer 1

You are recursing structurally, so you might want structural induction, but in AVL trees structural induction and induction on height are similar. You probably want to prove something a bit stronger than you need at the end - perhaps something like "AVL trees with height n return RB trees with black height n, and if n is even then neither child of the root is colored red."