`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

- 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

- 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

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

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

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

`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

## Equations

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

## Equations

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

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

## Equations

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

## Equations

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

## Equations

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

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

## Equations

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

## Equations

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

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.

## Equations

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

## Equations

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

An annotation for values that should never get shrinked.

## Equations

- SlimCheck.NoShrink α = α

## Equations

## Equations

## Equations

- SlimCheck.NoShrink.inhabited = inst

## Equations

- SlimCheck.NoShrink.repr = inst

## Equations

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

## Equations

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