HepLean Documentation

Plausible.Sampleable

`SampleableExt` Class #

This class permits the creation samples of a given type controlling the size of those values using the Gen monad.

`Shrinkable` Class #

This class helps minimize examples by creating smaller versions of given values.

When testing a proposition like ∀ n : Nat, Prime n → n ≤ 100, Plausible requires that Nat have an instance of SampleableExt and for Prime n to be decidable. Plausible will then use the instance of SampleableExt to generate small examples of Nat and progressively increase in size. For each example n, Prime n is tested. If it is false, the example will be rejected (not a test success nor a failure) and Plausible will move on to other examples. If Prime n is true, n ≤ 100 will be tested. If it is false, n is a counter-example of ∀ n : Nat, Prime n → n ≤ 100 and the test fails. If n ≤ 100 is true, the test passes and Plausible moves on to trying more examples.

Main definitions #

SampleableExt class
Shrinkable class

`SampleableExt` #

SampleableExt can be used in two ways. The first (and most common) is to simply generate values of a type directly using the Gen monad, if this is what you want to do then SampleableExt.mkSelfContained is the way to go.

Furthermore it makes it possible to express generators for types that do not lend themselves to introspection, such as Nat → Nat. If we test a quantification over functions the counter-examples cannot be shrunken or printed meaningfully. For that purpose, SampleableExt provides a proxy representation proxy that can be printed and shrunken as well as interpreted (using interp) as an object of the right type. If you are using it in the first way, this proxy type will simply be the type itself and the interp function id.

`Shrinkable` #

Given an example x : α, Shrinkable α gives us a way to shrink it and suggest simpler examples.

Shrinking #

Shrinking happens when Plausible finds a counter-example to a property. It is likely that the example will be more complicated than necessary so Plausible proceeds to shrink it as much as possible. Although equally valid, a smaller counter-example is easier for a user to understand and use.

The Shrinkable class, , has a shrink function so that we can use specialized knowledge while shrinking a value. It is not responsible for the whole shrinking process however. It only has to take one step in the shrinking process. Plausible will repeatedly call shrink until no more steps can be taken. Because shrink guarantees that the size of the candidates it produces is strictly smaller than the argument, we know that Plausible is guaranteed to terminate.

Tags #

random testing

References #

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

class Plausible.Shrinkable (α : Type u) :

Given an example x : α, Shrinkable α gives us a way to shrink it and suggest simpler examples.

shrink : α → List α

Instances

class Plausible.SampleableExt (α : Sort u) :

Sort (max u (v + 2))

SampleableExt can be used in two ways. The first (and most common) is to simply generate values of a type directly using the Gen monad, if this is what you want to do then SampleableExt.mkSelfContained is the way to go.

Furthermore it makes it possible to express generators for types that do not lend themselves to introspection, such as Nat → Nat. If we test a quantification over functions the counter-examples cannot be shrunken or printed meaningfully. For that purpose, SampleableExt provides a proxy representation proxy that can be printed and shrunken as well as interpreted (using interp) as an object of the right type.

proxy : Type v
proxyRepr : Repr (Plausible.SampleableExt.proxy α)
shrink : Plausible.Shrinkable (Plausible.SampleableExt.proxy α)
sample : Plausible.Gen (Plausible.SampleableExt.proxy α)
interp : Plausible.SampleableExt.proxy α → α

Instances

def Plausible.SampleableExt.mkSelfContained {α : Type u_1} [Repr α] [Plausible.Shrinkable α] (sample : Plausible.Gen α) :

Plausible.SampleableExt α

Use to generate instance whose purpose is to simply generate values of a type directly using the Gen monad

Equations

Plausible.SampleableExt.mkSelfContained sample = Plausible.SampleableExt.mk α sample id

Instances For

def Plausible.SampleableExt.interpSample (α : Type u) [Plausible.SampleableExt α] :

Plausible.Gen α

First samples a proxy value and interprets it. Especially useful if the proxy and target type are the same.

Equations

Plausible.SampleableExt.interpSample α = Plausible.SampleableExt.interp <$> Plausible.SampleableExt.sample

Instances For

instance Plausible.instShrinkableSum {α : Type u_1} {β : Type u_2} [Plausible.Shrinkable α] [Plausible.Shrinkable β] :

Plausible.Shrinkable (α ⊕ β)

Equations

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

instance Plausible.Unit.shrinkable :

Plausible.Shrinkable Unit

Equations

Plausible.Unit.shrinkable = { shrink := fun (x : Unit) => [] }

@[irreducible]

def Plausible.Nat.shrink (n : Nat) :

Nat.shrink' n creates a list of smaller natural numbers by successively dividing n by 2 . For example, Nat.shrink 5 = [2, 1, 0].

Equations

Plausible.Nat.shrink n = if h : 0 < n then let m := n / 2; m :: Plausible.Nat.shrink m else []

Instances For

instance Plausible.Nat.shrinkable :

Plausible.Shrinkable Nat

Equations

Plausible.Nat.shrinkable = { shrink := Plausible.Nat.shrink }

instance Plausible.Fin.shrinkable {n : Nat} :

Plausible.Shrinkable (Fin n.succ)

Equations

Plausible.Fin.shrinkable = { shrink := fun (m : Fin n.succ) => List.map Fin.ofNat (Plausible.Nat.shrink ↑m) }

instance Plausible.BitVec.shrinkable {n : Nat} :

Plausible.Shrinkable (BitVec n)

Equations

Plausible.BitVec.shrinkable = { shrink := fun (m : BitVec n) => List.map (BitVec.ofNat n) (Plausible.Nat.shrink m.toNat) }

instance Plausible.UInt8.shrinkable :

Plausible.Shrinkable UInt8

Equations

Plausible.UInt8.shrinkable = { shrink := fun (m : UInt8) => List.map UInt8.ofNat (Plausible.Nat.shrink m.toNat) }

instance Plausible.UInt16.shrinkable :

Plausible.Shrinkable UInt16

Equations

Plausible.UInt16.shrinkable = { shrink := fun (m : UInt16) => List.map UInt16.ofNat (Plausible.Nat.shrink m.toNat) }

instance Plausible.UInt32.shrinkable :

Plausible.Shrinkable UInt32

Equations

Plausible.UInt32.shrinkable = { shrink := fun (m : UInt32) => List.map UInt32.ofNat (Plausible.Nat.shrink m.toNat) }

instance Plausible.UInt64.shrinkable :

Plausible.Shrinkable UInt64

Equations

Plausible.UInt64.shrinkable = { shrink := fun (m : UInt64) => List.map UInt64.ofNat (Plausible.Nat.shrink m.toNat) }

instance Plausible.USize.shrinkable :

Plausible.Shrinkable USize

Equations

Plausible.USize.shrinkable = { shrink := fun (m : USize) => List.map USize.ofNat (Plausible.Nat.shrink m.toNat) }

instance Plausible.Int.shrinkable :

Plausible.Shrinkable Int

Int.shrinkable operates like Nat.shrinkable but also includes the negative variants.

Equations

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

instance Plausible.Bool.shrinkable :

Plausible.Shrinkable Bool

Equations

Plausible.Bool.shrinkable = { shrink := fun (x : Bool) => [] }

instance Plausible.Char.shrinkable :

Plausible.Shrinkable Char

Equations

Plausible.Char.shrinkable = { shrink := fun (x : Char) => [] }

instance Plausible.Option.shrinkable {α : Type u_1} [Plausible.Shrinkable α] :

Plausible.Shrinkable (Option α)

Equations

Plausible.Option.shrinkable = { shrink := fun (o : Option α) => match o with | some x => List.map some (Plausible.Shrinkable.shrink x) | none => [] }

instance Plausible.Prod.shrinkable {α : Type u_1} {β : Type u_2} [shrA : Plausible.Shrinkable α] [shrB : Plausible.Shrinkable β] :

Plausible.Shrinkable (α × β)

Equations

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

instance Plausible.Sigma.shrinkable {α : Type u_1} {β : Type u_2} [shrA : Plausible.Shrinkable α] [shrB : Plausible.Shrinkable β] :

Plausible.Shrinkable ((_ : α) × β)

Equations

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

instance Plausible.List.shrinkable {α : Type u_1} [Plausible.Shrinkable α] :

Plausible.Shrinkable (List α)

Shrink a list of a shrinkable type, either by discarding an element or shrinking an element.

Equations

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

instance Plausible.ULift.shrinkable {α : Type u_1} [Plausible.Shrinkable α] :

Plausible.Shrinkable (ULift α)

Equations

Plausible.ULift.shrinkable = { shrink := fun (u : ULift α) => List.map ULift.up (Plausible.Shrinkable.shrink u.down) }

instance Plausible.String.shrinkable :

Plausible.Shrinkable String

Equations

Plausible.String.shrinkable = { shrink := fun (s : String) => List.map String.mk (Plausible.Shrinkable.shrink s.toList) }

instance Plausible.Array.shrinkable {α : Type u_1} [Plausible.Shrinkable α] :

Plausible.Shrinkable (Array α)

Equations

Plausible.Array.shrinkable = { shrink := fun (xs : Array α) => List.map Array.mk (Plausible.Shrinkable.shrink xs.toList) }

instance Plausible.Subtype.shrinkable {α : Type u} {β : α → Prop} [Plausible.Shrinkable α] [(x : α) → Decidable (β x)] :

Plausible.Shrinkable { x : α // β x }

Equations

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

instance Plausible.Sum.SampleableExt {α : Type u_1} {β : Type u_2} [Plausible.SampleableExt α] [Plausible.SampleableExt β] :

Plausible.SampleableExt (α ⊕ β)

Equations

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

instance Plausible.Unit.sampleableExt :

Plausible.SampleableExt Unit

Equations

Plausible.Unit.sampleableExt = Plausible.SampleableExt.mkSelfContained (pure ())

instance Plausible.instSampleableExtSigma {α : Type u_1} {β : Type u_2} [Plausible.SampleableExt α] [Plausible.SampleableExt β] :

Plausible.SampleableExt ((_ : α) × β)

Equations

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

instance Plausible.Nat.sampleableExt :

Plausible.SampleableExt Nat

Equations

Plausible.Nat.sampleableExt = Plausible.SampleableExt.mkSelfContained do let __do_lift ← Plausible.Gen.getSize let a ← Plausible.Gen.choose Nat 0 __do_lift ⋯ pure a.val

instance Plausible.Fin.sampleableExt {n : Nat} :

Plausible.SampleableExt (Fin n.succ)

Equations

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

instance Plausible.BitVec.sampleableExt {n : Nat} :

Plausible.SampleableExt (BitVec n)

Equations

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

instance Plausible.UInt8.SampleableExt :

Plausible.SampleableExt UInt8

Equations

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

instance Plausible.UInt16.SampleableExt :

Plausible.SampleableExt UInt16

Equations

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

instance Plausible.UInt32.SampleableExt :

Plausible.SampleableExt UInt32

Equations

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

instance Plausible.UInt64.SampleableExt :

Plausible.SampleableExt UInt64

Equations

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

instance Plausible.USize.SampleableExt :

Plausible.SampleableExt USize

Equations

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

instance Plausible.Int.sampleableExt :

Plausible.SampleableExt Int

Equations

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

instance Plausible.Bool.sampleableExt :

Plausible.SampleableExt Bool

Equations

Plausible.Bool.sampleableExt = Plausible.SampleableExt.mkSelfContained (Plausible.Gen.chooseAny Bool)

def Plausible.Char.sampleable (length : Nat) (chars : List Char) (pos : 0 < chars.length) :

Plausible.SampleableExt Char

This can be specialized into customized SampleableExt Char instances. The resulting instance has 1 / length chances of making an unrestricted choice of characters and it otherwise chooses a character from chars with uniform probabilities.

Equations

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

Instances For

instance Plausible.Char.sampleableDefault :

Plausible.SampleableExt Char

Equations

Plausible.Char.sampleableDefault = Plausible.Char.sampleable 3 " 0123abcABC:,;`\\/".toList Plausible.Char.sampleableDefault.proof_1

instance Plausible.Option.sampleableExt {α : Type u_1} [Plausible.SampleableExt α] :

Plausible.SampleableExt (Option α)

Equations

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

instance Plausible.Prod.sampleableExt {α : Type u} {β : Type v} [Plausible.SampleableExt α] [Plausible.SampleableExt β] :

Plausible.SampleableExt (α × β)

Equations

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

instance Plausible.Prop.sampleableExt :

Plausible.SampleableExt Prop

Equations

Plausible.Prop.sampleableExt = Plausible.SampleableExt.mk Bool (Plausible.SampleableExt.interpSample Bool) Coe.coe

instance Plausible.List.sampleableExt {α : Type u_1} [Plausible.SampleableExt α] :

Plausible.SampleableExt (List α)

Equations

Plausible.List.sampleableExt = Plausible.SampleableExt.mk (List (Plausible.SampleableExt.proxy α)) Plausible.SampleableExt.sample.listOf (List.map Plausible.SampleableExt.interp)

instance Plausible.ULift.sampleableExt {α : Type u_1} [Plausible.SampleableExt α] :

Plausible.SampleableExt (ULift α)

Equations

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

instance Plausible.String.sampleableExt :

Plausible.SampleableExt String

Equations

Plausible.String.sampleableExt = Plausible.SampleableExt.mkSelfContained do let __do_lift ← Plausible.SampleableExt.sample.listOf pure { data := __do_lift }

instance Plausible.Array.sampleableExt {α : Type u_1} [Plausible.SampleableExt α] :

Plausible.SampleableExt (Array α)

Equations

Plausible.Array.sampleableExt = Plausible.SampleableExt.mk (Array (Plausible.SampleableExt.proxy α)) Plausible.SampleableExt.sample.arrayOf (Array.map Plausible.SampleableExt.interp)

def Plausible.NoShrink (α : Type u) :

An annotation for values that should never get shrunk.

Equations

Plausible.NoShrink α = α

Instances For

def Plausible.NoShrink.mk {α : Type u_1} (x : α) :

Plausible.NoShrink α

Equations

Plausible.NoShrink.mk x = x

Instances For

def Plausible.NoShrink.get {α : Type u_1} (x : Plausible.NoShrink α) :

α

Equations

x.get = x

Instances For

instance Plausible.NoShrink.inhabited {α : Type u_1} [inst : Inhabited α] :

Inhabited (Plausible.NoShrink α)

Equations

Plausible.NoShrink.inhabited = inst

instance Plausible.NoShrink.repr {α : Type u_1} [inst : Repr α] :

Repr (Plausible.NoShrink α)

Equations

Plausible.NoShrink.repr = inst

instance Plausible.NoShrink.shrinkable {α : Type u_1} :

Plausible.Shrinkable (Plausible.NoShrink α)

Equations

Plausible.NoShrink.shrinkable = { shrink := fun (x : Plausible.NoShrink α) => [] }

instance Plausible.NoShrink.sampleableExt {α : Type u_1} [Plausible.SampleableExt α] [Repr α] :

Plausible.SampleableExt (Plausible.NoShrink α)

Equations

Plausible.NoShrink.sampleableExt = Plausible.SampleableExt.mkSelfContained ((Plausible.NoShrink.mk ∘ Plausible.SampleableExt.interp) <$> Plausible.SampleableExt.sample)

def Plausible.printSamples {t : Type u} [Repr t] (g : Plausible.Gen t) :

Print (at most) 10 samples of a given type to stdout for debugging.

Equations

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

Instances For

def Plausible.«command#sample_» :

Lean.ParserDescr

#sample type, where type has an instance of SampleableExt, prints ten random values of type type using an increasing size parameter.

#sample Nat
-- prints
-- 0
-- 0
-- 2
-- 24
-- 64
-- 76
-- 5
-- 132
-- 8
-- 449
-- or some other sequence of numbers

#sample List Int
-- prints
-- []
-- [1, 1]
-- [-7, 9, -6]
-- [36]
-- [-500, 105, 260]
-- [-290]
-- [17, 156]
-- [-2364, -7599, 661, -2411, -3576, 5517, -3823, -968]
-- [-643]
-- [11892, 16329, -15095, -15461]
-- or whatever

Equations

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

Instances For