awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ eval step (stepRet (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
have 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)
Tactic: rw [stepRet, IHf]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.case g) k v) = do
    let v ← (f.case g).eval v
    eval step (Cfg.ret k v)
have 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)
Tactic: rw [stepNormal]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
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)
have 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)
Tactic: simp only [Code.eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ 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)
have 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)
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ 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)
have 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)
Tactic: cases v.headI
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ 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)
have 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)
Tactic: cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ 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)
have 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)
Tactic: cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal f.fix k v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)
have 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)
Tactic: rw [stepNormal]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
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)
have 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)
Tactic: rw [cont_eval_fix IHf]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
⊢ c.Ok
have cons : ∀ (f fs : Code) (IHf : f.Ok) (IHfs : fs.Ok), (f.cons fs).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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
c : Code
cons : ∀ (f fs : Code) (IHf : f.Ok) (IHfs : fs.Ok), (f.cons fs).Ok
⊢ c.Ok
have 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)
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ c.Ok
have comp : ∀ (f g : Code) (IHf : f.Ok) (IHg : g.Ok), (f.comp g).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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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
⊢ c.Ok
have 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)
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ c.Ok
have case : ∀ (f g : Code) (IHf : f.Ok) (IHg : g.Ok), (f.case g).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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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
⊢ c.Ok
have 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)
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ c.Ok
have fix : ∀ (f : Code) (IHf : f.Ok), f.fix.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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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
⊢ c.Ok
have 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)
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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)
⊢ c.Ok
have zero' : Code.zero'.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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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
⊢ c.Ok
have 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)
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]
Cleared hypotheses: c