slim_check: generators for functions

This file defines Sampleable instances for α → β functions and ℤ → ℤ 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 ℤ → ℤ 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 : ℤ → ℤ 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.

inductive SlimCheck.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 ((_ : α) × β) → β → SlimCheck.TotalFunction α β

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

Equations

• SlimCheck.TotalFunction.inhabited = { default := SlimCheck.TotalFunction.withDefault ∅ default }

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

Compose a total function with a regular function on the left

Equations

• SlimCheck.TotalFunction.comp f x = match x with | SlimCheck.TotalFunction.withDefault m y => SlimCheck.TotalFunction.withDefault (List.map (Sigma.map id fun (x : α) => f) m) (f y)

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

Apply a total function to an argument.

Equations

• x✝.apply x = match x✝, x with | SlimCheck.TotalFunction.withDefault m y, x => (List.dlookup x m).getD y

def SlimCheck.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.

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

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

Equations

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

instance SlimCheck.TotalFunction.instRepr (α : Type u) (β : Type v) [Repr α] [Repr β] : Repr (SlimCheck.TotalFunction α β)

Equations

• SlimCheck.TotalFunction.instRepr α β = { reprPrec := fun (f : SlimCheck.TotalFunction α β) (x : ℕ) => Std.Format.text f.repr }

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

Create a finmap from a list of pairs.

Equations

• SlimCheck.TotalFunction.List.toFinmap' xs = List.map Prod.toSigma xs

def SlimCheck.TotalFunction.shrink {α : Type u_1} {β : Type u_2} [DecidableEq α] [SlimCheck.Shrinkable α] [SlimCheck.Shrinkable β] : SlimCheck.TotalFunction α β → List (SlimCheck.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.

instance SlimCheck.TotalFunction.Pi.sampleableExt {α : Type u} {β : Type v} [SlimCheck.SampleableExt α] [SlimCheck.SampleableExt β] [DecidableEq α] [Repr α] : SlimCheck.SampleableExt (α → β)

Equations

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

def SlimCheck.TotalFunction.zeroDefault {α : Type u} {β : Type v} [Zero β] : SlimCheck.TotalFunction α β → SlimCheck.TotalFunction α β

Map a total_function to one whose default value is zero so that it represents a finsupp.

Equations

• x.zeroDefault = match x with | SlimCheck.TotalFunction.withDefault A a => SlimCheck.TotalFunction.withDefault A 0

def SlimCheck.TotalFunction.zeroDefaultSupp {α : Type u} {β : Type v} [Zero β] [DecidableEq α] [DecidableEq β] : SlimCheck.TotalFunction α β → Finset α

The support of a zero default TotalFunction.

Equations

• x.zeroDefaultSupp = match x with | SlimCheck.TotalFunction.withDefault A a => (List.map Sigma.fst (List.filter (fun (ab : (_ : α) × β) => decide (ab.snd ≠ 0)) A.dedupKeys)).toFinset

def SlimCheck.TotalFunction.applyFinsupp {α : Type u} {β : Type v} [Zero β] [DecidableEq α] [DecidableEq β] (tf : SlimCheck.TotalFunction α β) : α →₀ β

Create a finitely supported function from a total function by taking the default value to zero.

Equations

• tf.applyFinsupp = { support := tf.zeroDefaultSupp, toFun := tf.zeroDefault.apply, mem_support_toFun := ⋯ }

instance SlimCheck.TotalFunction.Finsupp.sampleableExt {α : Type u} {β : Type v} [Zero β] [DecidableEq α] [DecidableEq β] [SlimCheck.SampleableExt α] [SlimCheck.SampleableExt β] [Repr α] : SlimCheck.SampleableExt (α →₀ β)

Equations

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

instance SlimCheck.TotalFunction.DFinsupp.sampleableExt {α : Type u} {β : Type v} [Zero β] [DecidableEq α] [DecidableEq β] [SlimCheck.SampleableExt α] [SlimCheck.SampleableExt β] [Repr α] : SlimCheck.SampleableExt (Π₀ (x : α), β)

Equations

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

instance SlimCheck.TotalFunction.PiPred.sampleableExt {α : Type u} [SlimCheck.SampleableExt (α → Bool)] : SlimCheck.SampleableExt (α → Prop)

Equations

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

instance SlimCheck.TotalFunction.PiUncurry.sampleableExt {α : Type u} {β : Type v} {γ : Sort w} [SlimCheck.SampleableExt (α × β → γ)] : SlimCheck.SampleableExt (α → β → γ)

Equations

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

inductive SlimCheck.InjectiveFunction (α : Type u) : Type u

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.

mapToSelf f encodes x ↦ f x when x ∈ f and x ↦ x, i.e. x to itself, otherwise.

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

• mapToSelf: {α : Type u} → (xs : List ((_ : α) × α)) → (List.map Sigma.fst xs).Perm (List.map Sigma.snd xs) → (List.map Sigma.snd xs).Nodup → SlimCheck.InjectiveFunction α

instance SlimCheck.instInhabitedInjectiveFunction {α : Type u} : Inhabited (SlimCheck.InjectiveFunction α)

Equations

• SlimCheck.instInhabitedInjectiveFunction = { default := SlimCheck.InjectiveFunction.mapToSelf [] ⋯ ⋯ }

def SlimCheck.InjectiveFunction.apply {α : Type u} [DecidableEq α] : SlimCheck.InjectiveFunction α → α → α

Apply a total function to an argument.

Equations

• x✝.apply x = match x✝, x with | SlimCheck.InjectiveFunction.mapToSelf m a a_1, x => (List.dlookup x m).getD x

def SlimCheck.InjectiveFunction.repr {α : Type u} [Repr α] : SlimCheck.InjectiveFunction α → String

Produce a string for a given InjectiveFunction. The output is of the form [x₀ ↦ f x₀, .. xₙ ↦ f xₙ, x ↦ x]. Unlike for TotalFunction, the default value is not a constant but the identity function.

Equations

• x.repr = match x with | SlimCheck.InjectiveFunction.mapToSelf m a a_1 => toString "[" ++ toString (SlimCheck.TotalFunction.reprAux m) ++ toString "x ↦ x]"

instance SlimCheck.InjectiveFunction.instRepr (α : Type u) [Repr α] : Repr (SlimCheck.InjectiveFunction α)

Equations

• SlimCheck.InjectiveFunction.instRepr α = { reprPrec := fun (f : SlimCheck.InjectiveFunction α) (_p : ℕ) => Std.Format.text f.repr }

def SlimCheck.InjectiveFunction.List.applyId {α : Type u} [DecidableEq α] (xs : List (α × α)) (x : α) : α

Interpret a list of pairs as a total function, defaulting to the identity function when no entries are found for a given function

Equations

• SlimCheck.InjectiveFunction.List.applyId xs x = (List.dlookup x (List.map Prod.toSigma xs)).getD x

@[simp]

theorem SlimCheck.InjectiveFunction.List.applyId_cons {α : Type u} [DecidableEq α] (xs : List (α × α)) (x : α) (y : α) (z : α) : SlimCheck.InjectiveFunction.List.applyId ((y, z) :: xs) x = if y = x then z else SlimCheck.InjectiveFunction.List.applyId xs x

theorem SlimCheck.InjectiveFunction.List.applyId_zip_eq {α : Type u} [DecidableEq α] {xs : List α} {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.length = ys.length) (x : α) (y : α) (i : ℕ) (h₂ : xs.get? i = some x) : SlimCheck.InjectiveFunction.List.applyId (xs.zip ys) x = y ↔ ys.get? i = some y

theorem SlimCheck.InjectiveFunction.applyId_mem_iff {α : Type u} [DecidableEq α] {xs : List α} {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.Perm ys) (x : α) : SlimCheck.InjectiveFunction.List.applyId (xs.zip ys) x ∈ ys ↔ x ∈ xs

theorem SlimCheck.InjectiveFunction.List.applyId_eq_self {α : Type u} [DecidableEq α] {xs : List α} {ys : List α} (x : α) : x ∉ xs → SlimCheck.InjectiveFunction.List.applyId (xs.zip ys) x = x

theorem SlimCheck.InjectiveFunction.applyId_injective {α : Type u} [DecidableEq α] {xs : List α} {ys : List α} (h₀ : xs.Nodup) (h₁ : xs.Perm ys) : Function.Injective (SlimCheck.InjectiveFunction.List.applyId (xs.zip ys))

def SlimCheck.InjectiveFunction.Perm.slice {α : Type u} [DecidableEq α] (n : ℕ) (m : ℕ) : (xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup → (xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup

Remove a slice of length m at index n in a list and a permutation, maintaining the property that it is a permutation.

Equations

• SlimCheck.InjectiveFunction.Perm.slice n m x = match x with | ⟨xs, ⟨ys, ⋯⟩⟩ => let xs' := List.dropSlice n m xs; let_fun h₀ := ⋯; ⟨xs', ⟨ys.inter xs', ⋯⟩⟩

def SlimCheck.InjectiveFunction.sliceSizes : ℕ → LazyList ℕ+

A lazy list, in decreasing order, of sizes that should be sliced off a list of length n

Equations

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

def SlimCheck.InjectiveFunction.shrinkPerm {α : Type} [DecidableEq α] : (xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup → List ((xs : List α) ×' (ys : List α) ×' xs.Perm ys ∧ ys.Nodup)

Shrink a permutation of a list, slicing a segment in the middle.

The sizes of the slice being removed start at n (with n the length of the list) and then n / 2, then n / 4, etc down to 1. The slices will be taken at index 0, n / k, 2n / k, 3n / k, etc.

Equations

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

def SlimCheck.InjectiveFunction.shrink {α : Type} [DecidableEq α] : SlimCheck.InjectiveFunction α → List (SlimCheck.InjectiveFunction α)

Shrink an injective function slicing a segment in the middle of the domain and removing the corresponding elements in the codomain, hence maintaining the property that one is a permutation of the other.

Equations

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

def SlimCheck.InjectiveFunction.mk {α : Type u} (xs : List α) (ys : List α) (h : xs.Perm ys) (h' : ys.Nodup) : SlimCheck.InjectiveFunction α

Create an injective function from one list and a permutation of that list.

Equations

• SlimCheck.InjectiveFunction.mk xs ys h h' = let_fun h₀ := ⋯; let_fun h₁ := ⋯; SlimCheck.InjectiveFunction.mapToSelf (SlimCheck.TotalFunction.List.toFinmap' (xs.zip ys)) ⋯ ⋯

theorem SlimCheck.InjectiveFunction.injective {α : Type u} [DecidableEq α] (f : SlimCheck.InjectiveFunction α) : Function.Injective f.apply

instance SlimCheck.InjectiveFunction.PiInjective.sampleableExt : SlimCheck.SampleableExt { f : ℤ → ℤ // Function.Injective f }

Equations

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

instance SlimCheck.Injective.testable {α : Type u} {β : Type v} (f : α → β) [I : SlimCheck.Testable (SlimCheck.NamedBinder "x" (∀ (x : α), SlimCheck.NamedBinder "y" (∀ (y : α), SlimCheck.NamedBinder "H" (f x = f y → x = y))))] : SlimCheck.Testable (Function.Injective f)

Equations

• SlimCheck.Injective.testable f = I

instance SlimCheck.Monotone.testable {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) [I : SlimCheck.Testable (SlimCheck.NamedBinder "x" (∀ (x : α), SlimCheck.NamedBinder "y" (∀ (y : α), SlimCheck.NamedBinder "H" (x ≤ y → f x ≤ f y))))] : SlimCheck.Testable (Monotone f)

Equations

• SlimCheck.Monotone.testable f = I

instance SlimCheck.Antitone.testable {α : Type u} {β : Type v} [Preorder α] [Preorder β] (f : α → β) [I : SlimCheck.Testable (SlimCheck.NamedBinder "x" (∀ (x : α), SlimCheck.NamedBinder "y" (∀ (y : α), SlimCheck.NamedBinder "H" (x ≤ y → f y ≤ f x))))] : SlimCheck.Testable (Antitone f)

Equations

• SlimCheck.Antitone.testable f = I