`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

Tags #

random testing

testable Class #