OracleEnumerationNormalForm.lean

1 import RealizationBoundaries.ComputableQuotientCodes
2 import RealizationBoundaries.OraclePartialRecursionTraces
3 import RealizationBoundaries.OraclePartialMinimizationTraces
4 import Mathlib.Data.List.OfFn
5 
6 /-! # Finite witnesses for native oracle recursion -/
7 set_option autoImplicit false
8 set_option backward.isDefEq.respectTransparency false
9 noncomputable section
10 namespace RealizationBoundaries
11 
12 namespace OracleComputable
13 variable {X : ℕ → Bool} {f g : ℕ → ℕ}
14 
15 theorem eqFail (hf : OracleComputable X f) (hg : OracleComputable X g) :
16     OracleComputable X (fun n => if f n = g n then 0 else 1) := by
17   have hl : Primrec (fun k : ℕ => k.unpair.1) := Primrec.fst.comp Primrec.unpair
18   have hr : Primrec (fun k : ℕ => k.unpair.2) := Primrec.snd.comp Primrec.unpair
19   have he : Computable (fun k : ℕ => if k.unpair.1 = k.unpair.2 then 0 else 1) :=
20     (Primrec.ite (Primrec.eq.comp hl hr) (Primrec.const 0) (Primrec.const 1)).to_comp
21   exact (of_computable he).comp (hf.pair hg) |>.of_eq (fun k => by simp)
22 
23 /-- A finite sum of total oracle tests. -/
24 def boundedSum (test : ℕ → ℕ) (a n : ℕ) : ℕ :=
25   Nat.rec 0 (fun m r => r + test (Nat.pair a m)) n
26 
27 theorem boundedSum_computable (ht : OracleComputable X f) :
28     OracleComputable X (fun k => boundedSum f k.unpair.1 k.unpair.2) := by
29   have he := ht.comp (left.pair (left.comp right))
30   exact prec (step := fun a m r => r + f (Nat.pair a m)) (const 0)
31     ((right.comp right).add he)
32 
33 theorem boundedSum_zero_iff (test : ℕ → ℕ) (a n : ℕ) :
34     boundedSum test a n = 0 ↔ ∀ m < n, test (Nat.pair a m) = 0 := by
35   induction n with
36   | zero => simp [boundedSum]
37   | succ n ih =>
38     change boundedSum test a n + test (Nat.pair a n) = 0 ↔ _
39     rw [Nat.add_eq_zero_iff, ih]
40     constructor
41     · rintro ⟨h, hn⟩ m hm
42       rcases Nat.lt_succ_iff_lt_or_eq.mp hm with hm | rfl
43       · exact h m hm
44       · exact hn
45     · intro h
46       exact ⟨fun m hm => h m (Nat.lt_succ_of_lt hm), h n (Nat.lt_succ_self n)⟩
47 
48 end OracleComputable
49 
50 /-- A total oracle-computable finite witness verifier for the graph of a partial
51 function. A successful witness is a natural number, not an oracle for the graph. -/
52 structure OracleGraphSearch (X : ℕ → Bool) (f : ℕ →. ℕ) where
53   test : ℕ → ℕ
54   computable : OracleComputable X test
55   correct : ∀ n y, y ∈ f n ↔ ∃ t, test (Nat.pair n (Nat.pair y t)) = 0
56 
57 namespace OracleGraphSearch
58 variable {X : ℕ → Bool} {f g : ℕ →. ℕ}
59 
60 abbrev inp (k : ℕ) : ℕ := k.unpair.1
61 abbrev out (k : ℕ) : ℕ := k.unpair.2.unpair.1
62 abbrev wit (k : ℕ) : ℕ := k.unpair.2.unpair.2
63 
64 theorem comp_inp : OracleComputable X inp := OracleComputable.left
65 
66 theorem comp_out : OracleComputable X out :=
67   OracleComputable.left.comp OracleComputable.right
68 
69 theorem comp_wit : OracleComputable X wit :=
70   OracleComputable.right.comp OracleComputable.right
71 
72 /-- Total oracle functions have a trivial finite graph verifier. -/
73 def of_total (q : ℕ → ℕ) (hq : OracleComputable X q) :
74     OracleGraphSearch X (fun n => Part.some (q n)) where
75   test := fun k => if q (inp k) = out k then 0 else 1
76   computable := (hq.comp comp_inp).eqFail comp_out
77   correct := by intro n y; simp [inp, out, eq_comm]
78 
79 /-- Pairing combines two finite witness verifiers. -/
80 def pair (sf : OracleGraphSearch X f) (sg : OracleGraphSearch X g) :
81     OracleGraphSearch X (fun n => (f n).bind (fun u => (g n).map (Nat.pair u))) where
82   test := fun k => sf.test (Nat.pair (inp k) (Nat.pair (out k).unpair.1 (wit k).unpair.1)) +
83     sg.test (Nat.pair (inp k) (Nat.pair (out k).unpair.2 (wit k).unpair.2))
84   computable := by
85     exact (sf.computable.comp (comp_inp.pair
86       ((OracleComputable.left.comp comp_out).pair (OracleComputable.left.comp comp_wit)))).add
87       (sg.computable.comp (comp_inp.pair
88         ((OracleComputable.right.comp comp_out).pair (OracleComputable.right.comp comp_wit))))
89   correct := by
90     intro n y
91     simp only [Part.mem_bind_iff, Part.mem_map_iff]
92     constructor
93     · rintro ⟨u, hu, v, hv, hy⟩
94       obtain ⟨tf, htf⟩ := (sf.correct n u).mp hu
95       obtain ⟨tg, htg⟩ := (sg.correct n v).mp hv
96       subst y
97       exact ⟨Nat.pair tf tg, by simp [inp, out, wit, htf, htg]⟩
98     · rintro ⟨t, ht⟩
99       have hh : sf.test (Nat.pair n (Nat.pair y.unpair.1 t.unpair.1)) = 0 ∧
100           sg.test (Nat.pair n (Nat.pair y.unpair.2 t.unpair.2)) = 0 := by
101         simpa [inp, out, wit] using ht
102       exact ⟨y.unpair.1, (sf.correct n _).mpr ⟨t.unpair.1, hh.1⟩,
103         y.unpair.2, (sg.correct n _).mpr ⟨t.unpair.2, hh.2⟩, Nat.pair_unpair y⟩
104 
105 /-- Composition stores the intermediate result and both child certificates. -/
106 def comp (sf : OracleGraphSearch X f) (sg : OracleGraphSearch X g) :
107     OracleGraphSearch X (fun n => (g n).bind f) where
108   test := fun k => sg.test (Nat.pair (inp k)
109       (Nat.pair (wit k).unpair.1 (wit k).unpair.2.unpair.1)) +
110     sf.test (Nat.pair (wit k).unpair.1 (Nat.pair (out k) (wit k).unpair.2.unpair.2))
111   computable := by
112     have hm : OracleComputable X (fun k => (wit k).unpair.1) := OracleComputable.left.comp comp_wit
113     have htf : OracleComputable X (fun k => (wit k).unpair.2.unpair.2) :=
114       OracleComputable.right.comp (OracleComputable.right.comp comp_wit)
115     have htg : OracleComputable X (fun k => (wit k).unpair.2.unpair.1) :=
116       OracleComputable.left.comp (OracleComputable.right.comp comp_wit)
117     exact (sg.computable.comp (comp_inp.pair (hm.pair htg))).add
118       (sf.computable.comp (hm.pair (comp_out.pair htf)))
119   correct := by
120     intro n y
121     rw [Part.mem_bind_iff]
122     constructor
123     · rintro ⟨m, hm, hy⟩
124       obtain ⟨tg, htg⟩ := (sg.correct n m).mp hm
125       obtain ⟨tf, htf⟩ := (sf.correct m y).mp hy
126       exact ⟨Nat.pair m (Nat.pair tg tf), by simp [inp, out, wit, htg, htf]⟩
127     · rintro ⟨t, ht⟩
128       have hh : sg.test (Nat.pair n (Nat.pair t.unpair.1 t.unpair.2.unpair.1)) = 0 ∧
129           sf.test (Nat.pair t.unpair.1 (Nat.pair y t.unpair.2.unpair.2)) = 0 := by
130         simpa [inp, out, wit] using ht
131       exact ⟨t.unpair.1, (sg.correct _ _).mpr ⟨_, hh.1⟩,
132         (sf.correct _ _).mpr ⟨_, hh.2⟩⟩
133 
134 /-- Natural decoding of a finite list of paired state/certificate entries. -/
135 def traceList (t : ℕ) : List ℕ := (Encodable.decode t).getD []
136 
137 def traceEntry (t i : ℕ) : ℕ := (traceList t).getD i 0
138 
139 def traceState (t i : ℕ) : ℕ := (traceEntry t i).unpair.1
140 
141 def traceProof (t i : ℕ) : ℕ := (traceEntry t i).unpair.2
142 
143 theorem primrec_traceList : Primrec traceList :=
144   Primrec.option_getD.comp Primrec.decode (Primrec.const [])
145 
146 theorem primrec_traceEntry : Primrec₂ traceEntry :=
147   (Primrec.list_getD 0).comp (primrec_traceList.comp Primrec.fst) Primrec.snd
148 
149 theorem primrec_traceState : Primrec₂ traceState :=
150   ((Primrec.fst.comp Primrec.unpair).comp primrec_traceEntry)
151 
152 theorem primrec_traceProof : Primrec₂ traceProof :=
153   ((Primrec.snd.comp Primrec.unpair).comp primrec_traceEntry)
154 
155 theorem finiteTrace_exists (states proofs : ℕ → ℕ) (N : ℕ) :
156     ∃ t, ∀ i < N, traceState t i = states i ∧ traceProof t i = proofs i := by
157   refine ⟨Encodable.encode (List.ofFn (fun i : Fin N => Nat.pair (states i) (proofs i))), ?_⟩
158   intro i hi
159   simp [traceState, traceProof, traceEntry, traceList, List.getD_eq_getElem?_getD, hi]
160 
161 theorem primrec_inp : Primrec inp := Primrec.fst.comp Primrec.unpair
162 
163 theorem primrec_out : Primrec out :=
164   (Primrec.fst.comp Primrec.unpair).comp (Primrec.snd.comp Primrec.unpair)
165 
166 theorem primrec_wit : Primrec wit :=
167   (Primrec.snd.comp Primrec.unpair).comp (Primrec.snd.comp Primrec.unpair)
168 
169 theorem primrec_triple {a b c : ℕ → ℕ} (ha : Primrec a) (hb : Primrec b) (hc : Primrec c) :
170     Primrec (fun k => Nat.pair (a k) (Nat.pair (b k) (c k))) :=
171   Primrec₂.natPair.comp ha (Primrec₂.natPair.comp hb hc)
172 
173 def recBaseCode (k : ℕ) : ℕ :=
174   Nat.pair (inp k).unpair.1 (Nat.pair (traceState (wit k) 0) (traceProof (wit k) 0))
175 
176 def recStepCode (z : ℕ) : ℕ :=
177   let k := z.unpair.1
178   let i := z.unpair.2
179   Nat.pair (Nat.pair (inp k).unpair.1 (Nat.pair i (traceState (wit k) i)))
180     (Nat.pair (traceState (wit k) (i+1)) (traceProof (wit k) (i+1)))
181 
182 theorem primrec_recBaseCode : Primrec recBaseCode :=
183   primrec_triple ((Primrec.fst.comp Primrec.unpair).comp primrec_inp)
184     (primrec_traceState.comp primrec_wit (Primrec.const 0))
185     (primrec_traceProof.comp primrec_wit (Primrec.const 0))
186 
187 theorem primrec_recStepCode : Primrec recStepCode := by
188   have hl : Primrec (fun z : ℕ => z.unpair.1) := Primrec.fst.comp Primrec.unpair
189   have hr : Primrec (fun z : ℕ => z.unpair.2) := Primrec.snd.comp Primrec.unpair
190   have ha := hl.comp (primrec_inp.comp hl)
191   have ht := primrec_wit.comp hl
192   exact primrec_triple (primrec_triple ha hr (primrec_traceState.comp ht hr))
193     (primrec_traceState.comp ht (Primrec.succ.comp hr))
194     (primrec_traceProof.comp ht (Primrec.succ.comp hr))
195 
196 def recTest (sf : OracleGraphSearch X f) (sg : OracleGraphSearch X g) (k : ℕ) : ℕ :=
197   sf.test (recBaseCode k) +
198     OracleComputable.boundedSum (fun z => sg.test (recStepCode z)) k (inp k).unpair.2 +
199       if traceState (wit k) (inp k).unpair.2 = out k then 0 else 1
200 
201 theorem recTest_computable (sf : OracleGraphSearch X f) (sg : OracleGraphSearch X g) :
202     OracleComputable X (recTest sf sg) := by
203   have hb := sf.computable.comp (OracleComputable.of_computable primrec_recBaseCode.to_comp)
204   have hs := sg.computable.comp (OracleComputable.of_computable primrec_recStepCode.to_comp)
205   have hn : Primrec (fun k => (inp k).unpair.2) :=
206     (Primrec.snd.comp Primrec.unpair).comp primrec_inp
207   have ht := (OracleComputable.boundedSum_computable hs).comp
208     (OracleComputable.id.pair (OracleComputable.of_computable hn.to_comp))
209   have he : OracleComputable X (fun k => if traceState (wit k) (inp k).unpair.2 = out k then 0 else 1) :=
210     (OracleComputable.of_computable
211       (primrec_traceState.comp primrec_wit hn).to_comp).eqFail comp_out
212   exact (hb.add ht).add he |>.of_eq (fun k => by simp [recTest])
213 
214 theorem recTest_correct (sf : OracleGraphSearch X f) (sg : OracleGraphSearch X g)
215     (a n y t : ℕ) : recTest sf sg (Nat.pair (Nat.pair a n) (Nat.pair y t)) = 0 ↔
216       sf.test (Nat.pair a (Nat.pair (traceState t 0) (traceProof t 0))) = 0 ∧
217       (∀ i < n, sg.test (Nat.pair (Nat.pair a (Nat.pair i (traceState t i)))
218         (Nat.pair (traceState t (i+1)) (traceProof t (i+1)))) = 0) ∧ traceState t n = y := by
219   simp [recTest, recBaseCode, recStepCode, inp, out, wit,
220     OracleComputable.boundedSum_zero_iff, and_assoc]
221 
222 /-- Primitive recursion is verified by a finite trace of child computations. -/
223 def prec (sf : OracleGraphSearch X f) (sg : OracleGraphSearch X g) :
224     OracleGraphSearch X (fun p => oraclePartialRec f g p.unpair.1 p.unpair.2) where
225   test := recTest sf sg
226   computable := recTest_computable sf sg
227   correct := by
228     intro p y
229     have hp := Nat.pair_unpair p
230     conv_lhs => rw [← hp]
231     conv_rhs => rw [← hp]
232     simp only [Nat.unpair_pair]
233     rw [oraclePartialRec_mem_iff_trace]
234     constructor
235     · rintro ⟨states, hlast, hb, hs⟩
236       obtain ⟨b, hbase⟩ := (sf.correct _ _).mp hb
237       have hh : ∀ i, ∃ c, i < p.unpair.2 →
238           sg.test (Nat.pair (Nat.pair p.unpair.1 (Nat.pair i (states i)))
239             (Nat.pair (states (i+1)) c)) = 0 := by
240         intro i
241         by_cases hi : i < p.unpair.2
242         · obtain ⟨c, hc⟩ := (sg.correct _ _).mp (hs i hi)
243           exact ⟨c, fun _ => hc⟩
244         · exact ⟨0, fun h => False.elim (hi h)⟩
245       choose cs hcs using hh
246       let proofs := fun i => if i = 0 then b else cs (i-1)
247       obtain ⟨t, ht⟩ := finiteTrace_exists states proofs (p.unpair.2+1)
248       refine ⟨t, (recTest_correct sf sg _ _ _ _).mpr ?_⟩
249       have h0 := ht 0 (Nat.zero_lt_succ _)
250       have hn := ht p.unpair.2 (Nat.lt_succ_self _)
251       refine ⟨?_, ?_, hn.1.trans hlast⟩
252       · simpa [h0.1, h0.2, proofs] using hbase
253       · intro i hi
254         have hi0 := ht i (Nat.lt_succ_of_lt hi)
255         have hi1 := ht (i+1) (Nat.succ_lt_succ hi)
256         simpa [hi0.1, hi1.1, hi1.2, proofs] using hcs i hi
257     · rintro ⟨t, ht⟩
258       obtain ⟨hb, hs, hlast⟩ := (recTest_correct sf sg _ _ _ _).mp ht
259       refine ⟨traceState t, hlast, (sf.correct _ _).mpr ⟨_, hb⟩, ?_⟩
260       intro i hi
261       exact (sg.correct _ _).mpr ⟨_, hs i hi⟩
262 
263 def minStepCode (z : ℕ) : ℕ :=
264   let k := z.unpair.1
265   let i := z.unpair.2
266   Nat.pair (Nat.pair (inp k) i) (Nat.pair (traceState (wit k) i) (traceProof (wit k) i))
267 
268 def minNonzeroTest (z : ℕ) : ℕ :=
269   if traceState (wit z.unpair.1) z.unpair.2 = 0 then 1 else 0
270 
271 theorem primrec_minStepCode : Primrec minStepCode := by
272   have hl : Primrec (fun z : ℕ => z.unpair.1) := Primrec.fst.comp Primrec.unpair
273   have hr : Primrec (fun z : ℕ => z.unpair.2) := Primrec.snd.comp Primrec.unpair
274   have ht := primrec_wit.comp hl
275   exact primrec_triple (Primrec₂.natPair.comp (primrec_inp.comp hl) hr)
276     (primrec_traceState.comp ht hr) (primrec_traceProof.comp ht hr)
277 
278 theorem primrec_minNonzeroTest : Primrec minNonzeroTest := by
279   have hl : Primrec (fun z : ℕ => z.unpair.1) := Primrec.fst.comp Primrec.unpair
280   have hr : Primrec (fun z : ℕ => z.unpair.2) := Primrec.snd.comp Primrec.unpair
281   exact Primrec.ite (Primrec.eq.comp
282     (primrec_traceState.comp (primrec_wit.comp hl) hr) (Primrec.const 0))
283     (Primrec.const 1) (Primrec.const 0)
284 
285 def minTest (sf : OracleGraphSearch X f) (k : ℕ) : ℕ :=
286   OracleComputable.boundedSum (fun z => sf.test (minStepCode z)) k (out k+1) +
287     OracleComputable.boundedSum minNonzeroTest k (out k) + traceState (wit k) (out k)
288 
289 theorem minTest_computable (sf : OracleGraphSearch X f) :
290     OracleComputable X (minTest sf) := by
291   have hs : OracleComputable X (fun z => sf.test (minStepCode z)) :=
292     sf.computable.comp (OracleComputable.of_computable primrec_minStepCode.to_comp)
293   have hc : OracleComputable X (fun k =>
294       OracleComputable.boundedSum (fun z => sf.test (minStepCode z)) k (out k+1)) := by
295     exact ((OracleComputable.boundedSum_computable hs).comp
296       (OracleComputable.id.pair
297         (OracleComputable.of_computable (Primrec.succ.comp primrec_out).to_comp))).of_eq
298           (fun k => by simp)
299   have hp : OracleComputable X minNonzeroTest :=
300     OracleComputable.of_computable primrec_minNonzeroTest.to_comp
301   have hn : OracleComputable X (fun k =>
302       OracleComputable.boundedSum minNonzeroTest k (out k)) := by
303     exact ((OracleComputable.boundedSum_computable hp).comp
304       (OracleComputable.id.pair comp_out)).of_eq (fun k => by simp)
305   have hz : OracleComputable X (fun k => traceState (wit k) (out k)) :=
306     OracleComputable.of_computable (primrec_traceState.comp primrec_wit primrec_out).to_comp
307   exact (hc.add hn).add hz
308 
309 theorem minTest_correct (sf : OracleGraphSearch X f) (a y t : ℕ) :
310     minTest sf (Nat.pair a (Nat.pair y t)) = 0 ↔
311       (∀ i ≤ y, sf.test (Nat.pair (Nat.pair a i)
312         (Nat.pair (traceState t i) (traceProof t i))) = 0) ∧
313       (∀ i < y, traceState t i ≠ 0) ∧ traceState t y = 0 := by
314   simp [minTest, minStepCode, minNonzeroTest, inp, out, wit,
315     OracleComputable.boundedSum_zero_iff, and_assoc]
316 
317 /-- Native minimization is certified by all earlier defined nonzero child
318 outputs and the final zero, verified on one finite trace. -/
319 def rfind (sf : OracleGraphSearch X f) :
320     OracleGraphSearch X (fun a => Nat.rfind
321       (fun i => (fun m => decide (m = 0)) <$> f (Nat.pair a i))) where
322   test := minTest sf
323   computable := minTest_computable sf
324   correct := by
325     intro a y
326     rw [oracle_partial_minimization_trace]
327     constructor
328     · rintro ⟨states, hlast, hs, hn⟩
329       have hh : ∀ i, ∃ c, i ≤ y →
330           sf.test (Nat.pair (Nat.pair a i) (Nat.pair (states i) c)) = 0 := by
331         intro i
332         by_cases hi : i ≤ y
333         · obtain ⟨c, hc⟩ := (sf.correct _ _).mp (hs i hi)
334           exact ⟨c, fun _ => hc⟩
335         · exact ⟨0, fun h => False.elim (hi h)⟩
336       choose proofs hproofs using hh
337       obtain ⟨t, ht⟩ := finiteTrace_exists states proofs (y+1)
338       refine ⟨t, (minTest_correct sf _ _ _).mpr ⟨?_, ?_, ?_⟩⟩
339       · intro i hi
340         have hti := ht i (Nat.lt_succ_iff.mpr hi)
341         simpa [hti.1, hti.2] using hproofs i hi
342       · intro i hi
343         rw [(ht i (Nat.lt_succ_of_lt hi)).1]
344         exact hn i hi
345       · exact (ht y (Nat.lt_succ_self _)).1.trans hlast
346     · rintro ⟨t, ht⟩
347       obtain ⟨hs, hn, hlast⟩ := (minTest_correct sf _ _ _).mp ht
348       refine ⟨traceState t, hlast, ?_, hn⟩
349       intro i hi
350       exact (sf.correct _ _).mpr ⟨_, hs i hi⟩
351 
352 /-- Transport of an exact graph verifier across pointwise equality. -/
353 def of_eq (sf : OracleGraphSearch X f) (h : ∀ n, f n = g n) : OracleGraphSearch X g where
354   test := sf.test
355   computable := sf.computable
356   correct := by intro n y; rw [← h n]; exact sf.correct n y
357 
358 end OracleGraphSearch
359 
360 theorem part_pair_bind_eq (a b : Part ℕ) :
361     a.bind (fun u => b.map (Nat.pair u)) = Nat.pair <$> a <*> b := by
362   rw [seq_eq_bind_map]
363   change a.bind (fun u => b.map (Nat.pair u)) = (a.map Nat.pair).bind (fun v => b.map v)
364   rw [Part.bind_map]
365 
366 /-- Every native oracle-recursive partial function has a total oracle-computable
367 finite graph witness verifier. The proof follows every primitive-recursion and
368 minimization constructor; no relativized normal form is assumed. -/
369 theorem recursiveIn_has_graphSearch (X : ℕ → Bool) (f : ℕ →. ℕ)
370     (hf : Nat.RecursiveIn {selectorOracle X} f) : Nonempty (OracleGraphSearch X f) := by
371   induction hf with
372   | zero => exact ⟨OracleGraphSearch.of_total (fun _ => 0) (OracleComputable.const 0)⟩
373   | succ => exact ⟨OracleGraphSearch.of_total Nat.succ
374       (OracleComputable.of_computable Computable.succ)⟩
375   | left => exact ⟨OracleGraphSearch.of_total _ OracleComputable.left⟩
376   | right => exact ⟨OracleGraphSearch.of_total _ OracleComputable.right⟩
377   | oracle g hg =>
378     have he : g = selectorOracle X := Set.mem_singleton_iff.mp hg
379     subst g
380     exact ⟨OracleGraphSearch.of_total _ OracleComputable.oracle⟩
381   | pair _ _ ihf ihg =>
382     obtain ⟨sf⟩ := ihf
383     obtain ⟨sg⟩ := ihg
384     refine ⟨(sf.pair sg).of_eq ?_⟩
385     intro n
386     exact part_pair_bind_eq _ _
387   | comp _ _ ihf ihg =>
388     obtain ⟨sf⟩ := ihf
389     obtain ⟨sg⟩ := ihg
390     exact ⟨sf.comp sg⟩
391   | prec _ _ ihf ihg =>
392     obtain ⟨sf⟩ := ihf
393     obtain ⟨sg⟩ := ihg
394     exact ⟨sf.prec sg⟩
395   | rfind _ ihf =>
396     obtain ⟨sf⟩ := ihf
397     exact ⟨sf.rfind⟩
398 
399 /-- Native partial-oracle-domain enumerability has an explicit total searchable
400 stage test. This closes the semantics gap between the domain and listing APIs. -/
401 theorem oracleEnumerable_has_total_search (X : ℕ → Bool) (A : Set ℕ)
402     (hA : OracleEnumerable X A) :
403     ∃ test : ℕ → ℕ, OracleComputable X test ∧
404       ∀ n, n ∈ A ↔ ∃ t, test (Nat.pair n t) = 0 := by
405   obtain ⟨f, hf, hdom⟩ := hA
406   obtain ⟨s⟩ := recursiveIn_has_graphSearch X f hf
407   refine ⟨s.test, s.computable, ?_⟩
408   intro n
409   rw [← hdom]
410   constructor
411   · intro hn
412     obtain ⟨y, hy⟩ := Part.dom_iff_mem.mp hn
413     obtain ⟨t, ht⟩ := (s.correct n y).mp hy
414     exact ⟨Nat.pair y t, ht⟩
415   · rintro ⟨t, ht⟩
416     apply Part.dom_iff_mem.mpr
417     refine ⟨t.unpair.1, (s.correct n _).mpr ⟨t.unpair.2, ?_⟩⟩
418     simpa only [Nat.pair_unpair] using ht
419 
420 end RealizationBoundaries

Back to source controls