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 #

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.

source
instance Plausible.instInhabitedTestResult {a✝ : Prop} :
Inhabited (TestResult a✝)
Equations
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.

source
instance Plausible.instInhabitedConfiguration :
Inhabited Configuration
Equations
  • One or more equations did not get rendered due to their size.
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.
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.

Instances
    source
    @[instance 100]
    instance Plausible.instPrintableProp {p : Prop} :
    PrintableProp p
    Equations
    source
    class Plausible.Testable (p : Prop) :
    Type

    Testable p uses random examples to try to disprove p.

    Instances
      source
      def Plausible.NamedBinder (_n : String) (p : Prop) :
      Prop
      Equations
      source
      def Plausible.TestResult.toString {p : Prop} :
      TestResult p → String
      Equations
      source
      instance Plausible.TestResult.instToString {p : Prop} :
      ToString (TestResult p)
      Equations
      source
      def Plausible.TestResult.combine {p q : Prop} :
      Unit ⊕' (p → q) → Unit ⊕' p → Unit ⊕' q

      Applicative combinator proof carrying test results.

      Equations
      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
      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
      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
      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
      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
      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
      source
      def Plausible.TestResult.isFailure {p : Prop} :
      TestResult p → Bool
      Equations
      source
      def Plausible.Configuration.verbose :
      Configuration

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

      Equations
      source
      def Plausible.Testable.runProp (p : Prop) [Testable p] :
      Configuration → Bool → Gen (TestResult p)
      Equations
      source
      def Plausible.Testable.slimTrace {m : Type → Type u_1} [Pure m] (s : String) :
      m PUnit

      A dbgTrace with special formatting

      Equations
      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
      source
      def Plausible.Testable.addShrinks {p : Prop} (n : Nat) :
      TestResult p → TestResult p

      Increase the number of shrinking steps in a test result.

      Equations
      source
      instance Plausible.Testable.instInhabitedOptionTOfPure {α : Type u} {m : Type u → Type u_1} [Pure m] :
      Inhabited (OptionT m α)
      Equations
      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.
      source
      instance Plausible.Testable.varTestable {var : String} {α : Sort 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 (α → β))
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance 2000]
      instance Plausible.Testable.subtypeVarTestable {var : String} {α : Sort u_1} {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
      source
      instance Plausible.Ne.printableProp {α : Type u_1} [Repr α] {x y : α} :
      PrintableProp (x ≠ y)
      Equations
      source
      instance Plausible.LE.printableProp {α : Type u_1} [Repr α] [LE α] {x y : α} :
      PrintableProp (x ≤ y)
      Equations
      source
      instance Plausible.LT.printableProp {α : Type u_1} [Repr α] [LT α] {x y : α} :
      PrintableProp (x < y)
      Equations
      source
      instance Plausible.And.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] :
      PrintableProp (x ∧ y)
      Equations
      source
      instance Plausible.Or.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] :
      PrintableProp (x ∨ y)
      Equations
      source
      instance Plausible.Iff.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] :
      PrintableProp (x ↔ y)
      Equations
      source
      instance Plausible.Imp.printableProp {x y : Prop} [PrintableProp x] [PrintableProp y] :
      PrintableProp (x → y)
      Equations
      source
      instance Plausible.Not.printableProp {x : Prop} [PrintableProp x] :
      PrintableProp ¬x
      Equations
      source
      instance Plausible.True.printableProp :
      PrintableProp True
      Equations
      source
      instance Plausible.False.printableProp :
      PrintableProp False
      Equations
      source
      instance Plausible.Bool.printableProp {b : Bool} :
      PrintableProp (b = true)
      Equations
      source
      def Plausible.retry {p : Prop} (cmd : Rand (TestResult p)) :
      Nat → Rand (TestResult p)

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

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

      Count the number of times the test procedure gave up.

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

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

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

      Try to find a counter-example of p.

      Equations
      source
      def Plausible.Testable.checkIO (p : Prop) [Testable p] (cfg : Configuration := { }) :
      BaseIO (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.
      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
      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
      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.
      source
      def Plausible.«command#test_» :
      Lean.ParserDescr
      Equations