Enumerating Bounded Words

This file provides a small computable enumeration of all words up to a given length over an explicitly supplied finite alphabet list, plus a reusable bounded search combinator over such word lists.

def wordsOfLen {α : Type} (alphabet : List α) : ℕ → List (List α)

All words of exactly length n over the symbols in alphabet.

Equations

• wordsOfLen alphabet 0 = [[]]
• wordsOfLen alphabet k.succ = List.flatMap (fun (w : List α) => List.map (fun (a : α) => a :: w) alphabet) (wordsOfLen alphabet k)

def wordsUpTo {α : Type} (alphabet : List α) (n : ℕ) : List (List α)

All words of length at most n over the symbols in alphabet.

Equations

• wordsUpTo alphabet n = List.flatMap (wordsOfLen alphabet) (List.range (n + 1))

theorem wordsOfLen_eq {α : Type} (alphabet : List α) (n : ℕ) : wordsOfLen alphabet n = Nat.rec [[]] (fun (x : ℕ) (ih : List (List α)) => List.flatMap (fun (w : List α) => List.map (fun (a : α) => a :: w) alphabet) ih) n

theorem wordsOfLen_primrec {α : Type} [Primcodable α] : Primrec fun (x : List α × ℕ) => wordsOfLen x.1 x.2

theorem wordsUpTo_primrec {α : Type} [Primcodable α] : Primrec fun (x : List α × ℕ) => wordsUpTo x.1 x.2

theorem mem_wordsOfLen {α : Type} (alphabet : List α) (n : ℕ) (w : List α) : w ∈ wordsOfLen alphabet n ↔ w.length = n ∧ ∀ a ∈ w, a ∈ alphabet

theorem mem_wordsUpTo_univ {α : Type} [Fintype α] [DecidableEq α] (n : ℕ) (w : List α) : w ∈ wordsUpTo Finset.univ.toList n ↔ w.length ≤ n

def wordSearch {α : Type} (candidates : List (List α)) (p : List α → Bool) : Bool

Search a finite candidate list for a word satisfying p.

Equations

• wordSearch candidates p = Nat.rec false (fun (i : ℕ) (acc : Bool) => acc || p (candidates.getD i [])) candidates.length

theorem wordSearch_rec_true_iff {α : Type} (candidates : List (List α)) (p : List α → Bool) (k : ℕ) : Nat.rec false (fun (i : ℕ) (acc : Bool) => acc || p (candidates.getD i [])) k = true ↔ ∃ i < k, p (candidates.getD i []) = true

theorem wordSearch_true_iff_exists_mem {α : Type} (candidates : List (List α)) (p : List α → Bool) : wordSearch candidates p = true ↔ ∃ w ∈ candidates, p w = true

theorem wordSearch_computable {α δ : Type} [Primcodable α] [Primcodable δ] {candidates : δ → List (List α)} {p : δ → List α → Bool} (hcandidates : Computable candidates) (hp : Computable₂ p) : Computable fun (d : δ) => wordSearch (candidates d) (p d)