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.