control.random

# Rand Monad and Random Class #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This module provides tools for formulating computations guided by randomness and for defining objects that can be created randomly.

## Main definitions #

• rand monad for computations guided by randomness;
• random class for objects that can be generated randomly;
• random to generate one object;
• random_r to generate one object inside a range;
• random_series to generate an infinite series of objects;
• random_series_r to generate an infinite series of objects inside a range;
• io.mk_generator to create a new random number generator;
• io.run_rand to run a randomized computation inside the io monad;
• tactic.run_rand to run a randomized computation inside the tactic monad

## Local notation #

• i .. j : Icc i j, the set of values between i and j inclusively;

## References #

@[reducible]
def rand_g (g : Type) (α : Type u) :

A monad to generate random objects using the generator type g

Equations
@[reducible]
def rand (α : Type u_1) :
Type u_1

A monad to generate random objects using the generator type std_gen

Equations
@[protected, instance]
Equations
def rand_g.next {g : Type} [random_gen g] :

Generate one more ℕ

Equations
@[class]
structure bounded_random (α : Type u) [preorder α] :
Type (max 1 u)

bounded_random α gives us machinery to generate values of type α between certain bounds

Instances of this typeclass
Instances of other typeclasses for bounded_random
• bounded_random.has_sizeof_inst
@[class]
structure random (α : Type u) :
Type (max 1 u)
• random : Π (g : Type) [_inst_1 : , α

random α gives us machinery to generate values of type α

Instances of this typeclass
Instances of other typeclasses for random
• random.has_sizeof_inst
def shift_31_left  :

shift_31_left = 2^31; multiplying by it shifts the binary representation of a number left by 31 bits, dividing by it shifts it right by 31 bits

Equations
def rand.split (g : Type) [random_gen g] :
g

create a new random number generator distinct from the one stored in the state

Equations
def rand.random (α : Type u) {g : Type} [random_gen g] [random α] :
α

Generate a random value of type α.

Equations
def rand.random_series (α : Type u) {g : Type} [random_gen g] [random α] :
(stream α)

generate an infinite series of random values of type α

Equations
def rand.random_r {α : Type u} {g : Type} [random_gen g] [preorder α] (x y : α) (h : x y) :
(set.Icc x y)

Generate a random value between x and y inclusive.

Equations
• h = h
def rand.random_series_r {α : Type u} {g : Type} [random_gen g] [preorder α] (x y : α) (h : x y) :

generate an infinite series of random values of type α between x and y inclusive.

Equations

create and seed a random number generator

Equations
def io.run_rand {α : Type} (cmd : rand α) :
io α

Run cmd using a randomly seeded random number generator

Equations
def io.run_rand_with {α : Type} (seed : ) (cmd : rand α) :
io α

Run cmd using the provided seed.

Equations
def io.random {α : Type} [random α] :
io α

randomly generate a value of type α

Equations
def io.random_series {α : Type} [random α] :
io (stream α)

randomly generate an infinite series of value of type α

Equations
def io.random_r {α : Type} [preorder α] (x y : α) (p : x y) :

randomly generate a value of type α between x and y

Equations
• y p =
def io.random_series_r {α : Type} [preorder α] (x y : α) (h : x y) :

randomly generate an infinite series of value of type α between x and y

Equations
meta def tactic.mk_generator  :

create a seeded random number generator in the tactic monad

meta def tactic.run_rand {α : Type u} (cmd : rand α) :

run cmd using the a randomly seeded random number generator in the tactic monad

meta def tactic.random_r {α : Type u} [preorder α] (x y : α) (h : x y) :

Generate a random value between x and y inclusive.

meta def tactic.random_series_r {α : Type u} [preorder α] (x y : α) (h : x y) :

Generate an infinite series of random values of type α between x and y inclusive.

meta def tactic.random {α : Type u} [random α] :

randomly generate a value of type α

meta def tactic.random_series {α : Type u} [random α] :

randomly generate an infinite series of value of type α

@[protected]
def fin.random {g : Type} [random_gen g] {n : } [ne_zero n] :
(fin n)

generate a fin randomly

Equations
@[protected, instance]
Equations
@[protected, instance]

This bounded_random interval generates integers between x and y by first generating a natural number between 0 and y - x and shifting the result appropriately.

Equations
@[protected, instance]
def fin_random (n : ) [ne_zero n] :
Equations
@[protected, instance]
def fin_bounded_random (n : ) :
Equations
def random_fin_of_pos {n : } (h : 0 < n) :

A shortcut for creating a random (fin n) instance from a proof that 0 < n rather than on matching on fin (succ n)

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def bitvec.random {g : Type} [random_gen g] (n : ) :
(bitvec n)

generate a random bit vector of length n

Equations
def bitvec.random_r {g : Type} [random_gen g] {n : } (x y : bitvec n) (h : x y) :
(set.Icc x y)

generate a random bit vector of length n

Equations
@[protected, instance]
def random_bitvec (n : ) :
Equations
@[protected, instance]
def bounded_random_bitvec (n : ) :
Equations