# `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

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

Instances For

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

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

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

- Plausible.instInhabitedTestResult.default = Plausible.TestResult.gaveUp default

Instances For

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

Instances For

source
def Plausible.instInhabitedConfiguration.default :
Configuration
Equations

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

Instances For

source
instance Plausible.instInhabitedConfiguration :
Inhabited Configuration
Equations

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

source
instance Plausible.instToExprConfiguration :
Lean.ToExpr Configuration
Equations

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

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

Instances For

source
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

Instances

source
@[instance 100]
instance Plausible.instPrintableProp {p : Prop} :
PrintableProp p
Equations

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

source
class Plausible.Testable (p : Prop) :
Type

`Testable p` uses random examples to try to disprove `p`.

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

Instances

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

- Plausible.NamedBinder _n p = p

Instances For

source
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

Instances For

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

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

source
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 ()

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For

source
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 ⋯)

Instances For

source
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

Instances For

source
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

Instances For

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

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

Instances For

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

Instances For

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

- Plausible.Testable.runProp p = Plausible.Testable.run

Instances For

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

Instances For

source
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 ()

Instances For

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

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

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

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

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

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

source
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)", "-------------------"]

Instances For

source
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✝

Instances For

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

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

source
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`.

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

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
instance Plausible.True.printableProp :
PrintableProp True
Equations

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

source
instance Plausible.False.printableProp :
PrintableProp False
Equations

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

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

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

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

source
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.success (PSum.inl PUnit.unit)) = Plausible.TestResult.gaveUp x
- Plausible.giveUp x (Plausible.TestResult.success (PSum.inr p_1)) = Plausible.TestResult.success (PSum.inr p_1)
- Plausible.giveUp x (Plausible.TestResult.gaveUp n) = Plausible.TestResult.gaveUp (n + x)
- Plausible.giveUp x (Plausible.TestResult.failure h xs n) = Plausible.TestResult.failure h xs n

Instances For

source
partial 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`.

source
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.success (PSum.inl ())) cfg.numInst

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

Instances For

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

Instances For