awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' R' : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool} (e : (enc a).toList = l₁.reverseAux l₂),
    (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (enc a).toList R')
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
h :
  Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R')) =
    Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂) R')
⊢ (Tape.move Dir.left)^[l₁.length]
      (Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R'))) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
convert! IH e
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' R' : ListBlank Bool
b : Bool
l₁ : List Bool
IH :
  ∀ {l₂ : List Bool} (e : (enc a).toList = l₁.reverseAux l₂),
    (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (enc a).toList R')
l₂ : List Bool
e : (enc a).toList = (b :: l₁).reverseAux l₂
⊢ Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R')) =
    Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂) R')

Tactic:
simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]

Premises used: Turing.Tape.move_left_mk', Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Turing.ListBlank.append
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
R : ListBlank Γ
a : Γ
L : ListBlank Γ
L' R' : ListBlank Bool
l₁ l₂ : List Bool
e : (enc a).toList = l₁.reverseAux l₂
nil :
  ∀ {l₂ : List Bool} (e : (enc a).toList = List.reverseAux [] l₂),
    (Tape.move Dir.left)^[List.length (α := Bool) []] (Tape.mk' (ListBlank.append [] L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (enc a).toList R')
cons :
  ∀ (b : Bool) (l₁ : List Bool)
    (IH :
      ∀ {l₂ : List Bool} (e : (enc a).toList = l₁.reverseAux l₂),
        (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
          Tape.mk' L' (ListBlank.append (enc a).toList R'))
    {l₂ : List Bool} (e : (enc a).toList = (b :: l₁).reverseAux l₂),
    (Tape.move Dir.left)^[(b :: l₁).length] (Tape.mk' (ListBlank.append (b :: l₁) L') (ListBlank.append l₂ R')) =
      Tape.mk' L' (ListBlank.append (enc a).toList R')
⊢ (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
    Tape.mk' L' (ListBlank.append (enc a).toList R')

Tactic:
induction l₁ generalizing l₂ with
  | nil => cases e; rfl
  | cons b l₁ IH =>
    simp only [List.length, iterate_succ_apply]
    convert! IH e
    simp only [ListBlank.tail_cons, ListBlank.append, Tape.move_left_mk', ListBlank.head_cons]

Premises used: Turing.Tape.move_left_mk', Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Function.iterate_succ_apply, Turing.ListBlank.append, List.length
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
⊢ (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons R.head L) R.tail

Tactic:
(Eq.symm ?_).trans (this n _)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
refine :
  (Tape.move Dir.right)^[n] ((Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons R.head L) R.tail)) =
    (Tape.move Dir.right)^[n] (trTape' enc0 L R)
⊢ (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons R.head L) R.tail

Tactic:
refine (Eq.symm ?_).trans (this n _)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
this : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
⊢ (Tape.move Dir.right)^[n] ((Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons R.head L) R.tail)) =
    (Tape.move Dir.right)^[n] (trTape' enc0 L R)

Tactic:
simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons,
      ListBlank.tail_cons]

Premises used: Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Turing.TM1to1.trTape'_move_left, Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
suffices : ∀ (i : ℕ) (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
⊢ (Tape.move Dir.right)^[n] (trTape' enc0 L R) = trTape' enc0 (ListBlank.cons R.head L) R.tail

Tactic:
suffices ∀ i L, (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L by
    refine (Eq.symm ?_).trans (this n _)
    simp only [trTape'_move_left, ListBlank.cons_head_tail, ListBlank.head_cons,
      ListBlank.tail_cons]
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
i : ℕ
_ : ∀ (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L
⊢ ∀ (L : Tape Bool), (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L) = L

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L_1 : Tape Bool
⊢ (Tape.move Dir.right)^[0] ((Tape.move Dir.left)^[0] L_1) = L_1

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
L_1 : Tape Bool
i : ℕ
IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
succ : (Tape.move Dir.right)^[i] (Tape.move Dir.right ((Tape.move Dir.left)^[i + 1] L_1)) = L_1
succ₁ : (Tape.move Dir.right)^[i] (Tape.move Dir.right (Tape.move Dir.left ((Tape.move Dir.left)^[i] L_1))) = L_1
succ₂ : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
succ₃ succ₄ : L_1 = L_1
⊢ (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L_1) = L_1

Tactic:
rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]

Premises used: Function.iterate_succ_apply', Turing.Tape.move_left_right, Function.iterate_succ_apply
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
L R : ListBlank Γ
i : ℕ
L_1 : Tape Bool
zero : (Tape.move Dir.right)^[0] ((Tape.move Dir.left)^[0] L_1) = L_1
succ :
  ∀ (i : ℕ) (IH : (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1),
    (Tape.move Dir.right)^[i + 1] ((Tape.move Dir.left)^[i + 1] L_1) = L_1
⊢ (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1

Tactic:
induction i with
  | zero => rfl
  | succ i IH => rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]

Premises used: Function.iterate_succ_apply', Turing.Tape.move_left_right, Function.iterate_succ_apply
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
simp :
  Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (stepAux (write (enc a).toList q) v
      (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc b).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
    (stepAux q v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))
⊢ stepAux (write (enc a).toList q) v (trTape' enc0 L (ListBlank.cons b R)) =
    stepAux q v (trTape' enc0 (ListBlank.cons a L) R)

Tactic:
simp only [trTape', ListBlank.cons_flatMap]

Premises used: Turing.TM1to1.trTape', Turing.ListBlank.cons_flatMap
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
this :
  ∀ {L' R' : ListBlank Bool} (l₁ l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (stepAux (write (enc a).toList q) v
      (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc b).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
    (stepAux q v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))

Tactic:
this [] _ _ ((enc b).2.trans (enc a).2.symm)

Premises used: Turing.ListBlank.flatMap, List.reverse, Turing.ListBlank.append, Eq.symm, Eq.trans, Subtype.property, List.nil
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
this :
  ∀ {L' R' : ListBlank Bool} (l₁ l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (stepAux (write (enc a).toList q) v
      (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc b).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
    (stepAux q v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))

Tactic:
exact this [] _ _ ((enc b).2.trans (enc a).2.symm)

Premises used: Eq.symm, Eq.trans, Subtype.property, List.nil
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
suffices :
  ∀ {L' R' : ListBlank Bool} (l₁ l₂ l₂' : List Bool),
    l₂'.length = l₂.length →
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
        stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (stepAux (write (enc a).toList q) v
      (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc b).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
    (stepAux q v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))

Tactic:
suffices ∀ {L' R'} (l₁ l₂ l₂' : List Bool) (_ : l₂'.length = l₂.length),
      stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (L'.append (List.reverseAux l₂ l₁)) R') by
    exact this [] _ _ ((enc b).2.trans (enc a).2.symm)
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ l₂' : List Bool
e : l₂'.length = List.length (α := Bool) []
nil :
  ∀ (e : List.length (α := Bool) [] = List.length (α := Bool) []),
    stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
      stepAux q v (Tape.mk' (ListBlank.append (List.reverseAux [] l₁) L') R')
⊢ stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q v (Tape.mk' (ListBlank.append (List.reverseAux [] l₁) L') R')

Tactic:
cases List.length_eq_zero_iff.1 e

Premises used: Iff.mp, List.length_eq_zero_iff
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
e : List.length (α := Bool) [] = List.length (α := Bool) []
⊢ stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append (List.reverseAux [] l₁) L') R')

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool) (e : l₂'.length = l₂.length),
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ l₂' : List Bool
e : l₂'.length = (a :: l₂).length
cons :
  ∀ (e : List.length (α := Bool) [] = (a :: l₂).length),
    stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
      stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
cons₁ :
  ∀ (b : Bool) (l₂' : List Bool) (e : (b :: l₂').length = (a :: l₂).length),
    stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
      stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
rcases l₂' with - | ⟨b, l₂'⟩
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool) (e : l₂'.length = l₂.length),
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
e : List.length (α := Bool) [] = (a :: l₂).length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
simp only [List.length_nil, List.length_cons, Nat.succ_inj, reduceCtorEq] at e

Premises used: Nat.succ_inj, reduceCtorEq, List.length_cons, List.length_nil
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool) (e : l₂'.length = l₂.length),
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : (b :: l₂').length = (a :: l₂).length
⊢ l₂'.length = l₂.length

Tactic:
simp only [List.length_nil, List.length_cons, Nat.succ_inj, reduceCtorEq] at e

Premises used: Nat.succ_inj, reduceCtorEq, List.length_cons, List.length_nil
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool) (e : l₂'.length = l₂.length),
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
cons :
  stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂' R'))
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
rw [List.reverseAux, ← IH (a :: l₁) l₂' e]

Premises used: List.reverseAux, List.cons
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ l₂' : List Bool) (e : l₂'.length = l₂.length),
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
b : Bool
l₂' : List Bool
e : l₂'.length = l₂.length
⊢ stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (b :: l₂') R')) =
    stepAux (write l₂ q) v (Tape.mk' (ListBlank.append (a :: l₁) L') (ListBlank.append l₂' R'))

Tactic:
simp [stepAux, ListBlank.append, write]

Premises used: Turing.TM1.stepAux, Turing.TM1to1.write, Turing.ListBlank.append
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ l₂ l₂' : List Bool
e : l₂'.length = l₂.length
nil :
  ∀ (l₁ l₂' : List Bool) (e : l₂'.length = List.length (α := Bool) []),
    stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (ListBlank.append (List.reverseAux [] l₁) L') R')
cons :
  ∀ (a : Bool) (l₂ : List Bool)
    (IH :
      ∀ (l₁ l₂' : List Bool) (e : l₂'.length = l₂.length),
        stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
          stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R'))
    (l₁ l₂' : List Bool) (e : l₂'.length = (a :: l₂).length),
    stepAux (write (a :: l₂) q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
      stepAux q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
⊢ stepAux (write l₂ q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
induction l₂ generalizing l₁ l₂' with
  | nil => cases List.length_eq_zero_iff.1 e; rfl
  | cons a l₂ IH =>
    rcases l₂' with - | ⟨b, l₂'⟩ <;>
      simp only [List.length_nil, List.length_cons, Nat.succ_inj, reduceCtorEq] at e
    rw [List.reverseAux, ← IH (a :: l₁) l₂' e]
    simp [stepAux, ListBlank.append, write]

Premises used: Nat.succ_inj, reduceCtorEq, List.length_cons, List.reverseAux, Turing.TM1.stepAux, Turing.TM1to1.write, Turing.ListBlank.append, Iff.mp, List.length_nil, List.length_eq_zero_iff
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : 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 Γ
this :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
rw :
  stepAux (f R.head) v
      (trTape' enc0 (ListBlank.cons R.head L).tail (ListBlank.cons (ListBlank.cons R.head L).head R.tail)) =
    stepAux (f R.head) v (trTape' enc0 L R)
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
rw [read, this, stepAux_move, encdec, trTape'_move_left enc0]

Premises used: Turing.TM1to1.read, Turing.TM1to1.trTape'_move_left, Turing.TM1to1.stepAux_move
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : 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 Γ
this :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
⊢ stepAux (f R.head) v
      (trTape' enc0 (ListBlank.cons R.head L).tail (ListBlank.cons (ListBlank.cons R.head L).head R.tail)) =
    stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
simp only [ListBlank.head_cons, ListBlank.cons_head_tail, ListBlank.tail_cons]

Premises used: Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : 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 Γ
suffices :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)

Tactic:
suffices ∀ f, stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (L.cons R.head) R.tail) by
    rw [read, this, stepAux_move, encdec, trTape'_move_left enc0]
    simp only [ListBlank.head_cons, ListBlank.cons_head_tail, ListBlank.tail_cons]
-- Module: Mathlib.Computability.TuringMachine.PostTuringMachine
Goal:
Γ : 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 Γ
obtain :
  ∀ (a : Γ) (R : ListBlank Γ) (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L (ListBlank.cons a R)) =
      stepAux (f (enc (ListBlank.cons a R).head)) v
        (trTape' enc0 (ListBlank.cons (ListBlank.cons a R).head L) (ListBlank.cons a R).tail)
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux n f) v (trTape' enc0 L R) =
      stepAux (f (enc R.head)) v (trTape' enc0 (ListBlank.cons R.head L) R.tail)

Tactic:
obtain ⟨a, R, rfl⟩ := R.exists_cons

Premises used: Turing.ListBlank.exists_cons, rfl