Documentation

Plausible.Testable

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 #

References #

inductive Plausible.TestResult (p : Prop) :

Result of trying to disprove p

  • success: {p : Prop} → Unit ⊕' pPlausible.TestResult p

    Succeed when we find another example satisfying p. In success h, h is an optional proof of the proposition. Without the proof, all we know is that we found one example where p holds. With a proof, the one test was sufficient to prove that p holds and we do not need to keep finding examples.

  • gaveUp: {p : Prop} → NatPlausible.TestResult p

    Give up when a well-formed example cannot be generated. gaveUp n tells us that n invalid examples were tried.

  • failure: {p : Prop} → ¬pList StringNatPlausible.TestResult p

    A counter-example to p; the strings specify values for the relevant variables. failure h vs n also carries a proof that p 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
Equations

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.

  • randomSeed : Option Nat

    Hard code the seed to use for the RNG

  • quiet : Bool

    Disable output.

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.

Allow elaboration of Configuration arguments to tactics.

Equations
  • One or more equations did not get rendered due to their size.
@[instance 100]
Equations
  • Plausible.instPrintableProp = { printProp := "⋯" }
Equations
Equations
  • Plausible.TestResult.instToString = { toString := Plausible.TestResult.toString }
def Plausible.TestResult.combine {p q : Prop} :
Unit ⊕' (pq)Unit ⊕' pUnit ⊕' q

Applicative combinator proof carrying test results.

Equations

Test q by testing p and proving the equivalence between the two.

Equations
def Plausible.TestResult.addInfo {p q : Prop} (x : String) (h : qp) (r : Plausible.TestResult p) :

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
def Plausible.TestResult.addVarInfo {p q : Prop} {γ : Type u_1} [Repr γ] (var : String) (x : γ) (h : qp) (r : Plausible.TestResult p) :

Add some formatting to the information recorded by addInfo.

Equations

A configuration with all the trace options enabled, useful for debugging.

Equations
  • One or more equations did not get rendered due to their size.
def Plausible.Testable.slimTrace {m : TypeType u_1} [Pure m] (s : String) :

A dbgTrace with special formatting

Equations
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.
instance Plausible.Testable.decGuardTestable {p : Prop} {var : String} [Plausible.PrintableProp p] [Decidable p] {β : pProp} [(h : p) → Plausible.Testable (β h)] :
Plausible.Testable (Plausible.NamedBinder var (∀ (h : p), β h))
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.
@[instance 100]
Equations
  • One or more equations did not get rendered due to their size.

Format the counter-examples found in a test failure.

Equations

Increase the number of shrinking steps in a test result.

Equations
instance Plausible.Testable.instInhabitedOptionTOfPure {α : Type u} {m : Type u → Type u_1} [Pure m] :
Equations
  • Plausible.Testable.instInhabitedOptionTOfPure = { default := pure none }

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.
instance Plausible.Testable.varTestable {var : String} {α : Sort u_1} [Plausible.SampleableExt α] {β : αProp} [(x : α) → Plausible.Testable (β x)] :
Plausible.Testable (Plausible.NamedBinder var (∀ (x : α), β x))

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.
instance Plausible.Testable.propVarTestable {var : String} {β : PropProp} [(b : Bool) → Plausible.Testable (β (b = true))] :

Test a universal property about propositions

Equations
  • One or more equations did not get rendered due to their size.
@[instance 10000]
Equations
  • One or more equations did not get rendered due to their size.
@[instance 2000]
instance Plausible.Testable.subtypeVarTestable {var : String} {α : Sort u_1} {p β : αProp} [(x : α) → Plausible.PrintableProp (p x)] [(x : α) → Plausible.Testable (β x)] [Plausible.SampleableExt (Subtype p)] {var' : String} :
Plausible.Testable (Plausible.NamedBinder var (∀ (x : α), Plausible.NamedBinder var' (p xβ x)))
Equations
  • One or more equations did not get rendered due to their size.
@[instance 100]
Equations
  • One or more equations did not get rendered due to their size.
instance Plausible.Eq.printableProp {α : Type u_1} [Repr α] {x y : α} :
Equations
instance Plausible.Ne.printableProp {α : Type u_1} [Repr α] {x y : α} :
Equations
instance Plausible.LE.printableProp {α : Type u_1} [Repr α] [LE α] {x y : α} :
Equations
instance Plausible.LT.printableProp {α : Type u_1} [Repr α] [LT α] {x y : α} :
Equations
Equations
Equations
  • Plausible.Bool.printableProp = { printProp := if b = true then "true" else "false" }

Execute cmd and repeat every time the result is gaveUp (at most n times).

Equations

Try n times to find a counter-example for p.

Equations
def Plausible.Testable.runSuite (p : Prop) [Plausible.Testable p] (cfg : Plausible.Configuration := { numInst := 100, maxSize := 100, numRetries := 10, traceDiscarded := false, traceSuccesses := false, traceShrink := false, traceShrinkCandidates := false, randomSeed := none, quiet := false }) :

Try to find a counter-example of p.

Equations
def Plausible.Testable.checkIO (p : Prop) [Plausible.Testable p] (cfg : Plausible.Configuration := { numInst := 100, maxSize := 100, numRetries := 10, traceDiscarded := false, traceSuccesses := false, traceShrink := false, traceShrinkCandidates := false, randomSeed := none, quiet := false }) :

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.

Traverse the syntax of a proposition to find universal quantifiers quantifiers and add NamedBinder annotations next to them.

@[reducible, inline]

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

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
def Plausible.Testable.check (p : Prop) (cfg : Plausible.Configuration := { numInst := 100, maxSize := 100, numRetries := 10, traceDiscarded := false, traceSuccesses := false, traceShrink := false, traceShrinkCandidates := false, randomSeed := none, quiet := false }) (p' : Plausible.Decorations.DecorationsOf p := by mk_decorations) [Plausible.Testable p'] :

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.