mathlib documentation

tactic.slim_check

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 slim_check.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.slim_check.testable.

source
meta inductive tactic.interactive.instance_tree  :
Type

Tree structure representing a testable instance.

source
meta def tactic.interactive.summarize_instance (a : expr) :
tactic tactic.interactive.instance_tree

Gather information about a testable instance. Given an expression of type testable ?p, gather the name of the testable instances that it is built from and the proposition that they test.

source
meta def tactic.interactive.instance_tree.to_format (a : tactic.interactive.instance_tree) :
tactic format

format a instance_tree

source
@[instance]
meta def tactic.interactive.instance_tree.has_to_tactic_format  :
has_to_tactic_format tactic.interactive.instance_tree

source
meta def tactic.interactive.slim_check (cfg : slim_check.slim_check_cfg := {num_inst := 100, max_size := 100, enable_tracing := ff, random_seed := none ℕ, quiet := ff}) :
tactic unit

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.slim_check.testable.

Optional arguments given with slim_check_cfg

  • num_inst (default 100): number of examples to test properties with
  • max_size (default 100): final size argument
  • enable_tracing (default ff): enable the printing of discarded samples

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.instance true: print the instances of testable being used to test the proposition