## Finding counterexamples automatically using `slim_check`

#

A proposition can be tested by writing it out as:

```
example (xs : List ℕ) (w : ∃ x ∈ xs, x < 3) : ∀ y ∈ xs, y < 5 := by slim_check
-- ===================
-- Found problems!
-- xs := [0, 5]
-- x := 0
-- y := 5
-- -------------------
example (x : ℕ) (h : 2 ∣ x) : x < 100 := by slim_check
-- ===================
-- Found problems!
-- x := 258
-- -------------------
example (α : Type) (xs ys : List α) : xs ++ ys = ys ++ xs := by slim_check
-- ===================
-- Found problems!
-- α := ℤ
-- xs := [-4]
-- ys := [1]
-- -------------------
example : ∀ x ∈ [1,2,3], x < 4 := by slim_check
-- Success
```

In the first example, `slim_check`

is called on the following goal:

```
xs : List ℕ,
h : ∃ (x : ℕ) (H : x ∈ xs), x < 3
⊢ ∀ (y : ℕ), y ∈ xs → y < 5
```

The local constants are reverted and an instance is found for
`Testable (∀ (xs : List ℕ), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))`

.
The `Testable`

instance is supported by instances of `Sampleable (List ℕ)`

,
`Decidable (x < 3)`

and `Decidable (y < 5)`

. `slim_check`

builds a
`Testable`

instance step by step with:

```
- Testable (∀ (xs : List ℕ), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))
-: Sampleable (List xs)
- Testable ((∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))
- Testable (∀ x ∈ xs, x < 3 → (∀ y ∈ xs, y < 5))
- Testable (x < 3 → (∀ y ∈ xs, y < 5))
-: Decidable (x < 3)
- Testable (∀ y ∈ xs, y < 5)
-: Decidable (y < 5)
```

`Sampleable (List ℕ)`

lets us create random data of type `List ℕ`

in a way that
helps find small counter-examples. Next, the test of the proposition
hinges on `x < 3`

and `y < 5`

to both be decidable. The
implication between the two could be tested as a whole but it would be
less informative. Indeed, if we generate lists that only contain numbers
greater than `3`

, the implication will always trivially hold but we should
conclude that we haven't found meaningful examples. Instead, when `x < 3`

does not hold, we reject the example (i.e. we do not count it toward
the 100 required positive examples) and we start over. Therefore, when
`slim_check`

prints `Success`

, it means that a hundred suitable lists
were found and successfully tested.

If no counter-examples are found, `slim_check`

behaves like `admit`

.

`slim_check`

can also be invoked using `#eval`

:

```
#eval SlimCheck.Testable.check (∀ (α : Type) (xs ys : List α), xs ++ ys = ys ++ xs)
-- ===================
-- Found problems!
-- α := ℤ
-- xs := [-4]
-- ys := [1]
-- -------------------
```

For more information on writing your own `Sampleable`

and `Testable`

instances, see `Testing.SlimCheck.Testable`

.

`slim_check`

considers a proof goal and tries to generate examples
that would contradict the statement.

Let's consider the following proof goal.

```
xs : List ℕ,
h : ∃ (x : ℕ) (H : x ∈ xs), x < 3
⊢ ∀ (y : ℕ), y ∈ xs → y < 5
```

The local constants will be reverted and an instance will be found for
`Testable (∀ (xs : List ℕ), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5))`

.
The `Testable`

instance is supported by an instance of `Sampleable (List ℕ)`

,
`Decidable (x < 3)`

and `Decidable (y < 5)`

.

Examples will be created in ascending order of size (more or less)

The first counter-examples found will be printed and will result in an error:

```
===================
Found problems!
xs := [1, 28]
x := 1
y := 28
-------------------
```

If `slim_check`

successfully tests 100 examples, it acts like
admit. If it gives up or finds a counter-example, it reports an error.

For more information on writing your own `Sampleable`

and `Testable`

instances, see `Testing.SlimCheck.Testable`

.

Optional arguments given with `slim_check (config : { ... })`

`numInst`

(default 100): number of examples to test properties with`maxSize`

(default 100): final size argument

Options:

`set_option trace.slim_check.decoration true`

: print the proposition with quantifier annotations`set_option trace.slim_check.discarded true`

: print the examples discarded because they do not satisfy assumptions`set_option trace.slim_check.shrink.steps true`

: trace the shrinking of counter-example`set_option trace.slim_check.shrink.candidates true`

: print the lists of candidates considered when shrinking each variable`set_option trace.slim_check.instance true`

: print the instances of`testable`

being used to test the proposition`set_option trace.slim_check.success true`

: print the tested samples that satisfy a property