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

case succ
k : Cont
v : List ℕ
⊢ eval step ((fun k v => Cfg.ret k [Nat.succ (List.headI v)]) k v) = do
    let v ← Code.eval Code.succ v
    eval step (Cfg.ret k v)

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

case cons
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝¹ (Cont.cons₁ a✝ v k) v) k v) = do
    let v ← Code.eval (Code.cons a✝¹ a✝) v
    eval step (Cfg.ret k v)

case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
c : Code
⊢ Code.Ok c
induction c <;> intro k v <;> rw [stepNormal]
case cons
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝¹ (Cont.cons₁ a✝ v k) v) k v) = do
    let v ← Code.eval (Code.cons a✝¹ a✝) v
    eval step (Cfg.ret k v)

case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case zero'
k : Cont
v : List ℕ
⊢ eval step ((fun k v => Cfg.ret k (0 :: v)) k v) = do
    let v ← Code.eval Code.zero' v
    eval step (Cfg.ret k v)

case succ
k : Cont
v : List ℕ
⊢ eval step ((fun k v => Cfg.ret k [Nat.succ (List.headI v)]) k v) = do
    let v ← Code.eval Code.succ v
    eval step (Cfg.ret k v)

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

case cons
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝¹ (Cont.cons₁ a✝ v k) v) k v) = do
    let v ← Code.eval (Code.cons a✝¹ a✝) v
    eval step (Cfg.ret k v)

case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
iterate 3 simp only [Code.eval, pure_bind]
case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case cons
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝¹ (Cont.cons₁ a✝ v k) v) k v) = do
    let v ← Code.eval (Code.cons a✝¹ a✝) v
    eval step (Cfg.ret k v)

case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case cons f fs IHf IHfs =>
  rw [Code.eval, IHf]
  simp only [bind_assoc, Cont.eval, pure_bind]; congr ; funext v
  rw [reaches_eval]; swap; exact ReflTransGen.single rfl
  rw [stepRet, IHfs]; congr ; funext v'
  refine' Eq.trans _ (Eq.symm _) <;> try exact reaches_eval (ReflTransGen.single rfl)
case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case comp f g IHf IHg =>
  rw [Code.eval, IHg]
  simp only [bind_assoc, Cont.eval, pure_bind]; congr ; funext v
  rw [reaches_eval]; swap; exact ReflTransGen.single rfl
  rw [stepRet, IHf]
case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case case f g IHf IHg =>
  simp only [Code.eval]
  cases v.headI <;> simp only [Code.eval] <;> [apply IHf; apply IHg]
no goals
case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case fix f IHf => rw [cont_eval_fix IHf]
case cons
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝¹ (Cont.cons₁ a✝ v k) v) k v) = do
    let v ← Code.eval (Code.cons a✝¹ a✝) v
    eval step (Cfg.ret k v)

case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
case tail
k : Cont
v : List ℕ
⊢ eval step ((fun k v => Cfg.ret k (List.tail v)) k v) = do
    let v ← Code.eval Code.tail v
    eval step (Cfg.ret k v)

case cons
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝¹ (Cont.cons₁ a✝ v k) v) k v) = do
    let v ← Code.eval (Code.cons a✝¹ a✝) v
    eval step (Cfg.ret k v)

case comp
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.comp a✝¹ k) v) k v) = do
    let v ← Code.eval (Code.comp a✝¹ a✝) v
    eval step (Cfg.ret k v)

case case
a✝¹ a✝ : Code
a_ih✝¹ : Code.Ok a✝¹
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v =>
          Nat.rec (stepNormal a✝¹ k (List.tail v)) (fun y x => stepNormal a✝ k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case a✝¹ a✝) v
    eval step (Cfg.ret k v)

case fix
a✝ : Code
a_ih✝ : Code.Ok a✝
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal a✝ (Cont.fix a✝ k) v) k v) = do
    let v ← Code.eval (Code.fix a✝) v
    eval step (Cfg.ret k v)
simp only [Code.eval, pure_bind]
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← Code.eval f v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let v ←
      (fun v => do
            let n ← Code.eval f v
            let ns ← Code.eval fs v
            pure (List.headI n :: ns))
          v
    eval step (Cfg.ret k v)
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← Code.eval (Code.cons f fs) v
    eval step (Cfg.ret k v)
rw [Code.eval, IHf]
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← Code.eval f v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let x ← Code.eval f v
    let x_1 ← Code.eval fs v
    eval step (Cfg.ret k (List.headI x :: x_1))
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← Code.eval f v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let v ←
      (fun v => do
            let n ← Code.eval f v
            let ns ← Code.eval fs v
            pure (List.headI n :: ns))
          v
    eval step (Cfg.ret k v)
simp only [bind_assoc, Cont.eval, pure_bind]
case e_a
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) = fun x => do
    let x_1 ← Code.eval fs v
    eval step (Cfg.ret k (List.headI x :: x_1))
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v : List ℕ
⊢ (do
      let v_1 ← Code.eval f v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) =
    do
    let x ← Code.eval f v
    let x_1 ← Code.eval fs v
    eval step (Cfg.ret k (List.headI x :: x_1))
congr
case e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₁ fs v✝ k) v) = do
    let x ← Code.eval fs v✝
    eval step (Cfg.ret k (List.headI v :: x))
case e_a
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v : List ℕ
⊢ (fun v_1 => eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) = fun x => do
    let x_1 ← Code.eval fs v
    eval step (Cfg.ret k (List.headI x :: x_1))
funext v
case e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.196952 = do
    let x ← Code.eval fs v✝
    eval step (Cfg.ret k (List.headI v :: x))

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

f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ Cfg
case e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₁ fs v✝ k) v) = do
    let x ← Code.eval fs v✝
    eval step (Cfg.ret k (List.headI v :: x))
rw [reaches_eval]
case e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ Reaches step (Cfg.ret (Cont.cons₁ fs v✝ k) v) ?m.196952

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

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

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

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

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

f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ Cfg
exact ReflTransGen.single rfl
case e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ (do
      let v_1 ← Code.eval fs v✝
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← Code.eval fs v✝
    eval step (Cfg.ret k (List.headI v :: x))
case e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ fs v✝ k) v) = do
    let x ← Code.eval fs v✝
    eval step (Cfg.ret k (List.headI v :: x))
rw [stepRet, IHfs]
case e_a.h.e_a
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
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 (List.headI v :: x))
case e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v : List ℕ
⊢ (do
      let v_1 ← Code.eval fs v✝
      eval step (Cfg.ret (Cont.cons₂ v k) v_1)) =
    do
    let x ← Code.eval fs v✝
    eval step (Cfg.ret k (List.headI v :: x))
congr
case e_a.h.e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (List.headI v :: v'))
case e_a.h.e_a
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
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 (List.headI v :: x))
funext v'
no goals
case e_a.h.e_a.h
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (List.headI v :: v'))
refine' Eq.trans _ (Eq.symm _) <;> try exact reaches_eval (ReflTransGen.single rfl)
no goals
case e_a.h.e_a.h.refine'_3
f fs : Code
IHf : Code.Ok f
IHfs : Code.Ok fs
k : Cont
v✝ v v' : List ℕ
⊢ eval step (Cfg.ret k (List.headI v :: v')) = eval step (stepRet (Cont.cons₂ v k) v')
exact reaches_eval (ReflTransGen.single rfl)
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ (do
      let v ← Code.eval g v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let v ← (fun v => Code.eval g v >>= Code.eval f) v
    eval step (Cfg.ret k v)
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal g (Cont.comp f k) v) k v) = do
    let v ← Code.eval (Code.comp f g) v
    eval step (Cfg.ret k v)
rw [Code.eval, IHg]
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ (do
      let v ← Code.eval g v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let x ← Code.eval g v
    let v ← Code.eval f x
    eval step (Cfg.ret k v)
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ (do
      let v ← Code.eval g v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let v ← (fun v => Code.eval g v >>= Code.eval f) v
    eval step (Cfg.ret k v)
simp only [bind_assoc, Cont.eval, pure_bind]
case e_a
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ (fun v => eval step (Cfg.ret (Cont.comp f k) v)) = fun x => do
    let v ← Code.eval f x
    eval step (Cfg.ret k v)
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ (do
      let v ← Code.eval g v
      eval step (Cfg.ret (Cont.comp f k) v)) =
    do
    let x ← Code.eval g v
    let v ← Code.eval f x
    eval step (Cfg.ret k v)
congr
case e_a.h
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v✝ v : List ℕ
⊢ eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← Code.eval f v
    eval step (Cfg.ret k v)
case e_a
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ (fun v => eval step (Cfg.ret (Cont.comp f k) v)) = fun x => do
    let v ← Code.eval f x
    eval step (Cfg.ret k v)
funext v
case e_a.h
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v✝ v : List ℕ
⊢ eval step ?m.197726 = do
    let v ← Code.eval f v
    eval step (Cfg.ret k v)

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

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

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

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

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

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

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

f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v✝ v : List ℕ
⊢ Cfg
exact ReflTransGen.single rfl
no goals
case e_a.h
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v✝ v : List ℕ
⊢ eval step (stepRet (Cont.comp f k) v) = do
    let v ← Code.eval f v
    eval step (Cfg.ret k v)
rw [stepRet, IHf]
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ eval step (Nat.rec (stepNormal f k (List.tail v)) (fun y x => stepNormal g k (y :: List.tail v)) (List.headI v)) = do
    let v ← Nat.rec (Code.eval f (List.tail v)) (fun y x => Code.eval g (y :: List.tail v)) (List.headI v)
    eval step (Cfg.ret k v)
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ eval step
      ((fun k v => Nat.rec (stepNormal f k (List.tail v)) (fun y x => stepNormal g k (y :: List.tail v)) (List.headI v))
        k v) =
    do
    let v ← Code.eval (Code.case f g) v
    eval step (Cfg.ret k v)
simp only [Code.eval]
no goals
f g : Code
IHf : Code.Ok f
IHg : Code.Ok g
k : Cont
v : List ℕ
⊢ eval step (Nat.rec (stepNormal f k (List.tail v)) (fun y x => stepNormal g k (y :: List.tail v)) (List.headI v)) = do
    let v ← Nat.rec (Code.eval f (List.tail v)) (fun y x => Code.eval g (y :: List.tail v)) (List.headI v)
    eval step (Cfg.ret k v)
cases v.headI <;> simp only [Code.eval] <;> [apply IHf; apply IHg]
no goals
f : Code
IHf : Code.Ok f
k : Cont
v : List ℕ
⊢ eval step ((fun k v => stepNormal f (Cont.fix f k) v) k v) = do
    let v ← Code.eval (Code.fix f) v
    eval step (Cfg.ret k v)
rw [cont_eval_fix IHf]