Composable Enumerations

This file defines Enum α, a type of computable enumerations over a type α, together with a library of combinators for building complex enumerations from simple ones. This forms the "generator" half of the DSL.

Design

An Enum α is simply a function ℕ → Option α. Semantically, it represents a (possibly infinite) stream of elements: enum 0, enum 1, enum 2, ..., where none means "no output at this index" (allowing sparse enumerations).

The key combinators are:

• Enum.naturals — enumerate all natural numbers
• Enum.ofList — enumerate elements of a finite list
• Enum.ofEncodable — enumerate all elements of an Encodable type
• Enum.product — enumerate all pairs (dovetailing)
• Enum.bind — monadic bind (flatMap with dovetailing)
• Enum.map — apply a function to each element
• Enum.filterMap — filter and transform

Each combinator preserves the property that every element in the range eventually appears (surjectivity onto the range).

Main definitions

• Enum — the type of enumerations
• Enum.range — the set of elements that appear in an enumeration
• Enum.Surjective — every element in the range appears
• Various combinators with range correctness theorems

References

This is the "generator" layer of the DSL described in the module Langlib.Automata.Turing.DSL.SearchProcedure.

def Enum (α : Type u_1) : Type u_1

An enumeration of elements of type α.

Semantically, e : Enum α represents a computable sequence e 0, e 1, e 2, ... where each step either produces an element (some a) or is a no-op (none). The range of e is {a | ∃ n, e n = some a}.

Note: an Enum may produce the same element multiple times; what matters is that every element in the intended set appears at least once.

Equations

• Enum α = (ℕ → Option α)

def Enum.range {α : Type u_1} (e : Enum α) : Set α

The range (set of produced elements) of an enumeration.

Equations

• e.range = {a : α | ∃ (n : ℕ), e n = some a}

def Enum.SurjectiveOnto {α : Type u_1} (e : Enum α) (S : Set α) : Prop

An enumeration is surjective onto a set S if every element of S appears in the enumeration.

Equations

• e.SurjectiveOnto S = (S ⊆ e.range)

def Enum.Exact {α : Type u_1} (e : Enum α) (S : Set α) : Prop

An enumeration is exact for a set S if its range equals S.

Equations

• e.Exact S = (e.range = S)

theorem Enum.exact_iff_range_eq {α : Type u_1} (e : Enum α) (S : Set α) : e.Exact S ↔ e.range = S

Basic enumerations

def Enum.naturals : Enum ℕ

Enumerate all natural numbers: 0, 1, 2, ...

Equations

• Enum.naturals n = some n

theorem Enum.naturals_range : naturals.range = Set.univ

def Enum.ofList {α : Type u_1} (l : List α) : Enum α

Enumerate elements of a finite list.

Equations

• Enum.ofList l n = l[n]?

theorem Enum.ofList_range {α : Type u_1} (l : List α) : (ofList l).range = {a : α | a ∈ l}

def Enum.ofEncodable {α : Type u_1} [Encodable α] : Enum α

Enumerate all elements of an Encodable type.

Equations

• Enum.ofEncodable n = Encodable.decode n

theorem Enum.ofEncodable_range {α : Type u_1} [Encodable α] : ofEncodable.range = Set.univ

def Enum.empty {α : Type u_1} : Enum α

The empty enumeration.

Equations

• Enum.empty x✝ = none

theorem Enum.empty_range {α : Type u_1} : empty.range = ∅

def Enum.singleton {α : Type u_1} (a : α) : Enum α

Enumerate a single element.

Equations

• Enum.singleton a n = if n = 0 then some a else none

theorem Enum.singleton_range {α : Type u_1} (a : α) : (singleton a).range = {a}

Combinators

def Enum.map {α : Type u_1} {β : Type u_2} (f : α → β) (e : Enum α) : Enum β

Apply a function to each enumerated element.

Equations

• Enum.map f e n = Option.map f (e n)

theorem Enum.map_range {α : Type u_1} {β : Type u_2} (f : α → β) (e : Enum α) : (map f e).range = f '' e.range

def Enum.filterMap {α : Type u_1} {β : Type u_2} (f : α → Option β) (e : Enum α) : Enum β

Filter and transform an enumeration.

Equations

• Enum.filterMap f e n = (e n).bind f

theorem Enum.filterMap_range {α : Type u_1} {β : Type u_2} (f : α → Option β) (e : Enum α) : (filterMap f e).range = {b : β | ∃ a ∈ e.range, f a = some b}

def Enum.filter {α : Type u_1} (p : α → Bool) (e : Enum α) : Enum α

Filter an enumeration by a predicate.

Equations

• Enum.filter p e n = (e n).bind fun (a : α) => if p a = true then some a else none

theorem Enum.filter_range {α : Type u_1} (p : α → Bool) (e : Enum α) : (filter p e).range = {a : α | a ∈ e.range ∧ p a = true}

Pairing / Dovetailing

To enumerate all pairs (a, b) from two enumerations, we use the Cantor pairing function to dovetail.

def Enum.product {α : Type u_1} {β : Type u_2} (e₁ : Enum α) (e₂ : Enum β) : Enum (α × β)

Enumerate all pairs from two enumerations using dovetailing.

Equations

• e₁.product e₂ n = match Nat.unpair n with | (i, j) => match e₁ i, e₂ j with | some a, some b => some (a, b) | x, x_1 => none

theorem Enum.product_range {α : Type u_1} {β : Type u_2} (e₁ : Enum α) (e₂ : Enum β) : (e₁.product e₂).range = {p : α × β | p.1 ∈ e₁.range ∧ p.2 ∈ e₂.range}

def Enum.bind {α : Type u_1} {β : Type u_2} (e : Enum α) (f : α → Enum β) : Enum β

Monadic bind (flatMap) with dovetailing. For each element a from e, enumerate f a, interleaving all results.

Equations

• e.bind f n = match Nat.unpair n with | (i, j) => match e i with | some a => f a j | none => none

theorem Enum.bind_range {α : Type u_1} {β : Type u_2} (e : Enum α) (f : α → Enum β) : (e.bind f).range = {b : β | ∃ a ∈ e.range, b ∈ (f a).range}

Derived enumerations

def Enum.finLists {α : Type u_1} [Encodable α] : Enum (List α)

Enumerate all finite lists over an Encodable type.

Equations

• Enum.finLists = Enum.ofEncodable

theorem Enum.finLists_range {α : Type u_1} [Encodable α] : finLists.range = Set.univ

def Enum.natPairs : Enum (ℕ × ℕ)

Enumerate all pairs of natural numbers.

Equations

• Enum.natPairs = Enum.naturals.product Enum.naturals

theorem Enum.natPairs_range : natPairs.range = Set.univ