Computable and Recursively Enumerable Predicates

This file defines computable (ComputablePred) and recursively enumerable (REPred) predicates. It also provides basic closure properties and Post's theorem on the equivalence of recursive, r.e., and co-r.e. sets.

theorem Nat.Partrec.merge' {f g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) : ∃ (h : ℕ →. ℕ), Nat.Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)

theorem Partrec.merge' {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f g : α →. σ} (hf : Partrec f) (hg : Partrec g) : ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

theorem Partrec.merge {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {f g : α →. σ} (hf : Partrec f) (hg : Partrec g) (H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y) : ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α) (x : σ), x ∈ k a ↔ x ∈ f a ∨ x ∈ g a

theorem Partrec.cond {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] {c : α → Bool} {f g : α →. σ} (hc : Computable c) (hf : Partrec f) (hg : Partrec g) : Partrec fun (a : α) => bif c a then f a else g a

theorem Partrec.sumCasesOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ →. σ} (hf : Computable f) (hg : Partrec₂ g) (hh : Partrec₂ h) : Partrec fun (a : α) => Sum.casesOn (f a) (g a) (h a)

def ComputablePred {α : Type u_1} [Primcodable α] (p : α → Prop) : Prop

A computable predicate is one whose indicator function is computable.

theorem ComputablePred.decide {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hp : ComputablePred p) : Computable fun (a : α) => decide (p a)

theorem Computable.computablePred {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] (hp : Computable fun (a : α) => decide (p a)) : ComputablePred p

theorem computablePred_iff_computable_decide {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] : ComputablePred p ↔ Computable fun (a : α) => decide (p a)

theorem PrimrecPred.computablePred {α : Type u_1} [Primcodable α] {p : α → Prop} (hp : PrimrecPred p) : ComputablePred p

def REPred {α : Type u_1} [Primcodable α] (p : α → Prop) : Prop

A recursively enumerable predicate is one which is the domain of a computable partial function.

theorem REPred.of_eq {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : REPred p) (H : ∀ (a : α), p a ↔ q a) : REPred q

theorem Partrec.dom_re {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α →. β} (h : Partrec f) : REPred fun (a : α) => (f a).Dom

theorem ComputablePred.of_eq {α : Type u_1} [Primcodable α] {p q : α → Prop} (hp : ComputablePred p) (H : ∀ (a : α), p a ↔ q a) : ComputablePred q

theorem Computable.find {α : Type u_1} [Primcodable α] {P : α → ℕ → Prop} [DecidableRel P] (hP_comp : ComputablePred fun (p : α × ℕ) => P p.1 p.2) (hP_ex : ∀ (x : α), ∃ (n : ℕ), P x n) : Computable fun (x : α) => Nat.find ⋯

If P is computable, and if for every x there exists an n such that P x n holds, then the function mapping x to the minimal such n (using Nat.find) is computable. This formally bridges Partrec.rfind with total unbounded search.

theorem ComputablePred.computable_iff {α : Type u_1} [Primcodable α] {p : α → Prop} : ComputablePred p ↔ ∃ (f : α → Bool), Computable f ∧ p = fun (a : α) => f a = true

theorem ComputablePred.not {α : Type u_1} [Primcodable α] {p : α → Prop} (hp : ComputablePred p) : ComputablePred fun (a : α) => ¬p a

theorem ComputablePred.ite {f₁ f₂ : ℕ → ℕ} (hf₁ : Computable f₁) (hf₂ : Computable f₂) {c : ℕ → Prop} [DecidablePred c] (hc : ComputablePred c) : Computable fun (k : ℕ) => if c k then f₁ k else f₂ k

The computable functions are closed under if-then-else definitions with computable predicates.

theorem ComputablePred.to_re {α : Type u_1} [Primcodable α] {p : α → Prop} (hp : ComputablePred p) : REPred p

theorem ComputablePred.computable_iff_re_compl_re {α : Type u_1} [Primcodable α] {p : α → Prop} [DecidablePred p] : ComputablePred p ↔ REPred p ∧ REPred fun (a : α) => ¬p a

theorem ComputablePred.computable_iff_re_compl_re' {α : Type u_1} [Primcodable α] {p : α → Prop} : ComputablePred p ↔ REPred p ∧ REPred fun (a : α) => ¬p a