Semideciders on encoded values, not only on bit strings

MIPRE.Cost.exists_semidecider turns a recursively enumerable predicate on bit strings into a program of the ambient model halting on encode x exactly when the predicate holds. The obligation MIPRE.Halting.Obligations.sem_spec needs it on pairs: a program halting on encode (x, n) exactly off the class B at level n. The difference is not cosmetic — encode (x, n) is cons (encode x) (encode n), which is not the encoding of any bit string — and it cannot be arranged by choosing the predicate, since the criterion consumes the equivalence in both directions.

exists_semidecider_of_decode closes the gap once and for all, for every type whose SizedEncoding can be decoded primitive recursively: prefix the bit-string semidecider with Prog.serProg, the program that writes the postorder serialization of its input (Halting/Serial.lean). Serialization and Data.parse invert each other (Data.parse_toBitsPost), so the composite halts on encode a exactly when the bit-string semidecider halts on the serialization of encode a, which is where the predicate is read back. exists_semidecider_prod_nat is the instance the obligation asks for, and primrec_decode_prod_nat the decoding it needs.

The route through a serialization rather than a direct encoding is what keeps the ToPartrec translation of Cost/Semidecide.lean untouched: a ToPartrec code cannot see trailing zeros of its input list, which is why that file exists in the shape it does, and nothing here re-enters that argument.

Decoding a pair of a bit string and a number

theorem MIPRE.Cost.Data.decode_prod_cons {α : Type u_1} {β : Type u_2} [SizedEncoding α] [SizedEncoding β] (a b : Data) : decode (a.cons b) = match decode a, decode b with | some x, some y => some (x, y) | x, x_1 => none

The decoding of a pair out of a cons, spelled out.

theorem MIPRE.Cost.Data.primrec_decode_prod_nat : Primrec fun (d : Data) => decode d

The decoding of BitStr × ℕ out of data is primitive recursive: a pair is a cons, and its two components decode by Data.primrec_decode_bitStr and Data.primrec_decode_nat.

The semidecider

theorem MIPRE.Cost.exists_semidecider_of_decode {α : Type u_1} [SizedEncoding α] [Primcodable α] [Inhabited α] (hdec : Primrec fun (d : Data) => decode d) {p : α → Prop} (hp : REPred p) : ∃ (S : Prog), Prog.WellScoped 1 S ∧ ∀ (a : α), Halts S (encode a) ↔ p a

Recursively enumerable predicates on encoded values are halting sets. For a type whose encoding decodes primitive recursively and an r.e. predicate p on it, a well-scoped program halting on encode a exactly when p a: Cost.exists_semidecider with the input serialized by Prog.serProg first.

theorem MIPRE.Cost.exists_semidecider_prod_nat {p : BitStr → ℕ → Prop} (hp : REPred fun (q : BitStr × ℕ) => p q.1 q.2) : ∃ (S : Prog), Prog.WellScoped 1 S ∧ ∀ (x : BitStr) (n : ℕ), Halts S (encode (x, n)) ↔ p x n

The instance obligation O3 asks for: an r.e. predicate on (string, level) pairs is the halting set of a well-scoped program on encode (x, n).