Computing codes of primitive recursive functions

Stream: general

[Andrej Bauer]

I am trying to wrap my head around `Mathlib.Computability.PartrecCode. In particular, I would like to define codes of the combinators K and S. Let's consider K, which is easier. Intuitively, K is the primitive recursive function which takes a number n and outputs the number encoding Code.const n. It feels like PartrecCode should have the ability to do this. (We need a Batman-style signal for @Mario Carneiro)

[Andrej Bauer]

I think I want Mathlib.Computability.Code.exists_code but with a dependent sum instead of the existential, except that this is not the sort of thing I can hope to get, becuse it would give canonical codes of partial computable maps.

[Andrej Bauer]

It looks like I could show that there exists a code for the K combinator, but it won't let me actually compute the code – which is kind of funny, because the "correct" definition of a PCA asks for existence of K and S, rather than concrete instances of them.

[Andrej Bauer]

Is there some noncomputable trickery that would allow me to derive from ∃ x : A, p x an element a : A and a proof of p a?

[Edward van de Meent]

docs#Exists.choose and docs#Exists.choose_spec

[Edward van de Meent]

if you're doing things with Nat, docs#Nat.find might also be among your interests (as it is computable)

[Andrej Bauer]

Unfortunately no, the predicates involved are Π⁰₁ (namely that a number is the Godel code of a partial recursive map).

[Edward van de Meent]

actually, if this just concerns a proof, just using the obtain tactic should be sufficient

[Mario Carneiro]

@Andrej Bauer (the batmobile is in the shop, sorry for the delay) You seem to have found the answer already, but docs#Nat.Partrec.Code.const_prim is the theorem you are looking for, except that as you point out it is a mere existence statement. You could copy and paste it to construct the Code though. Another possibility is to refactor things so that most of the primrec theorems are data-carrying. I think at the time I reasoned that it's better not to use defs for primrec proofs because the concrete definitions are not at all good computationally and I didn't want to have to think about that

[Mario Carneiro]

but basically all of them are explicit constructive proofs so it's easy enough to refactor them to get witnesses as needed