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 #

source
@[protected, instance]
def slim_check.gen.monad  :
monad slim_check.gen
source
@[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
source
@[protected, instance]
def slim_check.gen.is_lawful_monad  :
is_lawful_monad slim_check.gen
source
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
source
def slim_check.gen.choose_any (α : Type u) [random α] :
slim_check.gen α

Lift random.random to the gen monad.

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

Lift random.random_r to the gen monad.

Equations
source
def slim_check.gen.choose_nat (x y : ℕ) (p : x ≤ y) :
slim_check.gen ↥(set.Icc x y)

Generate a nat example between x and y.

Equations
source
def slim_check.gen.choose_nat' (x y : ℕ) (p : x < y) :
slim_check.gen ↥(set.Ico x y)

Generate a nat example between x and y.

Equations
source
@[protected, instance]
def slim_check.gen.uliftable  :
uliftable slim_check.gen slim_check.gen
Equations
source
@[protected, instance]
def slim_check.gen.has_orelse  :
has_orelse slim_check.gen
Equations
source
def slim_check.gen.sized {α : Type u} (cmd : ℕ → slim_check.gen α) :
slim_check.gen α

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

Equations
source
def slim_check.gen.resize {α : Type u} (f : ℕ → ℕ) (cmd : slim_check.gen α) :
slim_check.gen α

Apply a function to the size parameter.

Equations
source
def slim_check.gen.vector_of {α : Type u} (n : ℕ) (cmd : slim_check.gen α) :
slim_check.gen (vector α n)

Create n examples using cmd.

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

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

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

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

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

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

Equations
source
def slim_check.gen.freq_aux {α : Type u} (xs : list (ℕ+ × slim_check.gen α)) (i : ℕ) :
i < (list.map (subtype.val ∘ prod.fst) xs).sum → slim_check.gen α

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
source
def slim_check.gen.freq {α : Type u} (xs : list (ℕ+ × slim_check.gen α)) (pos : 0 < xs.length) :
slim_check.gen α

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
source
def slim_check.gen.permutation_of {α : Type u} (xs : list α) :
slim_check.gen (subtype xs.perm)

Generate a random permutation of a given list.

Equations