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

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
⊢ (addBottom L).head.1 = true

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
S : Finset Λ
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t : List α
helem : ∀ t_1 ∈ (b :: t) :: U, t_1 ≠ [] ∧ P.rmatch t_1 = true
hsum : a = b ∧ x = t ++ U.flatten
⊢ b :: t ∈ (b :: t) :: U

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM2.Stmt Γ Λ σ
v : σ
S : (k : K) → List (Γ k)
f : σ → Option (Γ k) → σ
⊢ TM2.stepAux (stRun (StAct.peek f) q) v S =
    TM2.stepAux q (stVar v (S k) (StAct.peek f)) (update S k (stWrite v (S k) (StAct.peek f)))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trNormal (stRun s q) = goto fun x x_1 ↦ go k s q

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
k : K
s : StAct K Γ σ k
q : TM2.Stmt Γ Λ σ
⊢ trStmts₁ (stRun s q) = {go k s q, ret q} ∪ trStmts₁ q

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.star.rmatch x = true ↔ ∃ S, x = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m ||| n) = ↑m ||| ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
x : List α
⊢ P.rmatch x = true ↔ x ∈ P.matches'

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
this :
  ∀ (q : Stmt Γ Λ σ) (R : ListBlank Γ),
    Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L R))
      (trCfg enc enc0 (stepAux q v (Tape.mk' L R)))
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := some l₁, var := v, Tape := Tape.mk' L R })
    (step M { l := some l₁, var := v, Tape := Tape.mk' L R })

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
P : RegularExpression α
⊢ map f (P ^ 0) = map f P ^ 0

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R S : RegularExpression α
⊢ map id (R + S) = R + S

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R S : RegularExpression α
⊢ map id (R * S) = R * S

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
R : RegularExpression α
⊢ map id R.star = R.star

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R + S)) = map (g ∘ f) (R + S)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R S : RegularExpression α
⊢ map g (map f (R * S)) = map (g ∘ f) (R * S)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
R : RegularExpression α
⊢ map g (map f R.star) = map (g ∘ f) R.star

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (map f (char a)).matches' = (Language.map f) (char a).matches'

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R + S)).matches' = (Language.map f) (R + S).matches'

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R * S)).matches' = (Language.map f) (R * S).matches'

Tactic:
by

Goal state after:
Module: Mathlib.Computability.RegularExpressions

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
R : RegularExpression α
⊢ (map f R.star).matches' = (Language.map f) R.star.matches'

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Computable

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₀)
k : tm.K
h : k = tm.k₀
⊢ List (tm.Γ k)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Computable

Goal state before:
pp: tm : FinTM2
s : List (tm.Γ tm.k₁)
k : tm.K
h : k = tm.k₁
⊢ List (tm.Γ k)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Computable

Goal state before:
pp: α αΓ : Type
inst✝ : Fintype αΓ
ea : α → List αΓ
x✝ : α
⊢ 1 ≤ Polynomial.eval (ea x✝).length 1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: ⊢ zero'.eval = fun v ↦ pure (0 :: v)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: ⊢ succ.eval = fun v ↦ pure [v.headI.succ]

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: ⊢ tail.eval = fun v ↦ pure v.tail

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f fs : Code
⊢ (f.cons fs).eval = fun v ↦ do
    let n ← f.eval v
    let ns ← fs.eval v
    pure (n.headI :: ns)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f g : Code
⊢ (f.comp g).eval = fun v ↦ g.eval v >>= f.eval

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f g : Code
⊢ (f.case g).eval = fun v ↦ Nat.rec (f.eval v.tail) (fun y x ↦ g.eval (y :: v.tail)) v.headI

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: f : Code
⊢ f.fix.eval = PFun.fix fun v ↦ Part.map (fun v ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ nil.eval v = pure []

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ id.eval v = pure v

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ head.eval v = pure [v.headI]

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ zero.eval v = pure [0]

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: v : List ℕ
⊢ pred.eval v = pure [v.headI.pred]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m &&& n) = ↑m &&& ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : List.Vector ℕ m), cg.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval ↑v = pure <$> f v
v : List.Vector ℕ m
⊢ (cf.comp cg).eval ↑v = pure <$> ((Vector.mOfFn fun i ↦ g i v) >>= f)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Γ k
this :
  ∀ (L R : ListBlank (Γ' K Γ)) (n : ℕ),
    Tape.write ((R.nth n).1, update (R.nth n).2 k (some (f v))) ((Tape.move Dir.right)^[n] (Tape.mk' L R)) =
      (Tape.move Dir.right)^[n] (Tape.mk' L (ListBlank.modifyNth (fun a ↦ (a.1, update a.2 k (some (f v)))) n R))
⊢ TM1.stepAux q v
      (Tape.move Dir.right
        (Tape.write
          (((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))).head.1,
            update ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))).head.2 k (some (f v)))
          ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))))) =
    TM1.stepAux q v ((Tape.move Dir.right)^[(f v :: S k).length] (Tape.mk' ∅ (addBottom ?m.135)))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
v : List.Vector ℕ m
⊢ nil.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : List.Vector ℕ m), cl.eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i.succ v
v : List.Vector ℕ m
⊢ (cg.cons cl).eval ↑v = Subtype.val <$> Vector.mOfFn fun i ↦ g i v

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> f v
hg : ∀ (i : Fin n), ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : List.Vector ℕ m), c.eval ↑v = pure <$> ((Vector.mOfFn fun i ↦ g i v) >>= f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m.ldiff n) = (↑m).ldiff ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i : Fin n✝
n : ℕ
x✝ : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property✝ : (a :: as).length = n.succ
⊢ head.eval ↑⟨a :: as, property✝⟩ = pure <$> (↑fun v ↦ v.get 0) ⟨a :: as, property✝⟩

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case some.halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec Stmt.halt) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux Stmt.halt v (Tape.mk' L R)))

Tactic:
| halt =>

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x✝ : Cfg Γ Λ σ
l₁ : Option Λ
v : σ
T : Tape Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := l₁, var := v, Tape := T })
    (step M { l := l₁, var := v, Tape := T })

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝² : ℕ
f : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
i✝ : Fin n✝
n : ℕ
i : Fin n
c : Code
h : ∀ (v : List.Vector ℕ n), c.eval ↑v = pure <$> (↑fun v ↦ v.get i) v
v : List.Vector ℕ n.succ
⊢ (c.comp tail).eval ↑v = pure <$> (↑fun v ↦ v.get i.succ) v

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
this :
  ∀ (q : Stmt Γ Λ σ),
    SupportsStmt S q →
      (∀ q' ∈ writes q, q' ∈ trSupp M S) →
        SupportsStmt (trSupp M S) (trNormal dec q) ∧ ∀ q' ∈ writes q, SupportsStmt (trSupp M S) (tr enc dec M q')
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: ⊢ ∀ (m n : Num), ↑(m ^^^ n) = ↑m ^^^ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m : Num
n : ℕ
⊢ ↑(m <<< n) = ↑m <<< n

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: n : ℕ
IH : ∀ (m : PosNum), ↑(m >>> n) = ↑(pos m) >>> n
m : PosNum
⊢ ∀ (m : ℕ), (m + m).div2 = m

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m : Num
n : ℕ
⊢ ↑(m >>> n) = ↑m >>> n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
this :
  ∀ (a b : ℕ),
    a + b = n →
      n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
        PFun.fix
          (fun v ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a :: b :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)
⊢ (cf.prec cg).eval ((n + 1) :: (↑v).tail) =
    pure
      (pure
        (Nat.rec (f ((n + 1) ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ ((n + 1) ::ᵥ v.tail).tail))
          ((n + 1) ::ᵥ v.tail).head))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: m : Num
n : ℕ
⊢ m.testBit n = (↑m).testBit n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case halt
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
hs : SupportsStmt S Stmt.halt
hw : ∀ q' ∈ writes Stmt.halt, q' ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (trNormal dec Stmt.halt) ∧
    ∀ q' ∈ writes Stmt.halt, SupportsStmt (trSupp M S) (tr enc dec M q')

Tactic:
| halt =>

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
dec : List.Vector Bool n → Γ
M : Λ → Stmt Γ Λ σ
inst✝¹ : Fintype Γ
inst✝ : Inhabited Λ
S : Finset Λ
ss : Supports M S
q : Λ' Γ Λ σ
h : q ∈ trSupp M S
⊢ SupportsStmt (trSupp M S) (tr enc dec M q)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
q' : Λ
s : TM0.Stmt Γ
⊢ TM1.step (tr M) { l := some (Λ'.act s q'), var := (), Tape := T } =
    some
      { l := some (Λ'.normal q'), var := (),
        Tape :=
          match s with
          | TM0.Stmt.move d => Tape.move d T
          | TM0.Stmt.write a => Tape.write a T }

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: Γ : Type u_1
inst✝¹ : Inhabited Γ
Λ : Type u_2
inst✝ : Inhabited Λ
M : TM0.Machine Γ Λ
x✝ : TM0.Cfg Γ Λ
q : Λ
T : Tape Γ
⊢ FRespects (TM1.step (tr M)) (trCfg M) (trCfg M { q := q, Tape := T }) (TM0.step M { q := q, Tape := T })

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝² : ℕ
f✝¹ : List.Vector ℕ n✝² →. ℕ
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ → ℕ
n✝ : ℕ
f : List.Vector ℕ n✝ → ℕ
g : List.Vector ℕ (n✝ + 2) → ℕ
a✝² : Nat.Primrec' f
a✝¹ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n✝ + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
a✝ :
  (cf.prec cg).eval (n :: (↑v).tail) =
    pure (pure (Nat.rec (f (n ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (n ::ᵥ v.tail).tail)) (n ::ᵥ v.tail).head))
b : ℕ
IH :
  ∀ (a : ℕ),
    a + b = n →
      n.succ :: 0 :: g (n ::ᵥ Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) :: (↑v).tail ∈
        PFun.fix
          (fun v ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun x ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a :: b :: Nat.rec (f v.tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a :: (↑v).tail)
a : ℕ
e : a + (b + 1) = n
⊢ a + 1 + b = n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' : List ℕ
h1 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)
this :
  ∀ (v₁ : List ℕ),
    v' ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁ →
      ∀ (n_1 : ℕ),
        v₁ = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∀ m < 0, ¬f (m ::ᵥ v) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝ : ℕ
f✝ : List.Vector ℕ n✝ →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' : List ℕ
h1 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: ↑v)
this :
  ∀ (v₁ : List ℕ),
    v' ∈
        PFun.fix
          (fun v ↦
            (cf.eval v).bind fun y ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁ →
      ∀ (n_1 : ℕ),
        v₁ = n_1 :: ↑v →
          (∀ m < n_1, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = [v'.headI.pred]

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.StackTuringMachine

Goal state before:
pp: K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst✝ : DecidableEq K
k : K
q : TM1.Stmt (Γ' K Γ) (Λ' K Γ Λ σ) σ
v : σ
S : (k : K) → List (Γ k)
L : ListBlank ((k : K) → Option (Γ k))
hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse
f : σ → Option (Γ k) → σ
e : S k = []
⊢ (bif (addBottom L).head.1 then TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))
    else
      TM1.stepAux q (f v (∅.head.2 k))
        (Tape.write (∅.head.1, update ∅.head.2 k none) (Tape.mk' ∅.tail (ListBlank.cons ∅.head (addBottom L))))) =
    TM1.stepAux q (f v none) (Tape.mk' ∅ (addBottom L))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringDegree

Goal state before:
pp: f : ℕ →. ℕ
⊢ f ∈ {f}

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringDegree

Goal state before:
pp: f g h : ℕ →. ℕ
hg : f ≤ᵀ g
hh : g ≤ᵀ h
⊢ ∀ g_1 ∈ {g}, RecursiveIn {h} g_1

Tactic:
simpa using hh

Goal state after:
Module: Mathlib.Computability.TuringDegree

Goal state before:
pp: f g h : ℕ →. ℕ
hg : f ≤ᵀ g
hh : g ≤ᵀ h
⊢ ∀ g_1 ∈ {g}, RecursiveIn {h} g_1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v ↦
              (cf.eval v).bind fun y ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
⊢ Sum.inr (n.succ :: ↑v) ∈
    (cf.eval (n :: ↑v)).bind fun y ↦
      Part.some
        (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
        else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))

Tactic:
by

Goal state after: