awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal Code.succ k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.succ (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

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

Premises used: Option.none, Relation.TransGen.trans, And.intro, Turing.PartrecToTM2.succ_ok, Exists.intro, Turing.PartrecToTM2.head_main_ok, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal Code.succ k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.succ (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal Code.tail k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.tail (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
⟨_, ⟨o, rfl⟩, ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
tail :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.tail (trCont k))) s
      (elim (trList v) [] [] (trContStack k)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) o (elim (trList v.tail) [] [] (trContStack k)))
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal Code.tail k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.tail (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
refine ⟨_, ⟨o, rfl⟩, ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear natEnd main (Λ'.ret (trCont k)))) s
      (elim (trList v) [] [] (trContStack k)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) o
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack k)) main (trList v.tail)))

Tactic:
clear_ok _

Premises used: Turing.PartrecToTM2.clear_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
h :
  elim (trList v.tail) [] [] (trContStack k) =
    update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack k)) main (trList v.tail)
tail tail₁ : List Γ'
tail₂ : splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (trNat v.headI, o, trList v.tail)
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.tail (trCont k))) s
      (elim (trList v) [] [] (trContStack k)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) o (elim (trList v.tail) [] [] (trContStack k)))

Tactic:
convert! clear_ok _ using 2

Premises used: Turing.PartrecToTM2.clear_ok
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
h : elim (trList v.tail) [] [] (trContStack k) = elim (trList v.tail) [] [] (trContStack k)
⊢ elim (trList v.tail) [] [] (trContStack k) =
    update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack k)) main (trList v.tail)

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ elim (trList v.tail) [] [] (trContStack k) = elim (trList v.tail) [] [] (trContStack k)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ splitAtPred natEnd (elim (trList v) [] [] (trContStack k) main) = (trNat v.headI, o, trList v.tail)

Tactic:
splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) ?_

Premises used: Turing.PartrecToTM2.splitAtPred_eq, List.headI, Turing.PartrecToTM2.trNat, Turing.PartrecToTM2.trNat_natEnd
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
v : List ℕ
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') v none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
tail :
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  Option.elim' (elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ∧ trList (List.tail []) = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ++ a :: trList (List.tail []))
    o
tail₁ :
  ∀ (head : ℕ) (tail : List ℕ),
    let o : Option Γ' :=
      List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦
        some Γ'.cons;
    Option.elim'
      (elim (trList (head :: tail)) [] [] (trContStack k) main = trNat (head :: tail).headI ∧
        trList (head :: tail).tail = [])
      (fun (a : Γ') ↦
        natEnd a = true ∧
          elim (trList (head :: tail)) [] [] (trContStack k) main =
            trNat (head :: tail).headI ++ a :: trList (head :: tail).tail)
      o
⊢ Option.elim' (elim (trList v) [] [] (trContStack k) main = trNat v.headI ∧ trList v.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList v) [] [] (trContStack k) main = trNat v.headI ++ a :: trList v.tail)
    o

Tactic:
cases v
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
s : Option Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Option.elim' (elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ∧ trList (List.tail []) = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        elim (trList []) [] [] (trContStack k) main = trNat (List.headI []) ++ a :: trList (List.tail []))
    o

Tactic:
simp [o]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont
s : Option Γ'
head : ℕ
tail : List ℕ
o : Option Γ' :=
  List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Option.elim'
    (elim (trList (head :: tail)) [] [] (trContStack k) main = trNat (head :: tail).headI ∧
      trList (head :: tail).tail = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        elim (trList (head :: tail)) [] [] (trContStack k) main =
          trNat (head :: tail).headI ++ a :: trList (head :: tail).tail)
    o

Tactic:
simp [o]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
cons :
  ∀ (c : Cfg') (h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c)
    (h₂ :
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
          (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
        c),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.cons fs) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.cons fs) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none

Premises used: Option.none, Turing.ToPartrec.Cont.cons₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (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 (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ main ≠ rev

Tactic:
decide
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (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 (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
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 f (Cont'.cons₁ fs (trCont k))).copy) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
            ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
              elim (trList v) [] [] (trContStack k) stack))
          main [])
        rev
        ((update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
              ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
                elim (trList v) [] [] (trContStack k) stack)
              main).reverseAux
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
            ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
              elim (trList v) [] [] (trContStack k) stack)
            rev))))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.cons fs) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (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 (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ 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 f (Cont'.cons₁ fs (trCont k))).copy) none
      (elim [] ((trList v).reverseAux []) [] ((some Γ'.consₗ).getD default :: trContStack k)))
    c

Tactic:
(copy_ok _ none [] (trList v).reverse _ _).trans ?_

Premises used: Turing.PartrecToTM2.copy_ok, Turing.PartrecToTM2.trList, Turing.TM2.step, Option.none, Relation.TransGen.trans, List.reverse, List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (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 (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
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 f (Cont'.cons₁ fs (trCont k)))) none
      (elim ((trList v).reverse.reverseAux []) [] []
        ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k))))
    c
⊢ 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 f (Cont'.cons₁ fs (trCont k))).copy) none
      (elim [] ((trList v).reverseAux []) [] ((some Γ'.consₗ).getD default :: trContStack k)))
    c

Tactic:
refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_

Premises used: Turing.PartrecToTM2.copy_ok, Turing.PartrecToTM2.trList, Option.none, Relation.TransGen.trans, List.reverse, List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (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 (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c

Tactic:
h₂
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (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 (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
h :
  elim ((trList v).reverse.reverseAux []) [] []
      ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k)) =
    elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))
⊢ 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 f (Cont'.cons₁ fs (trCont k)))) none
      (elim ((trList v).reverse.reverseAux []) [] []
        ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k))))
    c

Tactic:
convert! h₂ using 2
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f fs : Code
IHf :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal fs k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
            (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 (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
⊢ elim ((trList v).reverse.reverseAux []) [] []
      ((trList v).reverse.reverseAux ((some Γ'.consₗ).getD default :: trContStack k)) =
    elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))

Tactic:
simp [List.reverseAux_eq, trContStack]

Premises used: Turing.PartrecToTM2.trContStack, List.reverseAux_eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f a : Code
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal a k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal a (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.comp a) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.comp a) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
IHg (Cont.comp f k) v s

Premises used: Turing.ToPartrec.Cont.comp, Turing.PartrecToTM2.trContStack, Turing.PartrecToTM2.contStack, Turing.PartrecToTM2.trNormal, Turing.ToPartrec.stepNormal, Turing.PartrecToTM2.trCont
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f a : Code
a_ih :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
IHg :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal a k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal a (trCont k))) s (elim (trList v) [] [] (trContStack k)))
          b₂
k : Cont
v : List ℕ
s : Option Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal (f.comp a) k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.comp a) (trCont k))) s
          (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
exact IHg (Cont.comp f k) v s

Premises used: Turing.ToPartrec.Cont.comp