refactor: make Nat.Partrec protected (#33891)

`Nat.Primrec` is protected to avoid confusion with `Primrec`, but `Nat.Partrec` is not.
Furthermore, `Nat.Partrec` is a definition in recursion theory, so frequently used under `open Nat`, and as it is an auxiliary definition of `Partrec`, confusion is particularly problematic.
In this PR, we make `Nat.Partrec` protected.

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

Mathlib/Computability/Halting.lean

@@ -305,7 +305,7 @@ open List.Vector Partrec Computable
 
 open Nat.Partrec'
 
-theorem to_part {n f} (pf : @Partrec' n f) : _root_.Partrec f := by
+theorem to_part {n f} (pf : @Partrec' n f) : Partrec f := by
   induction pf with
   | prim hf => exact hf.to_prim.to_comp
   | comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
@@ -390,7 +390,7 @@ theorem rfindOpt {n} {f : List.Vector ℕ (n + 1) → ℕ} (hf : @Partrec' (n +
 
 open Nat.Partrec.Code
 
-theorem of_part : ∀ {n f}, _root_.Partrec f → @Partrec' n f :=
+theorem of_part : ∀ {n f}, Partrec f → @Partrec' n f :=
   @(suffices ∀ f, Nat.Partrec f → @Partrec' 1 fun v => f v.head from fun {n f} hf => by
       let g := fun n₁ =>
         (Part.ofOption (decode (α := List.Vector ℕ n) n₁)).bind (fun a => Part.map encode (f a))
@@ -407,10 +407,10 @@ theorem of_part : ∀ {n f}, _root_.Partrec f → @Partrec' n f :=
               (Primrec.vector_head.pair (_root_.Primrec.const c)).pair <|
                 Primrec.vector_head.comp Primrec.vector_tail)
 
-theorem part_iff {n f} : @Partrec' n f ↔ _root_.Partrec f :=
+theorem part_iff {n f} : @Partrec' n f ↔ Partrec f :=
   ⟨to_part, of_part⟩
 
-theorem part_iff₁ {f : ℕ →. ℕ} : (@Partrec' 1 fun v => f v.head) ↔ _root_.Partrec f :=
+theorem part_iff₁ {f : ℕ →. ℕ} : (@Partrec' 1 fun v => f v.head) ↔ Partrec f :=
   part_iff.trans
     ⟨fun h =>
       (h.comp <| (Primrec.vector_ofFn fun _ => _root_.Primrec.id).to_comp).of_eq fun v => by

Mathlib/Computability/Partrec.lean

@@ -156,27 +156,29 @@ theorem rfindOpt_mono {α} {f : ℕ → Option α} (H : ∀ {a m n}, m ≤ n →
     have := (H (le_max_left _ _) h).symm.trans (H (le_max_right _ _) hk)
     simp at this; simp [this, get_mem]⟩
 
-/-- `Partrec f` means that the partial function `f : ℕ →. ℕ` is partially recursive. -/
-inductive Partrec : (ℕ →. ℕ) → Prop
-  | zero : Partrec (pure 0)
-  | succ : Partrec succ
-  | left : Partrec ↑fun n : ℕ => n.unpair.1
-  | right : Partrec ↑fun n : ℕ => n.unpair.2
-  | pair {f g} : Partrec f → Partrec g → Partrec fun n => pair <$> f n <*> g n
-  | comp {f g} : Partrec f → Partrec g → Partrec fun n => g n >>= f
-  | prec {f g} : Partrec f → Partrec g → Partrec (unpaired fun a n =>
+/-- `Nat.Partrec f` means that the partial function `f : ℕ →. ℕ` is partially recursive. -/
+protected inductive Partrec : (ℕ →. ℕ) → Prop
+  | zero : Nat.Partrec (pure 0)
+  | succ : Nat.Partrec succ
+  | left : Nat.Partrec ↑fun n : ℕ => n.unpair.1
+  | right : Nat.Partrec ↑fun n : ℕ => n.unpair.2
+  | pair {f g} : Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun n => pair <$> f n <*> g n
+  | comp {f g} : Nat.Partrec f → Nat.Partrec g → Nat.Partrec fun n => g n >>= f
+  | prec {f g} : Nat.Partrec f → Nat.Partrec g → Nat.Partrec (unpaired fun a n =>
       n.rec (f a) fun y IH => do let i ← IH; g (pair a (pair y i)))
-  | rfind {f} : Partrec f → Partrec fun a => rfind fun n => (fun m => m = 0) <$> f (pair a n)
+  | rfind {f} : Nat.Partrec f →
+    Nat.Partrec fun a => rfind fun n => (fun m => m = 0) <$> f (pair a n)
 
 namespace Partrec
 
-theorem of_eq {f g : ℕ →. ℕ} (hf : Partrec f) (H : ∀ n, f n = g n) : Partrec g :=
+theorem of_eq {f g : ℕ →. ℕ} (hf : Nat.Partrec f) (H : ∀ n, f n = g n) : Nat.Partrec g :=
   (funext H : f = g) ▸ hf
 
-theorem of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ} (hf : Partrec f) (H : ∀ n, g n ∈ f n) : Partrec g :=
+theorem of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ} (hf : Nat.Partrec f) (H : ∀ n, g n ∈ f n) :
+    Nat.Partrec g :=
   hf.of_eq fun n => eq_some_iff.2 (H n)
 
-theorem of_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : Partrec f := by
+theorem of_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : Nat.Partrec f := by
   induction hf with
   | zero => exact zero
   | succ => exact succ
@@ -196,21 +198,21 @@ theorem of_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : Partrec f := by
       simp only [mem_bind_iff, mem_some_iff]
       exact ⟨_, IH, rfl⟩
 
-protected theorem some : Partrec some :=
+protected theorem some : Nat.Partrec some :=
   of_primrec Primrec.id
 
-theorem none : Partrec fun _ => none :=
+theorem none : Nat.Partrec fun _ => none :=
   (of_primrec (Nat.Primrec.const 1)).rfind.of_eq fun _ =>
     eq_none_iff.2 fun _ ⟨h, _⟩ => by simp at h
 
-theorem prec' {f g h} (hf : Partrec f) (hg : Partrec g) (hh : Partrec h) :
-    Partrec fun a => (f a).bind fun n => n.rec (g a)
+theorem prec' {f g h} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (hh : Nat.Partrec h) :
+    Nat.Partrec fun a => (f a).bind fun n => n.rec (g a)
       fun y IH => do {let i ← IH; h (Nat.pair a (Nat.pair y i))} :=
   ((prec hg hh).comp (pair Partrec.some hf)).of_eq fun a =>
     ext fun s => by simp [Seq.seq]
 
 set_option linter.flexible false in -- TODO: revisit this after #13791 is merged
-theorem ppred : Partrec fun n => ppred n :=
+theorem ppred : Nat.Partrec fun n => ppred n :=
   have : Primrec₂ fun n m => if n = Nat.succ m then 0 else 1 :=
     (Primrec.ite
       (@PrimrecRel.comp _ _ _ _ _ _ _ _ _

Mathlib/Computability/PartrecCode.lean

@@ -1028,13 +1028,13 @@ theorem fixed_point₂ {f : Code → ℕ →. ℕ} (hf : Partrec₂ f) : ∃ c :
 end
 
 /-- There are only countably many partial recursive partial functions `ℕ →. ℕ`. -/
-instance : Countable {f : ℕ →. ℕ // _root_.Partrec f} := by
+instance : Countable {f : ℕ →. ℕ // Partrec f} := by
   apply Function.Surjective.countable (f := fun c => ⟨eval c, eval_part.comp (.const c) .id⟩)
   intro ⟨f, hf⟩; simpa using exists_code.1 hf
 
 /-- There are only countably many computable functions `ℕ → ℕ`. -/
 instance : Countable {f : ℕ → ℕ // Computable f} :=
-  @Function.Injective.countable {f : ℕ → ℕ // Computable f} {f : ℕ →. ℕ // _root_.Partrec f} _
+  @Function.Injective.countable {f : ℕ → ℕ // Computable f} {f : ℕ →. ℕ // Partrec f} _
     (fun f => ⟨f.val, f.2⟩)
     (fun _ _ h => Subtype.val_inj.1 (PFun.lift_injective (by simpa using h)))