Good way of testing a class in Coq

Question

Is there a good way to test the implementation of a class in Coq ?

For example, if I have the following very simple Class:

Theorem chekc_modulo (c: nat): {c mod 2 = 0} + {c mod 2 <> 0} .
Admitted.

Definition update(n: nat):= add n one.
  
Class test :={
  f: R -> nat;
  g: R -> nat;
  counting: nat;
  init: counting = zero /\ f 0 = 0 /\ g 0 = 0;
  output: forall t, t >= 0 -> 
  match chekc_modulo counting with
    |left _ => f t = 1 /\ g t = 0 /\ update counting
    |right _ => g t = 1 /\ g t = 0 /\ update counting
  end
    
}.

I would like to find a way to test this class, so basically to check that f and g have the required values after processing the output.

What I did so far: I manually implemented f and g by giving them the values I expect they will have at a given t, after processing in output. And now I try to create an instance of the Class test to see what happens with the output.

I am a bit stuck because i do not see how to get the actual output and therefore how to check that the implementation is actually correct.

Does anyone have a tip ? In general, is there a better way to test code in Coq, especially Classes ?

EDIT:

In my testing strategy, I have defined the expected behavior of f and g:

Definition f': nat -> nat :=
  fun t =>
    match chekc_modulo t with 
    |left _ => 1
    |right _ => 0
    end.

Definition g': nat -> nat :=
  fun t =>
    match chekc_modulo t with 
    |left _ => 0
    |right _ => 1
    end.

So the next step, would be to check that this behavior is indeed the same as what happens after output is processed.

user_1633770 · Answer

For testing Coq code, you might find the QuickChick plugin useful. It allows you to write properties that your definitions should satisfy, and generates random test cases to check if they hold. In principle, it should work fine with type classes as well.

However, given your code snippet, I have the impression that there is some misunderstanding about what classes in Coq are. For instance, the assertion counting = counting + 1 suggests that you are trying to update the value of counting somehow. In Coq, it is not possible to update the value of a variable: the assertion counting = counting + 1 means that the number counting equals its successor, which is impossible.

I don't know if this helps, but classes in Coq are closer to type classes in Haskell than to classes in object-oriented languages such as Java, and an "instance" of a class is more similar to a class that implements a Java interface than an object that is an instance of a class.

Perhaps we could provide more help if you gave us more context about what you are trying to do.

Good way of testing a class in Coq

1 Answers