The Coq mailing list

[Catherine Dubois <dubois AT iie.cnam.fr>]

Edsko de Vries a écrit :
> 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
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>   
We are currently integrating a similar tool for Focal, an environment 
for producing certified code.
See http://focal.inria.fr for information on focal.
Catherine Dubois