awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ListBlank Γ
a : Γ
R : ListBlank Γ
simp :
  ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
      (stepAux (readAux n f) v
        (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
          (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
      (stepAux (f (enc a)) v
        (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯))
          (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯)))
⊢ ∀ (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)

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

Premises used: Turing.TM1to1.trTape', Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, 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
dec : List.Vector Bool n → Γ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = i) l₂ h)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (stepAux (readAux n f) v
      (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
    (stepAux (f (enc a)) 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 n f (L.flatMap (fun x => (enc x).1.reverse) _)
      (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2

Premises used: Turing.ListBlank.flatMap, List.Vector, List.reverse, Turing.ListBlank.append, Subtype.val, List.Vector.toList, 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
dec : List.Vector Bool n → Γ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f_1 : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
this :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = i) l₂ h)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (stepAux (readAux n f) v
      (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
        (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
    (stepAux (f (enc a)) 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 n f (L.flatMap (fun x => (enc x).1.reverse) _)
      (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2

Premises used: Turing.ListBlank.flatMap, List.reverse, Subtype.val, 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
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 : ListBlank Γ
a : Γ
R : ListBlank Γ
suffices :
  ∀ (i : ℕ) (f : List.Vector Bool i → Stmt Bool (Λ' Γ Λ σ) σ) (L' R' : ListBlank Bool) (l₁ l₂ : List Bool)
    (h : l₂.length = i),
    stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = i) l₂ h)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
⊢ ∀ (f : List.Vector Bool n → Stmt Bool (Λ' Γ Λ σ) σ),
    Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
      (stepAux (readAux n f) v
        (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) ⋯)
          (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) ⋯))))
      (stepAux (f (enc a)) 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 ∀ i f L' R' l₁ l₂ h,
      stepAux (readAux i f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f ⟨l₂, h⟩) v (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R') by
    intro f
    exact this n f (L.flatMap (fun x => (enc x).1.reverse) _)
      (R.flatMap (fun x => (enc x).1) _) [] _ (enc a).2
-- 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
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
f : List.Vector Bool (List.length (α := Bool) []) → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (readAux (List.length (α := Bool) []) f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = List.length (α := Bool) []) [] ⋯)) 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
dec : List.Vector Bool n → Γ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
trans :
  stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
    stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
trans₁ :
  stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')) =
    stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = (a :: l₂).length) (a :: l₂) ⋯)) v
      (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
⊢ stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
    stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = (a :: l₂).length) (a :: l₂) ⋯)) v
      (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
trans stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
        (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))

Premises used: Turing.Tape.mk', Turing.TM1.stepAux, Turing.ListBlank.cons, Turing.TM1to1.readAux, Turing.ListBlank.append, List.length, List.Vector.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
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
dsimp :
  Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (bif (ListBlank.cons a (ListBlank.append l₂ R')).head then
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (true ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R'))))
    else
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (false ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R')))))
    (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
⊢ stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
    stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))

Tactic:
dsimp [readAux, stepAux]

Premises used: Turing.TM1.stepAux, Turing.TM1to1.readAux
-- 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
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
simp :
  Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (bif a then
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
    (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (bif (ListBlank.cons a (ListBlank.append l₂ R')).head then
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (true ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R'))))
    else
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (false ::ᵥ v)) v
        (Tape.move Dir.right (Tape.mk' (ListBlank.append l₁ L') (ListBlank.cons a (ListBlank.append l₂ R')))))
    (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))

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

Premises used: Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Turing.Tape.move_right_mk'
-- 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 Bool.false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
false :
  ∀ (f : List.Vector Bool (Bool.false :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ),
    Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
      (bif Bool.false then
        stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.true ::ᵥ v)) v
          (Tape.mk' (ListBlank.cons Bool.false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
      else
        stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.false ::ᵥ v)) v
          (Tape.mk' (ListBlank.cons Bool.false (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
      (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons Bool.false (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
true :
  ∀ (f : List.Vector Bool (Bool.true :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ),
    Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
      (bif Bool.true then
        stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.true ::ᵥ v)) v
          (Tape.mk' (ListBlank.cons Bool.true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
      else
        stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.false ::ᵥ v)) v
          (Tape.mk' (ListBlank.cons Bool.true (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
      (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons Bool.true (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (bif a then
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (Bool.false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
    (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))

Tactic:
cases a
-- 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
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (false :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (bif false then
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
    (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (false ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons false (ListBlank.append l₁ L')) (ListBlank.append 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
dec : List.Vector Bool n → Γ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (true :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
    (bif true then
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (true ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R'))
    else
      stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (false ::ᵥ v)) v
        (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append l₂ R')))
    (stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (true ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons true (ListBlank.append l₁ L')) (ListBlank.append 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
dec : List.Vector Bool n → Γ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
rw :
  stepAux (f (a ::ᵥ Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
      (Tape.mk' (ListBlank.append (l₂.reverseAux (a :: l₁)) L') R') =
    stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = (a :: l₂).length) (a :: l₂) ⋯)) v
      (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
⊢ stepAux (readAux l₂.length fun (v : List.Vector Bool l₂.length) ↦ f (a ::ᵥ v)) v
      (Tape.mk' (ListBlank.cons a (ListBlank.append l₁ L')) (ListBlank.append l₂ R')) =
    stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = (a :: l₂).length) (a :: l₂) ⋯)) v
      (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')

Tactic:
rw [← ListBlank.append, IH]

Premises used: Turing.ListBlank.append
-- 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
v : σ
L' R' : ListBlank Bool
a : Bool
l₂ : List Bool
IH :
  ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
        (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')
l₁ : List Bool
f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ
⊢ stepAux (f (a ::ᵥ Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
      (Tape.mk' (ListBlank.append (l₂.reverseAux (a :: l₁)) L') R') =
    stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = (a :: l₂).length) (a :: l₂) ⋯)) v
      (Tape.mk' (ListBlank.append ((a :: l₂).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
dec : List.Vector Bool n → Γ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
v : σ
L' R' : ListBlank Bool
l₁ l₂ : List Bool
f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ
nil :
  ∀ (l₁ : List Bool) (f : List.Vector Bool (List.length (α := Bool) []) → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux (List.length (α := Bool) []) f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = List.length (α := Bool) []) [] ⋯)) v
        (Tape.mk' (ListBlank.append (List.reverseAux [] l₁) L') R')
cons :
  ∀ (a : Bool) (l₂ : List Bool)
    (IH :
      ∀ (l₁ : List Bool) (f : List.Vector Bool l₂.length → Stmt Bool (Λ' Γ Λ σ) σ),
        stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
          stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
            (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R'))
    (l₁ : List Bool) (f : List.Vector Bool (a :: l₂).length → Stmt Bool (Λ' Γ Λ σ) σ),
    stepAux (readAux (a :: l₂).length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append (a :: l₂) R')) =
      stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = (a :: l₂).length) (a :: l₂) ⋯)) v
        (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
⊢ stepAux (readAux l₂.length f) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) =
    stepAux (f (Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ ⋯)) v
      (Tape.mk' (ListBlank.append (l₂.reverseAux l₁) L') R')

Tactic:
induction l₂ generalizing l₁ with
  | nil => rfl
  | cons a l₂ IH =>
    trans stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
        (Tape.mk' ((L'.append l₁).cons a) (R'.append l₂))
    · dsimp [readAux, stepAux]
      simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]
      cases a <;> rfl
    · rw [← ListBlank.append, IH]
      rfl

Premises used: Turing.ListBlank.head_cons, Turing.TM1.stepAux, Turing.ListBlank.tail_cons, Turing.TM1to1.readAux, Turing.ListBlank.append, Turing.Tape.move_right_mk'
-- 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 → Γ
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 Γ
obtain :
  ∀ (L R : ListBlank Γ),
    FRespects (step (tr enc dec M)) (trCfg enc enc0)
      (trCfg enc enc0 { l := l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })
      (step M { l := l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := l₁, var := v, Tape := T : Cfg Γ Λ σ })
    (step M { l := l₁, var := v, Tape := T : Cfg Γ Λ σ })

Tactic:
obtain ⟨L, R, rfl⟩ := T.exists_mk'

Premises used: Turing.Tape.exists_mk', rfl