-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
halt :
  ∀ (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet Cont.halt v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont Cont.halt))) s
            (elim (trList v) [] [] (trContStack Cont.halt)))
          b₂
cons₁ :
  ∀ (fs : Code) (as : List ℕ) (k : Cont),
    (∀ (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepRet k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k)))
              b₂) →
      ∀ (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepRet (Cont.cons₁ fs as k) v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
                (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
              b₂
cons₂ :
  ∀ (ns : List ℕ) (k : Cont)
    (IH :
      ∀ (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepRet k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k)))
              b₂)
    (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet (Cont.cons₂ ns k) v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.cons₂ ns k)))) s
            (elim (trList v) [] [] (trContStack (Cont.cons₂ ns k))))
          b₂
comp :
  ∀ (f : Code) (k : Cont),
    (∀ (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepRet k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k)))
              b₂) →
      ∀ (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepRet (Cont.comp f k) v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.comp f k)))) s
                (elim (trList v) [] [] (trContStack (Cont.comp f k))))
              b₂
fix :
  ∀ (f : Code) (k : Cont)
    (IH :
      ∀ (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepRet k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k)))
              b₂)
    (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepRet (Cont.fix f k) v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont (Cont.fix f k)))) s
            (elim (trList v) [] [] (trContStack (Cont.fix f k))))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) s (elim (trList v) [] [] (trContStack k))) b₂

Tactic:
induction k generalizing v s with
  | halt => exact ⟨_, rfl, TransGen.single rfl⟩
  | cons₁ fs as k _ =>
    obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none
    refine ⟨s', h₁, TransGen.head rfl ?_⟩; simp
    refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_; · rfl
    simp only [TM2.step, Option.mem_def, Option.elim, id_eq, elim_update_main, elim_main, elim_aux,
      List.append_nil, elim_update_aux]
    refine (move₂_ok (L₁ := ?_) (o := ?_) (L₂ := ?_) (by decide) rfl ?_).trans ?_
    pick_goal 4
    · exact splitAtPred_eq _ _ _ (some Γ'.consₗ) _
        (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, rfl⟩
    refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_; · rfl
    simp only [TM2.step, Option.mem_def, Option.elim, elim_update_stack, elim_main,
      List.append_nil, elim_update_main, id_eq, elim_update_aux,
      elim_aux, elim_stack]
    exact h₂
  | cons₂ ns k IH =>
    obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none
    exact ⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩
  | comp f k _ =>
    obtain ⟨s', h₁, h₂⟩ := trNormal_respects f k v s
    exact ⟨_, h₁, TransGen.head rfl h₂⟩
  | fix f k IH =>
    rw [stepRet]
    have :
      if v.headI = 0 then natEnd ((trList v).head?.getD default) = true ∧
          (trList v).tail = trList v.tail
      else
        natEnd ((trList v).head?.getD default) = false ∧
          (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail := by
      obtain - | n := v
      · exact ⟨rfl, rfl⟩
      rcases n with - | n
      · simp
      rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]
      cases (n : Num).succ' <;> exact ⟨rfl, rfl⟩
    by_cases h : v.headI = 0 <;> simp only [h, ite_true, ite_false] at this ⊢
    · obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?
      refine ⟨c, h₁, TransGen.head rfl ?_⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]
      exact h₂
    · obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)
      refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this.1]
      convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
      · simp
        convert! rfl
      · exact fun x h => trNat_natEnd _ _ (List.tail_subset _ h)
      · exact ⟨rfl, this.2⟩

Premises used: Turing.PartrecToTM2.halt, Turing.PartrecToTM2.tr, Turing.TM2.stepAux, Turing.PartrecToTM2.K'.elim_aux, Turing.PartrecToTM2.Γ'.consₗ, ite_false, Turing.PartrecToTM2.Γ'.cons, Option.some, Turing.PartrecToTM2.splitAtPred_false, Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_main, ite_true, Turing.TM2.step, Turing.PartrecToTM2.pop', List.tail, List.append_nil, Turing.PartrecToTM2.K'.elim_update_stack, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, And.intro, Turing.PartrecToTM2.clear_ok, Turing.PartrecToTM2.move₂_ok, List.headI, Turing.PartrecToTM2.K'.elim_stack, Option.elim, Turing.PartrecToTM2.trList_ne_consₗ, Turing.PartrecToTM2.trNat, Turing.PartrecToTM2.trCont, List.tail_subset, Turing.ToPartrec.stepRet, rfl, Bool.decide_false, id_eq, Turing.PartrecToTM2.trNat_natEnd, Turing.PartrecToTM2.K'.elim_update_aux, Option.mem_def