-- Mathlib/Computability/TMToPartrec.lean
theorem trNormal_respects (c k v s) :
    ∃ b₂,
      TrCfg (stepNormal c k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          ⟨some (trNormal c (trCont k)), s, K'.elim (trList v) [] [] (trContStack k)⟩ b₂

Proof state:
case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg ((fun k v => Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
simp only

Result:
case case
f g : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal g k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal g (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.case g) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Proof state:
case fix
f : Code
IH :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal f.fix k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal f.fix (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
apply IH

Result:
no goals

Proof state:
case h.e'_4.h.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = elim ?tail.convert_7 [] [] (trContStack k)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_1.h.e'_7
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.cons₁ fs v k))), var := none,
      stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k)) }
    c
⊢ elim ((trList v).reverse.reverseAux []) [] []
      ((trList v).reverse.reverseAux ((some Γ'.consₗ).iget :: trContStack k)) =
    elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))

Tactic:
simp [List.reverseAux_eq, trContStack]

Result:
no goals

Proof state:
case tail
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ Reaches₁ (TM2.step tr)
    { l := some (trNormal Code.tail (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) }
    { l := some (Λ'.ret (trCont k)), var := o, stk := elim (trList v.tail) [] [] (trContStack k) }

Tactic:
convert clear_ok _ using 2

Result:
case h.e'_4.h.e'_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = update (elim (trList v) [] [] (trContStack k)) main ?tail.convert_7

case tail.convert_5
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ List Γ'

case tail.convert_7
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ List Γ'

case tail.convert_9
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn v none fun x x => some Γ'.cons
⊢ splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (?tail.convert_5, o, ?tail.convert_7)

Proof state:
case cons.intro.intro
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.cons₁ fs v k))), var := none,
      stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k)) }
    c
⊢ ∃ b₂,
    TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal (f.cons fs) (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩

Result:
case cons.intro.intro
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal f (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
a_ih✝ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ b₂,
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step tr)
          { l := some (trNormal fs (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂
k : Cont
v : List ℕ
s : Option Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step tr)
    { l := some (trNormal f (trCont (Cont.cons₁ fs v k))), var := none,
      stk := elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k)) }
    c
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    { l := some (trNormal f (Cont'.cons₁ fs (trCont k))).copy, var := none,
      stk :=
        update
          (update
            (update (elim (trList v) [] [] (trContStack k)) stack
              ((fun s => ((fun x => some Γ'.consₗ) s).iget) s :: elim (trList v) [] [] (trContStack k) stack))
            main [])
          rev
          ((update (elim (trList v) [] [] (trContStack k)) stack
                ((fun s => ((fun x => some Γ'.consₗ) s).iget) s :: elim (trList v) [] [] (trContStack k) stack)
                main).reverseAux
            (update (elim (trList v) [] [] (trContStack k)) stack
              ((fun s => ((fun x => some Γ'.consₗ) s).iget) s :: elim (trList v) [] [] (trContStack k) stack) rev)) }
    c

Proof state:
case succ
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ b₂,
    TrCfg (stepNormal Code.succ k v) b₂ ∧
      Reaches₁ (TM2.step tr)
        { l := some (trNormal Code.succ (trCont k)), var := s, stk := elim (trList v) [] [] (trContStack k) } b₂

Tactic:
refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩

Result:
no goals