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₂
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.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))))
have h₃ : elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
    main (trList v.tail)
Tactic: convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
-- 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'
h₃ :
  elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
      main (trList v.tail)
⊢ 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))))
have neg : List Γ'
Tactic: convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
-- 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'
h₃ :
  elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
      main (trList v.tail)
neg : List Γ'
⊢ 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))))
have neg₁ : ∀ x ∈ (trNat v.headI).tail, natEnd x = false
Tactic: convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
-- 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'
h₃ :
  elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
      main (trList v.tail)
neg : List Γ'
neg₁ : ∀ x ∈ (trNat v.headI).tail, natEnd x = false
⊢ 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))))
have neg₂ : Option.elim'
  (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail main =
      (trNat v.headI).tail ∧
    trList v.tail = [])
  (fun (a : Γ') ↦
    natEnd a = true ∧
      update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail
          main =
        (trNat v.headI).tail ++ a :: trList v.tail)
  (some Γ'.cons)
Tactic: convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
-- 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'
⊢ elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ') (elim (trList v) [] [] (trContStack (Cont.fix f k))) main (trList v).tail)
      main (trList v.tail)
have h₃ : elim (trList v.tail) [] [] (trContStack (Cont.fix f k)) = elim (trList v.tail) [] [] (trContStack (Cont.fix f k))
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
k : Cont
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₂
have halt : ∀ (v : List ℕ) (s : Option Γ'),
  ∃ (b₂ : Cfg'),
    TrCfg (stepRet Cont.halt v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.ret (trCont Cont.halt))) s
          (elim (trList v) [] [] (trContStack Cont.halt)))
        b₂
Tactic: induction k generalizing v s with
  | halt => exact ⟨_, rfl, TransGen.single rfl⟩
  | cons₁ fs as k _ =>
    obtain ⟨s', h₁, h₂⟩ := trNormal_respects fs (Cont.cons₂ v k) as none
    refine ⟨s', h₁, TransGen.head rfl ?_⟩; simp
    refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_; · rfl
    simp only [TM2.step, Option.mem_def, Option.elim, id_eq, elim_update_main, elim_main, elim_aux,
      List.append_nil, elim_update_aux]
    refine (move₂_ok (L₁ := ?_) (o := ?_) (L₂ := ?_) (by decide) rfl ?_).trans ?_
    pick_goal 4
    · exact splitAtPred_eq _ _ _ (some Γ'.consₗ) _
        (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, rfl⟩
    refine (move₂_ok (by decide) ?_ (splitAtPred_false _)).trans ?_; · rfl
    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]
    exact h₂
  | cons₂ ns k IH =>
    obtain ⟨c, h₁, h₂⟩ := IH (ns.headI :: v) none
    exact ⟨c, h₁, TransGen.head rfl <| head_stack_ok.trans h₂⟩
  | comp f k _ =>
    obtain ⟨s', h₁, h₂⟩ := trNormal_respects f k v s
    exact ⟨_, h₁, TransGen.head rfl h₂⟩
  | fix f k IH =>
    rw [stepRet]
    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⟩
    by_cases h : v.headI = 0 <;> simp only [h, ite_true, ite_false] at this ⊢
    · obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head?
      refine ⟨c, h₁, TransGen.head rfl ?_⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this, elim_update_main]
      exact h₂
    · obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons)
      refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩
      rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this.1]
      convert! clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2
      · simp
        convert! rfl
      · exact fun x h => trNat_natEnd _ _ (List.tail_subset _ h)
      · exact ⟨rfl, this.2⟩
Cleared hypotheses: k, v, s
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
v : List ℕ
⊢ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) = halt <$> c.eval v
have obtain : ∀ (i : Cfg') (h₁ : TrCfg (stepNormal c Cont.halt v) i)
  (h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i),
  eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) = halt <$> c.eval v
Tactic: obtain ⟨i, h₁, h₂⟩ := tr_init c v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
⊢ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) = halt <$> c.eval v
have refine : ∀ (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
  x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) ↔ x ∈ halt <$> c.eval v
Tactic: refine Part.ext fun x => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) ↔ x ∈ halt <$> c.eval v
have rw : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ x ∈ halt <$> c.eval v
Tactic: rw [reaches_eval h₂.to_reflTransGen]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ x ∈ halt <$> c.eval v
have simp : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ ∃ a ∈ c.eval v, halt a = x
Tactic: simp only [Part.map_eq_map, Part.mem_map_iff]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ ∃ a ∈ c.eval v, halt a = x
have refine_1 : ∀ (h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i), ∃ a ∈ c.eval v, halt a = x
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
refine_1 : ∀ (h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i), ∃ a ∈ c.eval v, halt a = x
⊢ x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i ↔ ∃ a ∈ c.eval v, halt a = x
have refine_2 : (∃ a ∈ c.eval v, halt a = x) → x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
⊢ ∃ a ∈ c.eval v, halt a = x
have refine_1 : ∀ (c_1 : Cfg) (hc₁ : TrCfg c_1 x) (hc₂ : c_1 ∈ eval step (stepNormal c Cont.halt v)), ∃ a ∈ c.eval v, halt a = x
Tactic: obtain ⟨c, hc₁, hc₂⟩ := tr_eval_rev tr_respects h₁ h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
c_1 : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c_1 Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c_1 v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : c ∈ eval step (stepNormal c_1 Cont.halt v)
⊢ ∃ a ∈ c_1.eval v, halt a = x
have hc₃ : ∃ a ∈ c_1.eval v, Cfg.halt a = c
Tactic: simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff] at hc₂
Cleared hypotheses: hc₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
c_1 : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c_1 Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c_1 v) i
x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')
h : x ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
c : Cfg
hc₁ : TrCfg c x
hc₂ : ∃ a ∈ c_1.eval v, Cfg.halt a = c
⊢ ∃ a ∈ c_1.eval v, halt a = x
have refine_1 : ∀ (v' : List ℕ) (hv : v' ∈ c_1.eval v) (hc₁ : TrCfg (Cfg.halt v') x), ∃ a ∈ c_1.eval v, halt a = x
Tactic: obtain ⟨v', hv, rfl⟩ := hc₂
Cleared hypotheses: c, hc₁, hc₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
⊢ halt v' ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
have this : ∀ (ab : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v)),
  ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
    TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
Tactic: have := StateTransition.tr_eval (b₁ := Cfg.halt v') tr_respects h₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
c : Code
v : List ℕ
i : Cfg'
h₁ : TrCfg (stepNormal c Cont.halt v) i
h₂ : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (init c v) i
v' : List ℕ
hv : v' ∈ c.eval v
this :
  ∀ (ab : Cfg.halt v' ∈ eval step (stepNormal c Cont.halt v)),
    ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
      TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
⊢ halt v' ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
have this₁ : ∀ (ab : v' ∈ c.eval v),
  ∃ (b₂ : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')),
    TrCfg (Cfg.halt v') b₂ ∧ b₂ ∈ eval (TM2.step (Γ := fun (x : K') ↦ Γ') tr) i
Tactic: simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff, Cfg.halt.injEq,
      exists_eq_right] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have move : ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
  q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have clear : ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
  q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
clear :
  ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have copy : ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
clear :
  ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
copy :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have push : ∀ (k : K') (s : Option Γ' → Option Γ') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
  q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
clear :
  ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
copy :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
push :
  ∀ (k : K') (s : Option Γ' → Option Γ') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have read : ∀ (q : Option Γ' → Λ') (q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)),
  q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q q' : Λ'
move :
  ∀ (p : Γ' → Bool) (k₁ k₂ : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.move p k₁ k₂ q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.move p k₁ k₂ q)
clear :
  ∀ (p : Γ' → Bool) (k : K') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.clear p k q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.clear p k q)
copy :
  ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.copy → trStmts₁ q' ⊆ trStmts₁ q.copy
push :
  ∀ (k : K') (s : Option Γ' → Option Γ') (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q),
    q' ∈ trStmts₁ (Λ'.push k s q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.push k s q)
read :
  ∀ (q : Option Γ' → Λ') (q_ih : ∀ (a : Option Γ'), q' ∈ trStmts₁ (q a) → trStmts₁ q' ⊆ trStmts₁ (q a)),
    q' ∈ trStmts₁ (Λ'.read q) → trStmts₁ q' ⊆ trStmts₁ (Λ'.read q)
⊢ q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q
have succ : ∀ (q : Λ') (q_ih : q' ∈ trStmts₁ q → trStmts₁ q' ⊆ trStmts₁ q), q' ∈ trStmts₁ q.succ → trStmts₁ q' ⊆ trStmts₁ q.succ
Tactic: induction q with
  | move _ _ _ q q_ih => _ | clear _ _ q q_ih => _ | copy q q_ih => _ | push _ _ q q_ih => _
  | read q q_ih => _ | succ q q_ih => _ | pred q₁ q₂ q₁_ih q₂_ih => _ | ret => _
Cleared hypotheses: q