## `plausible`: generators for functions #

This file defines `Sampleable` instances for `α → β` functions and `Int → Int` injective functions.

Functions are generated by creating a list of pairs and one more value using the list as a lookup table and resorting to the additional value when a value is not found in the table.

Injective functions are generated by creating a list of numbers and a permutation of that list. The permutation insures that every input is mapped to a unique output. When an input is not found in the list the input itself is used as an output.

Injective functions `f : α → α` could be generated easily instead of `Int → Int` by generating a `List α`, removing duplicates and creating a permutation. One has to be careful when generating the domain to make it vast enough that, when generating arguments to apply `f` to, they argument should be likely to lie in the domain of `f`. This is the reason that injective functions `f : Int → Int` are generated by fixing the domain to the range `[-2*size .. 2*size]`, with `size` the size parameter of the `gen` monad.

Much of the machinery provided in this file is applicable to generate injective functions of type `α → α` and new instances should be easy to define.

Other classes of functions such as monotone functions can generated using similar techniques. For monotone functions, generating two lists, sorting them and matching them should suffice, with appropriate default values. Some care must be taken for shrinking such functions to make sure their defining property is invariant through shrinking. Injective functions are an example of how complicated it can get.

source
inductive Plausible.TotalFunction (α : Type u) (β : Type v) :
Type (max u v)

Data structure specifying a total function using a list of pairs and a default value returned when the input is not in the domain of the partial function.

`withDefault f y` encodes `x => f x` when `x ∈ f` and `x => y` otherwise.

We use `Σ` to encode mappings instead of `×` because we rely on the association list API defined in `Mathlib/Data/List/Sigma.lean`.

- withDefault {α : Type u} {β : Type v} : List ((_ : α) × β) → β → TotalFunction α β

Instances For

source
instance Plausible.TotalFunction.inhabited {α : Type u} {β : Type v} [Inhabited β] :
Inhabited (TotalFunction α β)
Equations

- Plausible.TotalFunction.inhabited = { default := Plausible.TotalFunction.withDefault ∅ default }

source
def Plausible.TotalFunction.comp {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) :
TotalFunction α β → TotalFunction α γ

Compose a total function with a regular function on the left

Equations

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

Instances For

source
def Plausible.TotalFunction.apply {α : Type u} {β : Type v} [DecidableEq α] :
TotalFunction α β → α → β

Apply a total function to an argument.

Equations

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

Instances For

source
def Plausible.TotalFunction.reprAux {α : Type u} {β : Type v} [Repr α] [Repr β] (m : List ((_ : α) × β)) :
String

Implementation of `Repr (TotalFunction α β)`.

Creates a string for a given `Finmap` and output, `x₀ => y₀, .. xₙ => yₙ` for each of the entries. The brackets are provided by the calling function.

Equations

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

Instances For

source
def Plausible.TotalFunction.repr {α : Type u} {β : Type v} [Repr α] [Repr β] :
TotalFunction α β → String

Produce a string for a given `TotalFunction`. The output is of the form `[x₀ => f x₀, .. xₙ => f xₙ, _ => y]`.

Equations

- (Plausible.TotalFunction.withDefault m y).repr = toString "[" ++ toString (Plausible.TotalFunction.reprAux m) ++ toString "_ => " ++ toString (repr y) ++ toString "]"

Instances For

source
instance Plausible.TotalFunction.instRepr (α : Type u) (β : Type v) [Repr α] [Repr β] :
Repr (TotalFunction α β)
Equations

- Plausible.TotalFunction.instRepr α β = { reprPrec := fun (f : Plausible.TotalFunction α β) (x : Nat) => Std.Format.text f.repr }

source
def Plausible.TotalFunction.List.toFinmap' {α : Type u} {β : Type v} (xs : List (α × β)) :
List ((_ : α) × β)

Create a `Finmap` from a list of pairs.

Equations

- Plausible.TotalFunction.List.toFinmap' xs = List.map (fun (x : α × β) => match x with | (a, b) => ⟨a, b⟩) xs

Instances For

source
def Plausible.TotalFunction.shrink {α : Type u_1} {β : Type u_2} [DecidableEq α] [Shrinkable α] [Shrinkable β] :
TotalFunction α β → List (TotalFunction α β)

Shrink a total function by shrinking the lists that represent it.

Equations

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

Instances For

source
def Plausible.TotalFunction.shrink.dedup {α : Type u_1} {β : Type u_2} [DecidableEq α] (m' : List ((_ : α) × β)) :
List ((_ : α) × β)
Equations

- Plausible.TotalFunction.shrink.dedup m' = List.foldl Plausible.TotalFunction.shrink.dedup.insertKey [] m'

Instances For

source
partial def Plausible.TotalFunction.shrink.dedup.insertKey {α : Type u_1} {β : Type u_2} [DecidableEq α] (xs : List ((_ : α) × β)) (pair : (_ : α) × β) :
List ((_ : α) × β)
source
instance Plausible.TotalFunction.Pi.sampleableExt {α : Type u} {β : Type v} [SampleableExt α] [SampleableExt β] [DecidableEq α] [Repr α] :
SampleableExt (α → β)
Equations

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

source
@[instance 2000]
instance Plausible.TotalFunction.PiPred.sampleableExt {α : Type u} [SampleableExt (α → Bool)] :
SampleableExt (α → Prop)
Equations

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

source
@[instance 2000]
instance Plausible.TotalFunction.PiUncurry.sampleableExt {α : Type u} {β : Type v} {γ : Sort w} [SampleableExt (α × β → γ)] :
SampleableExt (α → β → γ)
Equations

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