-- Mathlib/Computability/TMConfig.lean
theorem code_is_ok (c) : Code.Ok c

Proof state:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (do
      let v_1 ← fs.eval v✝
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
congr

Result:
case cons.e_a.h.e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x => eval step (Cfg.ret k (v.headI :: x))

Proof state:
case cons.e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) = fun x => do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Tactic:
funext v

Result:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₁ fs v✝ k) v) = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Proof state:
case tail
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.tail k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)

Tactic:
rw [stepNormal]

Result:
case tail
k : Cont
v : List ℕ
⊢ eval step ((fun k v => Cfg.ret k v.tail) k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)

Proof state:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (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

Result:
case comp.e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (fun v => eval step (Cfg.ret (Cont.comp f k) v)) = fun x => do
    let v ← f.eval x
    eval step (Cfg.ret k v)

Proof state:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v => 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]

Result:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let v ← (fun v => g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)

Proof state:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.141342

Tactic:
exact ReflTransGen.single rfl

Result:
no goals

Proof state:
case tail

⊢ Code.tail.Ok

Tactic:
intro k v

Result:
case tail
k : Cont
v : List ℕ
⊢ eval step (stepNormal Code.tail k v) = do
    let v ← Code.tail.eval v
    eval step (Cfg.ret k v)

Proof state:
case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.142146

Tactic:
exact ReflTransGen.single rfl

Result:
no goals

Proof state:
case cons.e_a.h.e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₂ v k) v_1)) = fun x => eval step (Cfg.ret k (v.headI :: x))

Tactic:
funext v'

Result:
case cons.e_a.h.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))

Proof state:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ fs v✝ k) v) = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
rw [stepRet, IHfs]

Result:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ (do
      let v_1 ← fs.eval v✝
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Proof state:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let v ← (fun v => g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)

Tactic:
simp only [bind_assoc, Cont.eval, pure_bind]

Result:
case comp
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (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)

Proof state:
case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.142146 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.142146

f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Tactic:
swap

Result:
case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.142146

case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.142146 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Proof state:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₁ fs v✝ k) v) = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

Tactic:
rw [reaches_eval]

Result:
case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.141342 = do
    let x ← fs.eval v✝
    eval step (Cfg.ret k (v.headI :: x))

case cons.e_a.h
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.141342

f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Proof state:
case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ 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]

Result:
case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.142146 = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.comp f k) v) ?m.142146

f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ Cfg

Proof state:
case case
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (Nat.rec (stepNormal f k v.tail) (fun y x => stepNormal g k (y :: v.tail)) v.headI) = do
    let v ← Nat.rec (f.eval v.tail) (fun y x => g.eval (y :: v.tail)) v.headI
    eval step (Cfg.ret k v)

Tactic:
cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]

Result:
no goals

Proof state:
case comp.e_a
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ (fun v => eval step (Cfg.ret (Cont.comp f k) v)) = fun x => do
    let v ← f.eval x
    eval step (Cfg.ret k v)

Tactic:
funext v

Result:
case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

Proof state:
case cons
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (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

Result:
case cons.e_a
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) = fun x => do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))

Proof state:
case tail
k : Cont
v : List ℕ
⊢ eval step ((fun k v => 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]

Result:
no goals

Proof state:
case comp.e_a.h
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v✝ v : List ℕ
⊢ eval step (stepRet (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)

Tactic:
rw [stepRet, IHf]

Result:
no goals

Proof state:
case fix
f : Code
IHf : f.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun k v => 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]

Result:
no goals