The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

Hi,

Does Coq have any facilities available to generate counter examples to 
theorems? Specifically, I want to be able to generate counter examples to 
theorems which make use of arbitrarily defined inductive data types. For 
instance, if I have an inductive definition for sorted lists and a theorem 
about sorted lists, I want to be able to generate valid terms of type sorted 
list and check if they invalidate my theorem.

If Coq doesn't have any facilities like this, does anyone know of any good 
approaches for implementing this, such as any external systems that could be 
utilised or existing tactics that could be adapted for this purpose?

Regards,

Sean