mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
⊢ x ∈ eval step (stepRet k v'.tail) → ∃ v₂ ∈ pure v'.tail, x ∈ eval step (Cfg.ret k v₂)

pp: case neg
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail) → ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)

Tactic:
<;>

Goal state after:
case pos
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : v'.headI = 0
⊢ x ∈ eval step (stepRet k v'.tail) → ∃ v₂ ∈ pure v'.tail, x ∈ eval step (Cfg.ret k v₂)

case neg
f : Code
k : Cont
v✝ : List ℕ
fok : f.Ok
x c : Cfg
he✝ : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂✝ : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail) → ∃ v₂ ∈ f.fix.eval v'.tail, x ∈ eval step (Cfg.ret k v₂)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case main
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' main = elim a' b c d main

pp: case rev
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' rev = elim a' b c d rev

pp: case aux
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' aux = elim a' b c d aux

pp: case stack
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' stack = elim a' b c d stack

Tactic:
<;>

Goal state after:
case main
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' main = elim a' b c d main

case rev
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' rev = elim a' b c d rev

case aux
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' aux = elim a' b c d aux

case stack
a b c d a' : List Γ'
⊢ update (elim a b c d) main a' stack = elim a' b c d stack
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case main
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' main = elim a b' c d main

pp: case rev
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' rev = elim a b' c d rev

pp: case aux
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' aux = elim a b' c d aux

pp: case stack
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' stack = elim a b' c d stack

Tactic:
<;>

Goal state after:
case main
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' main = elim a b' c d main

case rev
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' rev = elim a b' c d rev

case aux
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' aux = elim a b' c d aux

case stack
a b c d b' : List Γ'
⊢ update (elim a b c d) rev b' stack = elim a b' c d stack
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case main
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' main = elim a b c' d main

pp: case rev
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' rev = elim a b c' d rev

pp: case aux
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' aux = elim a b c' d aux

pp: case stack
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' stack = elim a b c' d stack

Tactic:
<;>

Goal state after:
case main
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' main = elim a b c' d main

case rev
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' rev = elim a b c' d rev

case aux
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' aux = elim a b c' d aux

case stack
a b c d c' : List Γ'
⊢ update (elim a b c d) aux c' stack = elim a b c' d stack
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case main
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' main = elim a b c d' main

pp: case rev
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' rev = elim a b c d' rev

pp: case aux
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' aux = elim a b c d' aux

pp: case stack
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' stack = elim a b c d' stack

Tactic:
<;>

Goal state after:
case main
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' main = elim a b c d' main

case rev
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' rev = elim a b c d' rev

case aux
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' aux = elim a b c d' aux

case stack
a b c d d' : List Γ'
⊢ update (elim a b c d) stack d' stack = elim a b c d' stack
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case none.nil
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ [], p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) none
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], none, l₂)

pp: case none.cons
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ : Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂) none
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, none, l₂)

Tactic:
<;>

Goal state after:
case none.nil
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ [], p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) none
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], none, l₂)

case none.cons
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ : Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂) none
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, none, l₂)
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case neg.none
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
⊢ (Option.map (fun a ↦ default k') none).getD default = [][i]?.getD default

pp: case neg.some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
val✝ : Γ k
⊢ (Option.map (fun a ↦ default k') (some val✝)).getD default = [][i]?.getD default

Tactic:
<;>

Goal state after:
case neg.none
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
⊢ (Option.map (fun a ↦ default k') none).getD default = [][i]?.getD default

case neg.some
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
k' : K
i : ℕ
this : ((proj k').f ∘ fun a ↦ update default k (some a)) = fun a ↦ (proj k').f (update default k (some a))
h : ¬k' = k
val✝ : Γ k
⊢ (Option.map (fun a ↦ default k') (some val✝)).getD default = [][i]?.getD default
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case e_Tape.e_head.e_snd
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse)).head

pp: case e_Tape.e_tail
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) L.reverse).tail

Tactic:
<;>

Goal state after:
case e_Tape.e_head.e_snd
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) L.reverse)).head

case e_Tape.e_tail
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) L.reverse).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) L.reverse).tail
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: case e_Tape.e_head.e_snd.nil
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) []).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) [])).head

pp: case e_Tape.e_head.e_snd.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
head✝ : Γ k
tail✝ : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) (head✝ :: tail✝)).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) (head✝ :: tail✝))).head

pp: case e_Tape.e_tail.nil
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) []).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) []).tail

pp: case e_Tape.e_tail.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
head✝ : Γ k
tail✝ : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) (head✝ :: tail✝)).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) (head✝ :: tail✝)).tail

Tactic:
<;>

Goal state after:
case e_Tape.e_head.e_snd.nil
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) []).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) [])).head

case e_Tape.e_head.e_snd.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
head✝ : Γ k
tail✝ : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) (head✝ :: tail✝)).headI.2 =
    (ListBlank.mk (List.map (fun a ↦ update default k (some a)) (head✝ :: tail✝))).head

case e_Tape.e_tail.nil
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) []).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) []).tail

case e_Tape.e_tail.cons
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝² : DecidableEq K
inst✝¹ : Inhabited Λ
inst✝ : Inhabited σ
k : K
L : List (Γ k)
head✝ : Γ k
tail✝ : List (Γ k)
⊢ (List.map (fun a ↦ (false, update (fun x ↦ none) k (some a))) (head✝ :: tail✝)).tail =
    List.map { f := Prod.mk false, map_pt' := ⋯ }.f (List.map (fun a ↦ update default k (some a)) (head✝ :: tail✝)).tail
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case some.nil
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o : α
h₁ : ∀ x ∈ [], p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], some o, l₂)

pp: case some.cons
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ : Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, some o, l₂)

Tactic:
<;>

Goal state after:
case some.nil
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o : α
h₁ : ∀ x ∈ [], p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    ([], some o, l₂)

case some.cons
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun a ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ : Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun a_1 ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂) (some o)
⊢ (bif p a then ([], some a, L)
    else
      match splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, some o, l₂)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ ∀ x ∈ l₁, p x = false

pp: α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ l₁.append (o :: l₂) = l₁ ++ o :: l₂

Tactic:
<;>

Goal state after:
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ ∀ x ∈ l₁, p x = false

α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun a ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ l₁.append (o :: l₂) = l₁ ++ o :: l₂
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case e_a.refine_1
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 (stepRet (Cont.cons₂ v k) v')

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

Tactic:
<;>

Goal state after:
case e_a.refine_1
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 (stepRet (Cont.cons₂ v k) v')

case e_a.refine_2
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v✝ v v' : List ℕ
⊢ eval step (Cfg.ret k (v.headI :: v')) = eval step (stepRet (Cont.cons₂ v k) v')
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case case.zero
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)) 0) = do
    let v ← Nat.rec (f.eval v.tail) (fun y x ↦ g.eval (y :: v.tail)) 0
    eval step (Cfg.ret k v)

pp: case case.succ
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
n✝ : ℕ
⊢ eval step (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) (n✝ + 1)) = do
    let v ← Nat.rec (f.eval v.tail) (fun y x ↦ g.eval (y :: v.tail)) (n✝ + 1)
    eval step (Cfg.ret k v)

Tactic:
<;>

Goal state after:
case case.zero
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)) 0) = do
    let v ← Nat.rec (f.eval v.tail) (fun y x ↦ g.eval (y :: v.tail)) 0
    eval step (Cfg.ret k v)

case case.succ
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
n✝ : ℕ
⊢ eval step (Nat.rec (stepNormal f k v.tail) (fun y x ↦ stepNormal g k (y :: v.tail)) (n✝ + 1)) = do
    let v ← Nat.rec (f.eval v.tail) (fun y x ↦ g.eval (y :: v.tail)) (n✝ + 1)
    eval step (Cfg.ret k v)
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case none
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x ↦ false) rev k₂ q))) none
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (id L₂)) k₂ (L₁ ++ S k₂) }

pp: case some
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x ↦ false) rev k₂ q))) (some val✝)
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) }

Tactic:
<;>

Goal state after:
case none
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x ↦ false) rev k₂ q))) none
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (id L₂)) k₂ (L₁ ++ S k₂) }

case some
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ TransGen
    (fun a b ↦
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x ↦ false) rev k₂ q))) (some val✝)
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) }