Finding counterexamples automatically using plausible

A proposition can be tested by writing it out as:

example (xs : List Nat) (w : ∃ x ∈ xs, x < 3) : ∀ y ∈ xs, y < 5 := by plausible
-- ===================
-- Found problems!

-- xs := [0, 5]
-- x := 0
-- y := 5
-- -------------------

example (x : Nat) (h : 2 ∣ x) : x < 100 := by plausible
-- ===================
-- Found problems!

-- x := 258
-- -------------------

example (α : Type) (xs ys : List α) : xs ++ ys = ys ++ xs := by plausible
-- ===================
-- Found problems!

-- α := Int
-- xs := [-4]
-- ys := [1]
-- -------------------

example : ∀ x ∈ [1,2,3], x < 4 := by plausible
-- Success

In the first example, plausible is called on the following goal:

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

The local constants are reverted and an instance is found for Testable (∀ (xs : List Nat), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5)). The Testable instance is supported by instances of Sampleable (List Nat), Decidable (x < 3) and Decidable (y < 5). plausible builds a Testable instance step by step with:

- Testable (∀ (xs : List Nat), (∃ 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 Nat) lets us create random data of type List Nat 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 plausible prints Success, it means that a hundred suitable lists were found and successfully tested.

If no counter-examples are found, plausible behaves like admit.

plausible can also be invoked using #eval:

#eval Plausible.Testable.check (∀ (α : Type) (xs ys : List α), xs ++ ys = ys ++ xs)
-- ===================
-- Found problems!

-- α := Int
-- xs := [-4]
-- ys := [1]
-- -------------------

For more information on writing your own Sampleable and Testable instances, see Testing.Plausible.Testable.

def plausibleSyntax : Lean.ParserDescr

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

Let's consider the following proof goal.

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

The local constants will be reverted and an instance will be found for Testable (∀ (xs : List Nat), (∃ x ∈ xs, x < 3) → (∀ y ∈ xs, y < 5)). The Testable instance is supported by an instance of Sampleable (List Nat), 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 plausible 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.Plausible.Testable.

Optional arguments given with plausible (config : { ... })

• numInst (default 100): number of examples to test properties with
• maxSize (default 100): final size argument

Options:

• set_option trace.plausible.decoration true: print the proposition with quantifier annotations
• set_option trace.plausible.discarded true: print the examples discarded because they do not satisfy assumptions
• set_option trace.plausible.shrink.steps true: trace the shrinking of counter-example
• set_option trace.plausible.shrink.candidates true: print the lists of candidates considered when shrinking each variable
• set_option trace.plausible.instance true: print the instances of testable being used to test the proposition
• set_option trace.plausible.success true: print the tested samples that satisfy a property

Equations

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