mathlib3 documentation

testing.slim_check.gen

gen Monad #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[protected, instance]
@[reducible]
def slim_check.gen (α : 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
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

Lift random.random to the gen monad.

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

Lift random.random_r to the gen monad.

Equations
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

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} (f : ) (cmd : slim_check.gen α) :

Apply a function to the size parameter.

Equations

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 α)) (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

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 α)) (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

Generate a random permutation of a given list.

Equations