Zulip Chat Archive

Stream: Is there code for X?

Topic: random number generator


Kenny Lau (May 15 2020 at 21:26):

Do we have an RNG? Presumably it will take in the system time in some way or another

Chris Hughes (May 15 2020 at 21:27):

I remember seeing one somewhere in core I think.

Kenny Lau (May 15 2020 at 21:27):

there's io.rand in https://github.com/leanprover-community/lean/blob/master/library/system/io.lean

Kenny Lau (May 15 2020 at 21:27):

but it doesn't use the system time

Reid Barton (May 15 2020 at 21:27):

You could read bytes from /dev/urandom (probably)

Kenny Lau (May 15 2020 at 21:30):

how do you read a file?

Chris Hughes (May 15 2020 at 21:31):

It's an actual function, so you can prove theorems about it if you want

Kenny Lau (May 15 2020 at 21:32):

I just want random numbers for a programming kata

Reid Barton (May 15 2020 at 21:36):

like this: https://github.com/leanprover-community/lean/blob/master/leanpkg/leanpkg/manifest.lean#L105

Kevin Buzzard (May 15 2020 at 21:37):

Kenny Lau said:

I just want random numbers for a programming kata

I would recommend 37

Jalex Stark (May 15 2020 at 22:05):

Kenny Lau said:

I just want random numbers for a programming kata

you want the tests to be random?
you could generate ~10 tests, hardcode them in, and not expose them to the user

Kenny Lau (May 15 2020 at 22:14):

that is impossible, as demonstrated by the back-and-forth in https://leanprover.zulipchat.com/#narrow/stream/238266-Codewars/topic/hackproofing.20programming.20katas

Jalex Stark (May 15 2020 at 22:17):

oof

Yaël Dillies (Jan 12 2022 at 10:21):

How does one use randomness? I'm trying to understand file#control/random ...

Yaël Dillies (Jan 12 2022 at 10:22):

Can it only be used within tactics? This doesn't work because it's missing {g : Type} [random_gen g].

import control.random

#eval rand.random_r (2 : ) 2 le_rfl = 2 -- don't know how to synthesize placeholder

Yaël Dillies (Jan 12 2022 at 10:29):

Ohoh! I think I figured out

import control.random

#eval rand_nat (mk_std_gen 37) 0 2564645983587834878

Replace 37 by whatever you want it will generate another random number.

Kevin Buzzard (Jan 12 2022 at 11:45):

Is 37 not random enough for you?

Mario Carneiro (Jan 13 2022 at 04:27):

obligatory XKCD: https://xkcd.com/221/


Last updated: Dec 20 2023 at 11:08 UTC