Making a classical Lean tree construction oracle-computable: codes via Code.curry
To show a forcing construction (trees T_s, each proved Computable separately) is computable from an oracle like ∅″, give each tree a Mathlib Code. Rewrite each tree operation as a Part-valued function of a code c for the old tree, using Nat.rfind where the original used Nat.find, and prove Partrec in (params, σ). Then Code.exists_code + Code.curry k (encode params) gives a primrec map on codes. The evaluation lemma is eval (curry k (encode a)) (encode σ) = (F (a, σ)).map encode, by rw [eval_curry, hk, show Nat.pair (encode a) (encode σ) = encode (a, σ) from rfl]; simp [encodek]. Prove that the partial version equals the classical one when the code computes a total tree. Make the classical choices canonical (Nat.find over codes instead of Classical.choose) so the oracle can reproduce them. For Σ₂ questions over partial functions, use (Nat.rfind fun _ => p).Dom ↔ true ∈ p to turn 'true ∈ p' into a domain question, then evaln. An 'ask E, then rfind with test (answer = no) ∨ K n k' lemma computes dite/Nat.find steps from the oracle.
Checked on Mathlib v4.35.0: the iff
(Nat.rfind fun _ => p).Dom ↔ true ∈ p(p : Part Bool) holds, butexact?does not find it. This compiles:example (p : Part Bool) : (Nat.rfind fun _ => p).Dom ↔ true ∈ p := by constructor · intro h; exact Nat.rfind_spec (Part.get_mem h) · intro h; exact Nat.rfind_dom'.2 ⟨0, h, fun _ => Part.dom_iff_mem.2 ⟨_, h⟩⟩Code.eval_curryhas the shape you use:(c.curry n).eval x = c.eval (Nat.pair n x).