partrec.lean

/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Mario Carneiro

The partial recursive functions are defined similarly to the primitive
recursive functions, but now all functions are partial, implemented
using the `roption` monad, and there is an additional operation, called
μ-recursion, which performs unbounded minimization.
-/
import computability.primrec data.pfun

open encodable denumerable roption

namespace nat

section rfind
parameter (p : ℕ →. bool)

private def lbp (m n : ℕ) : Prop := m = n + 1 ∧ ∀ k ≤ n, ff ∈ p k

parameter (H : ∃ n, tt ∈ p n ∧ ∀ k < n, (p k).dom)

private def wf_lbp : well_founded lbp :=
⟨let ⟨n, pn⟩ := H in begin
  suffices : ∀m k, n ≤ k + m → acc (lbp p) k,
  { from λa, this _ _ (nat.le_add_left _ _) },
  intros m k kn,
  induction m with m IH generalizing k;
    refine ⟨_, λ y r, _⟩; rcases r with ⟨rfl, a⟩,
  { injection mem_unique pn.1 (a _ kn) },
  { exact IH _ (by rw nat.add_right_comm; exact kn) }
end⟩

def rfind_x : {n // tt ∈ p n ∧ ∀m < n, ff ∈ p m} :=
suffices ∀ k, (∀n < k, ff ∈ p n) → {n // tt ∈ p n ∧ ∀m < n, ff ∈ p m},
from this 0 (λ n, (nat.not_lt_zero _).elim),
@well_founded.fix _ _ lbp wf_lbp begin
  intros m IH al,
  have pm : (p m).dom,
  { rcases H with ⟨n, h₁, h₂⟩,
    rcases decidable.lt_trichotomy m n with h₃|h₃|h₃,
    { exact h₂ _ h₃ },
    { rw h₃, exact h₁.fst },
    { injection mem_unique h₁ (al _ h₃) } },
  cases e : (p m).get pm,
  { suffices,
    exact IH _ ⟨rfl, this⟩ (λ n h, this _ (le_of_lt_succ h)),
    intros n h, cases decidable.lt_or_eq_of_le h with h h,
    { exact al _ h },
    { rw h, exact ⟨_, e⟩ } },
  { exact ⟨m, ⟨_, e⟩, al⟩ }
end

end rfind

def rfind (p : ℕ →. bool) : roption ℕ :=
⟨_, λ h, (rfind_x p h).1⟩

theorem rfind_spec {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) : tt ∈ p n :=
h.snd ▸ (rfind_x p h.fst).2.1

theorem rfind_min {p : ℕ →. bool} {n : ℕ} (h : n ∈ rfind p) :
  ∀ {m : ℕ}, m < n → ff ∈ p m :=
h.snd ▸ (rfind_x p h.fst).2.2

@[simp] theorem rfind_dom {p : ℕ →. bool} :
  (rfind p).dom ↔ ∃ n, tt ∈ p n ∧ ∀ {m : ℕ}, m < n → (p m).dom :=
iff.rfl

@[simp] theorem rfind_dom' {p : ℕ →. bool} :
  (rfind p).dom ↔ ∃ n, tt ∈ p n ∧ ∀ {m : ℕ}, m ≤ n → (p m).dom :=
exists_congr $ λ n, and_congr_right $ λ pn,
⟨λ H m h, (eq_or_lt_of_le h).elim (λ e, e.symm ▸ pn.fst) (H _),
 λ H m h, H (le_of_lt h)⟩

@[simp] theorem mem_rfind {p : ℕ →. bool} {n : ℕ} :
  n ∈ rfind p ↔ tt ∈ p n ∧ ∀ {m : ℕ}, m < n → ff ∈ p m :=
⟨λ h, ⟨rfind_spec h, @rfind_min _ _ h⟩,
  λ ⟨h₁, h₂⟩, let ⟨m, hm⟩ := dom_iff_mem.1 $
    (@rfind_dom p).2 ⟨_, h₁, λ m mn, (h₂ mn).fst⟩ in
  begin
    rcases lt_trichotomy m n with h|h|h,
    { injection mem_unique (h₂ h) (rfind_spec hm) },
    { rwa ← h },
    { injection mem_unique h₁ (rfind_min hm h) },
  end⟩

theorem rfind_min' {p : ℕ → bool} {m : ℕ} (pm : p m) :
  ∃ n ∈ rfind p, n ≤ m :=
have tt ∈ (p : ℕ →. bool) m, from ⟨trivial, pm⟩,
let ⟨n, hn⟩ := dom_iff_mem.1 $
  (@rfind_dom p).2 ⟨m, this, λ k h, ⟨⟩⟩ in
⟨n, hn, not_lt.1 $ λ h,
  by injection mem_unique this (rfind_min hn h)⟩

theorem rfind_zero_none
  (p : ℕ →. bool) (p0 : p 0 = none) : rfind p = none :=
eq_none_iff.2 $ λ a h,
let ⟨n, h₁, h₂⟩ := rfind_dom'.1 h.fst in
(p0 ▸ h₂ (zero_le _) : (@roption.none bool).dom)

def rfind_opt {α} (f : ℕ → option α) : roption α :=
(rfind (λ n, (f n).is_some)).bind (λ n, f n)

theorem rfind_opt_spec {α} {f : ℕ → option α} {a}
 (h : a ∈ rfind_opt f) : ∃ n, a ∈ f n :=
let ⟨n, h₁, h₂⟩ := mem_bind_iff.1 h in ⟨n, mem_coe.1 h₂⟩

theorem rfind_opt_dom {α} {f : ℕ → option α} :
  (rfind_opt f).dom ↔ ∃ n a, a ∈ f n :=
⟨λ h, (rfind_opt_spec ⟨h, rfl⟩).imp (λ n h, ⟨_, h⟩),
 λ h, begin
  have h' : ∃ n, (f n).is_some :=
    h.imp (λ n, option.is_some_iff_exists.2),
  have s := nat.find_spec h',
  have fd : (rfind (λ n, (f n).is_some)).dom :=
    ⟨nat.find h', by simpa using s.symm, λ _ _, trivial⟩,
  refine ⟨fd, _⟩,
  have := rfind_spec (get_mem fd),
  simp at this ⊢,
  cases option.is_some_iff_exists.1 this.symm with a e,
  rw e, trivial
end⟩

theorem rfind_opt_mono {α} {f : ℕ → option α}
  (H : ∀ {a m n}, m ≤ n → a ∈ f m → a ∈ f n)
  {a} : a ∈ rfind_opt f ↔ ∃ n, a ∈ f n :=
⟨rfind_opt_spec, λ ⟨n, h⟩, begin
  have h' := rfind_opt_dom.2 ⟨_, _, h⟩,
  cases rfind_opt_spec ⟨h', rfl⟩ with k hk,
  have := (H (le_max_left _ _) h).symm.trans
          (H (le_max_right _ _) hk),
  simp at this, simp [this, get_mem]
end⟩

inductive partrec : (ℕ →. ℕ) → Prop
| zero : partrec (pure 0)
| succ : partrec succ
| left : partrec (λ n, n.unpair.1)
| right : partrec (λ n, n.unpair.2)
| pair {f g} : partrec f → partrec g → partrec (λ n, mkpair <$> f n <*> g n)
| comp {f g} : partrec f → partrec g → partrec (λ n, g n >>= f)
| prec {f g} : partrec f → partrec g → partrec (unpaired (λ a n,
    n.elim (f a) (λ y IH, do i ← IH, g (mkpair a (mkpair y i)))))
| rfind {f} : partrec f → partrec (λ a,
    rfind (λ n, (λ m, m = 0) <$> f (mkpair a n)))

namespace partrec

theorem of_eq {f g : ℕ →. ℕ} (hf : partrec f) (H : ∀ n, f n = g n) : partrec g :=
(funext H : f = g) ▸ hf

theorem of_eq_tot {f : ℕ →. ℕ} {g : ℕ → ℕ}
  (hf : partrec f) (H : ∀ n, g n ∈ f n) : partrec g :=
hf.of_eq (λ n, eq_some_iff.2 (H n))

theorem of_primrec {f : ℕ → ℕ} (hf : primrec f) : partrec f :=
begin
  induction hf,
  case nat.primrec.zero { exact zero },
  case nat.primrec.succ { exact succ },
  case nat.primrec.left { exact left },
  case nat.primrec.right { exact right },
  case nat.primrec.pair : f g hf hg pf pg {
    refine (pf.pair pg).of_eq_tot (λ n, _),
    simp [has_seq.seq] },
  case nat.primrec.comp : f g hf hg pf pg {
    refine (pf.comp pg).of_eq_tot (λ n, _),
    simp },
  case nat.primrec.prec : f g hf hg pf pg {
    refine (pf.prec pg).of_eq_tot (λ n, _),
    simp,
    induction n.unpair.2 with m IH, {simp},
    simp, exact ⟨_, IH, rfl⟩ },
end

protected theorem some : partrec some := of_primrec primrec.id

theorem none : partrec (λ n, none) :=
(of_primrec (nat.primrec.const 1)).rfind.of_eq $
λ n, eq_none_iff.2 $ λ a ⟨h, e⟩, by simpa using h

theorem prec' {f g h}
  (hf : partrec f) (hg : partrec g) (hh : partrec h) :
  partrec (λ a, (f a).bind (λ n, n.elim (g a)
    (λ y IH, do i ← IH, h (mkpair a (mkpair y i))))) :=
((prec hg hh).comp (pair partrec.some hf)).of_eq $
λ a, ext $ λ s, by simp [(<*>)]; exact
⟨λ ⟨n, h₁, h₂⟩, ⟨_, ⟨_, h₁, rfl⟩, by simpa using h₂⟩,
 λ ⟨_, ⟨n, h₁, rfl⟩, h₂⟩, ⟨_, h₁, by simpa using h₂⟩⟩

theorem ppred : partrec (λ n, ppred n) :=
have primrec₂ (λ n m, if n = nat.succ m then 0 else 1),
from (primrec.ite
  (@@primrec_rel.comp _ _ _ _ _ _ _ primrec.eq
    primrec.fst
    (_root_.primrec.succ.comp primrec.snd))
  (_root_.primrec.const 0) (_root_.primrec.const 1)).to₂,
(of_primrec (primrec₂.unpaired'.2 this)).rfind.of_eq $
λ n, begin
  cases n; simp,
  { exact eq_none_iff.2 (λ a ⟨⟨m, h, _⟩, _⟩,
      by simpa [show 0 ≠ m.succ, by intro h; injection h] using h) },
  { refine eq_some_iff.2 _,
    simp, intros m h, simp [ne_of_gt h] }
end

end partrec

end nat

def partrec {α σ} [primcodable α] [primcodable σ]
  (f : α →. σ) := nat.partrec (λ n,
  roption.bind (decode α n) (λ a, (f a).map encode))

def partrec₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
  (f : α → β →. σ) := partrec (λ p : α × β, f p.1 p.2)

def computable {α σ} [primcodable α] [primcodable σ] (f : α → σ) := partrec (f : α →. σ)

def computable₂ {α β σ} [primcodable α] [primcodable β] [primcodable σ]
  (f : α → β → σ) := computable (λ p : α × β, f p.1 p.2)

theorem primrec.to_comp {α σ} [primcodable α] [primcodable σ]
  {f : α → σ} (hf : primrec f) : computable f :=
(nat.partrec.ppred.comp (nat.partrec.of_primrec hf)).of_eq $
λ n, by simp; cases decode α n; simp

theorem primrec₂.to_comp {α β σ} [primcodable α] [primcodable β] [primcodable σ]
  {f : α → β → σ} (hf : primrec₂ f) : computable₂ f := hf.to_comp

theorem computable.part {α σ} [primcodable α] [primcodable σ]
  {f : α → σ} (hf : computable f) : partrec (f : α →. σ) := hf

theorem computable₂.part {α β σ} [primcodable α] [primcodable β] [primcodable σ]
  {f : α → β → σ} (hf : computable₂ f) : partrec₂ (λ a, (f a : β →. σ)) := hf

namespace computable
variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]

theorem of_eq {f g : α → σ} (hf : computable f) (H : ∀ n, f n = g n) : computable g :=
(funext H : f = g) ▸ hf

theorem const (s : σ) : computable (λ a : α, s) :=
(primrec.const _).to_comp

theorem of_option {f : α → option β}
  (hf : computable f) : partrec (λ a, (f a : roption β)) :=
(nat.partrec.ppred.comp hf).of_eq $ λ n, begin
  cases decode α n with a; simp,
  cases f a with b; simp
end

theorem to₂ {f : α × β → σ} (hf : computable f) : computable₂ (λ a b, f (a, b)) :=
hf.of_eq $ λ ⟨a, b⟩, rfl

protected theorem id : computable (@id α) := primrec.id.to_comp

theorem fst : computable (@prod.fst α β) := primrec.fst.to_comp

theorem snd : computable (@prod.snd α β) := primrec.snd.to_comp

theorem pair {f : α → β} {g : α → γ}
  (hf : computable f) (hg : computable g) : computable (λ a, (f a, g a)) :=
(hf.pair hg).of_eq $
λ n, by cases decode α n; simp [(<*>)]

theorem unpair : computable nat.unpair := primrec.unpair.to_comp

theorem succ : computable nat.succ := primrec.succ.to_comp
theorem pred : computable nat.pred := primrec.pred.to_comp
theorem nat_bodd : computable nat.bodd := primrec.nat_bodd.to_comp
theorem nat_div2 : computable nat.div2 := primrec.nat_div2.to_comp

theorem sum_inl : computable (@sum.inl α β) := primrec.sum_inl.to_comp
theorem sum_inr : computable (@sum.inr α β) := primrec.sum_inr.to_comp

theorem list_cons : computable₂ (@list.cons α) := primrec.list_cons.to_comp
theorem list_reverse : computable (@list.reverse α) := primrec.list_reverse.to_comp
theorem list_nth : computable₂ (@list.nth α) := primrec.list_nth.to_comp
theorem list_append : computable₂ ((++) : list α → list α → list α) := primrec.list_append.to_comp
theorem list_concat : computable₂ (λ l (a:α), l ++ [a]) := primrec.list_concat.to_comp
theorem list_length : computable (@list.length α) := primrec.list_length.to_comp

theorem vector_cons {n} : computable₂ (@vector.cons α n) := primrec.vector_cons.to_comp
theorem vector_to_list {n} : computable (@vector.to_list α n) := primrec.vector_to_list.to_comp
theorem vector_length {n} : computable (@vector.length α n) := primrec.vector_length.to_comp
theorem vector_head {n} : computable (@vector.head α n) := primrec.vector_head.to_comp
theorem vector_tail {n} : computable (@vector.tail α n) := primrec.vector_tail.to_comp
theorem vector_nth {n} : computable₂ (@vector.nth α n) := primrec.vector_nth.to_comp
theorem vector_nth' {n} : computable (@vector.nth α n) := primrec.vector_nth'.to_comp
theorem vector_of_fn' {n} : computable (@vector.of_fn α n) := primrec.vector_of_fn'.to_comp

theorem fin_app {n} : computable₂ (@id (fin n → σ)) := primrec.fin_app.to_comp

protected theorem encode : computable (@encode α _) :=
primrec.encode.to_comp

protected theorem decode : computable (decode α) :=
primrec.decode.to_comp

protected theorem of_nat (α) [denumerable α] : computable (of_nat α) :=
(primrec.of_nat _).to_comp

theorem encode_iff {f : α → σ} : computable (λ a, encode (f a)) ↔ computable f :=
iff.rfl

theorem option_some : computable (@option.some α) :=
primrec.option_some.to_comp

end computable

namespace partrec
variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]

open computable

theorem of_eq {f g : α →. σ} (hf : partrec f) (H : ∀ n, f n = g n) : partrec g :=
(funext H : f = g) ▸ hf

theorem of_eq_tot {f : α →. σ} {g : α → σ}
  (hf : partrec f) (H : ∀ n, g n ∈ f n) : computable g :=
hf.of_eq (λ a, eq_some_iff.2 (H a))

theorem none : partrec (λ a : α, @roption.none σ) :=
nat.partrec.none.of_eq $ λ n, by cases decode α n; simp

protected theorem some : partrec (@roption.some α) := computable.id

theorem const' (s : roption σ) : partrec (λ a : α, s) :=
by haveI := classical.dec s.dom; exact
(of_option (const (to_option s))).of_eq (λ a, of_to_option s)

protected theorem bind {f : α →. β} {g : α → β →. σ}
  (hf : partrec f) (hg : partrec₂ g) : partrec (λ a, (f a).bind (g a)) :=
(hg.comp (nat.partrec.some.pair hf)).of_eq $
λ n, by simp [(<*>)]; cases e : decode α n with a;
  simp [e, encodek]

theorem map {f : α →. β} {g : α → β → σ}
  (hf : partrec f) (hg : computable₂ g) : partrec (λ a, (f a).map (g a)) :=
by simpa [bind_some_eq_map] using
   @@partrec.bind _ _ _ (λ a b, roption.some (g a b)) hf hg

theorem to₂ {f : α × β →. σ} (hf : partrec f) : partrec₂ (λ a b, f (a, b)) :=
hf.of_eq $ λ ⟨a, b⟩, rfl

theorem nat_elim
  {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ}
  (hf : computable f) (hg : partrec g) (hh : partrec₂ h) :
  partrec (λ a, (f a).elim (g a) (λ y IH, IH.bind (λ i, h a (y, i)))) :=
(nat.partrec.prec' hf hg hh).of_eq $ λ n, begin
  cases e : decode α n with a; simp [e],
  induction f a with m IH; simp,
  rw [IH, bind_map],
  congr, funext s,
  simp [encodek]
end

theorem comp {f : β →. σ} {g : α → β}
  (hf : partrec f) (hg : computable g) : partrec (λ a, f (g a)) :=
(hf.comp hg).of_eq $
λ n, by simp; cases e : decode α n with a;
  simp [e, encodek]

theorem nat_iff {f : ℕ →. ℕ} : partrec f ↔ nat.partrec f :=
by simp [partrec, map_id']

theorem map_encode_iff {f : α →. σ} : partrec (λ a, (f a).map encode) ↔ partrec f :=
iff.rfl

end partrec

namespace partrec₂
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]

theorem unpaired {f : ℕ → ℕ →. α} : partrec (nat.unpaired f) ↔ partrec₂ f :=
⟨λ h, by simpa using h.comp primrec₂.mkpair.to_comp,
 λ h, h.comp primrec.unpair.to_comp⟩

theorem unpaired' {f : ℕ → ℕ →. ℕ} : nat.partrec (nat.unpaired f) ↔ partrec₂ f :=
partrec.nat_iff.symm.trans unpaired

theorem comp
  {f : β → γ →. σ} {g : α → β} {h : α → γ}
  (hf : partrec₂ f) (hg : computable g) (hh : computable h) :
  partrec (λ a, f (g a) (h a)) := hf.comp (hg.pair hh)

theorem comp₂
  {f : γ → δ →. σ} {g : α → β → γ} {h : α → β → δ}
  (hf : partrec₂ f) (hg : computable₂ g) (hh : computable₂ h) :
  partrec₂ (λ a b, f (g a b) (h a b)) := hf.comp hg hh

end partrec₂

namespace computable
variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]

theorem comp {f : β → σ} {g : α → β}
  (hf : computable f) (hg : computable g) :
  computable (λ a, f (g a)) := hf.comp hg

theorem comp₂ {f : γ → σ} {g : α → β → γ}
  (hf : computable f) (hg : computable₂ g) :
  computable₂ (λ a b, f (g a b)) := hf.comp hg

end computable

namespace computable₂
variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable δ] [primcodable σ]

theorem comp
  {f : β → γ → σ} {g : α → β} {h : α → γ}
  (hf : computable₂ f) (hg : computable g) (hh : computable h) :
  computable (λ a, f (g a) (h a)) := hf.comp (hg.pair hh)

theorem comp₂
  {f : γ → δ → σ} {g : α → β → γ} {h : α → β → δ}
  (hf : computable₂ f) (hg : computable₂ g) (hh : computable₂ h) :
  computable₂ (λ a b, f (g a b) (h a b)) := hf.comp hg hh

end computable₂

namespace partrec
variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]

open computable

theorem rfind {p : α → ℕ →. bool} (hp : partrec₂ p) :
  partrec (λ a, nat.rfind (p a)) :=
(nat.partrec.rfind $ hp.map
  ((primrec.dom_bool (λ b, cond b 0 1))
    .comp primrec.snd).to₂.to_comp).of_eq $
λ n, begin
  cases e : decode α n with a;
    simp [e, nat.rfind_zero_none, map_id'],
  congr, funext n,
  simp [roption.map_map, (∘)],
  apply map_id' (λ b, _),
  cases b; refl
end

theorem rfind_opt {f : α → ℕ → option σ} (hf : computable₂ f) :
  partrec (λ a, nat.rfind_opt (f a)) :=
(rfind (primrec.option_is_some.to_comp.comp hf).part.to₂).bind
  (of_option hf)

theorem nat_cases_right
  {f : α → ℕ} {g : α → σ} {h : α → ℕ →. σ}
  (hf : computable f) (hg : computable g) (hh : partrec₂ h) :
  partrec (λ a, (f a).cases (some (g a)) (h a)) :=
(nat_elim hf hg (hh.comp fst (pred.comp $ hf.comp fst)).to₂).of_eq $
λ a, begin
  simp, cases f a; simp,
  refine ext (λ b, ⟨λ H, _, λ H, _⟩),
  { rcases mem_bind_iff.1 H with ⟨c, h₁, h₂⟩, exact h₂ },
  { have : ∀ m, (nat.elim (roption.some (g a))
      (λ y IH, IH.bind (λ _, h a n)) m).dom,
    { intro, induction m; simp [*, H.fst] },
    exact ⟨⟨this n, H.fst⟩, H.snd⟩ }
end

theorem bind_decode2_iff {f : α →. σ} : partrec f ↔
  nat.partrec (λ n, roption.bind (decode2 α n) (λ a, (f a).map encode)) :=
⟨λ hf, nat_iff.1 $ (of_option primrec.decode2.to_comp).bind $
  (map hf (computable.encode.comp snd).to₂).comp snd,
λ h, map_encode_iff.1 $ by simpa [encodek2]
  using (nat_iff.2 h).comp (@computable.encode α _)⟩

theorem vector_m_of_fn : ∀ {n} {f : fin n → α →. σ}, (∀ i, partrec (f i)) →
  partrec (λ (a : α), vector.m_of_fn (λ i, f i a))
| 0     f hf := const _
| (n+1) f hf := by simp [vector.m_of_fn]; exact
  (hf 0).bind (partrec.bind ((vector_m_of_fn (λ i, hf i.succ)).comp fst)
    (primrec.vector_cons.to_comp.comp (snd.comp fst) snd))

end partrec

@[simp] theorem vector.m_of_fn_roption_some {α n} : ∀ (f : fin n → α),
  vector.m_of_fn (λ i, roption.some (f i)) = roption.some (vector.of_fn f) :=
vector.m_of_fn_pure

namespace computable
variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]

theorem option_some_iff {f : α → σ} : computable (λ a, some (f a)) ↔ computable f :=
⟨λ h, encode_iff.1 $ primrec.pred.to_comp.comp $ encode_iff.2 h,
 option_some.comp⟩

theorem bind_decode_iff {f : α → β → option σ} : computable₂ (λ a n,
  (decode β n).bind (f a)) ↔ computable₂ f :=
⟨λ hf, nat.partrec.of_eq
    (((partrec.nat_iff.2 (nat.partrec.ppred.comp $
        nat.partrec.of_primrec $ primcodable.prim β)).comp snd).bind
      (computable.comp hf fst).to₂.part) $
  λ n, by simp;
    cases decode α n.unpair.1; simp;
    cases decode β n.unpair.2; simp,
λ hf, begin
  have : partrec (λ a : α × ℕ, (encode (decode β a.2)).cases
    (some option.none) (λ n, roption.map (f a.1) (decode β n))) :=
  partrec.nat_cases_right (primrec.encdec.to_comp.comp snd)
    (const none) ((of_option (computable.decode.comp snd)).map
      (hf.comp (fst.comp $ fst.comp fst) snd).to₂),
  refine this.of_eq (λ a, _),
  simp, cases decode β a.2; simp [encodek]
end⟩

theorem map_decode_iff {f : α → β → σ} : computable₂ (λ a n,
  (decode β n).map (f a)) ↔ computable₂ f :=
bind_decode_iff.trans option_some_iff

theorem nat_elim
  {f : α → ℕ} {g : α → σ} {h : α → ℕ × σ → σ}
  (hf : computable f) (hg : computable g) (hh : computable₂ h) :
  computable (λ a, (f a).elim (g a) (λ y IH, h a (y, IH))) :=
(partrec.nat_elim hf hg hh.part).of_eq $
λ a, by simp; induction f a; simp *

theorem nat_cases {f : α → ℕ} {g : α → σ} {h : α → ℕ → σ}
  (hf : computable f) (hg : computable g) (hh : computable₂ h) :
  computable (λ a, (f a).cases (g a) (h a)) :=
nat_elim hf hg (hh.comp fst $ fst.comp snd).to₂

theorem cond {c : α → bool} {f : α → σ} {g : α → σ}
  (hc : computable c) (hf : computable f) (hg : computable g) :
  computable (λ a, cond (c a) (f a) (g a)) :=
(nat_cases (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq $
λ a, by cases c a; refl

theorem option_cases {o : α → option β} {f : α → σ} {g : α → β → σ}
  (ho : computable o) (hf : computable f) (hg : computable₂ g) :
  @computable _ σ _ _ (λ a, option.cases_on (o a) (f a) (g a)) :=
option_some_iff.1 $
(nat_cases (encode_iff.2 ho) (option_some_iff.2 hf)
    (map_decode_iff.2 hg)).of_eq $
λ a, by cases o a; simp [encodek]; refl

theorem option_bind {f : α → option β} {g : α → β → option σ}
  (hf : computable f) (hg : computable₂ g) :
  computable (λ a, (f a).bind (g a)) :=
(option_cases hf (const option.none) hg).of_eq $
λ a, by cases f a; refl

theorem option_map {f : α → option β} {g : α → β → σ}
  (hf : computable f) (hg : computable₂ g) : computable (λ a, (f a).map (g a)) :=
option_bind hf (option_some.comp₂ hg)

theorem sum_cases
  {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ}
  (hf : computable f) (hg : computable₂ g) (hh : computable₂ h) :
  @computable _ σ _ _ (λ a, sum.cases_on (f a) (g a) (h a)) :=
option_some_iff.1 $
(cond (nat_bodd.comp $ encode_iff.2 hf)
  (option_map (computable.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hh)
  (option_map (computable.decode.comp $ nat_div2.comp $ encode_iff.2 hf) hg)).of_eq $
λ a, by cases f a with b c;
  simp [nat.div2_bit, nat.bodd_bit, encodek]; refl

theorem nat_strong_rec
  (f : α → ℕ → σ) {g : α → list σ → option σ} (hg : computable₂ g)
  (H : ∀ a n, g a ((list.range n).map (f a)) = some (f a n)) : computable₂ f :=
suffices computable₂ (λ a n, (list.range n).map (f a)), from
  option_some_iff.1 $
  (list_nth.comp (this.comp fst (succ.comp snd)) snd).to₂.of_eq $
  λ a, by simp [list.nth_range (nat.lt_succ_self a.2)]; refl,
option_some_iff.1 $
(nat_elim snd (const (option.some [])) (to₂ $
  option_bind (snd.comp snd) $ to₂ $
  option_map
    (hg.comp (fst.comp $ fst.comp fst) snd)
    (to₂ $ list_concat.comp (snd.comp fst) snd))).of_eq $
λ a, begin
  simp, induction a.2 with n IH, {refl},
  simp [IH, H, list.range_concat]
end

theorem list_of_fn : ∀ {n} {f : fin n → α → σ},
  (∀ i, computable (f i)) → computable (λ a, list.of_fn (λ i, f i a))
| 0     f hf := const []
| (n+1) f hf := by simp [list.of_fn_succ]; exact
  list_cons.comp (hf 0) (list_of_fn (λ i, hf i.succ))

theorem vector_of_fn {n} {f : fin n → α → σ}
  (hf : ∀ i, computable (f i)) : computable (λ a, vector.of_fn (λ i, f i a)) :=
(partrec.vector_m_of_fn hf).of_eq $ λ a, by simp

end computable

namespace partrec
variables {α : Type*} {β : Type*} {γ : Type*} {σ : Type*}
variables [primcodable α] [primcodable β] [primcodable γ] [primcodable σ]

open computable

theorem option_some_iff {f : α →. σ} :
  partrec (λ a, (f a).map option.some) ↔ partrec f :=
⟨λ h, (nat.partrec.ppred.comp h).of_eq $
   λ n, by simp [roption.bind_assoc, bind_some_eq_map],
 λ hf, hf.map (option_some.comp snd).to₂⟩

theorem option_cases_right {o : α → option β} {f : α → σ} {g : α → β →. σ}
  (ho : computable o) (hf : computable f) (hg : partrec₂ g) :
  @partrec _ σ _ _ (λ a, option.cases_on (o a) (some (f a)) (g a)) :=
have partrec (λ (a : α), nat.cases (roption.some (f a))
  (λ n, roption.bind (decode β n) (g a)) (encode (o a))) :=
nat_cases_right (encode_iff.2 ho) hf.part $
  ((@computable.decode β _).comp snd).of_option.bind
    (hg.comp (fst.comp fst) snd).to₂,
this.of_eq $ λ a, by cases o a with b; simp [encodek]

theorem sum_cases_right
  {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ →. σ}
  (hf : computable f) (hg : computable₂ g) (hh : partrec₂ h) :
  @partrec _ σ _ _ (λ a, sum.cases_on (f a) (λ b, some (g a b)) (h a)) :=
have partrec (λ a, (option.cases_on
  (sum.cases_on (f a) (λ b, option.none) option.some : option γ)
  (some (sum.cases_on (f a) (λ b, some (g a b))
     (λ c, option.none)))
  (λ c, (h a c).map option.some) : roption (option σ))) :=
option_cases_right
  (sum_cases hf (const option.none).to₂ (option_some.comp snd).to₂)
  (sum_cases hf (option_some.comp hg) (const option.none).to₂)
  (option_some_iff.2 hh),
option_some_iff.1 $ this.of_eq $ λ a, by cases f a; simp

theorem sum_cases_left
  {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ → σ}
  (hf : computable f) (hg : partrec₂ g) (hh : computable₂ h) :
  @partrec _ σ _ _ (λ a, sum.cases_on (f a) (g a) (λ c, some (h a c))) :=
(sum_cases_right (sum_cases hf
  (sum_inr.comp snd).to₂ (sum_inl.comp snd).to₂) hh hg).of_eq $
λ a, by cases f a; simp

private lemma fix_aux
  {f : α →. σ ⊕ α} (hf : partrec f)
  (a : α) (b : σ) :
  let F : α → ℕ →. σ ⊕ α := λ a n,
    n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
    sum.cases_on s (λ _, roption.some s) f in
  (∃ (n : ℕ), ((∃ (b' : σ), sum.inl b' ∈ F a n) ∧
        ∀ {m : ℕ}, m < n → (∃ (b : α), sum.inr b ∈ F a m)) ∧
      sum.inl b ∈ F a n) ↔ b ∈ pfun.fix f a :=
begin
  intro, refine ⟨λ h, _, λ h, _⟩,
  { rcases h with ⟨n, ⟨_x, h₁⟩, h₂⟩,
    have : ∀ m a' (_: sum.inr a' ∈ F a m)
      (_: b ∈ pfun.fix f a'), b ∈ pfun.fix f a,
    { intros m a' am ba,
      induction m with m IH generalizing a'; simp [F] at am,
      { rwa ← am },
      rcases am with ⟨a₂, am₂, fa₂⟩,
      exact IH _ am₂ (pfun.mem_fix_iff.2 (or.inr ⟨_, fa₂, ba⟩)) },
    cases n; simp [F] at h₂, {cases h₂},
    rcases h₂ with h₂ | ⟨a', am', fa'⟩,
    { cases h₁ (nat.lt_succ_self _) with a' h,
      injection mem_unique h h₂ },
    { exact this _ _ am' (pfun.mem_fix_iff.2 (or.inl fa')) } },
  { suffices : ∀ a' (_: b ∈ pfun.fix f a') k (_: sum.inr a' ∈ F a k),
       ∃ n, sum.inl b ∈ F a n ∧
         ∀ (m < n) (_ : k ≤ m), ∃ a₂, sum.inr a₂ ∈ F a m,
    { rcases this _ h 0 (by simp [F]) with ⟨n, hn₁, hn₂⟩,
      exact ⟨_, ⟨⟨_, hn₁⟩, λ m mn, hn₂ m mn (nat.zero_le _)⟩, hn₁⟩ },
    intros a₁ h₁,
    apply pfun.fix_induction h₁, intros a₂ h₂ IH k hk,
    rcases pfun.mem_fix_iff.1 h₂ with h₂ | ⟨a₃, am₃, fa₃⟩,
    { refine ⟨k.succ, _, λ m mk km, ⟨a₂, _⟩⟩,
      { simp [F], exact or.inr ⟨_, hk, h₂⟩ },
      { rwa le_antisymm (nat.le_of_lt_succ mk) km } },
    { rcases IH _ fa₃ am₃ k.succ _ with ⟨n, hn₁, hn₂⟩,
      { refine ⟨n, hn₁, λ m mn km, _⟩,
        cases lt_or_eq_of_le km with km km,
        { exact hn₂ _ mn km },
        { exact km ▸ ⟨_, hk⟩ } },
      { simp [F], exact ⟨_, hk, am₃⟩ } } }
end

theorem fix
  {f : α →. σ ⊕ α} (hf : partrec f) : partrec (pfun.fix f) :=
let F : α → ℕ →. σ ⊕ α := λ a n,
  n.elim (some (sum.inr a)) $ λ y IH, IH.bind $ λ s,
  sum.cases_on s (λ _, roption.some s) f in
have hF : partrec₂ F :=
partrec.nat_elim snd (sum_inr.comp fst).part
  (sum_cases_right (snd.comp snd)
    (snd.comp $ snd.comp fst).to₂
    (hf.comp snd).to₂).to₂,
let p := λ a n, @roption.map _ bool
  (λ s, sum.cases_on s (λ_, tt) (λ _, ff)) (F a n) in
have hp : partrec₂ p := hF.map ((sum_cases computable.id
  (const tt).to₂ (const ff).to₂).comp snd).to₂,
(hp.rfind.bind (hF.bind
  (sum_cases_right snd snd.to₂ none.to₂).to₂).to₂).of_eq $
λ a, ext $ λ b, by simp; apply fix_aux hf

end partrec