# mathlibdocumentation

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 #

• gen monad

## Local notation #

• i .. j : Icc i j, the set of values between i and j inclusively;

random testing

## References #

@[protected, instance]
@[reducible]
def slim_check.gen (α : Type u) :
Type 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
• = α
@[protected, instance]
def slim_check.io.run_gen {α : Type} (x : slim_check.gen α) (i : ) :
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
• = λ (_x : ,
def slim_check.gen.choose {α : Type u} [preorder α] (x y : α) (p : x y) :

Lift random.random_r to the gen monad.

Equations
• = λ (_x : , p
def slim_check.gen.choose_nat (x y : ) (p : x y) :

Generate a nat example between x and y.

Equations
def slim_check.gen.choose_nat' (x y : ) (p : x < y) :

Generate a nat example between x and y.

Equations
• = have this : ∀ (i : ), x < ii yi.pred < y, from _,
@[protected, instance]
Equations
@[protected, instance]
Equations
def slim_check.gen.sized {α : Type u} (cmd : ) :

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

Equations
• = λ (_x : , slim_check.gen.sized._match_1 cmd _x
• slim_check.gen.sized._match_1 cmd {down := sz} = (cmd sz).run {down := sz}
def slim_check.gen.resize {α : Type u} (f : ) (cmd : slim_check.gen α) :

Apply a function to the size parameter.

Equations
• = λ (_x : , slim_check.gen.resize._match_1 f cmd _x
• slim_check.gen.resize._match_1 f cmd {down := sz} = cmd.run {down := f sz}
def slim_check.gen.vector_of {α : Type u} (n : ) (cmd : slim_check.gen α) :

Create n examples using cmd.

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

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 ) (pos : 0 < xs.length) :

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

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

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

Equations
def slim_check.gen.freq_aux {α : Type u} (xs : list ) (i : ) :
i < xs).sum

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 ) (pos : 0 < xs.length) :

freq [(1, gena), (3, genb), (5, genc)] _ will choose one of gena, genb, genc with probabilities 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