English
Reaffirmation that eval(stepRet k v) equals halt mapped over k.eval v, in the monadic sense.
Русский
Утверждение, что eval(stepRet k v) = map halt (k.eval v).
LaTeX
$$$\\forall k\\,v.\\; eval\\ stepRet\\ k\\ v = \\operatorname{map}\\ (\\text{halt}) (k.eval\\ v)$$$
Lean4
theorem stepRet_eval {k v} : eval step (stepRet k v) = Cfg.halt <$> k.eval v := by
induction k generalizing v with
| halt =>
simp only [Cont.eval, map_pure]
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)
| cons₁ fs as k IH =>
rw [Cont.eval, stepRet, code_is_ok]
simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
rw [reaches_eval]; swap
· exact ReflTransGen.single rfl
rw [stepRet, IH, bind_pure_comp]
| cons₂ ns k IH => rw [Cont.eval, stepRet]; exact IH
| comp f k IH =>
rw [Cont.eval, stepRet, code_is_ok]
simp only [← bind_pure_comp, bind_assoc]; congr; funext v'
rw [reaches_eval]; swap
· exact ReflTransGen.single rfl
rw [IH, bind_pure_comp]
| fix f k IH =>
rw [Cont.eval, stepRet]; simp only
split_ifs; · exact IH
simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
congr; funext; rw [bind_pure_comp, ← IH]
exact reaches_eval (ReflTransGen.single rfl)
