coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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,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)!
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æ
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
- [Coq-Club] Pseudo random numbers in Coq, Marko Malikoviæ
- Re: [Coq-Club] Pseudo random numbers in Coq,
Adam Chlipala
- Re: [Coq-Club] Pseudo random numbers in Coq, Yves Bertot
- Re: [Coq-Club] Pseudo random numbers in Coq, Cedric Auger
- Re: [Coq-Club] Pseudo random numbers in Coq, Marko Malikoviæ
- Re: [Coq-Club] Pseudo random numbers in Coq,
Adam Chlipala
Archive powered by MhonArc 2.6.16.