awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 = []
⊢ 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'
have 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'
Tactic: refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 Γ')) ↦ 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'
have 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'
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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
        (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'
have cons₁ : List Γ'
Tactic: refine (move₂_ok (L₁ := ?_) (o := ?_) (L₂ := ?_) (by decide) rfl ?_).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 Γ'
⊢ 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'
have cons₄ : splitAtPred (fun (s : Γ') ↦ decide (s = Γ'.consₗ)) (elim [] [] (trList v) (trContStack (Cont.cons₁ fs as k)) stack) =
  (trList as, some Γ'.consₗ, trLList (contStack k))
Tactic: refine (move₂_ok (L₁ := ?_) (o := ?_) (L₂ := ?_) (by decide) rfl ?_).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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))
⊢ 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'
have 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'
Tactic: refine (move₂_ok (L₁ := ?_) (o := ?_) (L₂ := ?_) (by decide) rfl ?_).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 Γ')) ↦ 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'
have 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 =
  []
Tactic: refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 =
    []
⊢ 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'
have 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'
Tactic: refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 Γ')) ↦ 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'
have 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'
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]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
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₂
have cons₂ : ∀ (c : Cfg') (h₁ : TrCfg (stepRet k (ns.headI :: v)) c)
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) none
        (elim (trList (ns.headI :: v)) [] [] (trContStack k)))
      c),
  ∃ (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₂
Tactic: obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
f : Code
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 Γ'
⊢ ∃ (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₂
have comp : ∀ (s' : Cfg') (h₁ : TrCfg (stepNormal f k v) s')
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s (elim (trList v) [] [] (trContStack k)))
      s'),
  ∃ (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₂
Tactic: obtain ⟨s', h₁, h₂⟩ := trNormal_respects f k v s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
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 Γ'
⊢ 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
have nil : if Eq (α := ℕ) (List.headI []) 0 then
  natEnd ((trList []).head?.getD default) = true ∧ (trList []).tail = trList (List.tail [])
else
  natEnd ((trList []).head?.getD default) = false ∧
    (trList []).tail = (trNat (List.headI [])).tail ++ Γ'.cons :: trList (List.tail [])
Tactic: obtain - | n := v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
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 Γ'
nil :
  if Eq (α := ℕ) (List.headI []) 0 then
    natEnd ((trList []).head?.getD default) = true ∧ (trList []).tail = trList (List.tail [])
  else
    natEnd ((trList []).head?.getD default) = false ∧
      (trList []).tail = (trNat (List.headI [])).tail ++ Γ'.cons :: trList (List.tail [])
⊢ 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
have cons : ∀ (n : ℕ) (tail : List ℕ),
  if (n :: tail).headI = 0 then
    natEnd ((trList (n :: tail)).head?.getD default) = true ∧ (trList (n :: tail)).tail = trList (n :: tail).tail
  else
    natEnd ((trList (n :: tail)).head?.getD default) = false ∧
      (trList (n :: tail)).tail = (trNat (n :: tail).headI).tail ++ Γ'.cons :: trList (n :: tail).tail
Tactic: obtain - | n := v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
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₂
s : Option Γ'
n : ℕ
tail : List ℕ
⊢ if (n :: tail).headI = 0 then
    natEnd ((trList (n :: tail)).head?.getD default) = true ∧ (trList (n :: tail)).tail = trList (n :: tail).tail
  else
    natEnd ((trList (n :: tail)).head?.getD default) = false ∧
      (trList (n :: tail)).tail = (trNat (n :: tail).headI).tail ++ Γ'.cons :: trList (n :: tail).tail
have cons : if (0 :: tail).headI = 0 then
  natEnd ((trList (0 :: tail)).head?.getD default) = true ∧ (trList (0 :: tail)).tail = trList (0 :: tail).tail
else
  natEnd ((trList (0 :: tail)).head?.getD default) = false ∧
    (trList (0 :: tail)).tail = (trNat (0 :: tail).headI).tail ++ Γ'.cons :: trList (0 :: tail).tail
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
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₂
s : Option Γ'
n : ℕ
tail : List ℕ
cons :
  if (0 :: tail).headI = 0 then
    natEnd ((trList (0 :: tail)).head?.getD default) = true ∧ (trList (0 :: tail)).tail = trList (0 :: tail).tail
  else
    natEnd ((trList (0 :: tail)).head?.getD default) = false ∧
      (trList (0 :: tail)).tail = (trNat (0 :: tail).headI).tail ++ Γ'.cons :: trList (0 :: tail).tail
⊢ if (n :: tail).headI = 0 then
    natEnd ((trList (n :: tail)).head?.getD default) = true ∧ (trList (n :: tail)).tail = trList (n :: tail).tail
  else
    natEnd ((trList (n :: tail)).head?.getD default) = false ∧
      (trList (n :: tail)).tail = (trNat (n :: tail).headI).tail ++ Γ'.cons :: trList (n :: tail).tail
have cons₁ : ∀ (n : ℕ),
  if ((n + 1) :: tail).headI = 0 then
    natEnd ((trList ((n + 1) :: tail)).head?.getD default) = true ∧
      (trList ((n + 1) :: tail)).tail = trList ((n + 1) :: tail).tail
  else
    natEnd ((trList ((n + 1) :: tail)).head?.getD default) = false ∧
      (trList ((n + 1) :: tail)).tail = (trNat ((n + 1) :: tail).headI).tail ++ Γ'.cons :: trList ((n + 1) :: tail).tail
Tactic: rcases n with - | n
Cleared hypotheses: n