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 class
• Testable.check: a way to test a proposition using random examples

References

• https://hackage.haskell.org/package/QuickCheck

inductive Plausible.TestResult (p : Prop) : Type

Result of trying to disprove p

• success {p : Prop} : Unit ⊕' p → 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} : Nat → 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} : ¬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 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.

@[implicit_reducible]

instance Plausible.instInhabitedTestResult {a✝ : Prop} : Inhabited (TestResult a✝)

def Plausible.instInhabitedTestResult.default {a✝ : Prop} : TestResult a✝

structure Plausible.Configuration : Type

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.

• sorryIfNoTestable : Bool

  If true, when the Testable instance required to begin testing cannot be synthesized, silently admit the goal with sorry instead of throwing an error.

def Plausible.instInhabitedConfiguration.default : Configuration

@[implicit_reducible]

instance Plausible.instInhabitedConfiguration : Inhabited Configuration

@[implicit_reducible]

instance Plausible.instToExprConfiguration : Lean.ToExpr Configuration

def Plausible.elabConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Configuration

Allow elaboration of Configuration arguments to tactics.

class Plausible.PrintableProp (p : Prop) : Type

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

@[implicit_reducible, instance 100]

instance Plausible.instPrintableProp {p : Prop} : PrintableProp p

class Plausible.Testable (p : Prop) : Type

Testable p uses random examples to try to disprove p.

• run (cfg : Configuration) (minimize : Bool) : Gen (TestResult p)

def Plausible.NamedBinder (_n : String) (p : Prop) : Prop

def Plausible.TestResult.toString {p : Prop} : TestResult p → String

@[implicit_reducible]

instance Plausible.TestResult.instToString {p : Prop} : ToString (TestResult p)

def Plausible.TestResult.combine {p q : Prop} : Unit ⊕' (p → q) → Unit ⊕' p → Unit ⊕' q

Applicative combinator proof carrying test results.

def Plausible.TestResult.and {p q : Prop} : TestResult p → TestResult q → TestResult (p ∧ q)

Combine the test result for properties p and q to create a test for their conjunction.

def Plausible.TestResult.or {p q : Prop} : TestResult p → TestResult q → TestResult (p ∨ q)

Combine the test result for properties p and q to create a test for their disjunction.

def Plausible.TestResult.imp {p q : Prop} (h : q → p) (r : TestResult p) : optParam (Unit ⊕' (p → q)) (PSum.inl ()) → TestResult q

If q → p, then ¬ p → ¬ q which means that testing p can allow us to find counter-examples to q.

def Plausible.TestResult.iff {p q : Prop} (h : q ↔ p) (r : TestResult p) : TestResult q

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

def Plausible.TestResult.addInfo {p q : Prop} (x : String) (h : q → p) (r : TestResult p) : optParam (Unit ⊕' (p → q)) (PSum.inl ()) → TestResult q

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.

def Plausible.TestResult.addVarInfo {p q : Prop} {γ : Type u_1} [Repr γ] (var : String) (x : γ) (h : q → p) (r : TestResult p) : optParam (Unit ⊕' (p → q)) (PSum.inl ()) → TestResult q

Add some formatting to the information recorded by addInfo.

def Plausible.TestResult.isFailure {p : Prop} : TestResult p → Bool

def Plausible.Configuration.verbose : Configuration

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

def Plausible.Testable.runProp (p : Prop) [Testable p] : Configuration → Bool → Gen (TestResult p)

def Plausible.Testable.runPropE (p : Prop) [Testable p] (cfg : Configuration) (min : Bool) : Gen (TestResult p)

def Plausible.Testable.slimTrace {m : Type → Type u_1} [Pure m] (s : String) : m PUnit

A dbgTrace with special formatting

@[implicit_reducible]

instance Plausible.Testable.andTestable {p q : Prop} [Testable p] [Testable q] : Testable (p ∧ q)

@[implicit_reducible]

instance Plausible.Testable.orTestable {p q : Prop} [Testable p] [Testable q] : Testable (p ∨ q)

@[implicit_reducible]

instance Plausible.Testable.iffTestable {p q : Prop} [Testable (p ∧ q ∨ ¬p ∧ ¬q)] : Testable (p ↔ q)

@[implicit_reducible]

instance Plausible.Testable.decGuardTestable {p : Prop} {var : String} [PrintableProp p] [Decidable p] {β : p → Prop} [(h : p) → Testable (β h)] : Testable (NamedBinder var (∀ (h : p), β h))

@[implicit_reducible]

instance Plausible.Testable.forallTypesTestable {var : String} {f : Type → Prop} [Testable (f Int)] : Testable (NamedBinder var (∀ (x : Type), f x))

@[implicit_reducible, instance 100]

instance Plausible.Testable.forallTypesULiftTestable {var : String} {f : Type u → Prop} [Testable (f (ULift Int))] : Testable (NamedBinder var (∀ (x : Type u), f x))

def Plausible.Testable.formatFailure (s : String) (xs : List String) (n : Nat) : String

Format the counter-examples found in a test failure.

def Plausible.Testable.addShrinks {p : Prop} (n : Nat) : TestResult p → TestResult p

Increase the number of shrinking steps in a test result.

@[implicit_reducible]

instance Plausible.Testable.instInhabitedOptionTOfPure {α : Type u} {m : Type u → Type u_1} [Pure m] : Inhabited (OptionT m α)

partial def Plausible.Testable.minimizeAux {α : Sort u_1} [SampleableExt α] {β : α → Prop} [(x : α) → Testable (β x)] (cfg : Configuration) (var : String) (x : SampleableExt.proxy α) (n : Nat) : OptionT Gen ((x : SampleableExt.proxy α) × TestResult (β (SampleableExt.interp x)))

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.

def Plausible.Testable.minimize {α : Sort u_1} [SampleableExt α] {β : α → Prop} [(x : α) → Testable (β x)] (cfg : Configuration) (var : String) (x : SampleableExt.proxy α) (r : TestResult (β (SampleableExt.interp x))) : Gen ((x : SampleableExt.proxy α) × TestResult (β (SampleableExt.interp x)))

Once a property fails to hold on an example, look for smaller counter-examples to show the user.

@[implicit_reducible]

instance Plausible.Testable.varTestable {var : String} {α : Type u_1} [SampleableExt α] {β : α → Prop} [(x : α) → Testable (β x)] : Testable (NamedBinder var (∀ (x : α), β x))

Test a universal property by creating a sample of the right type and instantiating the bound variable with it.

@[implicit_reducible]

instance Plausible.Testable.propVarTestable {var : String} {β : Prop → Prop} [(b : Bool) → Testable (β (b = true))] : Testable (NamedBinder var (∀ (p : Prop), β p))

Test a universal property about propositions

@[implicit_reducible, instance 10000]

instance Plausible.Testable.unusedVarTestable {var : String} {α : Sort u_1} {β : Prop} [Nonempty α] [Testable β] : Testable (NamedBinder var (∀ (a : α), β))

@[implicit_reducible, instance 2000]

instance Plausible.Testable.subtypeVarTestable {var : String} {α : Type u} {p β : α → Prop} [(x : α) → PrintableProp (p x)] [(x : α) → Testable (β x)] [SampleableExt (Subtype p)] {var' : String} : Testable (NamedBinder var (∀ (x : α), NamedBinder var' (p x → β x)))

@[implicit_reducible, instance 100]

instance Plausible.Testable.decidableTestable {p : Prop} [PrintableProp p] [Decidable p] : Testable p

@[implicit_reducible]

instance Plausible.Eq.printableProp {α : Type u_1} [Repr α] {x y : α} : PrintableProp (x = y)

@[implicit_reducible]

instance Plausible.Ne.printableProp {α : Type u_1} [Repr α] {x y : α} : PrintableProp (x ≠ y)

@[implicit_reducible]

instance Plausible.LE.printableProp {α : Type u_1} [Repr α] [LE α] {x y : α} : PrintableProp (x ≤ y)

@[implicit_reducible]

instance Plausible.LT.printableProp {α : Type u_1} [Repr α] [LT α] {x y : α} : PrintableProp (x < y)

@[implicit_reducible]

instance Plausible.And.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] : PrintableProp (x ∧ y)

@[implicit_reducible]

instance Plausible.Or.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] : PrintableProp (x ∨ y)

@[implicit_reducible]

instance Plausible.Iff.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] : PrintableProp (x ↔ y)

@[implicit_reducible]

instance Plausible.Imp.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] : PrintableProp (x → y)

@[implicit_reducible]

instance Plausible.Not.printableProp {x : Prop} [PrintableProp x] : PrintableProp ¬x

@[implicit_reducible]

instance Plausible.True.printableProp : PrintableProp True

@[implicit_reducible]

instance Plausible.False.printableProp : PrintableProp False

@[implicit_reducible]

instance Plausible.Bool.printableProp {b : Bool} : PrintableProp (b = true)

def Plausible.retry {p : Prop} (cmd : Gen (TestResult p)) : Nat → Gen (TestResult p)

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

def Plausible.giveUp {p : Prop} (x : Nat) : TestResult p → TestResult p

Count the number of times the test procedure gave up.

def Plausible.Testable.runSuiteAux (p : Prop) [Testable p] (cfg : Configuration) : TestResult p → Nat → Gen (TestResult p)

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

def Plausible.Testable.runSuite (p : Prop) [Testable p] (cfg : Configuration := { }) : Gen (TestResult p)

Try to find a counter-example of p.

def Plausible.Testable.checkIO (p : Prop) [Testable p] (cfg : Configuration := { }) : IO (TestResult p)

Run a test suite for p in IO using the global RNG in stdGenRef.

partial def Plausible.Decorations.addDecorations (e : Lean.Expr) : Lean.MetaM Lean.Expr

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

@[reducible, inline]

abbrev Plausible.Decorations.DecorationsOf (_p : Prop) : Type

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.

def Plausible.Decorations.tacticMk_decorations : Lean.ParserDescr

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.

def Plausible.Testable.check (p : Prop) (cfg : Configuration := { }) (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : Lean.CoreM PUnit

Run a test suite for p and throw an exception if p does not hold.

def Plausible.«command#test_» : Lean.ParserDescr