Closure properties of computable and c.e. predicates

Mathlib's ComputablePred and REPred come with complementation and Post's theorem. This file adds the closure properties needed to read off the effectivity of predicates assembled from computable pieces:

• ComputablePred.and: computable predicates are closed under conjunction;
• ComputablePred.exists_eq_some_and: testing a computable predicate on the value of a computable optional function, when that value is present, is computable;
• ComputablePred.exists_lt: a bounded existential quantifier over a computable predicate is computable, uniformly in the bound;
• ComputablePred.rePred_exists: an unbounded existential quantifier over a computable predicate is c.e., by unbounded search.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter II.1.

theorem ComputablePred.and {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : ComputablePred p) (hq : ComputablePred q) : ComputablePred fun (a : α) => p a ∧ q a

Computable predicates are closed under conjunction.

theorem ComputablePred.exists_eq_some_and {α : Type u_1} [Primcodable α] {β : Type u_2} [Primcodable β] {f : α → Option β} {q : α → β → Prop} (hf : Computable f) (hq : ComputablePred fun (x : α × β) => q x.1 x.2) : ComputablePred fun (a : α) => ∃ (b : β), f a = some b ∧ q a b

Testing a computable predicate on the value of a computable optional function, when that value is present, is computable.

theorem ComputablePred.exists_lt {α : Type u_1} [Primcodable α] {p : α → ℕ → Prop} (hp : ComputablePred fun (x : α × ℕ) => p x.1 x.2) : ComputablePred fun (x : α × ℕ) => ∃ y < x.2, p x.1 y

A bounded existential quantifier over a computable predicate is computable, uniformly in the bound.

theorem ComputablePred.rePred_exists {α : Type u_1} [Primcodable α] {p : α → ℕ → Prop} (hp : ComputablePred fun (x : α × ℕ) => p x.1 x.2) : REPred fun (a : α) => ∃ (n : ℕ), p a n

An unbounded existential quantifier over a computable predicate is c.e.: search for a witness.