awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (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'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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))
      v₁.tail)
    v'
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v₁.tail)

Tactic:
IH v₁.tail ((Part.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩)

Premises used: Iff.mpr, List.tail, And.intro, Exists.intro, Part.mem_map_iff, if_neg
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (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'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  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))
      v₁.tail)
    v'
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v₁.tail)

Tactic:
exact IH v₁.tail ((Part.mem_map_iff _).2 ⟨_, he₁, if_neg h⟩)

Premises used: Iff.mpr, List.tail, And.intro, Exists.intro, Part.mem_map_iff, if_neg
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
cons :
  eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)
⊢ eval step (stepNormal (f.cons fs) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [stepNormal]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
cons :
  Eq (α := Part Cfg)
    (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
    do
    let v ←
      (fun (v : List ℕ) ↦
            (do
              let n ← f.eval v
              let ns ← fs.eval v
              pure (n.headI :: ns) : Part (List ℕ)))
          v
    eval step (Cfg.ret k v)
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [Code.eval, IHf]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
cons :
  Eq (α := Part Cfg)
    (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
⊢ Eq (α := Part Cfg)
    (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
    do
    let v ←
      (fun (v : List ℕ) ↦
            (do
              let n ← f.eval v
              let ns ← fs.eval v
              pure (n.headI :: ns) : Part (List ℕ)))
          v
    eval step (Cfg.ret k v)

Tactic:
simp only [bind_assoc, pure_bind]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.pure_bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
cons :
  Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) fun (x : List ℕ) ↦ do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
⊢ Eq (α := Part Cfg)
    (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
cons :
  ∀ (v_1 : List ℕ),
    eval step (Cfg.ret (Cont.cons₁ fs v k) v_1) = do
      let x ← fs.eval v
      eval step (Cfg.ret k (v_1.headI :: x))
⊢ Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) fun (x : List ℕ) ↦ do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Tactic:
funext v
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
cons :
  eval step (stepRet (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
cons₁ : Reaches step (Cfg.ret (Cont.cons₁ fs v_1 k) v) (stepRet (Cont.cons₁ fs v_1 k) v)
rw : Cfg
⊢ eval step (Cfg.ret (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
rw [reaches_eval]

Premises used: StateTransition.reaches_eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v_1 k) v) (stepRet (Cont.cons₁ fs v_1 k) v)

Tactic:
ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl, StateTransition.Reaches
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v_1 k) v) (stepRet (Cont.cons₁ fs v_1 k) v)

Tactic:
exact ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
cons :
  Eq (α := Part Cfg)
    (do
      let v_2 ← fs.eval v_1
      eval step (Cfg.ret (Cont.cons₂ v k) v_2))
    do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
⊢ eval step (stepRet (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
rw [stepRet, IHfs]

Premises used: Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
cons :
  Eq (α := List ℕ → Part Cfg) (fun (v_2 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_2)) fun (x : List ℕ) ↦
    eval step (Cfg.ret k (v.headI :: x))
⊢ Eq (α := Part Cfg)
    (do
      let v_2 ← fs.eval v_1
      eval step (Cfg.ret (Cont.cons₂ v k) v_2))
    do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
cons : ∀ (v' : List ℕ), eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))
⊢ Eq (α := List ℕ → Part Cfg) (fun (v_2 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_2)) fun (x : List ℕ) ↦
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
funext v'
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))

Tactic:
Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
cons : eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (stepRet (Cont.cons₂ v k) v')
cons₁ : eval step (Cfg.ret k (v.headI :: v')) = eval step (stepRet (Cont.cons₂ v k) v')
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))

Tactic:
refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (stepRet (Cont.cons₂ v k) v')

Tactic:
reaches_eval (ReflTransGen.single rfl)

Premises used: StateTransition.reaches_eval, Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (stepRet (Cont.cons₂ v k) v')

Tactic:
exact reaches_eval (ReflTransGen.single rfl)

Premises used: StateTransition.reaches_eval, Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
⊢ eval step (Cfg.ret k (v.headI :: v')) = eval step (stepRet (Cont.cons₂ v k) v')

Tactic:
reaches_eval (ReflTransGen.single rfl)

Premises used: StateTransition.reaches_eval, Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
⊢ eval step (Cfg.ret k (v.headI :: v')) = eval step (stepRet (Cont.cons₂ v k) v')

Tactic:
exact reaches_eval (ReflTransGen.single rfl)

Premises used: StateTransition.reaches_eval, Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
comp :
  eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal g (Cont.comp f k) v) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)
⊢ eval step (stepNormal (f.comp g) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [stepNormal]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
comp :
  Eq (α := Part Cfg)
    (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v))
    do
    let v ← (fun (v : List ℕ) ↦ g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal g (Cont.comp f k) v) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [Code.eval, IHg]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
comp :
  Eq (α := Part Cfg)
    (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v))
    do
    let x ← g.eval v
    let v ← f.eval x
    eval step (Cfg.ret k v)
⊢ Eq (α := Part Cfg)
    (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v))
    do
    let v ← (fun (v : List ℕ) ↦ g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)

Tactic:
simp only [bind_assoc]

Premises used: LawfulMonad.bind_assoc
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
comp :
  Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret (Cont.comp f k) v)) fun (x : List ℕ) ↦ do
    let v ← f.eval x
    eval step (Cfg.ret k v)
⊢ Eq (α := Part Cfg)
    (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v))
    do
    let x ← g.eval v
    let v ← f.eval x
    eval step (Cfg.ret k v)

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
comp :
  ∀ (v : List ℕ),
    eval step (Cfg.ret (Cont.comp f k) v) = do
      let v ← f.eval v
      eval step (Cfg.ret k v)
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret (Cont.comp f k) v)) fun (x : List ℕ) ↦ do
    let v ← f.eval x
    eval step (Cfg.ret k v)

Tactic:
funext v
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
comp :
  eval step (stepRet (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
comp₁ : Reaches step (Cfg.ret (Cont.comp f k) v) (stepRet (Cont.comp f k) v)
rw : Cfg
⊢ eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

Tactic:
rw [reaches_eval]

Premises used: StateTransition.reaches_eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) (stepRet (Cont.comp f k) v)

Tactic:
ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl, StateTransition.Reaches
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) (stepRet (Cont.comp f k) v)

Tactic:
exact ReflTransGen.single rfl

Premises used: Relation.ReflTransGen.single, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
comp :
  eval step (stepNormal f k v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
comp₁ comp₂ :
  Eq (α := Part Cfg)
    (do
      let v ← f.eval v
      eval step (Cfg.ret k v))
    do
    let v ← f.eval v
    eval step (Cfg.ret k v)
⊢ eval step (stepRet (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

Tactic:
rw [stepRet, IHf]

Premises used: Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
case :
  eval step
      ((fun (k : Cont) (v : List ℕ) ↦
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
              (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
            Cfg))
        k v) =
    do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)
⊢ eval step (stepNormal (f.case g) k v) = do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)

Tactic:
rw [stepNormal]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
case :
  eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) v.headI
    eval step (Cfg.ret k v)
⊢ eval step
      ((fun (k : Cont) (v : List ℕ) ↦
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
              (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
            Cfg))
        k v) =
    do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval]

Premises used: Turing.ToPartrec.Code.eval
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
case :
  eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) 0
    eval step (Cfg.ret k v)
case₁ :
  ∀ (n : ℕ),
    eval step
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1)) =
      do
      let v ←
        Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
            (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) (n + 1)
      eval step (Cfg.ret k v)
⊢ eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) v.headI
    eval step (Cfg.ret k v)

Tactic:
cases v.headI

Premises used: List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal f k v.tail) = (f.eval v.tail).bind fun (v : List ℕ) ↦ eval step (Cfg.ret k v)

Tactic:
apply IHf
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
n : ℕ
⊢ eval step (stepNormal g k (n :: v.tail)) = (g.eval (n :: v.tail)).bind fun (v : List ℕ) ↦ eval step (Cfg.ret k v)

Tactic:
apply IHg
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
fix :
  eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.fix f k) v) k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
⊢ eval step (stepNormal f.fix k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

Tactic:
rw [stepNormal]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
fix fix₁ :
  Eq (α := Part Cfg)
    (do
      let v ← f.fix.eval v
      eval step (Cfg.ret k v))
    do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.fix f k) v) k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

Tactic:
rw [cont_eval_fix IHf]

Premises used: Turing.ToPartrec.cont_eval_fix
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ Cfg.ret k (0 :: v)) k v) = do
    let v ← Code.zero'.eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval, pure_bind]

Premises used: Turing.ToPartrec.Code.eval, LawfulMonad.pure_bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ Cfg.ret k [v.headI.succ]) k v) = do
    let v ← Code.succ.eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval, pure_bind]

Premises used: Turing.ToPartrec.Code.eval, LawfulMonad.pure_bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ Cfg.ret k v.tail) k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)

Tactic:
simp only [Code.eval, pure_bind]

Premises used: Turing.ToPartrec.Code.eval, LawfulMonad.pure_bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
cons : ∀ (f fs : Code) (IHf : f.Ok) (IHfs : fs.Ok), (f.cons fs).Ok
cons₁ :
  ∀ (f fs : Code) (IHf : f.Ok) (IHfs : fs.Ok) (k : Cont) (v : List ℕ),
    eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
      let v ← (f.cons fs).eval v
      eval step (Cfg.ret k v)
comp : ∀ (f g : Code) (IHf : f.Ok) (IHg : g.Ok), (f.comp g).Ok
comp₁ :
  ∀ (f g : Code) (IHf : f.Ok) (IHg : g.Ok) (k : Cont) (v : List ℕ),
    eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal g (Cont.comp f k) v) k v) = do
      let v ← (f.comp g).eval v
      eval step (Cfg.ret k v)
case : ∀ (f g : Code) (IHf : f.Ok) (IHg : g.Ok), (f.case g).Ok
case₁ :
  ∀ (f g : Code) (IHf : f.Ok) (IHg : g.Ok) (k : Cont) (v : List ℕ),
    eval step
        ((fun (k : Cont) (v : List ℕ) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
                (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
              Cfg))
          k v) =
      do
      let v ← (f.case g).eval v
      eval step (Cfg.ret k v)
fix : ∀ (f : Code) (IHf : f.Ok), f.fix.Ok
fix₁ :
  ∀ (f : Code) (IHf : f.Ok) (k : Cont) (v : List ℕ),
    eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.fix f k) v) k v) = do
      let v ← f.fix.eval v
      eval step (Cfg.ret k v)
zero' : Code.zero'.Ok
zero'₁ :
  ∀ (k : Cont) (v : List ℕ),
    eval step ((fun (k : Cont) (v : List ℕ) ↦ Cfg.ret k (0 :: v)) k v) = do
      let v ← Code.zero'.eval v
      eval step (Cfg.ret k v)
succ : Code.succ.Ok
succ₁ :
  ∀ (k : Cont) (v : List ℕ),
    eval step ((fun (k : Cont) (v : List ℕ) ↦ Cfg.ret k [v.headI.succ]) k v) = do
      let v ← Code.succ.eval v
      eval step (Cfg.ret k v)
tail : Code.tail.Ok
tail₁ :
  ∀ (k : Cont) (v : List ℕ),
    eval step ((fun (k : Cont) (v : List ℕ) ↦ Cfg.ret k v.tail) k v) = do
      let v ← Code.tail.eval v
      eval step (Cfg.ret k v)
⊢ c.Ok

Tactic:
induction c with (intro k v; rw [stepNormal])
  | cons f fs IHf IHfs =>
    rw [Code.eval, IHf]
    simp only [bind_assoc, pure_bind]; congr; funext v
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IHfs]; congr; funext v'
    refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_) <;>
      exact reaches_eval (ReflTransGen.single rfl)
  | comp f g IHf IHg =>
    rw [Code.eval, IHg]
    simp only [bind_assoc]; congr; funext v
    rw [reaches_eval]; swap
    · exact ReflTransGen.single rfl
    rw [stepRet, IHf]
  | case f g IHf IHg =>
    simp only [Code.eval]
    cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]
  | fix f IHf => rw [cont_eval_fix IHf]
  | _ => simp only [Code.eval, pure_bind]

Premises used: Nat.rec_zero, LawfulMonad.bind_assoc, Turing.ToPartrec.Code.eval, StateTransition.reaches_eval, Relation.ReflTransGen.single, LawfulMonad.pure_bind, Turing.ToPartrec.stepNormal, Part.bind_eq_bind, Turing.ToPartrec.stepRet, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
v : List ℕ
⊢ eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

Tactic:
(code_is_ok c).zero

Premises used: Turing.ToPartrec.Code.Ok.zero, Turing.ToPartrec.code_is_ok
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
halt : eval step (stepRet Cont.halt v) = pure (Cfg.halt v)
⊢ eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v

Tactic:
simp only [Cont.eval, map_pure]

Premises used: Turing.ToPartrec.Cont.eval, LawfulApplicative.map_pure
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = pure (Cfg.halt v)

Tactic:
Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)

Premises used: Iff.mpr, Part.eq_some_iff, Relation.ReflTransGen.refl, StateTransition.mem_eval, And.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = pure (Cfg.halt v)

Tactic:
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.refl, rfl⟩)

Premises used: Iff.mpr, Part.eq_some_iff, Relation.ReflTransGen.refl, StateTransition.mem_eval, And.intro
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
cons₁ :
  (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    Cfg.halt <$>
      (fun (v : List ℕ) ↦
          (do
            let ns ← fs.eval as
            k.eval (v.headI :: ns) : Part (List ℕ)))
        v
⊢ eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v

Tactic:
rw [Cont.eval, stepRet, code_is_ok]

Premises used: Turing.ToPartrec.Cont.eval, Turing.ToPartrec.code_is_ok, Turing.ToPartrec.stepRet
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
cons₁ :
  Eq (α := Part Cfg)
    (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1))
    do
    let x ← fs.eval as
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)
⊢ (do
      let v_1 ← fs.eval as
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    Cfg.halt <$>
      (fun (v : List ℕ) ↦
          (do
            let ns ← fs.eval as
            k.eval (v.headI :: ns) : Part (List ℕ)))
        v

Tactic:
simp only [← bind_pure_comp, bind_assoc]

Premises used: LawfulMonad.bind_assoc, LawfulMonad.bind_pure_comp