Primitive recursive operations on binary finite-set codes

Primitive recursion certificates for membership, the characteristic function, bounded filtering and least-element search on binary finite-set codes, and for the codes of the set of entries of a list and of Finset.range n. The code operations and their finite-set interpretations are defined in TauCeti.Data.Nat.BitIndices, using Mathlib's Finset.equivBitIndices rather than another encoding or a Primcodable instance for finite sets.

The certificates are uniform in their numerical inputs and, for bounded filtering, in the primitive recursive predicate, so they can be used in computable finite-stage constructions.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter II.2.
• Mathlib's Finset.equivBitIndices supplies the binary finite-set equivalence.

theorem Primrec.mem_equivBitIndices : PrimrecRel fun (n x : ℕ) => x ∈ Finset.equivBitIndices n

Membership in the decoded binary finite set is primitive recursive.

theorem Primrec.indicator_equivBitIndices : Primrec₂ fun (n x : ℕ) => (↑(Finset.equivBitIndices n)).indicator 1 x

The characteristic function of the decoded binary finite set is primitive recursive in the code and the argument.

theorem Primrec.nat_filterBitIndices {α : Type u_1} [Primcodable α] {n b : α → ℕ} {p : α → ℕ → Bool} (hn : Primrec n) (hb : Primrec b) (hp : Primrec₂ p) : Primrec fun (a : α) => (n a).filterBitIndices (b a) (p a)

Bounded filtering of binary codes is primitive recursive, uniformly in a primitive recursive predicate and the code and bound supplied by the caller.

theorem Primrec.equivBitIndices_symm_toFinset : Primrec fun (l : List ℕ) => Finset.equivBitIndices.symm l.toFinset

The code of the set of entries of a list is primitive recursive.

theorem Primrec.equivBitIndices_symm_range : Primrec fun (n : ℕ) => Finset.equivBitIndices.symm (Finset.range n)

The code 2 ^ n - 1 of Finset.range n is primitive recursive in n.

theorem Primrec.nat_leastBitIndex : Primrec Nat.leastBitIndex

Least-element search on binary finite-set codes is primitive recursive.