mathlib documentation

testing.slim_check.gen

gen Monad

This monad is used to formulate randomized computations with a parameter to specify the desired size of the result.

This is a port of the Haskell QuickCheck library.

Main definitions

Local notation

Tags

random testing

References

def slim_check.gen  :
Type uType u

Monad to generate random examples to test properties with. It has a nat parameter so that the caller can decide on the size of the examples.

Equations
def slim_check.io.run_gen {α : Type} :
slim_check.gen αio α

Execute a gen inside the io monad using i as the example size and with a fresh random number generator.

Equations
def slim_check.gen.choose_any (α : Type u) [random α] :

Lift random.random to the gen monad.

Equations
def slim_check.gen.choose {α : Type u} [preorder α] [bounded_random α] (x y : α) :

Lift random.random_r to the gen monad.

Equations

Generate a nat example between x and y.

Equations

Generate a nat example between x and y.

Equations
def slim_check.gen.sized {α : Type u} :

Get access to the size parameter of the gen monad. For reasons of universe polymorphism, it is specified in continuation passing style.

Equations
def slim_check.gen.resize {α : Type u} :
()slim_check.gen αslim_check.gen α

Apply a function to the size parameter.

Equations
def slim_check.gen.vector_of {α : Type u} (n : ) :

Create n examples using cmd.

Equations
def slim_check.gen.list_of {α : Type u} :

Create a list of examples using cmd. The size is controlled by the size parameter of gen.

Equations
def slim_check.gen.one_of {α : Type u} (xs : list (slim_check.gen α)) :
0 < xs.lengthslim_check.gen α

Given a list of example generators, choose one to create an example.

Equations
def slim_check.gen.elements {α : Type u} (xs : list α) :
0 < xs.lengthslim_check.gen α

Given a list of example generators, choose one to create an example.

Equations
def slim_check.gen.freq_aux {α : Type u} (xs : list (ℕ+ × slim_check.gen α)) (i : ) :

freq_aux xs i _ takes a weighted list of generator and a number meant to select one of the generators.

If we consider freq_aux [(1, gena), (3, genb), (5, genc)] 4 _, we choose a generator by splitting the interval 1-9 into 1-1, 2-4, 5-9 so that the width of each interval corresponds to one of the number in the list of generators. Then, we check which interval 4 falls into: it selects genb.

Equations
def slim_check.gen.freq {α : Type u} (xs : list (ℕ+ × slim_check.gen α)) :
0 < xs.lengthslim_check.gen α

freq [(1, gena), (3, genb), (5, genc)] _ will choose one of gena, genb, genc with probabiities proportional to the number accompanying them. In this example, the sum of those numbers is 9, gena will be chosen with probability ~1/9, genb with ~3/9 (i.e. 1/3) and genc with probability 5/9.

Equations
def slim_check.gen.permutation_of {α : Type u} (xs : list α) :

Generate a random permutation of a given list.

Equations