no goals
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Partrec ↑f
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 => _
  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⟩
no goals
case zero
f : ℕ → ℕ
⊢ Partrec ↑fun x => 0
exact zero
no goals
case succ
f : ℕ → ℕ
⊢ Partrec ↑Nat.succ
exact succ
no goals
case left
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).fst
exact left
no goals
case right
f : ℕ → ℕ
⊢ Partrec ↑fun n => (unpair n).snd
exact right
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) ∈ Seq.seq (Nat.pair <$> ↑f✝ n) fun x => ↑g✝ n
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)
refine' (pf.pair pg).of_eq_tot fun n => _
no goals
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) ∈ Seq.seq (Nat.pair <$> ↑f✝ n) fun x => ↑g✝ n
simp [Seq.seq]
case comp
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ f✝ (g✝ n) ∈ ↑g✝ n >>= ↑f✝
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)
refine' (pf.comp pg).of_eq_tot fun n => _
no goals
case comp
f f✝ g✝ : ℕ → ℕ
a✝¹ : Nat.Primrec f✝
a✝ : Nat.Primrec g✝
pf : Partrec ↑f✝
pg : Partrec ↑g✝
n : ℕ
⊢ f✝ (g✝ n) ∈ ↑g✝ n >>= ↑f✝
simp
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
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)
refine' (pf.prec pg).of_eq_tot fun n => _
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).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) (unpair n).snd ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) (unpair n).snd
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
simp only [unpaired, PFun.coe_val, bind_eq_bind]
no goals
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).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) (unpair n).snd ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) (unpair n).snd
induction n.unpair.2 with
| zero => simp
| succ m IH =>
  simp only [mem_bind_iff, mem_some_iff]
  exact ⟨_, IH, rfl⟩
no goals
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).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) Nat.zero ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) Nat.zero
simp
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).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m
⊢ ∃ a,
    a ∈
        Nat.rec (Part.some (f✝ (unpair n).fst))
          (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m ∧
      g✝
          (Nat.pair (unpair n).fst
            (Nat.pair m (Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m))) =
        g✝ (Nat.pair (unpair n).fst (Nat.pair m a))
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).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m
⊢ Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) (Nat.succ m) ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) (Nat.succ m)
simp only [mem_bind_iff, mem_some_iff]
no goals
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).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m ∈
    Nat.rec (Part.some (f✝ (unpair n).fst))
      (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m
⊢ ∃ a,
    a ∈
        Nat.rec (Part.some (f✝ (unpair n).fst))
          (fun y IH => Part.bind IH fun i => Part.some (g✝ (Nat.pair (unpair n).fst (Nat.pair y i)))) m ∧
      g✝
          (Nat.pair (unpair n).fst
            (Nat.pair m (Nat.rec (f✝ (unpair n).fst) (fun y IH => g✝ (Nat.pair (unpair n).fst (Nat.pair y IH))) m))) =
        g✝ (Nat.pair (unpair n).fst (Nat.pair m a))
exact ⟨_, IH, rfl⟩