English
Evaluating stepRet k v yields halt mapped from k.eval v, i.e., the result is the halt state applied to the evaluation of k on v.
Русский
Оценка stepRet k v даёт переход к состоянию останова, отображённому на вычисление k на v.
LaTeX
$$$\\forall k\\,v.\\; eval\\ step\\ (stepRet\\ k\\ v) = \\operatorname{map}\\ (\\text{halt}) (k.eval\\ v)$$$
Lean4
theorem code_is_ok (c) : Code.Ok c := by
induction c with (intro k v; rw [stepNormal])
| cons f fs IHf IHfs =>
rw [Code.eval, IHf]
simp only [bind_assoc, pure_bind]; congr; funext v
rw [reaches_eval]; swap
· exact ReflTransGen.single rfl
rw [stepRet, IHfs]; congr; funext v'
refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_) <;>
exact reaches_eval (ReflTransGen.single rfl)
| comp f g IHf IHg =>
rw [Code.eval, IHg]
simp only [bind_assoc]; congr; funext v
rw [reaches_eval]; swap
· exact ReflTransGen.single rfl
rw [stepRet, IHf]
| case f g IHf IHg =>
simp only [Code.eval]
cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]
| fix f IHf => rw [cont_eval_fix IHf]
| _ => simp only [Code.eval, pure_bind]
