-- Mathlib/Computability/PartrecCode.lean
theorem exists_code {f : ℕ →. ℕ} : Nat.Partrec f ↔ ∃ c : Code, eval c = f

Proof state:
case refine_2.intro.pair
cf cg : Code
pf : Partrec cf.eval
pg : Partrec cg.eval
⊢ Partrec (cf.pair cg).eval

Tactic:
exact pf.pair pg

Result:
no goals

Proof state:
case refine_1.pair.intro
f g✝ : ℕ →. ℕ
pg : Partrec g✝
hg : ∃ c, c.eval = g✝
cf : Code
pf : Partrec cf.eval
⊢ ∃ c, c.eval = fun n => Nat.pair <$> cf.eval n <*> g✝ n

Tactic:
rcases hg with ⟨cg, rfl⟩

Result:
case refine_1.pair.intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
cg : Code
pg : Partrec cg.eval
⊢ ∃ c, c.eval = fun n => Nat.pair <$> cf.eval n <*> cg.eval n

Proof state:
case refine_1.comp
f f✝ g✝ : ℕ →. ℕ
pf : Partrec f✝
pg : Partrec g✝
hf : ∃ c, c.eval = f✝
hg : ∃ c, c.eval = g✝
⊢ ∃ c, c.eval = fun n => g✝ n >>= f✝

Tactic:
rcases hf with ⟨cf, rfl⟩

Result:
case refine_1.comp.intro
f g✝ : ℕ →. ℕ
pg : Partrec g✝
hg : ∃ c, c.eval = g✝
cf : Code
pf : Partrec cf.eval
⊢ ∃ c, c.eval = fun n => g✝ n >>= cf.eval

Proof state:
case refine_2.intro.zero

⊢ Partrec zero.eval

Tactic:
exact Nat.Partrec.zero

Result:
no goals

Proof state:
case refine_1.succ
f : ℕ →. ℕ
⊢ ∃ c, c.eval = ↑Nat.succ

Tactic:
exact ⟨succ, rfl⟩

Result:
no goals

Proof state:
case refine_1.pair
f f✝ g✝ : ℕ →. ℕ
pf : Partrec f✝
pg : Partrec g✝
hf : ∃ c, c.eval = f✝
hg : ∃ c, c.eval = g✝
⊢ ∃ c, c.eval = fun n => Nat.pair <$> f✝ n <*> g✝ n

Tactic:
rcases hf with ⟨cf, rfl⟩

Result:
case refine_1.pair.intro
f g✝ : ℕ →. ℕ
pg : Partrec g✝
hg : ∃ c, c.eval = g✝
cf : Code
pf : Partrec cf.eval
⊢ ∃ c, c.eval = fun n => Nat.pair <$> cf.eval n <*> g✝ n

Proof state:
case refine_2.intro.succ

⊢ Partrec succ.eval

Tactic:
exact Nat.Partrec.succ

Result:
no goals

Proof state:
case refine_2
f : ℕ →. ℕ
⊢ (∃ c, c.eval = f) → Partrec f

Tactic:
rintro ⟨c, rfl⟩

Result:
case refine_2.intro
c : Code
⊢ Partrec c.eval

Proof state:
case refine_2.intro.comp
cf cg : Code
pf : Partrec cf.eval
pg : Partrec cg.eval
⊢ Partrec (cf.comp cg).eval

Tactic:
exact pf.comp pg

Result:
no goals

Proof state:
case refine_1.rfind.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
⊢ ∃ c, c.eval = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> cf.eval (Nat.pair a n)

Tactic:
refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩

Result:
case refine_1.rfind.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
⊢ (cf.rfind'.comp (Code.id.pair zero)).eval = fun a =>
    Nat.rfind fun n => (fun m => decide (m = 0)) <$> cf.eval (Nat.pair a n)

Proof state:
case refine_1.prec
f f✝ g✝ : ℕ →. ℕ
pf : Partrec f✝
pg : Partrec g✝
hf : ∃ c, c.eval = f✝
hg : ∃ c, c.eval = g✝
⊢ ∃ c,
    c.eval =
      unpaired fun a n =>
        Nat.rec (f✝ a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

Tactic:
rcases hf with ⟨cf, rfl⟩

Result:
case refine_1.prec.intro
f g✝ : ℕ →. ℕ
pg : Partrec g✝
hg : ∃ c, c.eval = g✝
cf : Code
pf : Partrec cf.eval
⊢ ∃ c,
    c.eval =
      unpaired fun a n =>
        Nat.rec (cf.eval a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

Proof state:
case refine_2.intro
c : Code
⊢ Partrec c.eval

Tactic:
induction c with
| zero => exact Nat.Partrec.zero
| succ => exact Nat.Partrec.succ
| left => exact Nat.Partrec.left
| right => exact Nat.Partrec.right
| pair cf cg pf pg => exact pf.pair pg
| comp cf cg pf pg => exact pf.comp pg
| prec cf cg pf pg => exact pf.prec pg
| rfind' cf pf => exact pf.rfind'

Result:
no goals

Proof state:
case refine_1.zero
f : ℕ →. ℕ
⊢ ∃ c, c.eval = pure 0

Tactic:
exact ⟨zero, rfl⟩

Result:
no goals

Proof state:
case refine_1.pair.intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
cg : Code
pg : Partrec cg.eval
⊢ ∃ c, c.eval = fun n => Nat.pair <$> cf.eval n <*> cg.eval n

Tactic:
exact ⟨pair cf cg, rfl⟩

Result:
no goals

Proof state:
case refine_2.intro.left

⊢ Partrec left.eval

Tactic:
exact Nat.Partrec.left

Result:
no goals

Proof state:
case refine_1.right
f : ℕ →. ℕ
⊢ ∃ c, c.eval = ↑fun n => (unpair n).2

Tactic:
exact ⟨right, rfl⟩

Result:
no goals

Proof state:
case refine_2.intro.prec
cf cg : Code
pf : Partrec cf.eval
pg : Partrec cg.eval
⊢ Partrec (cf.prec cg).eval

Tactic:
exact pf.prec pg

Result:
no goals

Proof state:
case refine_1
f : ℕ →. ℕ
h : Partrec f
⊢ ∃ c, c.eval = f

Tactic:
induction h with
| zero => exact ⟨zero, rfl⟩
| succ => exact ⟨succ, rfl⟩
| left => exact ⟨left, rfl⟩
| right => exact ⟨right, rfl⟩
| pair pf pg hf hg =>
  rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
  exact ⟨pair cf cg, rfl⟩
| comp pf pg hf hg =>
  rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
  exact ⟨comp cf cg, rfl⟩
| prec pf pg hf hg =>
  rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
  exact ⟨prec cf cg, rfl⟩
| rfind pf hf =>
  rcases hf with ⟨cf, rfl⟩
  refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
  simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']

Result:
no goals

Proof state:
case refine_1.prec.intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
cg : Code
pg : Partrec cg.eval
⊢ ∃ c,
    c.eval =
      unpaired fun a n =>
        Nat.rec (cf.eval a)
          (fun y IH => do
            let i ← IH
            cg.eval (Nat.pair a (Nat.pair y i)))
          n

Tactic:
exact ⟨prec cf cg, rfl⟩

Result:
no goals

Proof state:
case refine_1.rfind
f f✝ : ℕ →. ℕ
pf : Partrec f✝
hf : ∃ c, c.eval = f✝
⊢ ∃ c, c.eval = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f✝ (Nat.pair a n)

Tactic:
rcases hf with ⟨cf, rfl⟩

Result:
case refine_1.rfind.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
⊢ ∃ c, c.eval = fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> cf.eval (Nat.pair a n)

Proof state:
case refine_1.comp.intro
f g✝ : ℕ →. ℕ
pg : Partrec g✝
hg : ∃ c, c.eval = g✝
cf : Code
pf : Partrec cf.eval
⊢ ∃ c, c.eval = fun n => g✝ n >>= cf.eval

Tactic:
rcases hg with ⟨cg, rfl⟩

Result:
case refine_1.comp.intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
cg : Code
pg : Partrec cg.eval
⊢ ∃ c, c.eval = fun n => cg.eval n >>= cf.eval

Proof state:
case refine_1.prec.intro
f g✝ : ℕ →. ℕ
pg : Partrec g✝
hg : ∃ c, c.eval = g✝
cf : Code
pf : Partrec cf.eval
⊢ ∃ c,
    c.eval =
      unpaired fun a n =>
        Nat.rec (cf.eval a)
          (fun y IH => do
            let i ← IH
            g✝ (Nat.pair a (Nat.pair y i)))
          n

Tactic:
rcases hg with ⟨cg, rfl⟩

Result:
case refine_1.prec.intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
cg : Code
pg : Partrec cg.eval
⊢ ∃ c,
    c.eval =
      unpaired fun a n =>
        Nat.rec (cf.eval a)
          (fun y IH => do
            let i ← IH
            cg.eval (Nat.pair a (Nat.pair y i)))
          n

Proof state:
case refine_1.rfind.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
⊢ (cf.rfind'.comp (Code.id.pair zero)).eval = fun a =>
    Nat.rfind fun n => (fun m => decide (m = 0)) <$> cf.eval (Nat.pair a n)

Tactic:
simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']

Result:
no goals

Proof state:
case refine_1.left
f : ℕ →. ℕ
⊢ ∃ c, c.eval = ↑fun n => (unpair n).1

Tactic:
exact ⟨left, rfl⟩

Result:
no goals

Proof state:
case refine_2.intro.right

⊢ Partrec right.eval

Tactic:
exact Nat.Partrec.right

Result:
no goals

Proof state:
case refine_2.intro.rfind'
cf : Code
pf : Partrec cf.eval
⊢ Partrec cf.rfind'.eval

Tactic:
exact pf.rfind'

Result:
no goals

Proof state:
f : ℕ →. ℕ
⊢ Partrec f ↔ ∃ c, c.eval = f

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
f : ℕ →. ℕ
h : Partrec f
⊢ ∃ c, c.eval = f

case refine_2
f : ℕ →. ℕ
⊢ (∃ c, c.eval = f) → Partrec f

Proof state:
case refine_1.comp.intro.intro
f : ℕ →. ℕ
cf : Code
pf : Partrec cf.eval
cg : Code
pg : Partrec cg.eval
⊢ ∃ c, c.eval = fun n => cg.eval n >>= cf.eval

Tactic:
exact ⟨comp cf cg, rfl⟩

Result:
no goals