awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ ∃ (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₂

Tactic:
⟨s', h₁, TransGen.head rfl ?_⟩

Premises used: Relation.TransGen.head, And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
cons₁ :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
    s'
⊢ ∃ (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₂

Tactic:
refine ⟨s', h₁, TransGen.head rfl ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ main ≠ rev ∧ aux ≠ rev ∧ main ≠ aux

Tactic:
decide
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
cons₁ : elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) rev = []
cons₂ :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ')
      (some
        (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
          (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs (trCont k).cons₂))))
      none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))) main
          (Option.elim none id List.cons []))
        aux
        (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) main ++
          elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) aux)))
    s'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ TM2.step (Γ := fun (x : K') ↦ Γ') tr a = some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.ret (trCont (Cont.cons₁ fs as k)))) s
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))))
    s'

Tactic:
refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_

Premises used: Turing.PartrecToTM2.splitAtPred_false, Relation.TransGen.trans, Turing.PartrecToTM2.move₂_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) rev = []

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
cons₁ :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ')
      (some
        (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
          (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs (trCont k).cons₂))))
      none (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))))
    s'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ')
      (some
        (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
          (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs (trCont k).cons₂))))
      none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k))) main
          (Option.elim none id List.cons []))
        aux
        (elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) main ++
          elim (trList v) [] [] (trContStack (Cont.cons₁ fs as k)) aux)))
    s'

Tactic:
simp only [TM2.step, Option.mem_def, Option.elim, id_eq, elim_update_main, elim_main, elim_aux,
      List.append_nil, elim_update_aux]

Premises used: Turing.PartrecToTM2.K'.elim_aux, Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_main, Turing.TM2.step, List.append_nil, Option.elim, id_eq, Turing.PartrecToTM2.K'.elim_update_aux, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ stack ≠ rev ∧ main ≠ rev ∧ stack ≠ main

Tactic:
decide
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
cons₁ : List Γ'
cons₂ : Option Γ'
cons₃ : List Γ'
cons₄ :
  splitAtPred (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) stack) =
    (trList as, some Γ'.consₗ, trLList (contStack k))
cons₅ :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs (trCont k).cons₂)))
      none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
          ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
        main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main)))
    s'
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ')
      (some
        (move₂ (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) stack main
          (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs (trCont k).cons₂))))
      none (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))))
    s'

Tactic:
refine (move₂_ok (L₁ := ?_) (o := ?_) (L₂ := ?_) (by decide) rfl ?_).trans ?_

Premises used: Relation.TransGen.trans, Turing.PartrecToTM2.move₂_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ splitAtPred (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) stack) =
    (trList as, some Γ'.consₗ, trLList (contStack k))

Tactic:
splitAtPred_eq _ _ _ (some Γ'.consₗ) _
        (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, rfl⟩

Premises used: Turing.PartrecToTM2.Γ'.consₗ, Option.some, Turing.PartrecToTM2.trContStack, Turing.PartrecToTM2.K'.elim, Turing.PartrecToTM2.trLList, Turing.PartrecToTM2.splitAtPred_eq, And.intro, Turing.PartrecToTM2.trList_ne_consₗ, rfl, Bool.decide_false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ splitAtPred (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) stack) =
    (trList as, some Γ'.consₗ, trLList (contStack k))

Tactic:
exact splitAtPred_eq _ _ _ (some Γ'.consₗ) _
        (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, rfl⟩

Premises used: Turing.PartrecToTM2.Γ'.consₗ, Option.some, Turing.PartrecToTM2.splitAtPred_eq, And.intro, Turing.PartrecToTM2.trList_ne_consₗ, rfl, Bool.decide_false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ aux ≠ rev ∧ stack ≠ rev ∧ aux ≠ stack

Tactic:
decide
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
cons₁ :
  update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
        ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
      main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) rev =
    []
cons₂ :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k).cons₂)) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
              ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
            main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main))
          aux (Option.elim none id List.cons []))
        stack
        (update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
              ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
            main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) aux ++
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
              ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
            main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) stack)))
    s'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (move₂ (fun (x : Γ') ↦ false) aux stack (trNormal fs (trCont k).cons₂)))
      none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
          ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
        main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main)))
    s'

Tactic:
refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_

Premises used: Turing.PartrecToTM2.splitAtPred_false, Relation.TransGen.trans, Turing.PartrecToTM2.move₂_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
        ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
      main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) rev =
    []

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
cons₁ :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k).cons₂)) none
      (elim (trList as) [] [] (trList v ++ Γ'.consₗ :: trLList (contStack k))))
    s'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k).cons₂)) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
              ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
            main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main))
          aux (Option.elim none id List.cons []))
        stack
        (update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
              ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
            main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) aux ++
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k))) stack
              ((some Γ'.consₗ).elim id List.cons (trLList (contStack k))))
            main (trList as ++ elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) main) stack)))
    s'

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

Premises used: Turing.PartrecToTM2.K'.elim_aux, Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_main, Turing.TM2.step, List.append_nil, Turing.PartrecToTM2.K'.elim_update_stack, Turing.PartrecToTM2.K'.elim_stack, Option.elim, id_eq, Turing.PartrecToTM2.K'.elim_update_aux, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k).cons₂)) none
      (elim (trList as) [] [] (trList v ++ Γ'.consₗ :: trLList (contStack k))))
    s'

Tactic:
h₂

Premises used: Turing.PartrecToTM2.trContStack, Turing.TM2.step, Turing.PartrecToTM2.trLList, StateTransition.Reaches₁, Turing.PartrecToTM2.trCont
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
fs : Code
as : List ℕ
k : Cont
a_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 Γ'
s' : Cfg'
h₁ : TrCfg (stepNormal fs (Cont.cons₂ v k) as) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont (Cont.cons₂ v k)))) none
      (elim (trList as) [] [] (trContStack (Cont.cons₂ v k))))
    s'
⊢ TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k).cons₂)) none
      (elim (trList as) [] [] (trList v ++ Γ'.consₗ :: trLList (contStack k))))
    s'

Tactic:
exact h₂