computable_pred and primcodable ℚ

Stream: Is there code for X?

[Keji Neri]

I was wondering if anyone had proved an analogous result to 'primrec_pred.comp' for computable_pred (I tried but I keep running into decidability problems). Also, why isn't the definition of 'computable_pred' the same as 'primrec_pred' but replacing 'primrec' with 'computable' everywhere? Lastly, I was wondering if anyone has shown primcodable ℚ, or done anything about computable functions on the rationals?

[Gabriel Ebner]

primrec_pred and computable_pred are almost identical. The only difference is that one of them bundles the decidable_pred instance, the other one doesn't. But it doesn't make a difference since that instance is a singleton anyhow.

[Gabriel Ebner]

To prove primrec_pred.comp you can use casesI to access the type class instance:

import computability.halting

namespace computability

variables {α β : Type*} [primcodable α] [primcodable β]

theorem computable_pred.comp {p : β → Prop} {f : α → β}
  (hp : computable_pred p) (hf : computable f) : computable_pred (λ x, p (f x)) :=
begin
  casesI hp,
  refine ⟨by apply_instance, _⟩,
  -- ....
end

[Keji Neri]

Thank you very much @Gabriel Ebner