mathlib3 documentation

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 #

Local notation #

Tags #

random monad io

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
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 α 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] :
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 : α) (h : 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 : α) (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 α] [bounded_random α] (x y : α) (p : x y) :

randomly generate a value of type α between x and y

Equations
def io.random_series_r {α : Type} [preorder α] [bounded_random α] (x y : α) (h : 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} (cmd : rand α) :

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 : α) (h : x y) :

Generate a random value between x and y inclusive.

meta def tactic.random_series_r {α : Type u} [preorder α] [bounded_random α] (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] :
rand_g g (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]
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 : ) :

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) :

generate a random bit vector of length n

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