Simple unit testing in Coq

July 25, 2015

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:

Require Import Coq.Lists.List.

Import ListNotations.

Definition test_pred :
  List.map pred [0; 1; 2; 5] = [0; 0; 1; 4] :=
  eq_refl.

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:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-cunit

Now we can test the plus function:

Require Import Coq.Lists.List.
Require Import CUnit.All.

Import ListNotations.

Definition test_plus : List.map_pair plus
  [(0, 0); (0, 3); (4, 0); (4, 3)] =
  [0; 3; 4; 7] :=
  eq_refl.

The complete list of maps in the package CUnit is the following:

  • List.map_pair {A B C} (f : A -> B -> C) (l : list (A * B)) : list C
  • List.map_triple {A B C D} (f : A -> B -> C -> D) (l : list (A * B * C)) : list D
  • List.map_quad {A B C D E} (f : A -> B -> C -> D -> E) (l : list (A * B * C * D)) : list E

Edit: this list of functions can be generalized to an arbitrary number of arguments. See the post Currying using Canonical Structures of Guillaume Allais.

blog comments powered by Disqus