tr_respects — Mathlib

English

The translation tr preserves the step relation up to equality of configurations.

Русский

Перевод tr сохраняет отношение перехода вплоть до равенства конфигураций.

LaTeX

$$tr_respects (M) : Respects (TM1.step M) (TM0.step (tr M)) (fun c1 c2 => trCfg M c1 = c2)$$

Lean4

theorem tr_respects [Inhabited Γ] :
    Respects (TM1.step M) (TM0.step (tr M)) fun (c₁ : TM1.Cfg Γ Λ σ) (c₂ : TM0.Cfg Γ (Λ' M)) ↦ trCfg M c₁ = c₂ :=
  fun_respects.2 fun ⟨l₁, v, T⟩ ↦ by
    rcases l₁ with - | l₁; · exact rfl
    simp only [trCfg, TM1.step, FRespects, Option.map]
    induction M l₁ generalizing v T with
    | move _ _ IH => exact TransGen.head rfl (IH _ _)
    | write _ _ IH => exact TransGen.head rfl (IH _ _)
    | load _ _ IH => exact (reaches₁_eq (by rfl)).2 (IH _ _)
    | branch p _ _ IH₁ IH₂ =>
      unfold TM1.stepAux; cases e : p T.1 v
      · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₂ _ _)
      · exact (reaches₁_eq (by simp only [TM0.step, tr, trAux, e]; rfl)).2 (IH₁ _ _)
    | _ => exact TransGen.single (congr_arg some (congr (congr_arg TM0.Cfg.mk rfl) (Tape.write_self T)))

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