mathlib3 documentation

testing.slim_check.sampleable

sampleable Class #

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

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 #

source
def slim_check.sizeof_lt {α : Sort u_1} [has_sizeof α] (x y : α) :
Prop

sizeof_lt x y compares the sizes of x and y.

Equations
source
@[reducible]
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
source
@[class]
structure slim_check.sampleable (α : Type u) :
Type u

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.

Instances of this typeclass
Instances of other typeclasses for slim_check.sampleable
  • slim_check.sampleable.has_sizeof_inst
source
@[class]
structure slim_check.sampleable_functor (F : Type u → Type 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 of this typeclass
Instances of other typeclasses for slim_check.sampleable_functor
  • slim_check.sampleable_functor.has_sizeof_inst
source
@[class]
structure slim_check.sampleable_bifunctor (F : Type u → Type v → Type 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 of this typeclass
Instances of other typeclasses for slim_check.sampleable_bifunctor
  • slim_check.sampleable_bifunctor.has_sizeof_inst
source
meta def slim_check.sampleable.mk_trivial_interp  :
tactic unit

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

source
@[class]
structure slim_check.sampleable_ext (α : Sort u) :
Sort (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 of this typeclass
Instances of other typeclasses for slim_check.sampleable_ext
  • slim_check.sampleable_ext.has_sizeof_inst
source
@[protected, instance]
def slim_check.sampleable_ext.of_sampleable {α : Type u_1} [slim_check.sampleable α] [has_repr α] :
slim_check.sampleable_ext α
Equations
source
@[protected, instance]
def slim_check.sampleable.functor {α : Type u_1} {F : Type u_1 → Type u_2} [functor F] [slim_check.sampleable_functor F] [slim_check.sampleable α] :
slim_check.sampleable (F α)
Equations
source
@[protected, instance]
def slim_check.sampleable.bifunctor {α : Type u_1} {β : Type u_2} {F : Type u_1 → Type u_2 → Type u_3} [bifunctor F] [slim_check.sampleable_bifunctor F] [slim_check.sampleable α] [slim_check.sampleable β] :
slim_check.sampleable (F α β)
Equations
source
@[protected, instance]
def slim_check.sampleable_ext.functor {α : Type u_1} {F : Type u_1 → Type u_2} [functor F] [slim_check.sampleable_functor F] [slim_check.sampleable_ext α] :
slim_check.sampleable_ext (F α)
Equations
source
@[protected, instance]
def slim_check.sampleable_ext.bifunctor {α : Type u_1} {β : Type u_2} {F : Type u_1 → Type u_2 → Type u_3} [bifunctor F] [slim_check.sampleable_bifunctor F] [slim_check.sampleable_ext α] [slim_check.sampleable_ext β] :
slim_check.sampleable_ext (F α β)
Equations
source
def slim_check.nat.shrink' (k n : ℕ) :
n ≤ k → list {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
source
def slim_check.nat.shrink (n : ℕ) :
list {m // has_well_founded.r m n}

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
source
def slim_check.sampleable.lift (α : Type u) {β : Type u} [slim_check.sampleable α] (f : α → β) (g : β → α) (h : ∀ (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
source
@[protected, instance]
def slim_check.nat.sampleable  :
slim_check.sampleable ℕ
Equations
source
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
source
@[protected, instance]
def slim_check.fin.sampleable {n : ℕ} [ne_zero n] :
slim_check.sampleable (fin n)
Equations
source
@[protected, instance]
def slim_check.fin.sampleable' {n : ℕ} :
slim_check.sampleable (fin n.succ)
Equations
source
@[protected, instance]
def slim_check.pnat.sampleable  :
slim_check.sampleable ℕ+
Equations
source
def slim_check.int.has_sizeof  :
has_sizeof ℤ

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

Equations
source
@[protected, instance]
def slim_check.int.sampleable  :
slim_check.sampleable ℤ
Equations
source
@[protected, instance]
def slim_check.bool.sampleable  :
slim_check.sampleable bool
Equations
source
def slim_check.prod.shrink {α : Type u_1} {β : Type u_2} [has_sizeof α] [has_sizeof β] (shr_a : slim_check.shrink_fn α) (shr_b : slim_check.shrink_fn β) :
slim_check.shrink_fn (α × β)

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
source
@[protected, instance]
def slim_check.prod.sampleable  :
slim_check.sampleable_bifunctor prod
Equations
source
@[protected, 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)
source
def slim_check.sum.shrink {α : Type u_1} {β : Type u_2} [has_sizeof α] [has_sizeof β] (shrink_α : slim_check.shrink_fn α) (shrink_β : slim_check.shrink_fn β) :
slim_check.shrink_fn (α ⊕ β)

shrinking function for sum types

Equations
source
@[protected, instance]
def slim_check.sum.sampleable  :
slim_check.sampleable_bifunctor sum
Equations
source
@[protected, instance]
def slim_check.rat.sampleable  :
slim_check.sampleable ℚ
Equations
source
def slim_check.sampleable_char (length : ℕ) (characters : string) :
slim_check.sampleable char

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
source
@[protected, instance]
def slim_check.char.sampleable  :
slim_check.sampleable char
Equations
source
theorem slim_check.list.sizeof_drop_lt_sizeof_of_lt_length {α : Type u} [has_sizeof α] {xs : list α} {k : ℕ} (hk : 0 < k) (hk' : k < xs.length) :
sizeof (list.drop k xs) < sizeof xs
source
theorem slim_check.list.sizeof_cons_lt_right {α : Type u} [has_sizeof α] (a b : α) {xs : list α} (h : sizeof a < sizeof b) :
sizeof (a :: xs) < sizeof (b :: xs)
source
theorem slim_check.list.sizeof_cons_lt_left {α : Type u} [has_sizeof α] (x : α) {xs xs' : list α} (h : sizeof xs < sizeof xs') :
sizeof (x :: xs) < sizeof (x :: xs')
source
theorem slim_check.list.sizeof_append_lt_left {α : Type u} [has_sizeof α] {xs ys ys' : list α} (h : sizeof ys < sizeof ys') :
sizeof (xs ++ ys) < sizeof (xs ++ ys')
source
theorem slim_check.list.one_le_sizeof {α : Type u} [has_sizeof α] (xs : list α) :
1 ≤ sizeof xs
source
def slim_check.list.shrink_removes {α : Type u} [has_sizeof α] (k : ℕ) (hk : 0 < k) (xs : list α) (n : ℕ) :
n = xs.length → lazy_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
source
def slim_check.list.shrink_one {α : Type u} [has_sizeof α] (shr : Π (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
source
def slim_check.list.shrink_with {α : Type u} [has_sizeof α] (shr : Π (x : α), lazy_list {y // slim_check.sizeof_lt y x}) (xs : list α) :
lazy_list {ys // slim_check.sizeof_lt ys xs}

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
source
@[protected, instance]
def slim_check.list.sampleable  :
slim_check.sampleable_functor list
Equations
source
@[protected, instance]
def slim_check.Prop.sampleable_ext  :
slim_check.sampleable_ext Prop
Equations
source
def slim_check.no_shrink (α : Type u_1) :
Type 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
Instances for slim_check.no_shrink
source
@[protected, instance]
def slim_check.no_shrink.inhabited {α : Type u_1} [inhabited α] :
inhabited (slim_check.no_shrink α)
Equations
source
def slim_check.no_shrink.mk {α : Type u_1} (x : α) :
slim_check.no_shrink α

Introduction of the no_shrink type.

Equations
source
def slim_check.no_shrink.get {α : Type u_1} (x : slim_check.no_shrink α) :
α

Selector of the no_shrink type.

Equations
source
@[protected, instance]
def slim_check.no_shrink.sampleable {α : Type u_1} [slim_check.sampleable α] :
slim_check.sampleable (slim_check.no_shrink α)
Equations
source
@[protected, instance]
def slim_check.string.sampleable  :
slim_check.sampleable string
Equations
source
def slim_check.tree.sample {α : Type u} (sample : slim_check.gen α) :
ℕ → slim_check.gen (tree α)

implementation of sampleable (tree α)

Equations
source
def slim_check.rec_shrink {α : Type u_1} [has_sizeof α] (t : α) (sh : Π (x : α), slim_check.sizeof_lt x t → lazy_list {y // slim_check.sizeof_lt y x}) :
slim_check.shrink_fn {t' // slim_check.sizeof_lt t' 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
source
theorem slim_check.tree.one_le_sizeof {α : Type u_1} [has_sizeof α] (t : tree α) :
1 ≤ sizeof t
source
@[protected, instance]
def slim_check.tree.functor  :
functor tree
Equations
source
def slim_check.rec_shrink_with {α : 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})) :
slim_check.shrink_fn α

Recursion principle for shrinking tree-like structures.

Equations
source
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
source
def slim_check.tree.shrink_with {α : Type u} [has_sizeof α] (shrink_a : slim_check.shrink_fn α) :
slim_check.shrink_fn (tree α)

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
source
@[protected, instance]
def slim_check.sampleable_tree  :
slim_check.sampleable_functor tree
Equations
source
def slim_check.small (α : Type u_1) :
Type u_1

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

Equations
Instances for slim_check.small
source
def slim_check.small.mk {α : Type u_1} (x : α) :
slim_check.small α

Add the small type tag

Equations
source
def slim_check.large (α : Type u_1) :
Type u_1

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

Equations
Instances for slim_check.large
source
def slim_check.large.mk {α : Type u_1} (x : α) :
slim_check.large α

Add the large type tag

Equations
source
@[protected, instance]
def slim_check.small.functor  :
functor slim_check.small
Equations
source
@[protected, instance]
def slim_check.large.functor  :
functor slim_check.large
Equations
source
@[protected, instance]
def slim_check.small.inhabited {α : Type u} [inhabited α] :
inhabited (slim_check.small α)
Equations
source
@[protected, instance]
def slim_check.large.inhabited {α : Type u} [inhabited α] :
inhabited (slim_check.large α)
Equations
source
@[protected, instance]
def slim_check.small.sampleable_functor  :
slim_check.sampleable_functor slim_check.small
Equations
source
@[protected, instance]
def slim_check.large.sampleable_functor  :
slim_check.sampleable_functor slim_check.large
Equations
source
@[protected, instance]
def slim_check.ulift.sampleable_functor  :
slim_check.sampleable_functor ulift
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 ℕ #

source
@[protected, instance]
def slim_check.nat_le.sampleable {y : ℕ} :
slim_check.sampleable {x // x ≤ y}
Equations
source
@[protected, instance]
def slim_check.nat_ge.sampleable {x : ℕ} :
slim_check.sampleable {y // x ≤ y}
Equations
source
@[protected, instance]
def slim_check.nat_gt.sampleable {x : ℕ} :
slim_check.sampleable {y // x < y}
Equations

Subtypes of any linear_ordered_add_comm_group #

source
@[protected, instance]
def slim_check.le.sampleable {α : Type u} {y : α} [slim_check.sampleable α] [linear_ordered_add_comm_group α] :
slim_check.sampleable {x // x ≤ y}
Equations
source
@[protected, instance]
def slim_check.ge.sampleable {α : Type u} {x : α} [slim_check.sampleable α] [linear_ordered_add_comm_group α] :
slim_check.sampleable {y // x ≤ y}
Equations

Subtypes of ℤ #

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

source
@[protected, instance]
def slim_check.int_le.sampleable {y : ℤ} :
slim_check.sampleable {x // x ≤ y}
Equations
source
@[protected, instance]
def slim_check.int_ge.sampleable {x : ℤ} :
slim_check.sampleable {y // x ≤ y}
Equations
source
@[protected, instance]
def slim_check.int_lt.sampleable {y : ℤ} :
slim_check.sampleable {x // x < y}
Equations
source
@[protected, instance]
def slim_check.int_gt.sampleable {x : ℤ} :
slim_check.sampleable {y // x < y}
Equations

Subtypes of any list #

source
@[protected, instance]
def slim_check.perm.slim_check {α : Type u} {xs : list α} :
slim_check.sampleable {ys // xs ~ ys}
Equations
source
@[protected, instance]
def slim_check.perm'.slim_check {α : Type u} {xs : list α} :
slim_check.sampleable {ys // ys ~ xs}
Equations
source
def slim_check.print_samples {t : Type u} [has_repr t] (g : slim_check.gen t) :
io unit

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

Equations
source
meta def slim_check.mk_generator (e : expr) :
tactic (expr × expr)

Create a gen α expression from the argument of #sample

source
meta def slim_check.sample_cmd (_x : interactive.parse (lean.parser.tk "#sample")) :
lean.parser unit

#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
```