English
Let k, v, s be given. There exists b2 such that TrCfg (stepRet k v) b2, and the machine, through a single TM2.step, reaches the configuration with ret k encoded, i.e., the state ⟨some (Λ'.ret (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩, yielding b2.
Русский
Пусть даны k, v, s. Существет b2 such, что TrCfg(stepRet k v) b2, и машина, выполняя один шаг TM2.step, достигает конфигурации с кодированным возвращением ret k: ⟨some (Λ'.ret (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩.
LaTeX
$$$\exists b_2\,\big(\operatorname{TrCfg}(\operatorname{stepRet}(k,v),b_2) \land \operatorname{Reaches}_1(\mathrm{TM2.step}\;\mathrm{tr})\;\langle\mathrm{some}(\Lambda'.ret(\operatorname{trCont}(k))),\; s,\; K'.elim(\operatorname{trList}(v))\ []\ []\ (\operatorname{trContStack}(k))\rangle\; b_2\big)$$$
Lean4
theorem tr_ret_respects (k v s) :
∃ b₂,
TrCfg (stepRet k v) b₂ ∧
Reaches₁ (TM2.step tr) ⟨some (Λ'.ret (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩ b₂ :=
by
induction k generalizing v s with
| halt => exact ⟨_, rfl, TransGen.single rfl⟩
| cons₁ fs as k _ =>
obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none
refine ⟨s', h₁, TransGen.head rfl ?_⟩; simp
refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_; · rfl
simp only [TM2.step, Option.mem_def, Option.elim, id_eq, elim_update_main, elim_main, elim_aux, List.append_nil,
elim_update_aux]
refine (move₂_ok (L₁ := ?_) (o := ?_) (L₂ := ?_) (by decide) rfl ?_).trans ?_
pick_goal 4
· exact splitAtPred_eq _ _ _ (some Γ'.consₗ) _ (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, rfl⟩
refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_; · rfl
simp only [TM2.step, Option.mem_def, Option.elim, elim_update_stack, elim_main, List.append_nil, elim_update_main,
id_eq, elim_update_aux, elim_aux, elim_stack]
exact h₂
| cons₂ ns k IH =>
obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none
exact ⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩
| comp f k _ =>
obtain ⟨s', h₁, h₂⟩ := trNormal_respects f k v s
exact ⟨_, h₁, TransGen.head rfl h₂⟩
| fix f k IH =>
rw [stepRet]
have :
if v.headI = 0 then natEnd (trList v).head?.iget = true ∧ (trList v).tail = trList v.tail
else natEnd (trList v).head?.iget = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail :=
by
obtain - | n := v
· exact ⟨rfl, rfl⟩
rcases n with - | n
· simp
rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]
cases (n : Num).succ' <;> exact ⟨rfl, rfl⟩
by_cases h : v.headI = 0 <;> simp only [h, ite_true, ite_false] at this ⊢
· obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?
refine ⟨c, h₁, TransGen.head rfl ?_⟩
rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]
exact h₂
· obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)
refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this.1]
convert clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
· simp
convert rfl
· exact fun x h => trNat_natEnd _ _ (List.tail_subset _ h)
· exact ⟨rfl, this.2⟩
