The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Adam Chlipala wrote:
> Marko Malikoviæ wrote:
> > I'm trying to find some function for generating random (pseudo-random)
> > numbers in Coq. It seems that it doesn't exists. Am I right?
> > If it doesn't exists than I need some seed state. But, I don't see some
> > time (or simmilary) function in Coq.
> >   
>
> Every Coq function is pure.  It is impossible to write a function of 
> type, e.g., [unit -> nat] that returns different values on different 
> calls.  Thus, there can exist no equivalents of C rand() or time(); 
> assuming such a function exists leads to a contradiction.
>
> You can still thread a time or random number seed through a program as 
> an explicit argument/return value, though.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/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
I devised one such pseudo-random function a few weeks ago, using two 
large prime numbers.

CoFixpoint rand (seed n1 n2 : Z) : Stream Z :=
   let seed' := Zmod seed n2 in Cons seed' (rand (seed' * n1) n1 n2).

Now, you would have to choose n1 n2 to be primes, and you would obtain a 
fairly uniform distribution of numbers between 1 and n2-1.  This is not 
a very good generator, but it was good enough for my purpose of 
generating large lists of numbers to test the efficiency of various 
sorting algorithms.  Note that, from the Coq
point of view, the whole sequence of numbers is viewed as one single 
object, and the head of this sequence is always the same: it is your 
responsibility to read data from the stream further and further as you 
consumes the generated numbers.  This corresponds to threading a time 
and random number seed as an explicit argument value, as Adam suggests.

Anyway, what is your context of usage?  If the random generator needs to 
interact with extracted code, you can easily adapt the code from

http://logical.saclay.inria.fr/cocorico/ZInterfacePackage

to design a new co-inductive stream similar to input_stream_Z but that 
would read off a random number generator instead of reading off the 
standard input.

Yves