The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Thu, Feb 22, 2007 at 12:40:13PM +0000, Sean Wilson wrote:
> 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?

Others have already mentioned QuickCheck; the one downside of QuickCheck
is that if you want to generate counterexamples for arbitrarily defined
inductive data types, you must define "generators" for each of those
datatypes. You could have a look at Gast, which is the QuickCheck
equivalent for Clean (rather than Haskell), but which is based on
generics and can therefore generate instances of inductive datatypes
without help from the programmer.

I don't know how stable it is; more details are at
http://www.cs.ru.nl/~pieter/gentest/gentest.html.

Edsko