English
There is a correspondence between the initialization configuration of TM2 and the initialization of TM1 under the translator tr.
Русский
Существует соответствие между инициализацией TM2 и инициализацией TM1 через переводчик tr.
LaTeX
$$$ TrCfg (TM2.init k L) (TM1.init (trInit k L)) $$$
Lean4
theorem trCfg_init (k) (L : List (Γ k)) :
TrCfg (TM2.init k L) (TM1.init (trInit k L) : TM1.Cfg (Γ' K Γ) (Λ' K Γ Λ σ) σ) :=
by
rw [(_ : TM1.init _ = _)]
· refine ⟨ListBlank.mk (L.reverse.map fun a ↦ update default k (some a)), fun k' ↦ ?_⟩
refine ListBlank.ext fun i ↦ ?_
rw [ListBlank.map_mk, ListBlank.nth_mk, List.getI_eq_iget_getElem?, List.map_map]
have :
((proj k').f ∘ fun a => update (β := fun k => Option (Γ k)) default k (some a)) = fun a =>
(proj k').f (update (β := fun k => Option (Γ k)) default k (some a)) :=
rfl
rw [this, List.getElem?_map, proj, PointedMap.mk_val]
simp only []
by_cases h : k' = k
· subst k'
simp only [Function.update_self]
rw [ListBlank.nth_mk, List.getI_eq_iget_getElem?, ← List.map_reverse, List.getElem?_map]
· simp only [Function.update_of_ne h]
rw [ListBlank.nth_mk, List.getI_eq_iget_getElem?, List.map, List.reverse_nil]
cases L.reverse[i]? <;> rfl
· rw [trInit, TM1.init]
congr <;> cases L.reverse <;> try rfl
simp only [List.map_map, List.tail_cons, List.map]
rfl
