tr_respects — Mathlib

English

A compatibility result: stepping TM0 configuration corresponds to stepping TM1 configuration after transformation.

Русский

Совместимость переходов: переход конфигурации TM00 соответствует переходу конфигурации TM1 после преобразования.

LaTeX

$$$$\\operatorname{tr\\_respects}: \\operatorname{Respects}(\\operatorname{TM0.step} M, \\operatorname{TM1.step}(\\operatorname{tr} M)) \\; (a,b) \\Rightarrow \\; \\operatorname{trCfg}(M,a) = b.$$$$

Lean4

theorem tr_respects : Respects (TM0.step M) (TM1.step (tr M)) fun a b ↦ trCfg M a = b :=
  fun_respects.2 fun ⟨q, T⟩ ↦ by
    rcases e : M q T.1 with - | val
    · simp only [TM0.step, trCfg, e]; exact Eq.refl none
    obtain ⟨q', s⟩ := val
    simp only [FRespects, TM0.step, trCfg, e, Option.isSome, cond, Option.map_some]
    revert e
    have :
      TM1.step (tr M) ⟨some (Λ'.act s q'), (), T⟩ =
        some
          ⟨some (Λ'.normal q'), (),
            match s with
            | TM0.Stmt.move d => T.move d
            | TM0.Stmt.write a => T.write a⟩ :=
      by cases s <;> rfl
    intro e
    refine TransGen.head ?_ (TransGen.head' this ?_)
    · simp only [TM1.step, TM1.stepAux, tr]
      rw [e]
      rfl
    cases e' : M q' _
    · apply ReflTransGen.single
      simp only [TM1.step, TM1.stepAux, tr]
      rw [e']
      rfl
    · rfl

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