Range of a p.c. function is C.E.

Stream: new members

[Janitha Aswedige]

I'm trying to prove that the range of a partial computable function is computably enumerable. I formalized the statement and I think it's correct. I just don't know if this has already been done. Any help is appreciated.

theorem rangePartrec_REPred {p : ℕ → Prop} (hp : ∃ (f : ℕ →. ℕ), Nat.Partrec f ∧ ∀ x, p x ↔ ∃ y, x ∈ f y ) :
    REPred p := by
      sorry

[Aaron Liu]

The statement looks correct but it's stated kind of weirdly

[Matt Diamond]

it might be simpler to state it like this:

theorem rangePartrec_REPred (f : ℕ →. ℕ) (hf : Nat.Partrec f) : REPred (fun x => ∃ y, x ∈ f y) := sorry

[Matt Diamond]

I spent way too long on this but here's a proof:

import Mathlib.Computability.Halting

open Nat.Partrec Primrec

lemma evaln_eq_some_prim (c : Code) : PrimrecRel fun (x y : ℕ) => c.evaln y.unpair.1 y.unpair.2 = some x :=
Primrec.eq.comp
  (Code.primrec_evaln.comp (.pair (.pair (fst.comp (unpair.comp .snd)) (.const c)) (snd.comp (unpair.comp .snd))))
  (Primrec.option_some.comp .fst)

theorem rangePartrec_REPred (f : ℕ →. ℕ) (hf : Nat.Partrec f) : REPred (fun y => ∃ x, y ∈ f x) :=
by
  obtain ⟨c, hc⟩ := Code.exists_code.mp hf
  have : REPred fun (y : ℕ) => (Nat.rfindOpt fun x => if c.evaln x.unpair.1 x.unpair.2 = some y then some () else none).Dom := by
    apply Partrec.dom_re
    apply Partrec.rfindOpt
    exact (Primrec.ite (evaln_eq_some_prim c) (.const _) (.const _)).to_comp
  apply this.of_eq
  intro y
  rw [Nat.rfindOpt_dom, ← hc]
  constructor
  · intro ⟨x, (), hx⟩
    have h : y ∈ c.evaln x.unpair.1 x.unpair.2 := by simpa using hx
    use x.unpair.2
    exact Code.evaln_sound h
  · intro ⟨x, hx⟩
    rw [Code.evaln_complete] at hx
    obtain ⟨k, hk⟩ := hx
    use Nat.pair k x, ()
    simpa using hk

[Janitha Aswedige]

@Matt Diamond Thanks this is neat. What I originally wanted to prove is that the image of a C.E. predicate under a partial computable function is C.E. Thought this theorem would help. Now I'm trying to figure that out.