awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 Γ'
tail : List ℕ
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
have cons : if n + 1 = 0 then
  natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
    (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail = trList tail
else
  natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
    (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail =
      (trNum (Num.pos (Num.succ' (↑n : Num)))).tail ++ Γ'.cons :: trList tail
Tactic: rw [trList, List.headI, trNat, Nat.cast_succ, Num.add_one, Num.succ, List.tail]
-- 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 Γ'
tail : List ℕ
n : ℕ
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos (Num.succ' (↑n : Num)))).tail ++ Γ'.cons :: trList tail
have cons : if n + 1 = 0 then
  natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
    (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail = trList tail
else
  natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
    (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail =
      (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail
Tactic: cases (n : Num).succ'
-- 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 Γ'
tail : List ℕ
n : ℕ
cons :
  if n + 1 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos (Num.succ' (↑n : Num)))).tail ++ Γ'.cons :: trList tail
have cons₁ : ∀ (a : PosNum),
  if n + 1 = 0 then
    natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = (trNum (Num.pos a.bit1)).tail ++ Γ'.cons :: trList tail
Tactic: cases (n : Num).succ'
-- 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 Γ'
tail : List ℕ
n : ℕ
cons :
  if n + 1 = 0 then
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos PosNum.one) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos PosNum.one)).tail ++ Γ'.cons :: trList tail
cons₁ :
  ∀ (a : PosNum),
    if n + 1 = 0 then
      natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
        (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail = trList tail
    else
      natEnd ((trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
        (trNum (Num.pos a.bit1) ++ Γ'.cons :: trList tail).tail =
          (trNum (Num.pos a.bit1)).tail ++ Γ'.cons :: trList tail
⊢ if n + 1 = 0 then
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos (Num.succ' (↑n : Num))) ++ Γ'.cons :: trList tail).tail =
        (trNum (Num.pos (Num.succ' (↑n : Num)))).tail ++ Γ'.cons :: trList tail
have cons₂ : ∀ (a : PosNum),
  if n + 1 = 0 then
    natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = true ∧
      (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail = trList tail
  else
    natEnd ((trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).head?.getD default) = false ∧
      (trNum (Num.pos a.bit0) ++ Γ'.cons :: trList tail).tail = (trNum (Num.pos a.bit0)).tail ++ Γ'.cons :: trList tail
Tactic: cases (n : Num).succ'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
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 Γ'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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₂
have this : 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
Tactic: 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⟩
-- 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 Γ'
this :
  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
⊢ ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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₂
have pos : ∀ (h : v.headI = 0),
  ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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₂
Tactic: by_cases h : v.headI = 0
-- 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 Γ'
this :
  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
pos :
  ∀ (h : v.headI = 0),
    ∃ (b₂ : Cfg'),
      TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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 (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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₂
have neg : ∀ (h : ¬v.headI = 0),
  ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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₂
Tactic: by_cases h : v.headI = 0
-- 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 Γ'
this :
  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
h : v.headI = 0
⊢ ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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₂
have pos : ∀ (this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail),
  ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v.tail) 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₂
Tactic: simp only [h, ite_true, ite_false] at this ⊢
Cleared hypotheses: this
-- 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 Γ'
this :
  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
h : ¬v.headI = 0
⊢ ∃ (b₂ : Cfg'),
    TrCfg (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) 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₂
have neg : ∀
  (this :
    natEnd ((trList v).head?.getD default) = false ∧
      (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail),
  ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f (Cont.fix f k) v.tail) 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₂
Tactic: simp only [h, ite_true, ite_false] at this ⊢
Cleared hypotheses: this
-- 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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v.tail) 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₂
have pos : ∀ (c : Cfg') (h₁ : TrCfg (stepRet k v.tail) c)
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
        (elim (trList v.tail) [] [] (trContStack k)))
      c),
  ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v.tail) 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₂
Tactic: obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?
-- 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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
      (elim (trList v.tail) [] [] (trContStack k)))
    c
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepRet k v.tail) 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₂
have pos : 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.fix f k)))) s
    (elim (trList v) [] [] (trContStack (Cont.fix f k))))
  c
Tactic: refine ⟨c, h₁, TransGen.head rfl ?_⟩
-- 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 Γ'
h : v.headI = 0
this : natEnd ((trList v).head?.getD default) = true ∧ (trList v).tail = trList v.tail
c : Cfg'
h₁ : TrCfg (stepRet k v.tail) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont k))) (trList v).head?
      (elim (trList v.tail) [] [] (trContStack k)))
    c
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' main
        (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
          bif natEnd (s.getD default) then Λ'.ret (trCont k)
          else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    c
have pos : 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 (bif true then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
    (trList v).head? (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
  c
Tactic: simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]
-- 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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f (Cont.fix f k) v.tail) 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₂
have neg : ∀ (s' : Cfg') (h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s')
  (h₂ :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
        (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
      s'),
  ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f (Cont.fix f k) v.tail) 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₂
Tactic: obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)
-- 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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal f (Cont.fix f k) v.tail) 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₂
have neg : 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.fix f k)))) s
    (elim (trList v) [] [] (trContStack (Cont.fix f k))))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
    (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
Tactic: refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
-- 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 Γ'
h : ¬v.headI = 0
this :
  natEnd ((trList v).head?.getD default) = false ∧ (trList v).tail = (trNat v.headI).tail ++ Γ'.cons :: trList v.tail
s' : Cfg'
h₁ : TrCfg (stepNormal f (Cont.fix f k) v.tail) s'
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.fix f k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
    s'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' main
        (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
          bif natEnd (s.getD default) then Λ'.ret (trCont k)
          else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
      s (elim (trList v) [] [] (trContStack (Cont.fix f k))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.fix f (trCont k)))) (some Γ'.cons)
      (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
have neg : 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 (bif false then Λ'.ret (trCont k) else Λ'.clear natEnd main (trNormal f (Cont'.fix f (trCont k)))))
    (trList v).head?
    (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.fix f (trCont k)))) (some Γ'.cons)
    (elim (trList v.tail) [] [] (trContStack (Cont.fix f k))))
Tactic: simp only [pop', TM2.stepAux, elim_main, this.1]