-- Mathlib/Computability/Partrec.lean
theorem of_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) : Partrec f

Proof state:
case succ
f : ℕ → ℕ
⊢ Partrec ↑Nat.succ

Tactic:
exact succ

Result:
no goals

Proof state:
case right
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).2

Tactic:
exact right

Result:
no goals

Proof state:
case pair
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑fun n => Nat.pair (f✝ n) (g✝ n)

Tactic:
refine (pf.pair pg).of_eq_tot fun n => ?_

Result:
case pair
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.pair (f✝ n) (g✝ n) ∈ Nat.pair <$> ↑f✝ n <*> ↑g✝ n

Proof state:
case comp
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑fun n => f✝ (g✝ n)

Tactic:
refine (pf.comp pg).of_eq_tot fun n => (by simp)

Result:
no goals

Proof state:
case prec.zero
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) 0 ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) 0

Tactic:
simp

Result:
no goals

Proof state:
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
⊢ Partrec ↑(unpaired fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (Nat.pair z (Nat.pair y IH))) n)

Tactic:
refine (pf.prec pg).of_eq_tot fun n => ?_

Result:
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (Nat.pair z (Nat.pair y IH))) n) n ∈
    unpaired
      (fun a n =>
        Nat.rec (↑f✝ a)
          (fun y IH => do
            let i ← IH
            ↑g✝ (Nat.pair a (Nat.pair y i)))
          n)
      n

Proof state:
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) (unpair n).2 ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) (unpair n).2

Tactic:
induction n.unpair.2 with
| zero => simp
| succ m IH =>
  simp only [mem_bind_iff, mem_some_iff]
  exact ⟨_, IH, rfl⟩

Result:
no goals

Proof state:
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Partrec ↑f

Tactic:
induction hf with
| zero => exact zero
| succ => exact succ
| left => exact left
| right => exact right
| pair _ _ pf pg =>
  refine (pf.pair pg).of_eq_tot fun n => ?_
  simp [Seq.seq]
| comp _ _ pf pg =>
  refine (pf.comp pg).of_eq_tot fun n => (by simp)
| prec _ _ pf pg =>
  refine (pf.prec pg).of_eq_tot fun n => ?_
  simp only [unpaired, PFun.coe_val, bind_eq_bind]
  induction n.unpair.2 with
  | zero => simp
  | succ m IH =>
    simp only [mem_bind_iff, mem_some_iff]
    exact ⟨_, IH, rfl⟩

Result:
no goals

Proof state:
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ f✝ (g✝ n) ∈ ↑g✝ n >>= ↑f✝

Tactic:
simp

Result:
no goals

Proof state:
case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) (m + 1) ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) (m + 1)

Tactic:
simp only [mem_bind_iff, mem_some_iff]

Result:
case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m
⊢ ∃
    a ∈
      Nat.rec (Part.some (f✝ (unpair n).1))
        (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m,
    g✝
        (Nat.pair (unpair n).1
          (Nat.pair m (Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m))) =
      g✝ (Nat.pair (unpair n).1 (Nat.pair m a))

Proof state:
case pair
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.pair (f✝ n) (g✝ n) ∈ Nat.pair <$> ↑f✝ n <*> ↑g✝ n

Tactic:
simp [Seq.seq]

Result:
no goals

Proof state:
case left
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).1

Tactic:
exact left

Result:
no goals

Proof state:
case prec.succ
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n m : ℕ
IH :
  Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m
⊢ ∃
    a ∈
      Nat.rec (Part.some (f✝ (unpair n).1))
        (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) m,
    g✝
        (Nat.pair (unpair n).1
          (Nat.pair m (Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) m))) =
      g✝ (Nat.pair (unpair n).1 (Nat.pair m a))

Tactic:
exact ⟨_, IH, rfl⟩

Result:
no goals

Proof state:
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ unpaired (fun z n => Nat.rec (f✝ z) (fun y IH => g✝ (Nat.pair z (Nat.pair y IH))) n) n ∈
    unpaired
      (fun a n =>
        Nat.rec (↑f✝ a)
          (fun y IH => do
            let i ← IH
            ↑g✝ (Nat.pair a (Nat.pair y i)))
          n)
      n

Tactic:
simp only [unpaired, PFun.coe_val, bind_eq_bind]

Result:
case prec
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ Nat.rec (f✝ (unpair n).1) (fun y IH => g✝ (Nat.pair (unpair n).1 (Nat.pair y IH))) (unpair n).2 ∈
    Nat.rec (Part.some (f✝ (unpair n).1))
      (fun y IH => IH.bind fun i => Part.some (g✝ (Nat.pair (unpair n).1 (Nat.pair y i)))) (unpair n).2

Proof state:
case zero
f : ℕ → ℕ
⊢ Partrec ↑fun x => 0

Tactic:
exact zero

Result:
no goals