awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ c.Ok
have succ : Code.succ.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
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
⊢ c.Ok
have 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)
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
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)
⊢ c.Ok
have tail : Code.tail.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
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
⊢ c.Ok
have 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)
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:
v : List ℕ
⊢ eval step (stepRet Cont.halt v) = Cfg.halt <$> Cont.halt.eval v
have halt : eval step (stepRet Cont.halt v) = pure (Cfg.halt v)
Tactic: simp only [Cont.eval, map_pure]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ fs as k) v) = Cfg.halt <$> (Cont.cons₁ fs as k).eval v
have 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
Tactic: rw [Cont.eval, stepRet, code_is_ok]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (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
have 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)
Tactic: simp only [← bind_pure_comp, bind_assoc]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ 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)
have cons₁ : Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) fun (x : List ℕ) ↦ do
  let a ← k.eval (v.headI :: x)
  pure (Cfg.halt a)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_1)) fun (x : List ℕ) ↦ do
    let a ← k.eval (v.headI :: x)
    pure (Cfg.halt a)
have cons₁ : ∀ (v' : List ℕ),
  eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
Tactic: funext v'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
have cons₁ : eval step (stepRet (Cont.cons₂ v k) v') = do
  let a ← k.eval (v.headI :: v')
  pure (Cfg.halt a)
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
cons₁ :
  eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
have cons₂ : Reaches step (Cfg.ret (Cont.cons₂ v k) v') (stepRet (Cont.cons₂ v k) v')
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
cons₁ :
  eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
cons₂ : Reaches step (Cfg.ret (Cont.cons₂ v k) v') (stepRet (Cont.cons₂ v k) v')
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
have rw : Cfg
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
have cons₁ : eval step (stepRet k (v.headI :: v')) = do
  let a ← k.eval (v.headI :: v')
  pure (Cfg.halt a)
Tactic: rw [stepRet, IH, bind_pure_comp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
cons₁ :
  eval step (stepRet k (v.headI :: v')) = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
have cons₂ : Cfg.halt <$> k.eval (v.headI :: v') = do
  let a ← k.eval (v.headI :: v')
  pure (Cfg.halt a)
Tactic: rw [stepRet, IH, bind_pure_comp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
fs : Code
as : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
cons₁ :
  eval step (stepRet k (v.headI :: v')) = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
cons₂ :
  Cfg.halt <$> k.eval (v.headI :: v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
⊢ eval step (stepRet (Cont.cons₂ v k) v') = do
    let a ← k.eval (v.headI :: v')
    pure (Cfg.halt a)
have cons₃ : Cfg.halt <$> k.eval (v.headI :: v') = Cfg.halt <$> k.eval (v.headI :: v')
Tactic: rw [stepRet, IH, bind_pure_comp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
ns : List ℕ
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.cons₂ ns k) v) = Cfg.halt <$> (Cont.cons₂ ns k).eval v
have cons₂ : eval step (stepRet k (ns.headI :: v)) = Cfg.halt <$> (fun (v : List ℕ) ↦ k.eval (ns.headI :: v)) v
Tactic: rw [Cont.eval, stepRet]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (stepRet (Cont.comp f k) v) = Cfg.halt <$> (Cont.comp f k).eval v
have comp : (do
    let v ← f.eval v
    eval step (Cfg.ret k v)) =
  Cfg.halt <$> (fun (v : List ℕ) ↦ f.eval v >>= k.eval) v
Tactic: rw [Cont.eval, stepRet, code_is_ok]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ (do
      let v ← f.eval v
      eval step (Cfg.ret k v)) =
    Cfg.halt <$> (fun (v : List ℕ) ↦ f.eval v >>= k.eval) v
have comp : Eq (α := Part Cfg)
  (do
    let v ← f.eval v
    eval step (Cfg.ret k v))
  do
  let x ← f.eval v
  let a ← k.eval x
  pure (Cfg.halt a)
Tactic: simp only [← bind_pure_comp, bind_assoc]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ Eq (α := Part Cfg)
    (do
      let v ← f.eval v
      eval step (Cfg.ret k v))
    do
    let x ← f.eval v
    let a ← k.eval x
    pure (Cfg.halt a)
have comp : Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
  let a ← k.eval x
  pure (Cfg.halt a)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)
have comp : ∀ (v' : List ℕ),
  eval step (Cfg.ret k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
Tactic: funext v'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (Cfg.ret k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
have comp : eval step (stepRet k v') = do
  let a ← k.eval v'
  pure (Cfg.halt a)
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
comp :
  eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
⊢ eval step (Cfg.ret k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
have comp₁ : Reaches step (Cfg.ret k v') (stepRet k v')
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
comp :
  eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
comp₁ : Reaches step (Cfg.ret k v') (stepRet k v')
⊢ eval step (Cfg.ret k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
have rw : Cfg
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
⊢ eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
have comp : Cfg.halt <$> k.eval v' = do
  let a ← k.eval v'
  pure (Cfg.halt a)
Tactic: rw [IH, bind_pure_comp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v v' : List ℕ
comp :
  Cfg.halt <$> k.eval v' = do
    let a ← k.eval v'
    pure (Cfg.halt a)
⊢ eval step (stepRet k v') = do
    let a ← k.eval v'
    pure (Cfg.halt a)
have comp₁ : Cfg.halt <$> k.eval v' = Cfg.halt <$> k.eval v'
Tactic: rw [IH, bind_pure_comp]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
⊢ eval step (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) =
    Cfg.halt <$> if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval
have pos : v.headI = 0 → eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
pos : v.headI = 0 → eval step (stepRet k v.tail) = Cfg.halt <$> k.eval v.tail
⊢ eval step (if v.headI = 0 then stepRet k v.tail else stepNormal f (Cont.fix f k) v.tail) =
    Cfg.halt <$> if v.headI = 0 then k.eval v.tail else f.fix.eval v.tail >>= k.eval
have neg : ¬v.headI = 0 → eval step (stepNormal f (Cont.fix f k) v.tail) = Cfg.halt <$> (f.fix.eval v.tail >>= k.eval)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
⊢ eval step (stepNormal f (Cont.fix f k) v.tail) = Cfg.halt <$> (f.fix.eval v.tail >>= k.eval)
have neg : Eq (α := Part Cfg)
  (do
    let v ← f.fix.eval v.tail
    eval step (Cfg.ret k v))
  do
  let x ← f.fix.eval v.tail
  let a ← k.eval x
  pure (Cfg.halt a)
Tactic: simp only [← bind_pure_comp, bind_assoc, cont_eval_fix (code_is_ok _)]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
⊢ Eq (α := Part Cfg)
    (do
      let v ← f.fix.eval v.tail
      eval step (Cfg.ret k v))
    do
    let x ← f.fix.eval v.tail
    let a ← k.eval x
    pure (Cfg.halt a)
have neg : Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
  let a ← k.eval x
  pure (Cfg.halt a)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret k v)) fun (x : List ℕ) ↦ do
    let a ← k.eval x
    pure (Cfg.halt a)
have neg : ∀ (x : List ℕ),
  eval step (Cfg.ret k x) = do
    let a ← k.eval x
    pure (Cfg.halt a)
Tactic: funext
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
IH : ∀ {v : List ℕ}, eval step (stepRet k v) = Cfg.halt <$> k.eval v
v : List ℕ
h : ¬v.headI = 0
x : List ℕ
⊢ eval step (Cfg.ret k x) = do
    let a ← k.eval x
    pure (Cfg.halt a)
have neg : eval step (Cfg.ret k x) = eval step (stepRet k x)
Tactic: rw [bind_pure_comp, ← IH]