Primitive Recursive Helpers

This file provides helper lemmas establishing that various list operations are primitive recursive, needed for showing that the CYK algorithm is computable.

theorem primrec₂_list_take {α : Type} [Primcodable α] : Primrec₂ fun (n : ℕ) (l : List α) => List.take n l

theorem primrec₂_list_drop {α : Type} [Primcodable α] : Primrec₂ fun (n : ℕ) (l : List α) => List.drop n l

theorem primrec_flatMap_finite {α β : Type} [Primcodable α] [Primcodable β] [Finite α] (h : α → List β) : Primrec fun (w : List α) => List.flatMap h w

A fixed string homomorphism out of a finite alphabet is primitive recursive on words.

theorem computable₂_flatMap_eq_finite {α β : Type} [DecidableEq β] [Primcodable α] [Primcodable β] [Finite α] (h : α → List β) : Computable₂ fun (w : List α) (u : List β) => decide (List.flatMap h w = u)

Equality against the image of a fixed finite-alphabet string homomorphism is computable.

theorem primrec_list_any {α : Type} [Primcodable α] {β : Type u_1} {f : α → List β} {p : α → β → Bool} [Primcodable β] (hf : Primrec f) (hp : Primrec₂ p) : Primrec fun (a : α) => (f a).any (p a)