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.

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

Equations

• Plausible.instInhabitedTestResult.default = Plausible.TestResult.gaveUp default

@[implicit_reducible]

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

Equations

• Plausible.instInhabitedTestResult = { default := Plausible.instInhabitedTestResult.default }

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.

def Plausible.instInhabitedConfiguration.default : Configuration

Equations

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

@[implicit_reducible]

instance Plausible.instInhabitedConfiguration : Inhabited Configuration

Equations

• Plausible.instInhabitedConfiguration = { default := Plausible.instInhabitedConfiguration.default }

@[implicit_reducible]

instance Plausible.instToExprConfiguration : Lean.ToExpr Configuration

Equations

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

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

Allow elaboration of Configuration arguments to tactics.

Equations

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

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

Equations

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

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

Equations

• Plausible.NamedBinder _n p = p

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

Equations

• (Plausible.TestResult.success (PSum.inl val)).toString = "success (no proof)"
• (Plausible.TestResult.success (PSum.inr val)).toString = "success (proof)"
• (Plausible.TestResult.gaveUp n).toString = toString "gave " ++ toString n ++ toString " times"
• (Plausible.TestResult.failure a counters a_1).toString = toString "failed " ++ toString counters

@[implicit_reducible]

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

Equations

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

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

Applicative combinator proof carrying test results.

Equations

• Plausible.TestResult.combine (PSum.inr f) (PSum.inr proof) = PSum.inr ⋯
• Plausible.TestResult.combine x✝¹ x✝ = PSum.inl ()

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.

Equations

• (Plausible.TestResult.failure h xs n).and x✝ = Plausible.TestResult.failure ⋯ xs n
• x✝.and (Plausible.TestResult.failure h xs n) = Plausible.TestResult.failure ⋯ xs n
• (Plausible.TestResult.success h1).and (Plausible.TestResult.success h2) = Plausible.TestResult.success (Plausible.TestResult.combine (Plausible.TestResult.combine (PSum.inr ⋯) h1) h2)
• (Plausible.TestResult.gaveUp n).and (Plausible.TestResult.gaveUp m) = Plausible.TestResult.gaveUp (n + m)
• (Plausible.TestResult.gaveUp n).and x✝ = Plausible.TestResult.gaveUp n
• x✝.and (Plausible.TestResult.gaveUp n) = Plausible.TestResult.gaveUp n

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.

Equations

• (Plausible.TestResult.failure h1 xs n).or (Plausible.TestResult.failure h2 ys m) = Plausible.TestResult.failure ⋯ (xs ++ ys) (n + m)
• (Plausible.TestResult.success h).or x✝ = Plausible.TestResult.success (Plausible.TestResult.combine (PSum.inr ⋯) h)
• x✝.or (Plausible.TestResult.success h) = Plausible.TestResult.success (Plausible.TestResult.combine (PSum.inr ⋯) h)
• (Plausible.TestResult.gaveUp n).or (Plausible.TestResult.gaveUp m) = Plausible.TestResult.gaveUp (n + m)
• (Plausible.TestResult.gaveUp n).or x✝ = Plausible.TestResult.gaveUp n
• x✝.or (Plausible.TestResult.gaveUp n) = Plausible.TestResult.gaveUp n

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.

Equations

• Plausible.TestResult.imp h (Plausible.TestResult.failure h2 xs n) p = Plausible.TestResult.failure ⋯ xs n
• Plausible.TestResult.imp h (Plausible.TestResult.success h2) p = Plausible.TestResult.success (Plausible.TestResult.combine p h2)
• Plausible.TestResult.imp h (Plausible.TestResult.gaveUp n) p = Plausible.TestResult.gaveUp n

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.

Equations

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

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.

Equations

• Plausible.TestResult.addInfo x h (Plausible.TestResult.failure h2 xs n) p = Plausible.TestResult.failure ⋯ (x :: xs) n
• Plausible.TestResult.addInfo x h r p = Plausible.TestResult.imp h r p

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.

Equations

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

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

Equations

• (Plausible.TestResult.failure h2 xs n).isFailure = true
• x✝.isFailure = false

def Plausible.Configuration.verbose : Configuration

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

Equations

• Plausible.Configuration.verbose = { traceDiscarded := true, traceSuccesses := true, traceShrink := true, traceShrinkCandidates := true }

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

Equations

• Plausible.Testable.runProp p = Plausible.Testable.run

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

Equations

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

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

A dbgTrace with special formatting

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[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))

Equations

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

@[implicit_reducible]

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

Equations

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

@[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))

Equations

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

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

Format the counter-examples found in a test failure.

Equations

• Plausible.Testable.formatFailure s xs n = "\n".intercalate ["\n===================", s, "\n".intercalate xs, toString "(" ++ toString n ++ toString " shrinks)", "-------------------"]

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

Increase the number of shrinking steps in a test result.

Equations

• Plausible.Testable.addShrinks n (Plausible.TestResult.failure h2 xs n_1) = Plausible.TestResult.failure h2 xs (n_1 + n)
• Plausible.Testable.addShrinks n x✝ = x✝

@[implicit_reducible]

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

Equations

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

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.

Equations

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

@[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.

Equations

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

@[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

Equations

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

@[implicit_reducible, instance 10000]

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

Equations

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

@[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)))

Equations

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

@[implicit_reducible, instance 100]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Plausible.True.printableProp : PrintableProp True

Equations

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

@[implicit_reducible]

instance Plausible.False.printableProp : PrintableProp False

Equations

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

@[implicit_reducible]

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Plausible.retry cmd 0 = pure (Plausible.TestResult.gaveUp 1)

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

Count the number of times the test procedure gave up.

Equations

• Plausible.giveUp x (Plausible.TestResult.gaveUp n) = Plausible.TestResult.gaveUp (n + x)
• Plausible.giveUp x x✝ = x✝

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.

Equations

• One or more equations did not get rendered due to their size.
• Plausible.Testable.runSuiteAux p cfg x✝ 0 = pure x✝

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

Try to find a counter-example of p.

Equations

• Plausible.Testable.runSuite p cfg = Plausible.Testable.runSuiteAux p cfg (Plausible.TestResult.gaveUp 0) cfg.numInst

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.

Equations

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

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.

Equations

• Plausible.Decorations.DecorationsOf _p = Prop

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.

Equations

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

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.

Equations

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

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

Equations

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