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
randmonad for computations guided by randomness;randomclass for objects that can be generated randomly;randomto generate one object;random_rto generate one object inside a range;random_seriesto generate an infinite series of objects;random_series_rto generate an infinite series of objects inside a range;
io.mk_generatorto create a new random number generator;io.run_randto run a randomized computation inside theiomonad;tactic.run_randto run a randomized computation inside thetacticmonad
Local notation
i .. j:Icc i j, the set of values betweeniandjinclusively;
Tags
random monad io
References
- Similar library in Haskell: https://hackage.haskell.org/package/MonadRandom
Equations
Generate one more ℕ
Equations
- rand_g.next = ⟨prod.map id ulift.up ∘ random_gen.next ∘ ulift.down⟩
- 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
- to_bounded_random : bounded_random α
- random : Π (g : Type) [_inst_1 : random_gen g], rand_g g α
random α gives us machinery to generate values of type α
Instances
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
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⟩
Generate a random value of type α.
Equations
- rand.random α = random.random α g
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)
Generate a random value between x and y inclusive.
Equations
- rand.random_r x y h = bounded_random.random_r g x y h
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)
create and a seed a random number generator
Equations
- io.mk_generator = io.rand 0 shift_31_left >>= λ (seed : ℕ), return (mk_std_gen seed)
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
randomly generate a value of type α
Equations
randomly generate an infinite series of value of type α
Equations
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)
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)
create a seeded random number generator in the tactic monad
run cmd using the a randomly seeded random number generator
in the tactic monad
Generate a random value between x and y inclusive.
Generate an infinite series of random values of type α between x and y inclusive.
randomly generate a value of type α
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)
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, _⟩}
Equations
- fin_random n = {to_bounded_random := {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_random._match_1 n g x y _p}, random := λ (g : Type) (inst : random_gen g), fin.random}
- fin_random._match_1 n g x y ⟨r, _⟩ = has_pure.pure ⟨⟨r, _⟩, _⟩
A shortcut for creating a random (fin n) instance from
a proof that 0 < n rather than on matching on fin (succ n)
Equations
- random_fin_of_pos _x = fin_random n.succ
- random_fin_of_pos h = _.elim
Equations
- bool.random = {to_bounded_random := {random_r := λ (g : Type) (_inst : random_gen g) (x y : bool) (p : x ≤ y), subtype.map bool.of_nat _ <$> bounded_random.random_r g x.to_nat y.to_nat _}, random := λ (g : Type) (inst : random_gen g), (bool.of_nat ∘ subtype.val) <$> bounded_random.random_r g 0 1 bool.random._proof_1}
generate a random bit vector of length n
Equations
- bitvec.random n = bitvec.of_fin <$> rand.random (fin (2 ^ n))
generate a random bit vector of length n
Equations
- x.random_r y h = have h' : ∀ (a : fin (2 ^ n)), a ∈ set.Icc x.to_fin y.to_fin → bitvec.of_fin a ∈ set.Icc x y, from _, subtype.map bitvec.of_fin h' <$> rand.random_r x.to_fin y.to_fin _
Equations
- random_bitvec n = {to_bounded_random := {random_r := λ (_x : Type) (inst : random_gen _x) (x y : bitvec n) (p : x ≤ y), x.random_r y p}, random := λ (_x : Type) (inst : random_gen _x), bitvec.random n}