Gen Monad

This monad is used to formulate randomized computations with a parameter to specify the desired size of the result.

Main definitions

• Gen monad

References

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

inductive Plausible.GenError : Type

Error thrown on generation failure, e.g. because you've run out of resources.

• genError : String → GenError

@[implicit_reducible]

instance Plausible.instInhabitedGenError : Inhabited GenError

@[implicit_reducible]

instance Plausible.instReprGenError : Repr GenError

def Plausible.instReprGenError.repr : GenError → Nat → Std.Format

@[implicit_reducible]

instance Plausible.instBEqGenError : BEq GenError

def Plausible.instBEqGenError.beq : GenError → GenError → Bool

def Plausible.Gen.genericFailure : GenError

Order-theoretic instances on Except GenError

These exist so that Gen (and definitions in it) can be the target of partial_fixpoint. We give Except GenError α the flat order with Except.error default as the bottom element, representing a non-terminating / undefined computation. Any other .error e is then incomparable with .ok _, which is why the bind_mono_* proofs only need the bot and refl cases.

@[implicit_reducible]

instance Plausible.instPartialOrderExceptGenError {α : Type u_1} : Lean.Order.PartialOrder (Except GenError α)

@[implicit_reducible]

instance Plausible.instCCPOExceptGenError {α : Type u_1} : Lean.Order.CCPO (Except GenError α)

instance Plausible.instMonoBindExceptGenError : Lean.Order.MonoBind (Except GenError)

@[reducible, inline]

abbrev Plausible.Gen (α : Type u) : Type u

Monad to generate random examples to test properties with. It has a Nat parameter so that the caller can decide on the size of the examples. It allows failure to generate via the Except monad

@[implicit_reducible]

instance Plausible.instMonadLiftGen {m : Type u_1 → Type u_2} [MonadLiftT m (ReaderT (ULift Nat) (Except GenError))] : MonadLiftT (RandGT StdGen m) Gen

@[implicit_reducible]

instance Plausible.instMonadErrorGen : MonadExcept GenError Gen

def Plausible.Gen.genFailure (e : GenError) : IO.Error

@[inline]

def Plausible.Gen.up {α : Type u} (x : Gen α) : Gen (ULift α)

@[inline]

def Plausible.Gen.down {α : Type u_1} (x : Gen (ULift α)) : Gen α

def Plausible.Gen.chooseAny (α : Type u) [Random Id α] : Gen α

Lift Random.random to the Gen monad.

def Plausible.Gen.choose (α : Type u) [LE α] [BoundedRandom Id α] (lo hi : α) (h : lo ≤ hi) : Gen { a : α // lo ≤ a ∧ a ≤ hi }

Lift BoundedRandom.randomR to the Gen monad.

def Plausible.Gen.chooseNatLt (lo hi : Nat) (h : lo < hi) : Gen { a : Nat // lo ≤ a ∧ a < hi }

Generate a Nat example between lo and hi (exclusively).

def Plausible.Gen.getSize : Gen Nat

Get access to the size parameter of the Gen monad.

def Plausible.Gen.resize {α : Type u_1} (f : Nat → Nat) (x : Gen α) : Gen α

Apply a function to the size parameter.

def Plausible.Gen.chooseNat : Gen Nat

Choose a Nat between 0 and getSize.

The following section defines various combinators for generators, which are used in the body of derived generators (for derived Arbitrary instances).

The code for these combinators closely mirrors those used in Rocq/Coq QuickChick (see link in the References section below).

References

• https://github.com/QuickChick/QuickChick/blob/master/src/Generators.v

def Plausible.Gen.outOfFuel : GenError

Raised when a fueled generator fails due to insufficient fuel.

def Plausible.Gen.pick {α : Type u_1} (default : Gen α) (xs : List (Nat × Gen α)) (n : Nat) : Nat × Gen α

pick default xs n chooses a weight & a generator (k, gen) from the list xs such that n < k. If xs is empty, the default generator with weight 0 is returned.

@[implicit_reducible]

instance Plausible.Gen.inhabitedGen {α : Type u_1} : Inhabited (Gen α)

def Plausible.Gen.backtrack {α : Type u_1} (gs : List (Nat × Gen α)) : Gen α

Tries all generators until one returns a Some value or all the generators failed once with None. The generators are picked at random according to their weights (like frequency in Haskell QuickCheck), and each generator is run at most once.

def Plausible.Gen.oneOfWithDefault {α : Type} (default : Gen α) (gs : List (Gen α)) : Gen α

Picks one of the generators in gs at random, returning the default generator if gs is empty.

(This is a more ergonomic version of Plausible's Gen.oneOf which doesn't require the caller to supply a proof that the list index is in bounds.)

def Plausible.Gen.frequency {α : Type} (default : Gen α) (gs : List (Nat × Gen α)) : Gen α

frequency picks a generator from the list gs according to the weights in gs. If gs is empty, the default generator is returned.

def Plausible.Gen.sized {α : Type} (f : Nat → Gen α) : Gen α

sized f constructs a generator that depends on its size parameter

def Plausible.Gen.arrayOf {α : Type u} (x : Gen α) : Gen (Array α)

Create an Array of examples using x. The size is controlled by the size parameter of Gen.

def Plausible.Gen.listOf {α : Type u} (x : Gen α) : Gen (List α)

Create a List of examples using x. The size is controlled by the size parameter of Gen.

def Plausible.Gen.oneOf {α : Type u} (xs : Array (Gen α)) (pos : 0 < xs.size := by decide) : Gen α

Given a list of example generators, choose one to create an example.

def Plausible.Gen.elements {α : Type u} (xs : List α) (pos : 0 < xs.length) : Gen α

Given a list of examples, choose one to create an example.

def Plausible.Gen.permutationOf {α : Type u} (xs : List α) : Gen { ys : List α // xs.Perm ys }

Generate a random permutation of a given list.

def Plausible.Gen.prodOf {α : Type u} {β : Type v} (x : Gen α) (y : Gen β) : Gen (α × β)

Given two generators produces a tuple consisting out of the result of both

@[implicit_reducible]

instance Plausible.instMonadLiftStateIOGen : MonadLift (ReaderT (ULift Nat) (Except GenError)) IO

def Plausible.Gen.run {α : Type} (x : Gen α) (size : Nat) : IO α

Execute a Gen inside the IO monad using size as the example size

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

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

def Plausible.Gen.runUntil {α : Type} (attempts : Option Nat := none) (x : Gen α) (size : Nat) : IO α

Execute a Gen until it actually produces an output. May diverge for bad generators!