Documentation

plausible

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

Tags:

Defined in module:

Plausible.Tactic