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

Tags

random testing

References

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

inductive SlimCheck.TestResult (p : Prop) : Type

Result of trying to disprove p The constructors are:

• success : (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 : ℕ → TestResult p give up when a well-formed example cannot be generated. gaveUp n tells us that n 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 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.

• success: {p : Prop} → Unit ⊕' p → SlimCheck.TestResult p
• gaveUp: {p : Prop} → ℕ → SlimCheck.TestResult p
• failure: {p : Prop} → ¬p → List String → ℕ → SlimCheck.TestResult p

instance SlimCheck.instInhabitedTestResult : {a : Prop} → Inhabited (SlimCheck.TestResult a)

Equations

• SlimCheck.instInhabitedTestResult = { default := SlimCheck.TestResult.success default }

structure SlimCheck.Configuration : Type

Configuration for testing a property.

• numInst : ℕ
• maxSize : ℕ
• numRetries : ℕ
• traceDiscarded : Bool
• traceSuccesses : Bool
• traceShrink : Bool
• traceShrinkCandidates : Bool
• randomSeed : Option ℕ
• quiet : Bool

instance SlimCheck.instInhabitedConfiguration : Inhabited SlimCheck.Configuration

Equations

• One or more equations did not get rendered due to their size.

instance SlimCheck.instToExprConfiguration : Lean.ToExpr SlimCheck.Configuration

Equations

• One or more equations did not get rendered due to their size.

def SlimCheck.elabConfig : Lean.Syntax → Lean.Elab.TermElabM SlimCheck.Configuration

Allow elaboration of Configuration arguments to tactics.

Equations

• One or more equations did not get rendered due to their size.

class SlimCheck.PrintableProp (p : Prop) : Type

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

@[instance 100]

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

Equations

• SlimCheck.instPrintableProp = { printProp := "⋯" }

class SlimCheck.Testable (p : Prop) : Type

Testable p uses random examples to try to disprove p.

• run : SlimCheck.Configuration → Bool → SlimCheck.Gen (SlimCheck.TestResult p)

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

Equations

• SlimCheck.NamedBinder _n p = p

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SlimCheck.TestResult.instToString = { toString := SlimCheck.TestResult.toString }

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

Applicative combinator proof carrying test results.

Equations

• SlimCheck.TestResult.combine x✝ x = match x✝, x with | PSum.inr f, PSum.inr proof => PSum.inr ⋯ | x, x_1 => PSum.inl ()

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• SlimCheck.TestResult.iff h r = SlimCheck.TestResult.imp ⋯ r (PSum.inr ⋯)

def SlimCheck.TestResult.addInfo {p : Prop} {q : Prop} (x : String) (h : q → p✝) (r : SlimCheck.TestResult p✝) (p : optParam (Unit ⊕' (p✝ → q)) (PSum.inl ())) : SlimCheck.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.

Equations

• SlimCheck.TestResult.addInfo x h r p = match r with | SlimCheck.TestResult.failure h2 xs n => SlimCheck.TestResult.failure ⋯ (x :: xs) n | x => SlimCheck.TestResult.imp h r p

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

Add some formatting to the information recorded by addInfo.

Equations

• SlimCheck.TestResult.addVarInfo var x h r p = SlimCheck.TestResult.addInfo (toString "" ++ toString var ++ toString " := " ++ toString (repr x) ++ toString "") h r p

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

Equations

• x.isFailure = match x with | SlimCheck.TestResult.failure a a_1 a_2 => true | x => false

def SlimCheck.Configuration.verbose : SlimCheck.Configuration

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 SlimCheck.Testable.runProp (p : Prop) [SlimCheck.Testable p] : SlimCheck.Configuration → Bool → SlimCheck.Gen (SlimCheck.TestResult p)

Equations

• SlimCheck.Testable.runProp p = SlimCheck.Testable.run

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

A dbgTrace with special formatting

Equations

• SlimCheck.Testable.slimTrace s = dbgTrace (toString "[SlimCheck: " ++ toString s ++ toString "]") fun (x : Unit) => pure ()

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

instance SlimCheck.Testable.factTestable {p : Prop} [SlimCheck.Testable p] : SlimCheck.Testable (Fact p)

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) }

def SlimCheck.Testable.formatFailure (s : String) (xs : List String) (n : ℕ) : String

Format the counter-examples found in a test failure.

Equations

• One or more equations did not get rendered due to their size.

def SlimCheck.Testable.addShrinks {p : Prop} (n : ℕ) : SlimCheck.TestResult p → SlimCheck.TestResult p

Increase the number of shrinking steps in a test result.

Equations

• SlimCheck.Testable.addShrinks n x = match x with | SlimCheck.TestResult.failure p_1 xs m => SlimCheck.TestResult.failure p_1 xs (m + n) | p => p

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

Equations

• SlimCheck.Testable.instInhabitedOptionTOfPure = { default := pure none }

partial def SlimCheck.Testable.minimizeAux {α : Sort u_1} [SlimCheck.SampleableExt α] {β : α → Prop} [(x : α) → SlimCheck.Testable (β x)] (cfg : SlimCheck.Configuration) (var : String) (x : SlimCheck.SampleableExt.proxy α) (n : ℕ) : OptionT SlimCheck.Gen ((x : SlimCheck.SampleableExt.proxy α) × SlimCheck.TestResult (β (SlimCheck.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 SlimCheck.Testable.minimize {α : Sort u_1} [SlimCheck.SampleableExt α] {β : α → Prop} [(x : α) → SlimCheck.Testable (β x)] (cfg : SlimCheck.Configuration) (var : String) (x : SlimCheck.SampleableExt.proxy α) (r : SlimCheck.TestResult (β (SlimCheck.SampleableExt.interp x))) : SlimCheck.Gen ((x : SlimCheck.SampleableExt.proxy α) × SlimCheck.TestResult (β (SlimCheck.SampleableExt.interp 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 SlimCheck.Testable.varTestable {var : String} {α : Sort u_1} [SlimCheck.SampleableExt α] {β : α → Prop} [(x : α) → SlimCheck.Testable (β x)] : SlimCheck.Testable (SlimCheck.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 SlimCheck.Testable.propVarTestable {var : String} {β : Prop → Prop} [(b : Bool) → SlimCheck.Testable (β (b = true))] : SlimCheck.Testable (SlimCheck.NamedBinder var (∀ (p : Prop), β p))

Test a universal property about propositions

Equations

• One or more equations did not get rendered due to their size.

@[instance 10000]

instance SlimCheck.Testable.unusedVarTestable {var : String} {α : Sort u_1} {β : Prop} [Nonempty α] [SlimCheck.Testable β] : SlimCheck.Testable (SlimCheck.NamedBinder var (α → β))

Equations

• One or more equations did not get rendered due to their size.

@[instance 2000]

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

Equations

• SlimCheck.Testable.subtypeVarTestable = { run := fun (cfg : SlimCheck.Configuration) (min : Bool) => do let r ← SlimCheck.Testable.run cfg min pure (SlimCheck.TestResult.iff ⋯ r) }

@[instance 100]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• SlimCheck.Eq.printableProp = { printProp := toString "" ++ toString (repr x) ++ toString " = " ++ toString (repr y) ++ toString "" }

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

Equations

• SlimCheck.Ne.printableProp = { printProp := toString "" ++ toString (repr x) ++ toString " ≠ " ++ toString (repr y) ++ toString "" }

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

Equations

• SlimCheck.LE.printableProp = { printProp := toString "" ++ toString (repr x) ++ toString " ≤ " ++ toString (repr y) ++ toString "" }

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

Equations

• SlimCheck.LT.printableProp = { printProp := toString "" ++ toString (repr x) ++ toString " < " ++ toString (repr y) ++ toString "" }

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

Equations

• SlimCheck.And.printableProp = { printProp := toString "" ++ toString (SlimCheck.printProp x) ++ toString " ∧ " ++ toString (SlimCheck.printProp y) ++ toString "" }

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

Equations

• SlimCheck.Or.printableProp = { printProp := toString "" ++ toString (SlimCheck.printProp x) ++ toString " ∨ " ++ toString (SlimCheck.printProp y) ++ toString "" }

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

Equations

• SlimCheck.Iff.printableProp = { printProp := toString "" ++ toString (SlimCheck.printProp x) ++ toString " ↔ " ++ toString (SlimCheck.printProp y) ++ toString "" }

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

Equations

• SlimCheck.Imp.printableProp = { printProp := toString "" ++ toString (SlimCheck.printProp x) ++ toString " → " ++ toString (SlimCheck.printProp y) ++ toString "" }

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

Equations

• SlimCheck.Not.printableProp = { printProp := toString "¬" ++ toString (SlimCheck.printProp x) ++ toString "" }

instance SlimCheck.True.printableProp : SlimCheck.PrintableProp True

Equations

• SlimCheck.True.printableProp = { printProp := "True" }

instance SlimCheck.False.printableProp : SlimCheck.PrintableProp False

Equations

• SlimCheck.False.printableProp = { printProp := "False" }

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

Equations

• SlimCheck.Bool.printableProp = { printProp := if b = true then "true" else "false" }

instance SlimCheck.Fact.printableProp {p : Prop} [SlimCheck.PrintableProp p] : SlimCheck.PrintableProp (Fact p)

Equations

• SlimCheck.Fact.printableProp = { printProp := SlimCheck.printProp p }

def SlimCheck.retry {p : Prop} (cmd : Rand (SlimCheck.TestResult p)) : ℕ → Rand (SlimCheck.TestResult 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)

def SlimCheck.giveUp {p : Prop} (x : ℕ) : SlimCheck.TestResult p → SlimCheck.TestResult p

Count the number of times the test procedure gave up.

Equations

• One or more equations did not get rendered due to their size.

def SlimCheck.Testable.runSuiteAux (p : Prop) [SlimCheck.Testable p] (cfg : SlimCheck.Configuration) : SlimCheck.TestResult p → ℕ → Rand (SlimCheck.TestResult p)

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

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

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

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

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.

partial def SlimCheck.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 SlimCheck.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.

Equations

• SlimCheck.Decorations.DecorationsOf _p = Prop

def SlimCheck.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.

Equations

• SlimCheck.Decorations.tacticMk_decorations = Lean.ParserDescr.node `SlimCheck.Decorations.tacticMk_decorations 1024 (Lean.ParserDescr.nonReservedSymbol "mk_decorations" false)

def SlimCheck.Testable.check (p : Prop) (cfg : optParam SlimCheck.Configuration { numInst := 100, maxSize := 100, numRetries := 10, traceDiscarded := false, traceSuccesses := false, traceShrink := false, traceShrinkCandidates := false, randomSeed := none, quiet := false }) (p' : autoParam (SlimCheck.Decorations.DecorationsOf p) _auto✝) [SlimCheck.Testable p'] : Lean.CoreM PUnit.{1}

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.

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

Equations

• SlimCheck.«command#test_» = Lean.ParserDescr.node `SlimCheck.command#test_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "#test ") (Lean.ParserDescr.cat `term 0))