Primitive-recursive list operations

Rotation and cyclic-permutation testing are primitive recursive on the standard list encoding. The bounded rotation criterion includes the empty list, so it also applies to cyclic reductions of trivial free-group words.

Searching a list for its first element passing a test, List.find?, is primitive recursive. Over List.range n this is the bounded least-witness search of finite-stage constructions, returning none when no number below n passes the test. A relation searched over all numbers up to the length of a primitive-recursively computed list stays primitive recursive (PrimrecRel.exists_le_length).

theorem Primrec.list_rotate {α : Type u_1} [Primcodable α] : Primrec₂ List.rotate

Rotating a list by a natural number is primitive recursive.

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

The first element of a list passing a test, if any, is primitive recursive, uniformly in a parameter on which the list and the test depend primitive recursively.

theorem PrimrecRel.exists_le_length {β : Type u_1} {γ : Type u_2} [Primcodable β] [Primcodable γ] {f : β → List γ} {R : ℕ → β → Prop} (hR : PrimrecRel R) (hf : Primrec f) : PrimrecPred fun (b : β) => ∃ n ≤ (f b).length, R n b

A relation searched over all n ≤ (f b).length, for f primitive recursive, stays primitive recursive.

theorem List.primrecRel_isRotated {α : Type u_1} [Primcodable α] : PrimrecRel IsRotated

Cyclic permutation is a primitive-recursive relation, including for empty lists.