Lean4
theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
Turing.eval step (stepNormal f (Cont.fix f k) v) = f.fix.eval v >>= fun v => Turing.eval step (Cfg.ret k v) :=
by
refine Part.ext fun x => ?_
simp only [Part.bind_eq_bind, Part.mem_bind_iff]
constructor
· suffices
∀ c,
x ∈ eval step c →
∀ v c',
c = Cfg.then c' (Cont.fix f k) →
Reaches step (stepNormal f Cont.halt v) c' →
∃ v₁ ∈ f.eval v,
∃ v₂ ∈ if List.headI v₁ = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
by
intro h
obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ := this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl
refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
simp only [Part.eq_some_iff.2 hv₁, Part.map_some]
split_ifs at hv₂ ⊢
· rw [Part.mem_some_iff.1 hv₂]
exact Or.inl (Part.mem_some _)
· exact Or.inr ⟨_, Part.mem_some _, hv₂⟩
refine fun c he => evalInduction he fun y h IH => ?_
rintro v (⟨v'⟩ | ⟨k', v'⟩) rfl hr <;> rw [Cfg.then] at h IH <;> simp only [] at h IH
· have := mem_eval.2 ⟨hr, rfl⟩
rw [fok, Part.bind_eq_bind, Part.mem_bind_iff] at this
obtain ⟨v'', h₁, h₂⟩ := this
rw [reaches_eval] at h₂
swap
· exact ReflTransGen.single rfl
cases Part.mem_unique h₂ (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
refine ⟨v', h₁, ?_⟩
rw [stepRet] at h
revert h
by_cases he : v'.headI = 0 <;> simp only [if_pos, if_false, he] <;> intro h
· refine ⟨_, Part.mem_some _, ?_⟩
rw [reaches_eval]
· exact h
exact ReflTransGen.single rfl
· obtain ⟨k₀, v₀, e₀⟩ := stepNormal.is_ret f Cont.halt v'.tail
have e₁ := stepNormal_then f Cont.halt (Cont.fix f k) v'.tail
rw [e₀, Cont.then, Cfg.then] at e₁
simp only [] at e₁
obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
IH (stepRet (k₀.then (Cont.fix f k)) v₀) (by rw [stepRet, if_neg he, e₁]; rfl) v'.tail _ stepRet_then
(by apply ReflTransGen.single; rw [e₀]; rfl)
refine ⟨_, PFun.mem_fix_iff.2 ?_, h₃⟩
simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]
split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂)); exact Or.inr ⟨_, rfl, hv₂⟩]
· exact IH _ rfl _ _ stepRet_then (ReflTransGen.tail hr rfl)
· rintro ⟨v', he, hr⟩
rw [reaches_eval] at hr
swap
· exact ReflTransGen.single rfl
refine PFun.fixInduction he fun v (he : v' ∈ f.fix.eval v) IH => ?_
rw [fok, Part.bind_eq_bind, Part.mem_bind_iff]
obtain he | ⟨v'', he₁', _⟩ := PFun.mem_fix_iff.1 he
· obtain ⟨v', he₁, he₂⟩ := (Part.mem_map_iff _).1 he
split_ifs at he₂ with h; cases he₂
refine ⟨_, he₁, ?_⟩
rw [reaches_eval]
swap
· exact ReflTransGen.single rfl
rwa [stepRet, if_pos h]
· obtain ⟨v₁, he₁, he₂⟩ := (Part.mem_map_iff _).1 he₁'
split_ifs at he₂ with h; cases he₂
clear he₁'
refine ⟨_, he₁, ?_⟩
rw [reaches_eval]
swap
· exact ReflTransGen.single rfl
rw [stepRet, if_neg h]
exact IH v₁.tail ((Part.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩)
