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 class

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

https://hackage.haskell.org/package/QuickCheck

@[class]

structure slim_check.sampleable (α : Type u) :

Type u

wf : has_sizeof α
sample : slim_check.gen α
shrink : Π (x : α), lazy_list {y // sizeof y < sizeof x}

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

def slim_check.nat.shrink' (k n : ℕ) (a : n ≤ k) (a_1 : 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

slim_check.nat.shrink' k n hn ls = dite (n ≤ 1) (λ (h : n ≤ 1), ls.reverse) (λ (h : ¬n ≤ 1), have h₂ : 0 < n, from _, have this : 1 * n / 2 < n, from _, have this : n / 2 < n, from _, let m : ℕ := n / 2 in have h₀ : m ≤ k, from _, have h₃ : 0 < m, from _, have h₁ : k - m < k, from _, slim_check.nat.shrink' k m h₀ (⟨k - m, h₁⟩ :: ls))

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

slim_check.nat.shrink n = dite (n > 0) (λ (h : n > 0), have this : ∀ (k : ℕ), 1 < k → n / k < n, from _, ⟨n / 11, _⟩ :: ⟨n / 3, _⟩ :: slim_check.nat.shrink' n n _ list.nil) (λ (h : ¬n > 0), list.nil)

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

slim_check.sampleable.lift α f g h = {wf := {sizeof := sizeof ∘ g}, sample := f <$> slim_check.sampleable.sample α, shrink := λ (x : β), have this : ∀ (a : α), sizeof a < sizeof (g x) → sizeof (g (f a)) < sizeof (g x), from _, subtype.map f this <$> slim_check.sampleable.shrink (g x)}

@[instance]

def slim_check.nat.sampleable :

slim_check.sampleable ℕ

Equations

slim_check.nat.sampleable = {wf := nat.has_sizeof, sample := slim_check.gen.sized (λ (sz : ℕ), coe <$> slim_check.gen.choose_any (fin (sz ^ 3).succ) <|> coe <$> slim_check.gen.choose_any (fin sz.succ)), shrink := λ (x : ℕ), lazy_list.of_list (slim_check.nat.shrink x)}

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

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

slim_check.iterate_shrink p = slim_check.iterate_shrink._proof_1.fix (λ (x : α) (f_rec : Π (y : α), has_well_founded.r y x → option α), trace ("" ++ to_string x ++ (" : " ++ to_string (slim_check.sampleable.shrink x).to_list ++ "")) (λ («_» : unit), pure ()) >>= λ (_x : unit), lazy_list.find (λ (a : {y // sizeof y < sizeof x}), p ↑a) (slim_check.sampleable.shrink x) >>= λ (y : {y // sizeof y < sizeof x}), f_rec ↑y _ <|> some y.val)

@[instance]

def slim_check.fin.sampleable {n : ℕ} [fact (0 < n)] :

slim_check.sampleable (fin n)

Equations

slim_check.fin.sampleable = slim_check.sampleable.lift ℕ fin.of_nat' subtype.val slim_check.fin.sampleable._proof_1

@[instance]

def slim_check.fin.sampleable' {n : ℕ} :

slim_check.sampleable (fin n.succ)

Equations

slim_check.fin.sampleable' = slim_check.sampleable.lift ℕ fin.of_nat subtype.val slim_check.fin.sampleable'._proof_1

@[instance]

def slim_check.pnat.sampleable :

slim_check.sampleable ℕ+

Equations

slim_check.pnat.sampleable = slim_check.sampleable.lift ℕ nat.succ_pnat pnat.nat_pred slim_check.pnat.sampleable._proof_1

@[instance]

def slim_check.int.sampleable :

slim_check.sampleable ℤ

Equations

slim_check.int.sampleable = {wf := {sizeof := int.nat_abs}, sample := slim_check.gen.sized (λ (sz : ℕ), let k : ℕ := sz ^ 5 in (λ (n : fin k.succ), ↑(n.val) - int.of_nat (k / 2)) <$> slim_check.gen.choose_any (fin k.succ)), shrink := λ (x : ℤ), lazy_list.of_list ((slim_check.nat.shrink x.nat_abs).bind (λ (_x : {m // has_well_founded.r m x.nat_abs}), slim_check.int.sampleable._match_1 x _x))}
slim_check.int.sampleable._match_1 x ⟨y, h⟩ = [⟨↑y, h⟩, ⟨-↑y, _⟩]

@[instance]

def slim_check.bool.sampleable :

slim_check.sampleable bool

Equations

slim_check.bool.sampleable = {wf := bool.has_sizeof, sample := slim_check.gen.choose_any bool >>= λ (x : bool), return x, shrink := λ (_x : bool), lazy_list.nil}

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

slim_check.sizeof_lt x y = (sizeof x < sizeof y)

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

slim_check.shrink_fn α = Π (x : α), lazy_list {y // slim_check.sizeof_lt y x}

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

slim_check.prod.shrink shr_a shr_b (x₀, x₁) = let xs₀ : lazy_list {y // slim_check.sizeof_lt y (x₀, x₁)} := lazy_list.map (subtype.map (λ (a : α), (a, x₁)) _) (shr_a x₀), xs₁ : lazy_list {y // slim_check.sizeof_lt y (x₀, x₁)} := lazy_list.map (subtype.map (λ (a : β), (x₀, a)) _) (shr_b x₁) in xs₀.append (λ («_» : unit), xs₁)

@[instance]

def slim_check.prod.sampleable (α : Type u) {β : Type v} [slim_check.sampleable α] [slim_check.sampleable β] :

slim_check.sampleable (α × β)

Equations

slim_check.prod.sampleable α = {wf := prod.has_sizeof α β slim_check.sampleable.wf, sample := uliftable.up (slim_check.sampleable.sample α) >>= λ (_p : ulift α), slim_check.prod.sampleable._match_2 α _p, shrink := slim_check.prod.shrink slim_check.sampleable.shrink slim_check.sampleable.shrink}
slim_check.prod.sampleable._match_2 α {down := x} = uliftable.up (slim_check.sampleable.sample β) >>= λ (_p : ulift β), slim_check.prod.sampleable._match_1 α x _p
slim_check.prod.sampleable._match_1 α x {down := y} = pure (x, y)

def slim_check.sum.shrink (α : Type u) {β : Type u_1} [slim_check.sampleable α] [slim_check.sampleable β] (x : α ⊕ β) :

lazy_list {y // has_well_founded.r y x}

shrinking function for sum types

Equations

slim_check.sum.shrink α (sum.inr x) = lazy_list.map (subtype.map sum.inr _) (slim_check.sampleable.shrink x)
slim_check.sum.shrink α (sum.inl x) = lazy_list.map (subtype.map sum.inl _) (slim_check.sampleable.shrink x)

@[instance]

def slim_check.sum.sampleable (α : Type u) {β : Type u} [slim_check.sampleable α] [slim_check.sampleable β] :

slim_check.sampleable (α ⊕ β)

Equations

slim_check.sum.sampleable α = {wf := sum.has_sizeof α β slim_check.sampleable.wf, sample := uliftable.up_map sum.inl (slim_check.sampleable.sample α) <|> uliftable.up_map sum.inr (slim_check.sampleable.sample β), shrink := slim_check.sum.shrink α _inst_2}

@[instance]

def slim_check.rat.sampleable :

slim_check.sampleable ℚ

Equations

slim_check.rat.sampleable = slim_check.sampleable.lift (ℤ × ℕ+) (λ (x : ℤ × ℕ+), x.cases_on rat.mk_pnat) (λ (r : ℚ), (r.num, ⟨r.denom, _⟩)) slim_check.rat.sampleable._proof_1

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

slim_check.sampleable_char length characters = {wf := char.has_sizeof, sample := slim_check.gen.choose_nat 0 length _ >>= λ (x : ↥(set.Icc 0 length)), ite (x.val = 0) (slim_check.sampleable.sample ℕ >>= λ (n : ℕ), pure (char.of_nat n)) (slim_check.gen.choose_nat 0 (characters.length - 1) _ >>= λ (i : ↥(set.Icc 0 (characters.length - 1))), pure (characters.mk_iterator.nextn ↑i).curr), shrink := λ (_x : char), lazy_list.nil}

@[instance]

def slim_check.char.sampleable :

slim_check.sampleable char

Equations

slim_check.char.sampleable = slim_check.sampleable_char 3 " 0123abcABC:,;`\\/"

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

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)

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')

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')

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 : ℕ) (a : 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

slim_check.list.shrink_removes k hk xs n hn = dite (k > n) (λ (hkn : k > n), lazy_list.nil) (λ (hkn : ¬k > n), dite (k = n) (λ (hkn' : k = n), have this : 1 < xs.sizeof, from _, lazy_list.singleton ⟨list.nil α, this⟩) (λ (hkn' : ¬k = n), have h₂ : k < xs.length, from _, slim_check.list.shrink_removes._match_1 k hk xs n hn h₂ (λ (xs₁ xs₂ : list α) (h : (xs₁, xs₂) = list.split_at k xs) (h₄ : xs₁ = list.take k xs) (h₃ : xs₂ = list.drop k xs) (this : sizeof xs₂ < sizeof xs) (h₁ : n - k = xs₂.length) (h₅ : ∀ (a : list α), slim_check.sizeof_lt a xs₂ → slim_check.sizeof_lt (xs₁ ++ a) xs), slim_check.list.shrink_removes k hk xs₂ (n - k) h₁) (list.split_at k xs) _))
slim_check.list.shrink_removes._match_1 k hk xs n hn h₂ _f_1 (xs₁, xs₂) h = have h₄ : xs₁ = list.take k xs, from _, have h₃ : xs₂ = list.drop k xs, from _, have this : sizeof xs₂ < sizeof xs, from _, have h₁ : n - k = xs₂.length, from _, have h₅ : ∀ (a : list α), slim_check.sizeof_lt a xs₂ → slim_check.sizeof_lt (xs₁ ++ a) xs, from _, lazy_list.cons ⟨xs₂, this⟩ (λ («_» : unit), subtype.map (append xs₁) h₅ <$> _f_1 xs₁ xs₂ h h₄ h₃ this h₁ h₅)

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

slim_check.list.shrink_one shr (x :: xs) = (subtype.map (λ (x' : α), x' :: xs) _ <$> shr x).append (λ («_» : unit), subtype.map ((λ (_x : α) (_y : list α), _x :: _y) x) _ <$> slim_check.list.shrink_one shr xs)
slim_check.list.shrink_one shr list.nil = lazy_list.nil

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

slim_check.list.shrink_with shr xs = let n : ℕ := xs.length in ((lazy_list.cons n (λ («_» : unit), lazy_list.map subtype.val (slim_check.sampleable.shrink n).reverse)).bind (λ (k : ℕ), dite (0 < k) (λ (hk : 0 < k), slim_check.list.shrink_removes k hk xs n rfl) (λ (hk : ¬0 < k), lazy_list.nil))).append (λ («_» : unit), slim_check.list.shrink_one shr xs)

@[instance]

def slim_check.list.sampleable {α : Type u} [slim_check.sampleable α] :

slim_check.sampleable (list α)

Equations

slim_check.list.sampleable = {wf := list.has_sizeof α slim_check.sampleable.wf, sample := (slim_check.sampleable.sample α).list_of, shrink := slim_check.list.shrink_with slim_check.sampleable.shrink}

@[instance]

def slim_check.prop.sampleable :

slim_check.sampleable Prop

Equations

slim_check.prop.sampleable = {wf := default_has_sizeof Prop, sample := slim_check.gen.choose_any bool >>= λ (x : bool), return ↑x, shrink := λ (_x : Prop), lazy_list.nil}

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

slim_check.no_shrink α = α

@[instance]

def slim_check.inhabited {α : Type u_1} [inhabited α] :

inhabited (slim_check.no_shrink α)

Equations

slim_check.inhabited = {default := default α _inst_1}

def slim_check.no_shrink.mk {α : Type u_1} (x : α) :

slim_check.no_shrink α

Introduction of the no_shrink type.

Equations

slim_check.no_shrink.mk x = x

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

α

Selector of the no_shrink type.

Equations

x.get = x

@[instance]

def slim_check.no_shrink.sampleable {α : Type u_1} [slim_check.sampleable α] :

slim_check.sampleable (slim_check.no_shrink α)

Equations

slim_check.no_shrink.sampleable = {wf := default_has_sizeof (slim_check.no_shrink α), sample := slim_check.no_shrink.mk <$> slim_check.sampleable.sample α, shrink := λ (_x : slim_check.no_shrink α), lazy_list.nil}

@[instance]

def slim_check.string.sampleable :

slim_check.sampleable string

Equations

slim_check.string.sampleable = {wf := slim_check.sampleable.wf (slim_check.sampleable.lift (list char) list.as_string string.to_list slim_check.string.sampleable._proof_1), sample := (slim_check.sampleable.sample char).list_of >>= λ (x : list char), pure x.as_string, shrink := slim_check.sampleable.shrink (slim_check.sampleable.lift (list char) list.as_string string.to_list slim_check.string.sampleable._proof_1)}

def slim_check.tree.sample {α : Type u} (sample : slim_check.gen α) (a : ℕ) :

slim_check.gen (tree α)

implementation of sampleable (tree α)

Equations

slim_check.tree.sample sample n = ite (n > 0) (tree.node <$> sample <*> slim_check.tree.sample sample (n / 2) <*> slim_check.tree.sample sample (n / 2)) (pure tree.nil)

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

slim_check.rec_shrink t sh ⟨t', ht'⟩ = (λ (t'' : {y // slim_check.sizeof_lt y t'}), ⟨⟨t''.val, _⟩, _⟩) <$> sh t' ht'

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

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

slim_check.tree.shrink_with shrink_a = slim_check.tree.shrink_with._proof_1.fix (λ (t : tree α), slim_check.tree.shrink_with._match_1 shrink_a t t)
slim_check.tree.shrink_with._match_1 shrink_a t (tree.node x t₀ t₁) = λ (f_rec : Π (y : tree α), sizeof_measure (tree α) y (tree.node x t₀ t₁) → lazy_list {y_1 // slim_check.sizeof_lt y_1 y}), let shrink_tree : slim_check.shrink_fn {t' // slim_check.sizeof_lt t' (tree.node x t₀ t₁)} := λ (t' : {t' // slim_check.sizeof_lt t' (tree.node x t₀ t₁)}), slim_check.rec_shrink (tree.node x t₀ t₁) f_rec t' in have h₂ : slim_check.sizeof_lt tree.nil (tree.node x t₀ t₁), from _, have h₀ : slim_check.sizeof_lt t₀ (tree.node x t₀ t₁), from _, have h₁ : slim_check.sizeof_lt t₁ (tree.node x t₀ t₁), from _, (lazy_list.of_list [lazy_list.of_list [⟨tree.nil α, h₂⟩, ⟨t₀, h₀⟩, ⟨t₁, h₁⟩]]).join.append (λ («_» : unit), lazy_list.map (λ (_x : {y // slim_check.sizeof_lt y (x, ⟨t₀, h₀⟩, ⟨t₁, h₁⟩)}), slim_check.tree.shrink_with._match_2 x t₀ t₁ h₀ h₁ _x) (slim_check.prod.shrink shrink_a (slim_check.prod.shrink shrink_tree shrink_tree) (x, ⟨t₀, h₀⟩, ⟨t₁, h₁⟩)))
slim_check.tree.shrink_with._match_1 shrink_a t tree.nil = λ (f_rec : Π (y : tree α), sizeof_measure (tree α) y tree.nil → lazy_list {y_1 // slim_check.sizeof_lt y_1 y}), lazy_list.nil
slim_check.tree.shrink_with._match_2 x t₀ t₁ h₀ h₁ ⟨(y, ⟨t'₀, _x⟩, ⟨t'₁, _x_1⟩), hy⟩ = ⟨tree.node y t'₀ t'₁, _⟩

@[instance]

def slim_check.tree.sampleable {α : Type u} [slim_check.sampleable α] :

slim_check.sampleable (tree α)

Equations

slim_check.tree.sampleable = {wf := tree.has_sizeof_inst α slim_check.sampleable.wf, sample := slim_check.gen.sized (slim_check.tree.sample (slim_check.sampleable.sample α)), shrink := slim_check.tree.shrink_with slim_check.sampleable.shrink}

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.

@[instance]

def slim_check.nat_le.sampleable {y : ℕ} :

slim_check.sampleable {x // x ≤ y}

Equations

slim_check.nat_le.sampleable = {wf := subtype.has_sizeof (λ (x : ℕ), x ≤ y), sample := slim_check.gen.choose_nat 0 y slim_check.nat_le.sampleable._proof_1 >>= λ (_p : ↥(set.Icc 0 y)), slim_check.nat_le.sampleable._match_1 _p, shrink := λ (_x : {x // x ≤ y}), lazy_list.nil}
slim_check.nat_le.sampleable._match_1 ⟨x, h⟩ = pure ⟨x, _⟩

@[instance]

def slim_check.nat_ge.sampleable {x : ℕ} :

slim_check.sampleable {y // x ≤ y}

Equations

slim_check.nat_ge.sampleable = {wf := subtype.has_sizeof (λ (y : ℕ), x ≤ y), sample := slim_check.sampleable.sample ℕ >>= λ (_p : ℕ), slim_check.nat_ge.sampleable._match_1 _p, shrink := λ (_x : {y // x ≤ y}), lazy_list.nil}
slim_check.nat_ge.sampleable._match_1 y = pure ⟨x + y, _⟩

@[instance]

def slim_check.nat_gt.sampleable {x : ℕ} :

slim_check.sampleable {y // x < y}

Equations

slim_check.nat_gt.sampleable = {wf := subtype.has_sizeof (λ (y : ℕ), x < y), sample := slim_check.sampleable.sample ℕ >>= λ (_p : ℕ), slim_check.nat_gt.sampleable._match_1 _p, shrink := λ (_x : {y // x < y}), lazy_list.nil}
slim_check.nat_gt.sampleable._match_1 y = pure ⟨x + y + 1, _⟩

@[instance]

def slim_check.int_lt.sampleable {y : ℤ} :

slim_check.sampleable {x // x < y}

Equations

slim_check.int_lt.sampleable = {wf := subtype.has_sizeof (λ (x : ℤ), x < y), sample := slim_check.sampleable.sample ℕ >>= λ (x : ℕ), pure ⟨y - (↑x + 1), _⟩, shrink := λ (_x : {x // x < y}), lazy_list.nil}

@[instance]

def slim_check.int_gt.sampleable {x : ℤ} :

slim_check.sampleable {y // x < y}

Equations

slim_check.int_gt.sampleable = {wf := subtype.has_sizeof (λ (y : ℤ), x < y), sample := slim_check.sampleable.sample ℕ >>= λ (_p : ℕ), slim_check.int_gt.sampleable._match_1 _p, shrink := λ (_x : {y // x < y}), lazy_list.nil}
slim_check.int_gt.sampleable._match_1 y = pure ⟨x + ↑y + 1, _⟩

@[instance]

def slim_check.le.sampleable {α : Type u} {y : α} [decidable_linear_ordered_add_comm_group α] [slim_check.sampleable α] :

slim_check.sampleable {x // x ≤ y}

Equations

slim_check.le.sampleable = {wf := subtype.has_sizeof (λ (x : α), x ≤ y), sample := slim_check.sampleable.sample α >>= λ (x : α), pure ⟨y - abs x, _⟩, shrink := λ (_x : {x // x ≤ y}), lazy_list.nil}

@[instance]

def slim_check.ge.sampleable {α : Type u} {x : α} [decidable_linear_ordered_add_comm_group α] [slim_check.sampleable α] :

slim_check.sampleable {y // x ≤ y}

Equations

slim_check.ge.sampleable = {wf := subtype.has_sizeof (λ (y : α), x ≤ y), sample := slim_check.sampleable.sample α >>= λ (y : α), pure ⟨x + abs y, _⟩, shrink := λ (_x : {y // x ≤ y}), lazy_list.nil}

@[instance]

def slim_check.perm.slim_check {α : Type u} {xs : list α} :

slim_check.sampleable {ys // xs ~ ys}

Equations

slim_check.perm.slim_check = {wf := subtype.has_sizeof (λ (ys : list α), xs ~ ys), sample := slim_check.gen.permutation_of xs, shrink := λ (_x : {ys // xs ~ ys}), lazy_list.nil}

@[instance]

def slim_check.perm'.slim_check {α : Type u} {xs : list α} :

slim_check.sampleable {ys // ys ~ xs}

Equations

slim_check.perm'.slim_check = {wf := subtype.has_sizeof (λ (ys : list α), ys ~ xs), sample := subtype.map id list.perm.symm <$> slim_check.gen.permutation_of xs, shrink := λ (_x : {ys // ys ~ xs}), lazy_list.nil}

def slim_check.print_samples (t : Type u) [slim_check.sampleable t] [has_repr t] :

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

Equations

slim_check.print_samples t = io.run_rand (uliftable.down (mmap ((slim_check.sampleable.sample t).run ∘ ulift.up) (list.range 10) >>= λ (xs : list t), pure {down := list.map repr xs})) >>= λ (xs : list string), mmap' io.put_str_ln xs

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