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 SlimCheck
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 SlimCheck
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
SlimCheck
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 : ℕ
y : ℕ
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,h⟩ ↦
let proxy := Shrinkable.shrink (x, y - x)
proxy.map (fun ⟨⟨fst, snd⟩, ha⟩ ↦ ⟨⟨fst, fst + snd, sorry⟩, sorry⟩)
instance : SampleableExt MyType :=
SampleableExt.mkSelfContained do
let x ← SampleableExt.interpSample Nat
let xyDiff ← SampleableExt.interpSample Nat
pure <| ⟨x, x + xyDiff, sorry⟩
Again, we take advantage of the fact that other types have useful
Shrinkable
implementations, in this case Prod
. Note that the second
proof is heavily based on WellFoundedRelation
since it's used for termination so
the first step you want to take is almost always to simp_wf
in order to
get through the WellFoundedRelation
.
Main definitions #
Testable
classTestable.check
: a way to test a proposition using random examples
Tags #
random testing
References #
Result of trying to disprove p
The constructors are:
success : (Unit ⊕' p) → TestResult p
succeed when we find another example satisfyingp
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 : ℕ → TestResult p
give up when a well-formed example cannot be generated.gaveUp n
tells us thatn
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) → ℕ → TestResult p
a counter-example top
; 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.
- success: {p : Prop} → Unit ⊕' p → SlimCheck.TestResult p
- gaveUp: {p : Prop} → ℕ → SlimCheck.TestResult p
- failure: {p : Prop} → ¬p → List String → ℕ → SlimCheck.TestResult p
Instances For
Equations
- SlimCheck.instInhabitedTestResult = { default := SlimCheck.TestResult.success default }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Allow elaboration of Configuration
arguments to tactics.
Equations
- One or more equations did not get rendered due to their size.
Instances For
PrintableProp p
allows one to print a proposition so that
SlimCheck
can indicate how values relate to each other.
It's basically a poor man's delaborator.
- printProp : String
Instances
Equations
- SlimCheck.instPrintableProp = { printProp := "⋯" }
Testable p
uses random examples to try to disprove p
.
- run : SlimCheck.Configuration → Bool → SlimCheck.Gen (SlimCheck.TestResult p)
Instances
Equations
- SlimCheck.NamedBinder _n p = p
Instances For
Equations
- (SlimCheck.TestResult.success (PSum.inl val)).toString = "success (no proof)"
- (SlimCheck.TestResult.success (PSum.inr val)).toString = "success (proof)"
- (SlimCheck.TestResult.gaveUp n).toString = toString "gave " ++ toString n ++ toString " times"
- (SlimCheck.TestResult.failure a counters a_1).toString = toString "failed " ++ toString counters ++ toString ""
Instances For
Equations
- SlimCheck.TestResult.instToString = { toString := SlimCheck.TestResult.toString }
Combine the test result for properties p
and q
to create a test for their conjunction.
Equations
- (SlimCheck.TestResult.failure h xs n).and x = SlimCheck.TestResult.failure ⋯ xs n
- x.and (SlimCheck.TestResult.failure h xs n) = SlimCheck.TestResult.failure ⋯ xs n
- (SlimCheck.TestResult.success h1).and (SlimCheck.TestResult.success h2) = SlimCheck.TestResult.success (SlimCheck.TestResult.combine (SlimCheck.TestResult.combine (PSum.inr ⋯) h1) h2)
- (SlimCheck.TestResult.gaveUp n).and (SlimCheck.TestResult.gaveUp m) = SlimCheck.TestResult.gaveUp (n + m)
- (SlimCheck.TestResult.gaveUp n).and x = SlimCheck.TestResult.gaveUp n
- x.and (SlimCheck.TestResult.gaveUp n) = SlimCheck.TestResult.gaveUp n
Instances For
Combine the test result for properties p
and q
to create a test for their disjunction.
Equations
- (SlimCheck.TestResult.failure h1 xs n).or (SlimCheck.TestResult.failure h2 ys m) = SlimCheck.TestResult.failure ⋯ (xs ++ ys) (n + m)
- (SlimCheck.TestResult.success h).or x = SlimCheck.TestResult.success (SlimCheck.TestResult.combine (PSum.inr ⋯) h)
- x.or (SlimCheck.TestResult.success h) = SlimCheck.TestResult.success (SlimCheck.TestResult.combine (PSum.inr ⋯) h)
- (SlimCheck.TestResult.gaveUp n).or (SlimCheck.TestResult.gaveUp m) = SlimCheck.TestResult.gaveUp (n + m)
- (SlimCheck.TestResult.gaveUp n).or x = SlimCheck.TestResult.gaveUp n
- x.or (SlimCheck.TestResult.gaveUp n) = SlimCheck.TestResult.gaveUp n
Instances For
If q → p
, then ¬ p → ¬ q
which means that testing p
can allow us
to find counter-examples to q
.
Equations
- SlimCheck.TestResult.imp h (SlimCheck.TestResult.failure h2 xs n) p = SlimCheck.TestResult.failure ⋯ xs n
- SlimCheck.TestResult.imp h (SlimCheck.TestResult.success h2) p = SlimCheck.TestResult.success (SlimCheck.TestResult.combine p h2)
- SlimCheck.TestResult.imp h (SlimCheck.TestResult.gaveUp n) p = SlimCheck.TestResult.gaveUp n
Instances For
Test q
by testing p
and proving the equivalence between the two.
Equations
- SlimCheck.TestResult.iff h r = SlimCheck.TestResult.imp ⋯ r (PSum.inr ⋯)
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
- SlimCheck.TestResult.addInfo x h (SlimCheck.TestResult.failure h2 xs n) p = SlimCheck.TestResult.failure ⋯ (x :: xs) n
- SlimCheck.TestResult.addInfo x h r p = SlimCheck.TestResult.imp h r p
Instances For
Equations
- (SlimCheck.TestResult.failure h2 xs n).isFailure = true
- x.isFailure = false
Instances For
A configuration with all the trace options enabled, useful for debugging.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- SlimCheck.Testable.runProp p = SlimCheck.Testable.run
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- SlimCheck.Testable.factTestable = { run := fun (cfg : SlimCheck.Configuration) (min : Bool) => do let h ← SlimCheck.Testable.runProp p cfg min pure (SlimCheck.TestResult.iff ⋯ h) }
Format the counter-examples found in a test failure.
Equations
Instances For
Increase the number of shrinking steps in a test result.
Equations
- SlimCheck.Testable.addShrinks n (SlimCheck.TestResult.failure h2 xs n_1) = SlimCheck.TestResult.failure h2 xs (n_1 + n)
- SlimCheck.Testable.addShrinks n x = x
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
- One or more equations did not get rendered due to their size.
Instances For
Test a universal property by creating a sample of the right type and instantiating the bound variable with it.
Equations
- One or more equations did not get rendered due to their size.
Test a universal property about propositions
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- SlimCheck.Testable.subtypeVarTestable = { run := fun (cfg : SlimCheck.Configuration) (min : Bool) => do let r ← SlimCheck.Testable.run cfg min pure (SlimCheck.TestResult.iff ⋯ r) }
Equations
- One or more equations did not get rendered due to their size.
Equations
- SlimCheck.True.printableProp = { printProp := "True" }
Equations
- SlimCheck.False.printableProp = { printProp := "False" }
Equations
- SlimCheck.Fact.printableProp = { printProp := SlimCheck.printProp p }
Execute cmd
and repeat every time the result is gave_up
(at most n
times).
Equations
- One or more equations did not get rendered due to their size.
- SlimCheck.retry cmd 0 = pure (SlimCheck.TestResult.gaveUp 1)
Instances For
Count the number of times the test procedure gave up.
Equations
- SlimCheck.giveUp x (SlimCheck.TestResult.success (PSum.inl PUnit.unit)) = SlimCheck.TestResult.gaveUp x
- SlimCheck.giveUp x (SlimCheck.TestResult.success (PSum.inr p_1)) = SlimCheck.TestResult.success (PSum.inr p_1)
- SlimCheck.giveUp x (SlimCheck.TestResult.gaveUp n) = SlimCheck.TestResult.gaveUp (n + x)
- SlimCheck.giveUp x (SlimCheck.TestResult.failure h xs n) = SlimCheck.TestResult.failure h xs n
Instances For
Try n
times to find a counter-example for p
.
Equations
- One or more equations did not get rendered due to their size.
- SlimCheck.Testable.runSuiteAux p cfg x 0 = pure x
Instances For
Try to find a counter-example of p
.
Equations
- SlimCheck.Testable.runSuite p cfg = SlimCheck.Testable.runSuiteAux p cfg (SlimCheck.TestResult.success (PSum.inl ())) cfg.numInst
Instances For
Run a test suite for p
in BaseIO
using the global RNG in stdGenRef
.
Equations
- One or more equations did not get rendered due to their size.
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
- SlimCheck.Decorations.tacticMk_decorations = Lean.ParserDescr.node `SlimCheck.Decorations.tacticMk_decorations 1024 (Lean.ParserDescr.nonReservedSymbol "mk_decorations" false)
Instances For
Run a test suite for p
and throw an exception if p
does not hold.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- SlimCheck.«command#test_» = Lean.ParserDescr.node `SlimCheck.command#test_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#test ") (Lean.ParserDescr.cat `term 0))