random number generator

Stream: new members

[Alfredo Garcia]

I am trying to generate a random bitvec using the mathlib control.random however my lack of knowledge with monads is giving me a hard time trying to make it happen. I basically need to generate something random and print it to get myself started:

import control.random

#eval (random_bitvec 3)

however that will not return me the inner generated number, i think it was not generated yet with that code so it should be maybe something more as:

def r : random(bitvec 2) :=
do
...

however i was not able to make it work yet. any help or code reference will be very appreciated. thanks.

[Jason Rute]

I think in Lean 3 (this is Lean 3, right?), that #eval only runs deterministic pure code, so you can’t have a function which is random in there. However, main : IO unit (which can be run from the command line) does allow nondeterministic code. Also, tactics can be nondeterministic (but shouldn’t be for any kind of tactic you intend to use permanently in a proof).

It would help if you explain the #xy problem, namely what are you trying to use a random number generator for in Lean?

[Jason Rute]

https://agentultra.github.io/lean-for-hackers/ Is a good resource for how to write code in Lean 3 which runs like normal software, including having IO and non-deterministic effects. It explains the IO monad too. (I however wouldn’t use their hack for random numbers. I think there are better ways to get random numbers in the IO monad, although I’m not 100% sure.)

[Jason Rute]

Also all of this is easier in Lean 4, since Lean 4 is intended as a real programming language.

[Jason Rute]

For lean 4: https://leanprover.github.io/functional_programming_in_lean

[Alfredo Garcia]

hey there, thank you for the response. i am basically doing some cryptography experiments, proving some basic stuff and creating some example algorithms so is mostly just for learning purposes.
i am aware lean4 is easier for this kind of stuff but as i am also interested in mathlib, so i am working with lean3 which is harder for some of my purposes.

thank you for the lean for hackers link, i think that will help.