English
A constructive expression of Nat.casesOn on data produced by a computable function yields a partial recursion.
Русский
Конструктивно выражается Nat.casesOn на данных, полученных вычислимой функцией, что даёт частичную рекурсию.
LaTeX
$$$\forall f,g,h,\Computable(f) \land \Computable(g) \land \Partrec_2(h) \Rightarrow Partrec(\lambda a. Nat.casesOn (f(a)) (Part.some (g(a))) (h(a))).$$
Lean4
theorem nat_casesOn_right {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ} (hf : Computable f) (hg : Computable g)
(hh : Partrec₂ h) : Partrec fun a => (f a).casesOn (some (g a)) (h a) :=
(nat_rec hf hg (hh.comp fst (pred.comp <| hf.comp fst)).to₂).of_eq fun a =>
by
simp only [PFun.coe_val, Nat.pred_eq_sub_one]; rcases f a with - | n <;> simp
refine ext fun b => ⟨fun H => ?_, fun H => ?_⟩
· rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩
exact h₂
· have : ∀ m, (Nat.rec (motive := fun _ => Part σ) (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom :=
by
intro m
induction m <;> simp [*, H.fst]
exact ⟨⟨this n, H.fst⟩, H.snd⟩
