awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
k : Cont
v : List ℕ
cons :
  ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
    (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
comp :
  ∀ (f _g : Code) (_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'
case :
  ∀ (f g : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'
fix :
  ∀ (f : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f.fix k v = Cfg.ret k' v'
zero' : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.zero' k v = Cfg.ret k' v'
succ : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.succ k v = Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'
have tail : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.tail k v = Cfg.ret k' v'
Tactic: induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩
Cleared hypotheses: c, k, v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
⊢ eval step (stepNormal f (Cont.fix f k) v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
have refine : ∀ (x : Cfg),
  x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔
    Membership.mem (γ := Part Cfg)
      (do
        let v ← f.fix.eval v
        eval step (Cfg.ret k v))
      x
Tactic: refine Part.ext fun x => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔
    Membership.mem (γ := Part Cfg)
      (do
        let v ← f.fix.eval v
        eval step (Cfg.ret k v))
      x
have simp : x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
Tactic: simp only [Part.bind_eq_bind, Part.mem_bind_iff]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
have mp : x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
mp : x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
have mpr : (∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)) → x ∈ eval step (stepNormal f (Cont.fix f k) v)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
⊢ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
have obtain : ∀ (v₁ : List ℕ) (hv₁ : v₁ ∈ f.eval v) (v₂ : List ℕ)
  (hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail) (h₃ : x ∈ eval step (Cfg.ret k v₂)),
  ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
Tactic: obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
        this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
have refine : Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v₂) ∨
  ∃ (a' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr a') ∧
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
          a')
        v₂
Tactic: refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v₂) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
          (Sum.inr a') ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
            a')
          v₂
have simp : Sum.inl v₂ ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
  ∃ (a' : List ℕ),
    Sum.inr a' ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
          a')
        v₂
Tactic: simp only [Part.eq_some_iff.2 hv₁, Part.map_some]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ Sum.inl v₂ ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      Sum.inr a' ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
            a')
          v₂
have pos : v₁.headI = 0 →
  ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₂) ∨
      ∃ (a' : List ℕ),
        Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inr a') ∧
          Membership.mem (γ := Part (List ℕ))
            (PFun.fix
              (fun (v : List ℕ) ↦
                Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
              a')
            v₂
Tactic: split_ifs at hv₂ ⊢
Cleared hypotheses: hv₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
pos :
  v₁.headI = 0 →
    ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₂) ∨
        ∃ (a' : List ℕ),
          Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inr a') ∧
            Membership.mem (γ := Part (List ℕ))
              (PFun.fix
                (fun (v : List ℕ) ↦
                  Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
                a')
              v₂
⊢ Sum.inl v₂ ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      Sum.inr a' ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
            a')
          v₂
have neg : ¬v₁.headI = 0 →
  ∀ (hv₂ : v₂ ∈ f.fix.eval v₁.tail),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr v₁.tail)) (Sum.inl v₂) ∨
      ∃ (a' : List ℕ),
        Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr v₁.tail)) (Sum.inr a') ∧
          Membership.mem (γ := Part (List ℕ))
            (PFun.fix
              (fun (v : List ℕ) ↦
                Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
              a')
            v₂
Tactic: split_ifs at hv₂ ⊢
Cleared hypotheses: hv₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : v₁.headI = 0
hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₂) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inr a') ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
            a')
          v₂
have pos : Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₁.tail) ∨
  ∃ (a' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inr a') ∧
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
          a')
        v₁.tail
Tactic: rw [Part.mem_some_iff.1 hv₂]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
have mp : ∀ (c : Cfg),
  x ∈ eval step c →
    ∀ (v : List ℕ) (c' : Cfg),
      c = c'.then (Cont.fix f k) →
        Reaches step (stepNormal f Cont.halt v) c' →
          ∃ v₁ ∈ f.eval v,
            ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Tactic: suffices ∀ c, x ∈ eval step c → ∀ v c', c = Cfg.then c' (Cont.fix f k) →
      Reaches step (stepNormal f Cont.halt v) c' →
        ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if List.headI v₁ = 0 then pure v₁.tail else f.fix.eval v₁.tail,
          x ∈ eval step (Cfg.ret k v₂) by
      intro h
      obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
        this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl
      refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
      simp only [Part.eq_some_iff.2 hv₁, Part.map_some]
      split_ifs at hv₂ ⊢
      · rw [Part.mem_some_iff.1 hv₂]
        exact Or.inl (Part.mem_some _)
      · exact Or.inr ⟨_, Part.mem_some _, hv₂⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
⊢ ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have mp : ∀ (c : Cfg) (he : x ∈ eval step c) (y : Cfg) (h : x ∈ eval step y)
  (IH :
    ∀ (a' : Cfg),
      step y = some a' →
        ∀ (v : List ℕ) (c' : Cfg),
          a' = c'.then (Cont.fix f k) →
            Reaches step (stepNormal f Cont.halt v) c' →
              ∃ v₁ ∈ f.eval v,
                ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂))
  (v : List ℕ) (c' : Cfg),
  y = c'.then (Cont.fix f k) →
    Reaches step (stepNormal f Cont.halt v) c' →
      ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Tactic: refine fun c he => evalInduction he fun y h IH => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step ((Cfg.halt v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.halt v').then (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have h₁ : x ∈ eval step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k))
Tactic: rw [Cfg.then] at h IH
Cleared hypotheses: h, IH, hr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step ((Cfg.halt v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.halt v').then (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : x ∈ eval step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k))
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have IH₁ : ∀ (a' : Cfg),
  step ((fun (k' : Cont) ↦ stepRet k' v') (Cont.fix f k)) = some a' →
    ∀ (v : List ℕ) (c' : Cfg),
      a' = c'.then (Cont.fix f k) →
        Reaches step (stepNormal f Cont.halt v) c' →
          ∃ v₁ ∈ f.eval v,
            ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Tactic: rw [Cfg.then] at h IH
Cleared hypotheses: h, IH, hr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step ((Cfg.ret k' v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.ret k' v').then (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.ret k' v')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have h₁ : x ∈ eval step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k))
Tactic: rw [Cfg.then] at h IH
Cleared hypotheses: h, IH, hr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v : List ℕ
k' : Cont
v' : List ℕ
h : x ∈ eval step ((Cfg.ret k' v').then (Cont.fix f k))
IH :
  ∀ (a' : Cfg),
    step ((Cfg.ret k' v').then (Cont.fix f k)) = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.ret k' v')
h₁ : x ∈ eval step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k))
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have IH₁ : ∀ (a' : Cfg),
  step ((fun (k'_1 : Cont) ↦ Cfg.ret (k'.then k'_1) v') (Cont.fix f k)) = some a' →
    ∀ (v : List ℕ) (c' : Cfg),
      a' = c'.then (Cont.fix f k) →
        Reaches step (stepNormal f Cont.halt v) c' →
          ∃ v₁ ∈ f.eval v,
            ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Tactic: rw [Cfg.then] at h IH
Cleared hypotheses: h, IH, hr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have this : Cfg.halt v' ∈ eval step (stepNormal f Cont.halt v)
Tactic: have := mem_eval.2 ⟨hr, rfl⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
this : Cfg.halt v' ∈ eval step (stepNormal f Cont.halt v)
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have this₁ : ∃ a ∈ f.eval v, Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt a)
Tactic: rw [fok, Part.bind_eq_bind, Part.mem_bind_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
this : ∃ a ∈ f.eval v, Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt a)
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have mp : ∀ (v'' : List ℕ) (h₁ : v'' ∈ f.eval v) (h₂ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')),
  ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Tactic: obtain ⟨v'', h₁, h₂⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he : x ∈ eval step c
v v' : List ℕ
h : x ∈ eval step (stepRet (Cont.fix f k) v')
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
v'' : List ℕ
h₁ : v'' ∈ f.eval v
h₂ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v'')
⊢ ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
have mp : ∀ (h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v'')),
  ∃ v₁ ∈ f.eval v, ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
Tactic: rw [reaches_eval] at h₂