English
The clear operation updates the stack deterministically in the TM2 translation, preserving the unraveling of the continuation.
Русский
Операция clear детерминирована в переводе TM2 и сохраняет развёртывание продолжения.
LaTeX
$$$\\text{clear\\_ok} : \\; \\text{Reaches}_1 (\\text{TM2.step } tr)(\\langle \\dots,\\operatorname{clear}(p,k,q)\\rangle) \\Rightarrow \\langle\\dots\\rangle$$$
Lean4
theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)) :
Reaches₁ (TM2.step tr) ⟨some (Λ'.clear p k q), s, S⟩ ⟨some q, o, update S k L₂⟩ := by
induction L₁ generalizing S s with
| nil =>
refine TransGen.head' rfl ?_
rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
revert e; rcases S k with - | ⟨a, Sk⟩ <;> intro e
· cases e
rfl
simp only [splitAtPred, List.head?, List.tail_cons] at e ⊢
revert e;
cases p a <;> intro e <;> simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and, reduceCtorEq] at e ⊢
rcases e with ⟨e₁, e₂⟩
rw [e₁, e₂]
| cons a L₁ IH =>
refine TransGen.head rfl ?_
rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e
· cases e
cases e₂ : p a' <;> simp only [e₂, cond] at e
swap
· cases e
rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩
rw [e₃] at e
cases e
simp only [List.head?_cons, e₂, List.tail_cons, cond_false]
convert @IH _ (update S k Sk) _ using 2 <;> simp [e₃]
