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;

Tags #

random monad io

References #

Similar library in Haskell: https://hackage.haskell.org/package/MonadRandom

source

@[reducible]

def rand_g (g : Type) (α : Type u) :

Type u

A monad to generate random objects using the generator type g

Equations

rand_g g α = state (ulift g) α

source

@[reducible]

def rand (α : Type u_1) :

Type u_1

A monad to generate random objects using the generator type std_gen

Equations

rand = rand_g std_gen

source

@[protected, instance]

def rand_g.uliftable (g : Type) :

uliftable (rand_g g) (rand_g g)

Equations

rand_g.uliftable g = state_t.uliftable' (equiv.ulift.trans equiv.ulift.symm)

source

def rand_g.next {g : Type} [random_gen g] :

rand_g g ℕ

Generate one more ℕ

Equations

rand_g.next = ⟨prod.map id ulift.up ∘ random_gen.next ∘ ulift.down⟩

source

@[class]

structure bounded_random (α : Type u) [preorder α] :

Type (max 1 u)

random_r : Π (g : Type) [_inst_1_1 : random_gen g] (x y : α), x ≤ y → rand_g g ↥(set.Icc x y)

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

source

@[class]

structure random (α : Type u) :

Type (max 1 u)

random : Π (g : Type) [_inst_1 : random_gen g], rand_g g α

random α gives us machinery to generate values of type α

Instances of this typeclass

Instances of other typeclasses for random

random.has_sizeof_inst

source

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

shift_31_left = 2147483648

source

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

rand.split g = ⟨prod.map id ulift.up ∘ random_gen.split ∘ ulift.down⟩

source

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

rand_g g α

Generate a random value of type α.

Equations

rand.random α = random.random α g

source

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

rand.random_series α = uliftable.up (rand.split g) >>= λ (gen : ulift g), has_pure.pure (stream.corec_state (random.random α g) gen)

source

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

rand_g g ↥(set.Icc x y)

Generate a random value between x and y inclusive.

Equations

rand.random_r x y h = bounded_random.random_r g x y h

source

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

rand_g g (stream ↥(set.Icc x y))

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

Equations

rand.random_series_r x y h = uliftable.up (rand.split g) >>= λ (gen : ulift g), has_pure.pure (stream.corec_state (bounded_random.random_r g x y h) gen)

source

def io.mk_generator :

io std_gen

create and seed a random number generator

Equations

io.mk_generator = io.rand 0 shift_31_left >>= λ (seed : ℕ), return (mk_std_gen seed)

source

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

io α

Run cmd using a randomly seeded random number generator

Equations

io.run_rand cmd = io.mk_generator >>= λ (g : std_gen), return (cmd.run {down := g}).fst

source

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

io α

Run cmd using the provided seed.

Equations

io.run_rand_with seed cmd = return (cmd.run {down := mk_std_gen seed}).fst

source

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

io α

randomly generate a value of type α

Equations

io.random = io.run_rand (rand.random α)

source

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

io (stream α)

randomly generate an infinite series of value of type α

Equations

io.random_series = io.run_rand (rand.random_series α)

source

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

io ↥(set.Icc x y)

randomly generate a value of type α between x and y

Equations

io.random_r x y p = io.run_rand (bounded_random.random_r std_gen x y p)

source

def io.random_series_r {α : Type} [preorder α] [bounded_random α] (x y : α) (h : x ≤ y) :

io (stream ↥(set.Icc x y))

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

Equations

io.random_series_r x y h = io.run_rand (rand.random_series_r x y h)

source

meta def tactic.mk_generator :

tactic std_gen

create a seeded random number generator in the tactic monad

source

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

tactic α

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

source

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

tactic ↥(set.Icc x y)

Generate a random value between x and y inclusive.

source

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

tactic (stream ↥(set.Icc x y))

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

source

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

tactic α

randomly generate a value of type α

source

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

tactic (stream α)

randomly generate an infinite series of value of type α

source

@[protected]

def fin.random {g : Type} [random_gen g] {n : ℕ} [ne_zero n] :

rand_g g (fin n)

generate a fin randomly

Equations

fin.random = ⟨λ (_x : ulift g), fin.random._match_1 _x⟩
fin.random._match_1 {down := g_1} = prod.map fin.of_nat' ulift.up (rand_nat g_1 0 n)

source

@[protected, instance]

def nat_bounded_random :

bounded_random ℕ

Equations

nat_bounded_random = {random_r := λ (g : Type) (inst : random_gen g) (x y : ℕ) (hxy : x ≤ y), fin.random >>= λ (z : fin (y - x).succ), has_pure.pure ⟨z.val + x, _⟩}

source

@[protected, instance]

def int_bounded_random :

bounded_random ℤ

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

int_bounded_random = {random_r := λ (g : Type) (inst : random_gen g) (x y : ℤ) (hxy : x ≤ y), bounded_random.random_r g 0 (y - x).nat_abs _ >>= λ (_p : ↥(set.Icc 0 (y - x).nat_abs)), int_bounded_random._match_1 g x y hxy _p}
int_bounded_random._match_1 g x y hxy ⟨z, _⟩ = has_pure.pure ⟨↑z + x, _⟩

source

@[protected, instance]

def fin_random (n : ℕ) [ne_zero n] :

random (fin n)

Equations

fin_random n = {random := λ (g : Type) (inst : random_gen g), fin.random}

source

@[protected, instance]

def fin_bounded_random (n : ℕ) :

bounded_random (fin n)

Equations

fin_bounded_random n = {random_r := λ (g : Type) (inst : random_gen g) (x y : fin n) (p : x ≤ y), rand.random_r x.val y.val p >>= λ (_p : ↥(set.Icc x.val y.val)), fin_bounded_random._match_1 n g x y _p}
fin_bounded_random._match_1 n g x y ⟨r, _⟩ = has_pure.pure ⟨⟨r, _⟩, _⟩