Lean4
theorem tr_respects_aux₂ [DecidableEq K] {k : K} {q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ} {v : σ} {S : ∀ k, List (Γ k)}
{L : ListBlank (∀ k, Option (Γ k))} (hL : ∀ k, L.map (proj k) = ListBlank.mk ((S k).map some).reverse)
(o : StAct K Γ σ k) :
let v' := stVar v (S k) o
let Sk' := stWrite v (S k) o
let S' := update S k Sk'
∃ L' : ListBlank (∀ k, Option (Γ k)),
(∀ k, L'.map (proj k) = ListBlank.mk ((S' k).map some).reverse) ∧
TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) =
TM1.stepAux q v' ((Tape.move Dir.right)^[(S' k).length] (Tape.mk' ∅ (addBottom L'))) :=
by simp only [Function.update_self];
cases o with simp only [stWrite, stVar, trStAct, TM1.stepAux]
| push f =>
have := Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k (some (f v)))
refine
⟨_, fun k' ↦ ?_, by
-- Porting note: `rw [...]` to `erw [...]; rfl`.
-- https://github.com/leanprover-community/mathlib4/issues/5164
rw [Tape.move_right_n_head, List.length, Tape.mk'_nth_nat, this]
erw [addBottom_modifyNth fun a ↦ update a k (some (f v))]
rw [Nat.add_one, iterate_succ']
rfl⟩
refine ListBlank.ext fun i ↦ ?_
rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
by_cases h' : k' = k
· subst k'
split_ifs with h <;> simp only [List.reverse_cons, Function.update_self, ListBlank.nth_mk, List.map]
·
rw [List.getI_eq_getElem _, List.getElem_append_right] <;>
simp only [List.length_append, List.length_reverse, List.length_map, ← h, Nat.sub_self, List.length_singleton,
List.getElem_singleton, le_refl, Nat.lt_succ_self]
rw [← proj_map_nth, hL, ListBlank.nth_mk]
rcases lt_or_gt_of_ne h with h | h
· rw [List.getI_append]
simpa only [List.length_map, List.length_reverse] using h
·
rw [List.getI_eq_default, List.getI_eq_default] <;>
simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse, List.length_append,
List.length_map]
· split_ifs <;> rw [Function.update_of_ne h', ← proj_map_nth, hL]
rw [Function.update_of_ne h']
| peek f =>
rw [Function.update_eq_self]
use L, hL; rw [Tape.move_left_right]; congr
cases e : S k; · rfl
rw [List.length_cons, iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head, Tape.mk'_nth_nat,
addBottom_nth_snd, stk_nth_val _ (hL k), e, List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length]
rfl
| pop f =>
rcases e : S k with - | ⟨hd, tl⟩
· simp only [Tape.mk'_head, ListBlank.head_cons, Tape.move_left_mk', List.length, Tape.write_mk', List.head?,
iterate_zero_apply, List.tail_nil]
rw [← e, Function.update_eq_self]
exact ⟨L, hL, by rw [addBottom_head_fst, cond]⟩
· refine
⟨_, fun k' ↦ ?_, by
erw [List.length_cons, Tape.move_right_n_head, Tape.mk'_nth_nat, addBottom_nth_succ_fst, cond_false,
iterate_succ', Function.comp, Tape.move_right_left, Tape.move_right_n_head, Tape.mk'_nth_nat,
Tape.write_move_right_n fun a : Γ' K Γ ↦ (a.1, update a.2 k none),
addBottom_modifyNth fun a ↦ update a k none, addBottom_nth_snd, stk_nth_val _ (hL k), e,
show (List.cons hd tl).reverse[tl.length]? = some hd by
rw [List.reverse_cons, ← List.length_reverse, List.getElem?_concat_length],
List.head?, List.tail]⟩
refine ListBlank.ext fun i ↦ ?_
rw [ListBlank.nth_map, ListBlank.nth_modifyNth, proj, PointedMap.mk_val]
by_cases h' : k' = k
· subst k'
split_ifs with h <;> simp only [Function.update_self, ListBlank.nth_mk, List.tail]
· rw [List.getI_eq_default]
· rfl
rw [h, List.length_reverse, List.length_map]
rw [← proj_map_nth, hL, ListBlank.nth_mk, e, List.map, List.reverse_cons]
rcases lt_or_gt_of_ne h with h | h
· rw [List.getI_append]
simpa only [List.length_map, List.length_reverse] using h
·
rw [List.getI_eq_default, List.getI_eq_default] <;>
simp only [Nat.add_one_le_iff, h, List.length, le_of_lt, List.length_reverse, List.length_append,
List.length_map]
· split_ifs <;> rw [Function.update_of_ne h', ← proj_map_nth, hL]
rw [Function.update_of_ne h']
