Testable
Class #
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
, SampleableExt
and Shrinkable
are the
means by which Plausible
creates samples and tests them. For instance,
the proposition ∀ i j : Nat, i ≤ j
has a Testable
instance because Nat
is sampleable and i ≤ j
is decidable. Once Plausible
finds the Testable
instance, it can start using the instance to repeatedly creating samples
and checking whether they satisfy the property. Once it has found a
counter-example it will then use a Shrinkable
instance to reduce the
example. This allows the user to create new instances and apply
Plausible
to new situations.
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 MyType where
x : Nat
y : Nat
h : x ≤ y
deriving Repr
How do we test a property about MyType
? For instance, let us consider
Testable.check <| ∀ a b : MyType, 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 Shrinkable MyType
and SampleableExt MyType
. We can define one as follows:
instance : Shrinkable MyType where
shrink := fun ⟨x, y, _⟩ =>
let proxy := Shrinkable.shrink (x, y - x)
proxy.map (fun (fst, snd) => ⟨fst, fst + snd, by omega⟩)
instance : SampleableExt MyType :=
SampleableExt.mkSelfContained do
let x ← SampleableExt.interpSample Nat
let xyDiff ← SampleableExt.interpSample Nat
return ⟨x, x + xyDiff, by omega⟩
Again, we take advantage of the fact that other types have useful
Shrinkable
implementations, in this case Prod
.
Main definitions #
Testable
classTestable.check
: a way to test a proposition using random examples
References #
Result of trying to disprove p
- success
{p : Prop}
: Unit ⊕' p → TestResult p
Succeed when we find another example satisfying
p
. Insuccess h
,h
is an optional proof of the proposition. Without the proof, all we know is that we found one example wherep
holds. With a proof, the one test was sufficient to prove thatp
holds and we do not need to keep finding examples. - gaveUp
{p : Prop}
: Nat → TestResult p
Give up when a well-formed example cannot be generated.
gaveUp n
tells us thatn
invalid examples were tried. - failure
{p : Prop}
: ¬p → List String → Nat → TestResult p
A counter-example to
p
; the strings specify values for the relevant variables.failure h vs n
also carries a proof thatp
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
Configuration for testing a property.
- numInst : Nat
How many test instances to generate.
- maxSize : Nat
The maximum size of the values to generate.
- numRetries : Nat
- traceDiscarded : Bool
Enable tracing of values that didn't fulfill preconditions and were thus discarded.
- traceSuccesses : Bool
Enable tracing of values that fulfilled the property and were thus discarded.
- traceShrink : Bool
Enable basic tracing of shrinking.
- traceShrinkCandidates : Bool
Enable tracing of all attempted values during shrinking.
Hard code the seed to use for the RNG
- quiet : Bool
Disable output.
Instances For
PrintableProp p
allows one to print a proposition so that
Plausible
can indicate how values relate to each other.
It's basically a poor man's delaborator.
- printProp : String
Instances
Combine the test result for properties p
and q
to create a test for their conjunction.
Equations
Instances For
Combine the test result for properties p
and q
to create a test for their disjunction.
Equations
Instances For
If q → p
, then ¬ p → ¬ q
which means that testing p
can allow us
to find counter-examples to q
.
Equations
Instances For
Test q
by testing p
and proving the equivalence between the two.
Equations
Instances For
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
Instances For
Add some formatting to the information recorded by addInfo
.
Equations
Instances For
A configuration with all the trace options enabled, useful for debugging.
Equations
Instances For
Equations
Instances For
Equations
Equations
Increase the number of shrinking steps in a test result.
Equations
Instances For
Shrink a counter-example x
by using Shrinkable.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
.
Once a property fails to hold on an example, look for smaller counter-examples to show the user.
Equations
Instances For
Test a universal property by creating a sample of the right type and instantiating the bound variable with it.
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Count the number of times the test procedure gave up.
Equations
Instances For
Try n
times to find a counter-example for p
.
Equations
Instances For
Try to find a counter-example of p
.
Equations
Instances For
Run a test suite for p
in BaseIO
using the global RNG in stdGenRef
.
Equations
Instances For
Traverse the syntax of a proposition to find universal quantifiers
quantifiers and add NamedBinder
annotations next to them.
DecorationsOf 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
Instances For
In a goal of the shape ⊢ DecorationsOf p
, mk_decoration
examines
the syntax of p
and adds NamedBinder
around universal quantifications
to improve error messages. This tool can be used in the declaration of a
function as follows:
def foo (p : Prop) (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : ...
p
is the parameter given by the user, p'
is a definitionally equivalent
proposition where the quantifiers are annotated with NamedBinder
.
Equations
Instances For
Run a test suite for p
and throw an exception if p
does not hold.