-- Mathlib/Computability/Primrec.lean
theorem of_prim {n f} : Primrec f → @Primrec' n f :=
  suffices ∀ f, Nat.Primrec f → @Primrec' 1 fun v => f v.head from fun hf =>
    (pred.comp₁ _ <|
          (this _ hf).comp₁ (fun m => Encodable.encode <| (@decode (List.Vector ℕ n) _ m).map f)
            Primrec'.encode).of_eq
      fun i => by simp [encodek]
  fun f hf => by
  induction hf with
  | zero => exact const 0
  | succ => exact succ
  | left => exact unpair₁ head
  | right => exact unpair₂ head
  | pair _ _ hf hg => exact natPair.comp₂ _ hf hg
  | comp _ _ hf hg => exact hf.comp₁ _ hg
  | prec _ _ hf hg =>
    simpa using
      prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
        (hg.comp₁ _ <|
          natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))

Proof state:
case prec
n : ℕ
f✝¹ : List.Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
hf : Primrec' fun v => f✝ v.head
hg : Primrec' fun v => g✝ v.head
⊢ Primrec' fun v => unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (pair z (pair y IH))) n) v.head

Tactic:
simpa using
  prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
    (hg.comp₁ _ <|
      natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))

Result:
no goals

Proof state:
case zero
n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun x => 0) v.head

Tactic:
exact const 0

Result:
no goals

Proof state:
case succ
n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => v.head.succ

Tactic:
exact succ

Result:
no goals

Proof state:
n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Primrec' fun v => f v.head

Tactic:
induction hf with
| zero => exact const 0
| succ => exact succ
| left => exact unpair₁ head
| right => exact unpair₂ head
| pair _ _ hf hg => exact natPair.comp₂ _ hf hg
| comp _ _ hf hg => exact hf.comp₁ _ hg
| prec _ _ hf hg =>
  simpa using
    prec' (unpair₂ head) (hf.comp₁ _ (unpair₁ head))
      (hg.comp₁ _ <|
        natPair.comp₂ _ (unpair₁ <| tail <| tail head) (natPair.comp₂ _ head (tail head)))

Result:
no goals

Proof state:
case pair
n : ℕ
f✝¹ : List.Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
hf : Primrec' fun v => f✝ v.head
hg : Primrec' fun v => g✝ v.head
⊢ Primrec' fun v => (fun n => pair (f✝ n) (g✝ n)) v.head

Tactic:
exact natPair.comp₂ _ hf hg

Result:
no goals

Proof state:
case left
n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).1) v.head

Tactic:
exact unpair₁ head

Result:
no goals

Proof state:
case right
n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
⊢ Primrec' fun v => (fun n => (unpair n).2) v.head

Tactic:
exact unpair₂ head

Result:
no goals

Proof state:
n : ℕ
f : List.Vector ℕ n → ℕ
this : ∀ (f : ℕ → ℕ), Nat.Primrec f → Primrec' fun v => f v.head
hf : Primrec f
i : List.Vector ℕ n
⊢ ((fun m => encode (Option.map f (decode m))) (encode i)).pred = f i

Tactic:
simp [encodek]

Result:
no goals

Proof state:
case comp
n : ℕ
f✝¹ : List.Vector ℕ n → ℕ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
hf : Primrec' fun v => f✝ v.head
hg : Primrec' fun v => g✝ v.head
⊢ Primrec' fun v => (fun n => f✝ (g✝ n)) v.head

Tactic:
exact hf.comp₁ _ hg

Result:
no goals