mathlib documentation

system.random.basic

Rand Monad and Random Class

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

Main definitions

Local notation

Tags

random monad io

References

def rand_g  :
Type → Type uType u

A monad to generate random objects using the generator type g

Equations
def rand  :
Type u_1Type u_1

A monad to generate random objects using the generator type std_gen

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
@[class]
structure random  :
Type uType (max 1 u)

random α gives us machinery to generate values of type α

Instances
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] :
rand_g 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 α] :
rand_g g α

Generate a random value of type α.

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

generate an infinite series of random values of type α

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

Generate a random value between x and y inclusive.

Equations
def rand.random_series_r {α : Type u} {g : Type} [random_gen g] [preorder α] [bounded_random α] (x y : α) :
x yrand_g g (stream (set.Icc x y))

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

Equations

create and a seed a random number generator

Equations
def io.run_rand {α : Type} :
rand αio α

Run cmd using a randomly seeded random number generator

Equations
def io.run_rand_with {α : Type} :
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 α] [bounded_random α] (x y : α) :
x yio (set.Icc x y)

randomly generate a value of type α between x and y

Equations
def io.random_series_r {α : Type} [preorder α] [bounded_random α] (x y : α) :
x yio (stream (set.Icc x y))

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

Equations

create a seeded random number generator in the tactic monad

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

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

meta def tactic.random_r {α : Type u} [preorder α] [bounded_random α] (x y : α) :
x ytactic (set.Icc x y)

Generate a random value between x and y inclusive.

meta def tactic.random_series_r {α : Type u} [preorder α] [bounded_random α] (x y : α) :
x ytactic (stream (set.Icc 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 α

def fin.random {g : Type} [random_gen g] {n : } [fact (0 < n)] :
rand_g g (fin n)

generate a fin randomly

Equations
@[instance]

Equations
@[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
@[instance]
def fin_random (n : ) [fact (0 < n)] :

Equations
@[instance]

Equations
def random_fin_of_pos {n : } :
0 < nrandom (fin 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
@[instance]

Equations
@[instance]

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

generate a random bit vector of length n

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

generate a random bit vector of length n

Equations
@[instance]
def random_bitvec (n : ) :

Equations
@[instance]

Equations