quickcheck tutorial 0.0.0

Here is a short first tutorial on how to use the quickcheck tool (download quickcheck.pure) interactively:

Installation

• Copy the quickcheck.pure file to your working directory (in pure, type  > ! pwd (without >) to know where is it and > ! cd mydir to change it if you wish).
• Start pure (if it not already started).

 Working with quickcheck

• Checking logical propositions (built-ins).

 Load the library: 
> using quickcheck;

Suppose we want to check Pierce's law : $((a \Rightarrow b)  \Rightarrow a) \Leftrightarrow a$.

First, declare some new operators (with arbitrarily the same priority as ||): 
> infix (||) ==> <=>;

in order to define some helper functions: 
> p ==> q = ~p || q; 
> p <=> q = (p ==> q) && (q ==> p);

Then define the proposition (for the moment - May 2nd 2013 - it is impossible to include the arguments as lambdas in the definitions so the following proposition can't be defined as prop_Pierce = \ a::bool b::bool -> ((a ==> b) ==> a) <=> a yet): 
> prop_Pierce a::bool b::bool = ((a ==> b) ==> a) <=> a;

This function is nothing but the mathematical predicate where the free variables have been explicitely given a type. Note that these (boolean here) types are mandatory since this is the only way for the program to decide what the possible values for $a$ and $b$ are.

Finally, run the tests:
> quickcheck prop_Pierce;

The answer:
OK, passed 100 tests.
()
>

means that no contradiction was found (of course, a lot of the tests are redondant here since with 2 possible values for 2 variables, we could have get this result in 4 tests.)

• Checking numerical properties (built-ins) 

 Distributivity of the multiplication over the addition: 
> distrib_mult_over_add_big a::bigint b::bigint c::bigint = a*(b+c) == a*b+a*c;
> quickcheck distrib_mult_over_add_big;

OK, tests are passed, we could have guessed. What about: 
> distrib_mult_over_add a::int b::int c::int = a*(b+c) == a*b+a*c;
> quickcheck distrib_mult_over_add;
> quickcheck distrib_mult_over_add;
> quickcheck distrib_mult_over_add;

Tests always pass. But wait, isn't it surprinsing despite the possible overflows ? Well, it isn't since the int type is a sort of modular ring but we have to be careful with interpretation and remember, for instance, that even if 2*(1500 000 000+1500 000 000) = 2*1500 000 000+2*1500 000 000, each member equals 1705032704.

Indeed, with: 
> distrib_mult_over_add_mix a::int b::bigint c::int = a*(b+c) == a*b+a*c;
> quickcheck distrib_mult_over_add_mix;

the output: 
Falsifiable, after 0 tests:
[-795755684,-9167850166993051345L,-1459775657]
>

warns that, with triple (a,b,c) where a=-795755684, b=-9167850166993051345L and c=-1459775657, the equality doesn't hold.

to be continued...