Verify a red black tree

Question

I am trying to verify whether a binary tree is a red-black one. Some properties I need to check is that:

1. Root is black
2. There cannot be 2 consecutive red nodes.
3. You need to add empty nodes as leaf nodes, whose color is taken as black.
4. Every path from a leaf to the root contains the same number of black nodes

Somehow, my test cases are all passed but I am sure I did not implement the number 4 above.

How can I check whether any depth from root till Empty (the end) has the same number of black nodes?

I define my tree to be :

type 'a tree = Empty | T of color * 'a tree * 'a * 'a tree 

My code simply matches the current tree with some bad cases and return false. Otherwise, call the recursive function on the left and right branches.

let rec good_RB t = match t with
   | Empty -> true
   | T (R, T (R, _, _, _), _, _)
   | T (R , _, _, T (R, _, _, _)
     -> false
   | T (_, lft, _, rgt) -> good_RB lft && good_RB rgt

Answer 1

Well, you need to keep a counter :

let rec nb_blacks_lftmst acc = function
  | Empty -> acc
  | T (c, lft, _, _) ->
    nb_blacks_lftmst (match c with R -> acc | B -> acc + 1) lft

let good_count = function
  | Empty -> true
  | T (_, lft, _, rgt) ->
    let cpt = nb_blacks_lftmst 0 lft in
    let rec aux acc = function
      | Empty -> acc = cpt
      | T (c, lft, _, rgt) ->
        let acc = match c with R -> acc | B -> acc + 1 in
        aux acc lft && aux acc rgt
    in
    aux 0 lft && aux 0 rgt

Something like this should work. (in my answer, the leftmost path is visited twice, first time to get the witness counter, second times because I don't want to write a complicated code to not visit it a second time)