Complete Partrec module: prove prec closure and fix sub_computable (#27)

- Prove URMComputable1.prec: primitive recursion closure for unary functions
  - Build nested pair composition g_step(a,k,acc) = g(pair(a, pair(k, acc)))
  - Apply URMComputable.primRec closure theorem
  - Compose with unpair to get URMComputable 1
  - Prove semantic equivalence via induction on recursion depth

- Fix sub_computable: replace sorry with monus_computable (identical theorem)

This completes Nat.Partrec.toURMComputable1 without any sorries, establishing
that every Nat.Partrec function is URM-computable.

Author: jessealama

Urm/Partrec.lean

@@ -80,8 +80,8 @@ section Arithmetic
 
 /-- Monus (truncated subtraction) is URM-computable.
     sub(x, 0) = x, sub(x, y+1) = pred(sub(x, y)) -/
-theorem sub_computable : URMComputable 2 (fun xy => Part.some (xy 0 - xy 1)) := by
-  sorry
+theorem sub_computable : URMComputable 2 (fun xy => Part.some (xy 0 - xy 1)) :=
+  monus_computable
 
 -- mul_computable is now provided by Urm.Arithmetic
 
@@ -1167,9 +1167,111 @@ theorem URMComputable1.prec {f g : ℕ →. ℕ}
     (hf : URMComputable1 f) (hg : URMComputable1 g) :
     URMComputable1 (Nat.unpaired fun a n =>
       n.rec (f a) fun y IH => do let i ← IH; g (Nat.pair a (Nat.pair y i))) := by
-  -- Adapt: f_base(x) = f(x 0), g_step(x,k,acc) = g(pair(x 0, pair(k, acc)))
-  -- Then compose PrFunction with unpair using unpairLeft_computable, unpairRight_computable
-  sorry
+  unfold URMComputable1 at *
+
+  -- Step 1: Build nested pair: (Fin 3 → ℕ) → Part ℕ computing pair(x0, pair(x1, x2))
+
+  -- Inner pair: projects (xka 1, xka 2) then pairs them
+  let innerPairGs : Fin 2 → (Fin 3 → ℕ) → Part ℕ := fun i xka =>
+    if i.val = 0 then Part.some (xka 1) else Part.some (xka 2)
+  have h_innerPairGs : ∀ i, URMComputable 3 (innerPairGs i) := fun i => by
+    fin_cases i <;> simp only [innerPairGs, ↓reduceIte,
+      Nat.one_ne_zero] <;> exact URMComputable.proj_computable _ _
+  have h_innerPair := URMComputable.comp_general (m := 2) (n := 3) pair_computable h_innerPairGs
+
+  -- Prove the composition equals pair(xka 1, xka 2)
+  have h_innerPair_eq : compFunction 2 3 (fun xy => Part.some (Nat.pair (xy 0) (xy 1))) innerPairGs
+      = fun xka => Part.some (Nat.pair (xka 1) (xka 2)) := by
+    funext xka
+    simp only [compFunction, Part.sequence, innerPairGs, Fin.val_zero, ↓reduceIte, Part.bind_some,
+      Part.map_some, Fin.cons_zero, Fin.cons_one, Fin.val_succ, Nat.add_one_ne_zero]
+
+  -- Outer pair: projects (xka 0, innerPair) then pairs them
+  let outerPairGs : Fin 2 → (Fin 3 → ℕ) → Part ℕ := fun i xka =>
+    if i.val = 0 then Part.some (xka 0)
+    else Part.some (Nat.pair (xka 1) (xka 2))
+  have h_outerPairGs : ∀ i, URMComputable 3 (outerPairGs i) := fun i => by
+    fin_cases i
+    · simp only [outerPairGs, ↓reduceIte]
+      exact URMComputable.proj_computable _ _
+    · simp only [outerPairGs, Nat.one_ne_zero, ↓reduceIte]
+      rw [← h_innerPair_eq]
+      exact h_innerPair.toComputable
+  have h_nestedPair := URMComputable.comp_general (m := 2) (n := 3) pair_computable h_outerPairGs
+
+  -- Prove the composition equals pair(xka 0, pair(xka 1, xka 2))
+  have h_nestedPair_eq : compFunction 2 3 (fun xy => Part.some (Nat.pair (xy 0) (xy 1))) outerPairGs
+      = fun xka => Part.some (Nat.pair (xka 0) (Nat.pair (xka 1) (xka 2))) := by
+    funext xka
+    simp only [compFunction, Part.sequence, outerPairGs, Fin.val_zero, ↓reduceIte, Part.bind_some,
+      Part.map_some, Fin.cons_zero, Fin.cons_one, Fin.val_succ, Nat.add_one_ne_zero]
+
+  -- Step 2: Build g_step = g ∘ nestedPair
+  let nestedPairGs : Fin 1 → (Fin 3 → ℕ) → Part ℕ := fun _ xka =>
+    Part.some (Nat.pair (xka 0) (Nat.pair (xka 1) (xka 2)))
+  have h_nestedPairGs : ∀ i, URMComputable 3 (nestedPairGs i) := fun _ => by
+    simp only [nestedPairGs]
+    rw [← h_nestedPair_eq]
+    exact h_nestedPair.toComputable
+  have h_gstep := URMComputable.comp_general (m := 1) (n := 3) hg h_nestedPairGs
+
+  -- Prove g_step computes g(pair(xka 0, pair(xka 1, xka 2)))
+  have h_gstep_eq : compFunction 1 3 (fun x => g (x 0)) nestedPairGs
+      = fun xka => g (Nat.pair (xka 0) (Nat.pair (xka 1) (xka 2))) := by
+    funext xka
+    simp only [compFunction, Part.sequence, nestedPairGs, Part.bind_some, Part.map_some,
+      Fin.cons_zero]
+
+  -- Step 3: Apply primRec
+  let g_step : (Fin 3 → ℕ) → Part ℕ := fun xka => g (Nat.pair (xka 0) (Nat.pair (xka 1) (xka 2)))
+  have h_gstep_computable : URMComputable 3 g_step := by
+    simp only [g_step]
+    rw [← h_gstep_eq]
+    exact h_gstep.toComputable
+
+  have h_primRec := URMComputable.primRec (n := 1) hf h_gstep_computable
+
+  -- Step 4: Compose with unpair to get URMComputable 1
+  let unpairGs : Fin 2 → (Fin 1 → ℕ) → Part ℕ := fun i x =>
+    if i.val = 0 then Part.some (x 0).unpair.1 else Part.some (x 0).unpair.2
+  have h_unpairGs : ∀ i, URMComputable 1 (unpairGs i) := fun i => by
+    fin_cases i
+    · simp only [unpairGs, ↓reduceIte]; exact unpairLeft_computable
+    · simp only [unpairGs, Nat.one_ne_zero, ↓reduceIte]; exact unpairRight_computable
+  have h_final := URMComputable.comp_general (m := 2) (n := 1) h_primRec h_unpairGs
+
+  -- Step 5: Prove semantic equivalence
+  convert h_final.toComputable using 1
+  funext x
+  -- Simplify the compFunction on RHS
+  simp only [Nat.unpaired, compFunction, Part.sequence, unpairGs, Fin.val_zero, ↓reduceIte,
+    Part.bind_some, Part.map_some, Fin.val_succ, Nat.add_one_ne_zero]
+  -- Now RHS is: PrFunction ... (Fin.cons (unpair (x 0)).1 (Fin.cons (unpair (x 0)).2 Fin.elim0))
+
+  -- Generalize for induction
+  set a := (x 0).unpair.1
+  set n := (x 0).unpair.2
+
+  -- Key lemma: PrFunction unfolds as Pr
+  simp only [PrFunction, Pr]
+
+  -- Helper: compute initInputs and lastInput on Fin.cons a (Fin.cons m Fin.elim0)
+  have h_init : ∀ m, initInputs (Fin.cons a (Fin.cons m Fin.elim0)) = fun _ : Fin 1 => a := by
+    intro m; funext i; fin_cases i; simp [initInputs, Fin.castSucc_zero, Fin.cons_zero]
+  have h_last : ∀ m, lastInput (Fin.cons a (Fin.cons m Fin.elim0)) = m := by
+    intro m; simp [lastInput, Fin.cons_one, Fin.cons_zero]
+
+  simp only [h_init, h_last]
+
+  -- Prove by induction on n
+  induction n with
+  | zero =>
+    -- Both sides reduce to: f a = f ((fun _ => a) 0)
+    simp only [Nat.rec_zero]
+  | succ n ih =>
+    -- Both sides reduce to: (n.rec ...).bind (fun acc => g (pair a (pair n acc)))
+    -- The Fin.snoc expressions are definitionally equal: snoc (snoc _ k) acc i = [a,k,acc][i]
+    rfl
 
 /-- Minimization preserves URMComputable1.