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.

def slimCheckSyntax : Lean.ParserDescr

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

Equations

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