Documentation

Mathlib.Testing.SlimCheck.Sampleable

`SampleableExt` Class #

This class permits the creation samples of a given type controlling the size of those values using the Gen monad`.

`Shrinkable` Class #

This class helps minimize examples by creating smaller versions of given values.

When testing a proposition like ∀ n : ℕ, prime n → n ≤ 100∀ n : ℕ, prime n → n ≤ 100→ n ≤ 100≤ 100, SlimCheck requires that ℕ have an instance of SampleableExt and for prime n to be decidable. SlimCheck will then use the instance of SampleableExt 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 SlimCheck will move on to other examples. If prime n is true, n ≤ 100≤ 100 will be tested. If it is false, n is a counter-example of ∀ n : ℕ, prime n → n ≤ 100∀ n : ℕ, prime n → n ≤ 100→ n ≤ 100≤ 100 and the test fails. If n ≤ 100≤ 100 is true, the test passes and SlimCheck moves on to trying more examples.

This is a port of the Haskell QuickCheck library.

Main definitions #

SampleableExt class
Shrinkable class

`SampleableExt` #

SampleableExt can be used in two ways. The first (and most common) is to simply generate values of a type directly using the Gen monad, if this is what you want to do then SampleableExt.mkSelfContained is the way to go.

Furthermore it makes it possible to express generators 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, SampleableExt provides a proxy representation proxy that can be printed and shrunken as well as interpreted (using interp) as an object of the right type. If you are using it in the first way, this proxy type will simply be the type itself and the interp function id.

`Shrinkable #

Given an example x : α, Shrinkable α gives us a way to shrink it and suggest simpler examples.

Shrinking #

Shrinking happens when SlimCheck find a counter-example to a property. It is likely that the example will be more complicated than necessary so SlimCheck 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 Shrinkable class, , 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. SlimCheck 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 SlimCheck is guaranteed to terminate.

Tags #

random testing

References #

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

class SlimCheck.Shrinkable (α : Type u) extends WellFoundedRelation :

shrink : (x : α) → List { y // WellFoundedRelation.rel y x }

Given an example x : α, Shrinkable α gives us a way to shrink it and suggest simpler examples.

Instances

class SlimCheck.SampleableExt (α : Sort u) :

Sort (maxu(v+2))

proxy : Type v
proxyRepr : Repr proxy
shrink : SlimCheck.Shrinkable proxy
sample : SlimCheck.Gen proxy
interp : proxy → α

SampleableExt can be used in two ways. The first (and most common) is to simply generate values of a type directly using the Gen monad, if this is what you want to do then SampleableExt.mkSelfContained is the way to go.

Furthermore it makes it possible to express generators 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, SampleableExt provides a proxy representation proxy that can be printed and shrunken as well as interpreted (using interp) as an object of the right type.

Instances

def SlimCheck.SampleableExt.mkSelfContained {α : Type u_1} [inst : Repr α] [inst : SlimCheck.Shrinkable α] (sample : SlimCheck.Gen α) :

SlimCheck.SampleableExt α

Use to generate instance whose purpose is to simply generate values of a type directly using the Gen monad

Equations

SlimCheck.SampleableExt.mkSelfContained sample = SlimCheck.SampleableExt.mk α sample id

def SlimCheck.SampleableExt.interpSample (α : Type u) [inst : SlimCheck.SampleableExt α] :

SlimCheck.Gen α

First samples a proxy value and interprets it. Especially useful if the proxy and target type are the same.

Equations

SlimCheck.SampleableExt.interpSample α = SlimCheck.SampleableExt.interp <$> SlimCheck.SampleableExt.sample

def SlimCheck.Nat.shrink (n : ℕ) :

List { y // WellFoundedRelation.rel y n }

Nat.shrink' n creates a list of smaller natural numbers by successively dividing n by 2 . For example, Nat.shrink 5 = [2, 1, 0].

Equations

One or more equations did not get rendered due to their size.

instance SlimCheck.Nat.shrinkable :

SlimCheck.Shrinkable ℕ

Equations

SlimCheck.Nat.shrinkable = SlimCheck.Shrinkable.mk SlimCheck.Nat.shrink

def SlimCheck.Fin.shrink {n : ℕ} (m : Fin (Nat.succ n)) :

List { y // WellFoundedRelation.rel y m }

Fin.shrink works like Nat.shrink but instead operates on Fin.

Equations

SlimCheck.Fin.shrink m = let shrinks := SlimCheck.Nat.shrink ↑m; List.map (fun x => { val := ↑↑x, property := (_ : WellFoundedRelation.rel (↑↑x) m) }) shrinks

instance SlimCheck.Fin.shrinkable {n : ℕ} :

SlimCheck.Shrinkable (Fin (Nat.succ n))

Equations

SlimCheck.Fin.shrinkable = SlimCheck.Shrinkable.mk SlimCheck.Fin.shrink

def SlimCheck.Int_sizeOfAbs :

Equations

SlimCheck.Int_sizeOfAbs = { sizeOf := Int.natAbs }

instance SlimCheck.Int.shrinkable :

SlimCheck.Shrinkable ℤ

Int.shrinkable operates like Nat.shrinkable but also includes the negative variants.

Equations

One or more equations did not get rendered due to their size.

instance SlimCheck.Bool.shrinkable :

SlimCheck.Shrinkable Bool

Equations

SlimCheck.Bool.shrinkable = SlimCheck.Shrinkable.mk fun x => []

instance SlimCheck.Char.shrinkable :

SlimCheck.Shrinkable Char

Equations

SlimCheck.Char.shrinkable = SlimCheck.Shrinkable.mk fun x => []

instance SlimCheck.Prod.shrinkable {α : Type u_1} {β : Type u_2} [shrA : SlimCheck.Shrinkable α] [shrB : SlimCheck.Shrinkable β] :

SlimCheck.Shrinkable (α × β)

Equations

One or more equations did not get rendered due to their size.

instance SlimCheck.Nat.sampleableExt :

SlimCheck.SampleableExt ℕ

Equations

SlimCheck.Nat.sampleableExt = SlimCheck.SampleableExt.mkSelfContained do let __do_lift ← SlimCheck.Gen.getSize Lean.Internal.coeM (SlimCheck.Gen.choose ℕ 0 __do_lift (_ : 0 ≤ __do_lift))

instance SlimCheck.Fin.sampleableExt {n : ℕ} :

SlimCheck.SampleableExt (Fin (Nat.succ n))

Equations

One or more equations did not get rendered due to their size.

instance SlimCheck.Int.sampleableExt :

SlimCheck.SampleableExt ℤ

Equations

One or more equations did not get rendered due to their size.

instance SlimCheck.Bool.sampleableExt :

SlimCheck.SampleableExt Bool

Equations

SlimCheck.Bool.sampleableExt = SlimCheck.SampleableExt.mkSelfContained (SlimCheck.Gen.chooseAny Bool)

def SlimCheck.Char.sampleable (length : ℕ) (chars : List Char) (pos : 0 < List.length chars) :

SlimCheck.SampleableExt Char

This can be specialized into customized SampleableExt Char instances. The resulting instance has 1 / length chances of making an unrestricted choice of characters and it otherwise chooses a character from chars with uniform probabilities.

Equations

One or more equations did not get rendered due to their size.

instance SlimCheck.Char.sampleableDefault :

SlimCheck.SampleableExt Char

Equations

SlimCheck.Char.sampleableDefault = SlimCheck.Char.sampleable 3 (String.toList " 0123abcABC:,;`\\/") SlimCheck.Char.sampleableDefault.proof_1

instance SlimCheck.Prod.sampleableExt {α : Type u} {β : Type u} [inst : SlimCheck.SampleableExt α] [inst : SlimCheck.SampleableExt β] :

SlimCheck.SampleableExt (α × β)

Equations

One or more equations did not get rendered due to their size.

instance SlimCheck.Prop.sampleableExt :

SlimCheck.SampleableExt Prop

Equations

SlimCheck.Prop.sampleableExt = SlimCheck.SampleableExt.mk Bool (SlimCheck.SampleableExt.interpSample Bool) Coe.coe

def SlimCheck.NoShrink (α : Type u) :

An annotation for values that should never get shrinked.

Equations

SlimCheck.NoShrink α = α

def SlimCheck.NoShrink.mk {α : Type u_1} (x : α) :

SlimCheck.NoShrink α

Equations

SlimCheck.NoShrink.mk x = x

def SlimCheck.NoShrink.get {α : Type u_1} (x : SlimCheck.NoShrink α) :

α

Equations

SlimCheck.NoShrink.get x = x

instance SlimCheck.NoShrink.inhabited {α : Type u_1} [inst : Inhabited α] :

Inhabited (SlimCheck.NoShrink α)

Equations

SlimCheck.NoShrink.inhabited = inst

instance SlimCheck.NoShrink.repr {α : Type u_1} [inst : Repr α] :

Repr (SlimCheck.NoShrink α)

Equations

SlimCheck.NoShrink.repr = inst

instance SlimCheck.NoShrink.shrinkable {α : Type u_1} :

SlimCheck.Shrinkable (SlimCheck.NoShrink α)

Equations

SlimCheck.NoShrink.shrinkable = SlimCheck.Shrinkable.mk fun x => []

instance SlimCheck.NoShrink.sampleableExt {α : Type u_1} [inst : SlimCheck.SampleableExt α] [inst : Repr α] :

SlimCheck.SampleableExt (SlimCheck.NoShrink α)

Equations

SlimCheck.NoShrink.sampleableExt = SlimCheck.SampleableExt.mkSelfContained ((SlimCheck.NoShrink.mk ∘ SlimCheck.SampleableExt.interp) <$> SlimCheck.SampleableExt.sample)