-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k) L = ListBlank.mk (List.map some (S k)).reverse
o : StAct K Γ σ k
push :
  ∀ (f : σ → Γ k),
    ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
      (∀ (k_1 : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
            ListBlank.mk
              (List.map some
                  (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) (StAct.push (Γ := Γ) f))
                    k_1)).reverse) ∧
        TM1.stepAux (trStAct (Γ := Γ) q (StAct.push (Γ := Γ) f)) v
            ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
          TM1.stepAux q (stVar (Γ := Γ) v (S k) (StAct.push (Γ := Γ) f))
            ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) (StAct.push (Γ := Γ) f)).length]
              (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
push₁ :
  ∀ (f : σ → Γ k),
    ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
      (∀ (k_1 : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
            ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (f v :: S k) k_1)).reverse) ∧
        TM1.stepAux q v
            (Tape.move Dir.right
              (Tape.write
                (((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1,
                  update (β := fun (k : K) ↦ Option (Γ k))
                    ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.2 k (some (f v)))
                ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
          TM1.stepAux q v ((Tape.move Dir.right)^[(f v :: S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
peek :
  ∀ (f : σ → Option (Γ k) → σ),
    ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
      (∀ (k_1 : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
            ListBlank.mk
              (List.map some
                  (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
                    k_1)).reverse) ∧
        TM1.stepAux (trStAct (Γ := Γ) q (StAct.peek (Γ := Γ) f)) v
            ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
          TM1.stepAux q (stVar (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f))
            ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) (StAct.peek (Γ := Γ) f)).length]
              (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
peek₁ :
  ∀ (f : σ → Option (Γ k) → σ),
    ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
      (∀ (k_1 : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
            ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (S k) k_1)).reverse) ∧
        TM1.stepAux q
            (f v
              ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                k))
            (Tape.move Dir.right
              (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))))) =
          TM1.stepAux q (f v (S k).head?) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
pop :
  ∀ (f : σ → Option (Γ k) → σ),
    ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
      (∀ (k_1 : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
            ListBlank.mk
              (List.map some
                  (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) (StAct.pop (Γ := Γ) f))
                    k_1)).reverse) ∧
        TM1.stepAux (trStAct (Γ := Γ) q (StAct.pop (Γ := Γ) f)) v
            ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
          TM1.stepAux q (stVar (Γ := Γ) v (S k) (StAct.pop (Γ := Γ) f))
            ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) (StAct.pop (Γ := Γ) f)).length]
              (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
pop₁ :
  ∀ (f : σ → Option (Γ k) → σ),
    ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
      (∀ (k_1 : K),
          ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
            ListBlank.mk (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (S k).tail k_1)).reverse) ∧
        (bif ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))).head.1 then
            TM1.stepAux q (f v none) ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))
          else
            TM1.stepAux q
              (f v
                ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                  k))
              (Tape.write
                ((Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.1,
                  update (β := fun (k : K) ↦ Option (Γ k))
                    (Tape.move Dir.left
                          ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))).head.2
                    k none)
                (Tape.move Dir.left ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L)))))) =
          TM1.stepAux q (f v (S k).head?)
            ((Tape.move Dir.right)^[(S k).tail.length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))
⊢ ∃ (L' : ListBlank ((k : K) → Option (Γ k))),
    (∀ (k_1 : K),
        ListBlank.map (proj (Γ := fun (k : K) ↦ Option (Γ k)) k_1) L' =
          ListBlank.mk
            (List.map some (update (β := fun (a : K) ↦ List (Γ a)) S k (stWrite (Γ := Γ) v (S k) o) k_1)).reverse) ∧
      TM1.stepAux (trStAct (Γ := Γ) q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L))) =
        TM1.stepAux q (stVar (Γ := Γ) v (S k) o)
          ((Tape.move Dir.right)^[(stWrite (Γ := Γ) v (S k) o).length] (Tape.mk' ∅ (addBottom (Γ := Γ) L')))

Tactic:
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']

Premises used: List.head?, Turing.proj, Function.update_eq_self, le_refl, List.getElem_singleton, Turing.Tape.move_right_n_head, Turing.Tape.move_left_mk', Turing.ListBlank.nth_modifyNth, Turing.TM2to1.stk_nth_val, List.length_cons, List.map, List.length_reverse, Function.iterate_succ', List.getI_append, le_of_lt, Function.comp, List.length_singleton, Nat.lt_succ_self, List.length_append, List.getElem?_concat_length, Turing.ListBlank.head_cons, Turing.TM1.stepAux, List.tail, Turing.Tape.write_mk', Turing.Tape.mk'_head, Nat.sub_self, List.reverse_cons, List.getI_eq_default, List.tail_nil, Nat.add_one_le_iff, Turing.Tape.move_left_right, Turing.Tape.move_right_left, Turing.TM2to1.trStAct, List.length_map, List.getI_eq_getElem, Turing.ListBlank.ext, Turing.Tape.mk'_nth_nat, Function.update_self, Function.iterate_zero_apply, Turing.ListBlank.nth_map, Turing.PointedMap.mk_val, List.length, Turing.ListBlank.nth_mk, Turing.TM2to1.addBottom_nth_snd, Turing.TM2to1.stVar, Turing.proj_map_nth, Turing.TM2to1.stWrite, List.getElem_append_right