trNormal_respects — Mathlib

English

Let c, k, v, s be given. There exists a final state b2 such that the next-step normal run from c on k with v yields a configuration b2, and the machine, via a single-step transition, reaches b2 from the initial encoded state described by c, k, v, s.

Русский

Пусть заданы c, k, v, s. Существует финальное состояние b2 такое, что переход stepNormal(c, k, v) приводит к b2 в конфигурации TrCfg, а машина по одному шагу TM2.step достигает b2 из начального состояния, закодированного триггерами c, k, v, s.

LaTeX

$$$\exists b_2\,\big(\operatorname{TrCfg}(\operatorname{stepNormal}(c,k,v),b_2) \land \Reaches_1(\mathrm{TM2.step}\;\mathrm{tr})\;\langle\mathrm{some}(\operatorname{trNormal}(c,\mathrm{trCont}(k))),\; s,\; K'.\elim(\operatorname{trList}(v))\ []\ []\ (\operatorname{trContStack}(k))\rangle\; b_2\big)$$$

Lean4

theorem trNormal_respects (c k v s) :
    ∃ b₂,
      TrCfg (stepNormal c k v) b₂ ∧
        Reaches₁ (TM2.step tr) ⟨some (trNormal c (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩ b₂ :=
  by
  induction c generalizing k v s with
  | zero' => refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩; simp
  | succ => refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩
  | tail =>
    let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons
    refine ⟨_, ⟨o, rfl⟩, ?_⟩; convert clear_ok _ using 2
    · simp; rfl
    swap
    refine splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) ?_
    cases v <;> simp [o]
  | cons f fs IHf _ =>
    obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
    refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
    simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main, elim_main, elim_rev,
      elim_update_rev]
    refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
    convert h₂ using 2
    simp [List.reverseAux_eq, trContStack]
  | comp f _ _ IHg => exact IHg (Cont.comp f k) v s
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only
    obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
    revert h; rcases v.headI with - | n <;> intro h
    · obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
  | fix f IH => apply IH

Похожие утверждения