Lean4
theorem exists_code {n} {f : List.Vector ℕ n →. ℕ} (hf : Nat.Partrec' f) :
∃ c : Code, ∀ v : List.Vector ℕ n, c.eval v.1 = pure <$> f v := by
induction hf with
| prim hf =>
induction hf with
| zero => exact ⟨zero', fun ⟨[], _⟩ => rfl⟩
| succ => exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩
| get i =>
refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
· exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩
· obtain ⟨c, h⟩ := IH
exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩
| comp g hf hg IHf IHg => simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg
| @prec n f g _ _ IHf IHg =>
obtain ⟨cf, hf⟩ := IHf
obtain ⟨cg, hg⟩ := IHg
simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg
refine ⟨prec cf cg, fun v => ?_⟩
rw [← v.cons_head_tail]
specialize hf v.tail
replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
simp only [Vector.cons_val, Vector.tail_val] at hf hg
simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons, Vector.head_cons, PFun.coe_val,
Vector.tail_val]
simp only [← Part.pure_eq_some] at hf hg ⊢
induction v.head with simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
| succ n
_ =>
suffices
∀ a b,
a + b = n →
(n.succ ::
0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: v.val.tail :
List ℕ) ∈
PFun.fix
(fun v : List ℕ =>
Part.bind (cg.eval (v.headI :: v.tail.tail))
(fun x =>
Part.some
(if v.tail.headI = 0 then
Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
(a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail)
by
erw [Part.eq_some_iff.2 (this 0 n (zero_add n))]
simp only [List.headI, Part.bind_some, List.tail_cons]
intro a b e
induction b generalizing a with
| zero =>
refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
rfl
| succ b IH =>
refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
simp only [hg, Part.bind_some, List.tail_cons, pure]
exact Part.mem_some_iff.2 rfl
| comp g _ _ IHf IHg => exact exists_code.comp IHf IHg
| @rfind n f _ IHf =>
obtain ⟨cf, hf⟩ := IHf; refine ⟨rfind cf, fun v => ?_⟩
replace hf := fun a => hf (a ::ᵥ v)
simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val,
show ∀ x, pure x = [x] from fun _ => rfl] at hf ⊢
refine Part.ext fun x => ?_
simp only [rfind, Part.bind_eq_bind, Part.pure_eq_some, Part.bind_some, cons_eval, comp_eval, fix_eval, tail_eval,
succ_eval, zero'_eval, List.headI_cons, pred_eval, Part.map_some, false_eq_decide_iff, Part.mem_bind_iff,
Part.mem_map_iff, Nat.mem_rfind, List.tail_cons, true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]
constructor
· rintro ⟨v', h1, rfl⟩
suffices
∀ v₁ : List ℕ,
v' ∈
PFun.fix
(fun v =>
(cf.eval v).bind fun y =>
Part.some <|
if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail))
v₁ →
∀ n,
(v₁ = n :: v.val) →
(∀ m < n, ¬f (m ::ᵥ v) = 0) →
∃ a : ℕ, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
by exact this _ h1 0 rfl (by rintro _ ⟨⟩)
clear h1
intro v₀ h1
refine PFun.fixInduction h1 fun v₁ h2 IH => ?_
clear h1
rintro n rfl hm
have := PFun.mem_fix_iff.1 h2
simp only [hf, Part.bind_some] at this
split_ifs at this with h
· simp only [List.headI_cons, exists_false, or_false, Part.mem_some_iff, List.tail_cons, false_and, Sum.inl.injEq,
reduceCtorEq] at this
subst this
exact ⟨_, ⟨h, @(hm)⟩, rfl⟩
· refine IH (n.succ :: v.val) (by simp_all) _ rfl fun m h' => ?_
obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h'
exacts [hm _ h, h]
· rintro ⟨n, ⟨hn, hm⟩, rfl⟩
refine ⟨n.succ :: v.1, ?_, rfl⟩
have :
(n.succ :: v.1 : List ℕ) ∈
PFun.fix
(fun v =>
(cf.eval v).bind fun y =>
Part.some <| if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail))
(n :: v.val) :=
PFun.mem_fix_iff.2 (Or.inl (by simp [hf, hn]))
generalize (n.succ :: v.1 : List ℕ) = w at this ⊢
clear hn
induction n with
| zero => exact this
| succ n
IH =>
refine IH (fun {m} h' => hm (Nat.lt_succ_of_lt h')) (PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, this⟩))
simp only [hf, hm n.lt_succ_self, Part.bind_some, List.headI, if_false, Part.mem_some_iff, List.tail_cons]
