Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Pseudo random numbers in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pseudo random numbers in Coq


chronological Thread 
  • From: Cedric Auger <Cedric.Auger AT lri.fr>
  • To: Marko Malikovi� <marko AT ffri.hr>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Pseudo random numbers in Coq
  • Date: Thu, 12 Mar 2009 14:28:48 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Marko Malikoviæ a écrit :
Greetings,

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.

Thank you and greetings from Croatia,

Marko Malikoviæ


A random number generator easily be defined in coq and I am almost sure it has already be done with seed, but you cant use time (only seeds)!

There is no time function and I hope there will never be one, because coq functions must be total and well defined, I want to be able to prove "time tt = time tt" with refl_equal, but:
- if you assume a mechanism such that "time tt" is constant during whole execution, then there is no interest having such a function
- if you assume "time tt" is not constant, you break consistency of coq, and there is no more interest in it.

All you can do is either
- use only one seed for all your program and assume:
"Variable seed : positive."
(best solution I think)

- use a monad:
"Definition time_ := positive."
"Record time_result (A : Type) : Type := mktime {tm : time_; value : A}."
"Axiom wait : time_ -> time_." which simulates time
"Hypothesis time_increase : forall t, t<wait t."
and change all your function call to update time, for example
"Definition time (t : time_) (u : unit) :=
let new_time := wait t in
   mktime (t t)."
"Definition random (t : time_) (u : unit) :=
let r := [pseudo random generation using t] in
mktime (wait t) r."

and now you have that
~(let (t1, t2) := time t tt in let (t3, t4) := time t1 tt in t2 = t4)
which expresses that "time ()<> time()", a common fact in most programming languages.
It is very heavy and you will probably forgot to update it at right time. Furthermore you need to rewrite all.

Conclusion: forget about time...

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay





Archive powered by MhonArc 2.6.16.

Top of Page