mathlib documentation

testing.slim_check.sampleable

sampleable Class

This class permits the creation samples of a given type controlling the size of those values using the gen monad`. It also helps minimize examples by creating smaller versions of given values.

When testing a proposition like ∀ n : ℕ, prime n → n ≤ 100, slim_check requires that have an instance of sampleable and for prime n to be decidable. slim_check will then use the instance of sampleable to generate small examples of ℕ and progressively increase in size. For each example n, prime n is tested. If it is false, the example will be rejected (not a test success nor a failure) and slim_check will move on to other examples. If prime n is true, n ≤ 100 will be tested. If it is false, n is a counter-example of ∀ n : ℕ, prime n → n ≤ 100 and the test fails. If n ≤ 100 is true, the test passes and slim_check moves on to trying more examples.

This is a port of the Haskell QuickCheck library.

Main definitions

sampleable

sampleable α provides ways of creating examples of type α, and given such an example x : α, gives us a way to shrink it and find simpler examples.

sampleable_ext

sampleable_ext generalizes the behavior of sampleable and makes it possible to express instances for types that do not lend themselves to introspection, such as ℕ → ℕ. If we test a quantification over functions the counter-examples cannot be shrunken or printed meaningfully.

For that purpose, sampleable_ext provides a proxy representation proxy_repr that can be printed and shrunken as well as interpreted (using interp) as an object of the right type.

sampleable_functor and sampleable_bifunctor

sampleable_functor F and sampleable_bifunctor F makes it possible to create samples of and shrink F α given a sampling function and a shrinking function for arbitrary α.

This allows us to separate the logic for generating the shape of a collection from the logic for generating its contents. Specifically, the contents could be generated using either sampleable or sampleable_ext instance and the sampleable_(bi)functor does not need to use that information

Shrinking

Shrinking happens when slim_check find a counter-example to a property. It is likely that the example will be more complicated than necessary so slim_check proceeds to shrink it as much as possible. Although equally valid, a smaller counter-example is easier for a user to understand and use.

The sampleable class, beside having the sample function, has a shrink function so that we can use specialized knowledge while shrinking a value. It is not responsible for the whole shrinking process however. It only has to take one step in the shrinking process. slim_check will repeatedly call shrink until no more steps can be taken. Because shrink guarantees that the size of the candidates it produces is strictly smaller than the argument, we know that slim_check is guaranteed to terminate.

Tags

random testing

References

def slim_check.sizeof_lt {α : Sort u_1} [has_sizeof α] :
α → α → Prop

sizeof_lt x y compares the sizes of x and y.

Equations
def slim_check.shrink_fn (α : Type u_1) [has_sizeof α] :
Type u_1

shrink_fn α is the type of functions that shrink an argument of type α

Equations
@[class]
structure slim_check.sampleable_functor (F : Type uType v) [functor F] :
Type (max (u+1) v)

sampleable_functor F makes it possible to create samples of and shrink F α given a sampling function and a shrinking function for arbitrary α

Instances
@[class]
structure slim_check.sampleable_bifunctor (F : Type uType vType w) [bifunctor F] :
Type (max (u+1) (v+1) w)

sampleable_bifunctor F makes it possible to create samples of and shrink F α β given a sampling function and a shrinking function for arbitrary α and β

Instances

This function helps infer the proxy representation and interpretation in sampleable_ext instances.

@[class]
structure slim_check.sampleable_ext  :
Sort uSort (max (imax (v+1) u) (v+2))

sampleable_ext generalizes the behavior of sampleable and makes it possible to express instances for types that do not lend themselves to introspection, such as ℕ → ℕ. If we test a quantification over functions the counter-examples cannot be shrunken or printed meaningfully.

For that purpose, sampleable_ext provides a proxy representation proxy_repr that can be printed and shrunken as well as interpreted (using interp) as an object of the right type.

Instances
def slim_check.nat.shrink' (k n : ) :
n klist {m // has_well_founded.r m k}list {m // has_well_founded.r m k}

nat.shrink' k n creates a list of smaller natural numbers by successively dividing n by 2 and subtracting the difference from k. For example, nat.shrink 100 = [50, 75, 88, 94, 97, 99].

Equations

nat.shrink n creates a list of smaller natural numbers by successively dividing by 2 and subtracting the difference from n. For example, nat.shrink 100 = [50, 75, 88, 94, 97, 99].

Equations
def slim_check.sampleable.lift (α : Type u) {β : Type u} [slim_check.sampleable α] (f : α → β) (g : β → α) :
(∀ (a : α), sizeof (g (f a)) sizeof a)slim_check.sampleable β

Transport a sampleable instance from a type α to a type β using functions between the two, going in both directions.

Function g is used to define the well-founded order that shrink is expected to follow.

Equations
def slim_check.iterate_shrink {α : Type} [has_to_string α] [slim_check.sampleable α] (p : α → Prop) [decidable_pred p] :
α → option α

iterate_shrink p x takes a decidable predicate p and a value x of some sampleable type and recursively shrinks x. It first calls shrink x to get a list of candidate sample, finds the first that satisfies p and recursively tries to shrink that one.

Equations
@[instance]

Equations

Redefine sizeof for int to make it easier to use with nat

Equations
@[instance]

Equations
@[instance]

Equations
def slim_check.prod.shrink {α : Type u_1} {β : Type u_2} [has_sizeof α] [has_sizeof β] :

Provided two shrinking functions prod.shrink shrinks a pair (x, y) by first shrinking x and pairing the results with y and then shrinking y and pairing the results with x.

All pairs either contain x untouched or y untouched. We rely on shrinking being repeated for x to get maximally shrunken and then for y to get shrunken too.

Equations
@[instance]

Equations
@[instance]
def slim_check.sigma.sampleable {α : Type u_1} {β : Type u_2} [slim_check.sampleable α] [slim_check.sampleable β] :
slim_check.sampleable (Σ (_x : α), β)

Equations
  • slim_check.sigma.sampleable = slim_check.sampleable.lift × β) (λ (_x : α × β), slim_check.sigma.sampleable._match_1 _x) (λ (_x : Σ (_x : α), β), slim_check.sigma.sampleable._match_2 _x) slim_check.sigma.sampleable._proof_1
  • slim_check.sigma.sampleable._match_1 (x, y) = x, y⟩
  • slim_check.sigma.sampleable._match_2 x, y⟩ = (x, y)
def slim_check.sum.shrink {α : Type u_1} {β : Type u_2} [has_sizeof α] [has_sizeof β] :

shrinking function for sum types

Equations
@[instance]

Equations
@[instance]

Equations

sampleable_char can be specialized into customized sampleable char instances.

The resulting instance has 1 / length chances of making an unrestricted choice of characters and it otherwise chooses a character from characters with uniform probabilities.

Equations
theorem slim_check.list.sizeof_drop_lt_sizeof_of_lt_length {α : Type u} [has_sizeof α] {xs : list α} {k : } :
0 < kk < xs.lengthsizeof (list.drop k xs) < sizeof xs

theorem slim_check.list.sizeof_cons_lt_right {α : Type u} [has_sizeof α] (a b : α) {xs : list α} :
sizeof a < sizeof bsizeof (a :: xs) < sizeof (b :: xs)

theorem slim_check.list.sizeof_cons_lt_left {α : Type u} [has_sizeof α] (x : α) {xs xs' : list α} :
sizeof xs < sizeof xs'sizeof (x :: xs) < sizeof (x :: xs')

theorem slim_check.list.sizeof_append_lt_left {α : Type u} [has_sizeof α] {xs ys ys' : list α} :
sizeof ys < sizeof ys'sizeof (xs ++ ys) < sizeof (xs ++ ys')

theorem slim_check.list.one_le_sizeof {α : Type u} [has_sizeof α] (xs : list α) :
1 sizeof xs

def slim_check.list.shrink_removes {α : Type u} [has_sizeof α] (k : ) (hk : 0 < k) (xs : list α) (n : ) :
n = xs.lengthlazy_list {ys // slim_check.sizeof_lt ys xs}

list.shrink_removes shrinks a list by removing chunks of size k in the middle of the list.

Equations
def slim_check.list.shrink_one {α : Type u} [has_sizeof α] :
(Π (x : α), lazy_list {y // slim_check.sizeof_lt y x})slim_check.shrink_fn (list α)

list.shrink_one xs shrinks list xs by shrinking only one item in the list.

Equations
def slim_check.list.shrink_with {α : Type u} [has_sizeof α] (shr : Π (x : α), lazy_list {y // slim_check.sizeof_lt y x}) (xs : list α) :

list.shrink_with shrink_f xs shrinks xs by first considering xs with chunks removed in the middle (starting with chunks of size xs.length and halving down to 1) and then shrinks only one element of the list.

This strategy is taken directly from Haskell's QuickCheck

Equations
@[instance]

Equations
def slim_check.no_shrink  :
Type u_1Type u_1

no_shrink is a type annotation to signal that a certain type is not to be shrunk. It can be useful in combination with other types: e.g. xs : list (no_shrink ℤ) will result in the list being cut down but individual integers being kept as is.

Equations
@[instance]

Equations
def slim_check.no_shrink.mk {α : Type u_1} :

Introduction of the no_shrink type.

Equations
def slim_check.no_shrink.get {α : Type u_1} :

Selector of the no_shrink type.

Equations
def slim_check.tree.sample {α : Type u} :

implementation of sampleable (tree α)

Equations
def slim_check.rec_shrink {α : Type u_1} [has_sizeof α] (t : α) :

rec_shrink x f_rec takes the recursive call f_rec introduced by well_founded.fix and turns it into a shrinking function whose result is adequate to use in a recursive call.

Equations
theorem slim_check.tree.one_le_sizeof {α : Type u_1} [has_sizeof α] (t : tree α) :

@[instance]

Equations

Recursion principle for shrinking tree-like structures.

Equations
theorem slim_check.rec_shrink_with_eq {α : Type u} [has_sizeof α] (shrink_a : Π (x : α), slim_check.shrink_fn {y // slim_check.sizeof_lt y x}list (lazy_list {y // slim_check.sizeof_lt y x})) (x : α) :
slim_check.rec_shrink_with shrink_a x = (lazy_list.of_list (shrink_a x (λ (t' : {y // slim_check.sizeof_lt y x}), slim_check.rec_shrink x (λ (x_1 : α) (h' : slim_check.sizeof_lt x_1 x), slim_check.rec_shrink_with shrink_a x_1) t'))).join

tree.shrink_with shrink_f t shrinks xs by using the empty tree, each subtrees, and by shrinking the subtree to recombine them.

This strategy is taken directly from Haskell's QuickCheck

Equations
@[instance]

Equations
def slim_check.small  :
Type u_1Type u_1

Type tag that signals to slim_check to use small values for a given type.

Equations
def slim_check.small.mk {α : Type u_1} :

Add the small type tag

Equations
def slim_check.large  :
Type u_1Type u_1

Type tag that signals to slim_check to use large values for a given type.

Equations
def slim_check.large.mk {α : Type u_1} :

Add the large type tag

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations

Subtype instances

The following instances are meant to improve the testing of properties of the form ∀ i j, i ≤ j, ...

The naive way to test them is to choose two numbers i and j and check that the proper ordering is satisfied. Instead, the following instances make it so that j will be chosen with considerations to the required ordering constraints. The benefit is that we will not have to discard any choice of j.

Subtypes of

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations

Subtypes of any decidable_linear_ordered_add_comm_group

@[instance]

Equations
@[instance]

Equations

Subtypes of

Specializations of le.sampleable and ge.sampleable for to help instance search.

@[instance]

Equations
@[instance]

Equations
@[instance]

Equations
@[instance]

Equations

Subtypes of any list

@[instance]
def slim_check.perm.slim_check {α : Type u} {xs : list α} :
slim_check.sampleable {ys // xs ~ ys}

Equations
@[instance]
def slim_check.perm'.slim_check {α : Type u} {xs : list α} :
slim_check.sampleable {ys // ys ~ xs}

Equations
def slim_check.print_samples {t : Type u} [has_repr t] :

Print (at most) 10 samples of a given type to stdout for debugging.

Equations

Create a gen α expression from the argument of #sample

#sample my_type, where my_type has an instance of sampleable, prints ten random values of type my_type of using an increasing size parameter.

#sample nat
-- prints
-- 0
-- 0
-- 2
-- 24
-- 64
-- 76
-- 5
-- 132
-- 8
-- 449
-- or some other sequence of numbers

#sample list int
-- prints
-- []
-- [1, 1]
-- [-7, 9, -6]
-- [36]
-- [-500, 105, 260]
-- [-290]
-- [17, 156]
-- [-2364, -7599, 661, -2411, -3576, 5517, -3823, -968]
-- [-643]
-- [11892, 16329, -15095, -15461]
-- or whatever