# mathlib3documentation

testing.slim_check.testable

# testable Class #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Testable propositions have a procedure that can generate counter-examples together with a proof that they invalidate the proposition.

This is a port of the Haskell QuickCheck library.

## Creating Customized Instances #

The type classes testable and sampleable are the means by which slim_check creates samples and tests them. For instance, the proposition ∀ i j : ℕ, i ≤ j has a testable instance because ℕ is sampleable and i ≤ j is decidable. Once slim_check finds the testable instance, it can start using the instance to repeatedly creating samples and checking whether they satisfy the property. This allows the user to create new instances and apply slim_check to new situations.

### Polymorphism #

The property testable.check (∀ (α : Type) (xs ys : list α), xs ++ ys = ys ++ xs) shows us that type-polymorphic properties can be tested. α is instantiated with ℤ first and then tested as normal monomorphic properties.

The monomorphisation limits the applicability of slim_check to polymorphic properties that can be stated about integers. The limitation may be lifted in the future but, for now, if one wishes to use a different type than ℤ, one has to refer to the desired type.

### What do I do if I'm testing a property about my newly defined type? #

Let us consider a type made for a new formalization:

structure my_type :=
(x y : ℕ)
(h : x ≤ y)


How do we test a property about my_type? For instance, let us consider testable.check $∀ a b : my_type, a.y ≤ b.x → a.x ≤ b.y. Writing this property as is will give us an error because we do not have an instance of sampleable my_type. We can define one as follows: instance : sampleable my_type := { sample := do x ← sample ℕ, xy_diff ← sample ℕ, return { x := x, y := x + xy_diff, h := /- some proof -/ } }  We can see that the instance is very simple because our type is built up from other type that have sampleable instances. sampleable also has a shrink method but it is optional. We may want to implement one for ease of testing as: /- ... -/ shrink := λ ⟨x,y,h⟩, (λ ⟨x,y⟩, { x := x, y := x + y, h := /- proof -/}) <$> shrink (x, y - x) }


Again, we take advantage of the fact that other types have useful shrink implementations, in this case prod.

### Optimizing the sampling #

Some properties are guarded by a proposition. For instance, recall this example:

#eval testable.check (∀ x : ℕ, 2 ∣ x → x < 100)


When testing the above example, we generate a natural number, we check that it is even and test it if it is even or throw it away and start over otherwise. Statistically, we can expect half of our samples to be thrown away by such a filter. Sometimes, the filter is more restrictive. For instance we might need x to be a prime number. This would cause most of our samples to be discarded.

We can help slim_check find good samples by providing specialized sampleable instances. Below, we show an instance for the subtype of even natural numbers. This means that, when producing a sample, it is forced to produce a proof that it is even.

instance {k : ℕ} [fact (0 < k)] : sampleable { x : ℕ // k ∣ x } :=
{ sample := do { n ← sample ℕ, pure ⟨k*n, dvd_mul_right _ _⟩ },
shrink := λ ⟨x,h⟩, (λ y, ⟨k*y, dvd_mul_right _ _⟩) <$> shrink x }  Such instance will be preferred when testing a proposition of the shape ∀ x : T, p x → q We can observe the effect by enabling tracing: /- no specialized sampling -/ #eval testable.check (∀ x : ℕ, 2 ∣ x → x < 100) { trace_discarded := tt } -- discard -- x := 1 -- discard -- x := 41 -- discard -- x := 3 -- discard -- x := 5 -- discard -- x := 5 -- discard -- x := 197 -- discard -- x := 469 -- discard -- x := 9 -- discard -- =================== -- Found problems! -- x := 552 -- ------------------- /- let us define a specialized sampling instance -/ instance {k : ℕ} : sampleable { x : ℕ // k ∣ x } := { sample := do { n ← sample ℕ, pure ⟨k*n, dvd_mul_right _ _⟩ }, shrink := λ ⟨x,h⟩, (λ y, ⟨k*y, dvd_mul_right _ _⟩) <$> shrink x }

#eval testable.check (∀ x : ℕ, 2 ∣ x → x < 100) { enable_tracing := tt }
-- ===================
-- Found problems!

-- x := 358
-- -------------------


Similarly, it is common to write properties of the form: ∀ i j, i ≤ j → ... as the following example show:

#eval check (∀ i j k : ℕ, j < k → i - k < i - j)


Without subtype instances, the above property discards many samples because j < k does not hold. Fortunately, we have appropriate instance to choose k intelligently.

## Main definitions #

• testable class
• testable.check: a way to test a proposition using random examples

random testing

## References #

inductive slim_check.test_result (p : Prop) :
• success : Π {p : Prop},
• gave_up : Π {p : Prop},
• failure : Π {p : Prop},

Result of trying to disprove p

The constructors are:

• success : (psum unit p) → test_result succeed when we find another example satisfying p In success h, h is an optional proof of the proposition. Without the proof, all we know is that we found one example where p holds. With a proof, the one test was sufficient to prove that p holds and we do not need to keep finding examples.
• gave_up {} : ℕ → test_result give up when a well-formed example cannot be generated. gave_up n tells us that n invalid examples were tried. Above 100, we give up on the proposition and report that we did not find a way to properly test it.
• failure : ¬ p → (list string) → ℕ → test_result a counter-example to p; the strings specify values for the relevant variables. failure h vs n also carries a proof that p does not hold. This way, we can guarantee that there will be no false positive. The last component, n, is the number of times that the counter-example was shrunk.
Instances for slim_check.test_result
@[protected, instance]
def slim_check.test_result.inhabited (p : Prop) [a : inhabited p] :
@[protected]

format a test_result as a string.

Equations
• _x).to_string = "failed " ++ ++ ""
• = "gave up " ++ ++ " times"
• = "success (with proof)"
• = "success (without proof)"
@[protected, instance]
• num_inst :
• max_size :
• trace_success : bool
• trace_shrink : bool
• trace_shrink_candidates : bool
• random_seed :
• quiet : bool

configuration for testing a property

Instances for slim_check.slim_check_cfg
@[protected, instance]
@[protected, instance]
Equations
@[class]
structure slim_check.printable_prop (p : Prop) :
• print_prop :

printable_prop p allows one to print a proposition so that slim_check can indicate how values relate to each other.

Instances of this typeclass
Instances of other typeclasses for slim_check.printable_prop
• slim_check.printable_prop.has_sizeof_inst
@[protected, instance]
Equations
@[class]
structure slim_check.testable (p : Prop) :

testable p uses random examples to try to disprove p.

Instances of this typeclass
Instances of other typeclasses for slim_check.testable
• slim_check.testable.has_sizeof_inst
def slim_check.combine {p q : Prop} :
(p q) p q

applicative combinator proof carrying test results

Equations
def slim_check.and_counter_example {p q : Prop} :

Combine the test result for properties p and q to create a test for their conjunction.

Equations
def slim_check.or_counter_example {p q : Prop} :

Combine the test result for properties p and q to create a test for their disjunction

Equations
def slim_check.convert_counter_example {p q : Prop} (h : q p) :
(p q) :=

If q → p, then ¬ p → ¬ q which means that testing p can allow us to find counter-examples to q.

Equations
def slim_check.convert_counter_example' {p q : Prop} (h : p q) (r : slim_check.test_result p) :

Test q by testing p and proving the equivalence between the two.

Equations
def slim_check.add_to_counter_example (x : string) {p q : Prop} (h : q p) :
(p q) :=

When we assign a value to a universally quantified variable, we record that value using this function so that our counter-examples can be informative.

Equations
def slim_check.add_var_to_counter_example {γ : Type v} [has_repr γ] (var : string) (x : γ) {p q : Prop} (h : q p) :
(p q) :=

Add some formatting to the information recorded by add_to_counter_example.

Equations
@[simp, nolint]
def slim_check.named_binder (n : string) (p : Prop) :
Prop

Gadget used to introspect the name of bound variables.

It is used with the testable typeclass so that testable (named_binder "x" (∀ x, p x)) can use the variable name of x in error messages displayed to the user. If we find that instantiating the above quantifier with 3 falsifies it, we can print:

==============
Problem found!
==============
x := 3

Equations
Instances for slim_check.named_binder
def slim_check.is_failure {p : Prop} :

Is the given test result a failure?

Equations
@[protected, instance]
def slim_check.and_testable (p q : Prop)  :
Equations
@[protected, instance]
def slim_check.or_testable (p q : Prop)  :
Equations
• = {run := λ (cfg : slim_check.slim_check_cfg) (min : bool), min >>= λ (xp : , slim_check.or_testable._match_1 p q cfg min xp xp}
• slim_check.or_testable._match_1 p q cfg min xp ᾰ_2) = min >>= λ (xq : ,
• slim_check.or_testable._match_1 p q cfg min xp = min >>= λ (xq : ,
• slim_check.or_testable._match_1 p q cfg min xp =
• slim_check.or_testable._match_1 p q cfg min xp =
@[protected, instance]
Equations
@[protected, instance]
def slim_check.dec_guard_testable (var : string) (p : Prop) [decidable p] (β : p Prop) [Π (h : p), slim_check.testable (β h)] :
slim_check.testable ( (h : p), β h))
Equations
def slim_check.use_has_to_string (α : Type u_1) :
Type u_1

Type tag that replaces a type's has_repr instance with its has_to_string instance.

Equations
Instances for slim_check.use_has_to_string
@[protected, instance]
Equations
def slim_check.use_has_to_string.mk {α : Type u_1} (x : α) :

Add the type tag use_has_to_string to an expression's type.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def slim_check.trace_if_giveup {p : Prop} {α : Type u_1} {β : Type u_2} [has_repr α] (tracing_enabled : bool) (var : string) (val : α) :

Trace the value of sampled variables if the sample is discarded.

Equations
@[protected, instance]
def slim_check.test_forall_in_list (var var' : string) (α : Type u) (β : α Prop) [Π (x : α), slim_check.testable (β x)] [has_repr α] (xs : list α) :
slim_check.testable ( (x : α), (x xs β x)))

testable instance for a property iterating over the element of a list

Equations
def slim_check.combine_testable (p : Prop) (t : list ) (h : 0 < t.length) :

Test proposition p by randomly selecting one of the provided testable instances.

Equations

Format the counter-examples found in a test failure.

Equations
def slim_check.format_failure' (s : string) {p : Prop} :

Format the counter-examples found in a test failure.

Equations
def slim_check.add_shrinks {p : Prop} (n : ) :

Increase the number of shrinking steps in a test result.

Equations
def slim_check.minimize_aux (α : Type u) (β : α Prop) [Π (x : α), slim_check.testable (β x)] (cfg : slim_check.slim_check_cfg) (var : string) :

Shrink a counter-example x by using shrink x, picking the first candidate that falsifies a property and recursively shrinking that one.

The process is guaranteed to terminate because shrink x produces a proof that all the values it produces are smaller (according to sizeof) than x.

Equations
def slim_check.minimize (α : Type u) (β : α Prop) [Π (x : α), slim_check.testable (β x)] (cfg : slim_check.slim_check_cfg) (var : string) (r : slim_check.test_result ) :

Once a property fails to hold on an example, look for smaller counter-examples to show the user.

Equations
@[protected, instance]
def slim_check.exists_testable (var var' : string) (α : Type u) (β : α Prop) (p : Prop) [slim_check.testable ( (x : α), (β x p)))] :
slim_check.testable ( (x : α), β x) p))
Equations
@[protected, instance]
def slim_check.var_testable (var : string) (α : Type u) (β : α Prop) [Π (x : α), slim_check.testable (β x)] :
slim_check.testable ( (x : α), β x))

Test a universal property by creating a sample of the right type and instantiating the bound variable with it

Equations
@[protected, instance]
def slim_check.prop_var_testable (var : string) (β : Prop Prop) [I : Π (b : bool), slim_check.testable b)] :
slim_check.testable ( (p : Prop), β p))

Test a universal property about propositions

Equations
@[protected, instance]
def slim_check.unused_var_testable (var : string) (α : Type u) (β : Prop) [inhabited α]  :
Equations
@[protected, instance]
def slim_check.subtype_var_testable (var var' : string) (α : Type u) (β : α Prop) {p : α Prop} [Π (x : α), ] [Π (x : α), slim_check.testable (β x)] [I : slim_check.sampleable_ext (subtype p)] :
slim_check.testable ( (x : α), (p x β x)))
Equations
@[protected, instance]
Equations
@[protected, instance]
def slim_check.eq.printable_prop {α : Type u_1} [has_repr α] (x y : α) :
Equations
@[protected, instance]
def slim_check.ne.printable_prop {α : Type u_1} [has_repr α] (x y : α) :
Equations
@[protected, instance]
def slim_check.le.printable_prop {α : Type u_1} [has_le α] [has_repr α] (x y : α) :
Equations
@[protected, instance]
def slim_check.lt.printable_prop {α : Type u_1} [has_lt α] [has_repr α] (x y : α) :
Equations
@[protected, instance]
def slim_check.perm.printable_prop {α : Type u_1} [has_repr α] (xs ys : list α) :
Equations
@[protected, instance]
def slim_check.and.printable_prop (x y : Prop)  :
Equations
@[protected, instance]
def slim_check.or.printable_prop (x y : Prop)  :
Equations
@[protected, instance]
def slim_check.iff.printable_prop (x y : Prop)  :
Equations
@[protected, instance]
def slim_check.imp.printable_prop (x y : Prop)  :
Equations
@[protected, instance]
def slim_check.not.printable_prop (x : Prop)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
def slim_check.retry {p : Prop} (cmd : rand ) :

Execute cmd and repeat every time the result is gave_up (at most n times).

Equations
• n.succ = cmd >>= λ (r : , slim_check.retry._match_1 (slim_check.retry cmd n) r
• slim_check.retry._match_1 _f_1 n) = return n)
• slim_check.retry._match_1 _f_1 = _f_1
• slim_check.retry._match_1 _f_1 =
def slim_check.give_up {p : Prop} (x : ) :

Count the number of times the test procedure gave up.

Equations

Try n times to find a counter-example for p.

Equations

Try to find a counter-example of p.

Equations

Run a test suite for p in io.

Equations

## Decorations #

Instances of testable use named_binder as a decoration on propositions in order to access the name of bound variables, as in named_binder "x" (forall x, x < y). This helps the testable instances create useful error messages where variables are matched with values that falsify a given proposition.

The following functions help support the gadget so that the user does not have to put them in themselves.

add_existential_decorations p adds anamed_binderannotation at the root ofpifp is an existential quantification.

Traverse the syntax of a proposition to find universal quantifiers and existential quantifiers and add named_binder annotations next to them.

@[nolint, reducible]

decorations_of p is used as a hint to mk_decorations to specify that the goal should be satisfied with a proposition equivalent to p with added annotations.

Equations

In a goal of the shape ⊢ tactic.decorations_of p, mk_decoration examines the syntax of p and add named_binder around universal quantifications and existential quantifications to improve error messages.

This tool can be used in the declaration of a function as follows:

def foo (p : Prop) (p' : tactic.decorations_of p . mk_decorations) [testable p'] : ...


p is the parameter given by the user, p' is an equivalent proposition where the quantifiers are annotated with named_binder.

def slim_check.testable.check (p : Prop) (cfg : slim_check.slim_check_cfg := ) (p' : . "mk_decorations")  :

Run a test suite for p and return true or false: should we believe that p` holds?

Equations