Even if we can prove things in Coq, unit testing remains an extremely simple and powerful technique to verify what we write. Thanks to the dependent types, we can run unit tests in Coq at compile time by computing into the types. For example, in:

Definition test_pred : pred 5 = 4 :=
eq_refl.

we check that the predecessor of 5 is 4 by saying that they are logically equal. The proof of the equality is its only constructor eq_refl. We force the type-checker of Coq to reduce both pred 5 and 4 to check that they are the same.

Usually we want to check many values, what we can do with a list:

We map the pred function on the values 0, 1, 2, 5 and check the results.

The CUnit package

For functions with several parameters, the trick of the List.map function does not work well because of the currying. What need instead is a map over lists of tuples. I made the package CUnit to provide such a map. Install it with OPAM: