-- Mathlib/Computability/TMConfig.lean
theorem exists_code {n} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) :
    ∃ c : Code, ∀ v : List.Vector ℕ n, c.eval v.1 = pure <$> f v

Proof state:
case prim.prec.intro.intro.succ.succ
n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ : (cf.prec cg).eval (n :: (↑v).tail) = pure (pure (Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n))
b : ℕ
IH :
  ∀ (a : ℕ),
    a + b = n →
      n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
        PFun.fix
          (fun v =>
            (cg.eval (v.headI :: v.tail.tail)).bind fun x =>
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)
a : ℕ
e : a + (b + 1) = n
⊢ Sum.inr
      ((a + 1) :: b :: g (a ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ v.tail) :: (↑v).tail) ∈
    Part.some
      (if ((b + 1) :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI = 0 then
        Sum.inl
          ((a :: (b + 1) :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
            ((b + 1) :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.pred ::
              [g
                      ((a ::
                            (b + 1) ::
                              Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::ᵥ
                        Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ v.tail)].headI ::
                (↑v).tail)
      else
        Sum.inr
          ((a :: (b + 1) :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.succ ::
            ((b + 1) :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI.pred ::
              [g
                      ((a ::
                            (b + 1) ::
                              Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail).headI ::ᵥ
                        Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ v.tail)].headI ::
                (↑v).tail))

Tactic:
exact Part.mem_some_iff.2 rfl

Result:
no goals

Proof state:
case prim.succ
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
⊢ ∃ c, ∀ (v : List.Vector ℕ 1), c.eval ↑v = pure <$> (↑fun v => v.head.succ) v

Tactic:
exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩

Result:
no goals

Proof state:
case prim.prec.intro.intro
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval ↑(v.head ::ᵥ v.tail) =
    pure <$> (↑fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) (v.head ::ᵥ v.tail)

Tactic:
simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons,
  Vector.head_cons, PFun.coe_val, Vector.tail_val]

Result:
case prim.prec.intro.intro
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (v.head :: (↑v).tail) =
    Part.some (pure (Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head))

Proof state:
case prim.prec.intro
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
IHg : ∃ c, ∀ (v : List.Vector ℕ (n + 2)), c.eval ↑v = pure <$> ↑g v
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> ↑f v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval ↑v = pure <$> (↑fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v

Tactic:
obtain ⟨cg, hg⟩ := IHg

Result:
case prim.prec.intro.intro
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> ↑f v
cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval ↑v = pure <$> ↑g v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval ↑v = pure <$> (↑fun v => Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) v.head) v

Proof state:
n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
n : ℕ
x✝ : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property✝ : (a :: as).length = n.succ
⊢ Part.some [a] = pure <$> Part.some (List.Vector.head ⟨a :: as, property✝⟩)

Tactic:
rfl

Result:
no goals

Proof state:
case rfind.intro.mpr.intro.intro.intro.succ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
w : List ℕ
n : ℕ
IH :
  (∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0) →
    w ∈
        PFun.fix
          (fun v =>
            (cf.eval v).bind fun y =>
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (n :: ↑v) →
      w ∈
        PFun.fix
          (fun v =>
            (cf.eval v).bind fun y =>
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          (0 :: ↑v)
hm : ∀ {m : ℕ}, m < n + 1 → ¬f (m ::ᵥ v) = 0
this :
  w ∈
    PFun.fix
      (fun v =>
        (cf.eval v).bind fun y =>
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      ((n + 1) :: ↑v)
⊢ Sum.inr ((n + 1) :: ↑v) ∈
    (cf.eval (n :: ↑v)).bind fun y =>
      Part.some
        (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
        else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))

Tactic:
simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, eq_self_iff_true, if_false,
  Part.mem_some_iff, and_self_iff, List.tail_cons]

Result:
no goals

Proof state:
case rfind.intro
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval ↑v = pure <$> ↑f v
⊢ ∃ c,
    ∀ (v : List.Vector ℕ n),
      c.eval ↑v = pure <$> (fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))) v

Tactic:
refine ⟨rfind cf, fun v => ?_⟩

Result:
case rfind.intro
n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval ↑v = pure <$> ↑f v
v : List.Vector ℕ n
⊢ cf.rfind.eval ↑v = pure <$> (fun v => Nat.rfind fun n_1 => Part.some (decide (f (n_1 ::ᵥ v) = 0))) v