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 → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
l₁ : Option Λ
v : σ
L R : ListBlank Γ
none :
  FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := Option.none, var := v, Tape := Tape.mk' L R })
    (step M { l := Option.none, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })
some :
  ∀ (l₁ : Λ),
    FRespects (step (tr enc dec M)) (trCfg enc enc0)
      (trCfg enc enc0 { l := Option.some l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })
      (step M { l := Option.some 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 := Tape.mk' L R : Cfg Γ Λ σ })
    (step M { l := l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })

Tactic:
rcases l₁ with - | l₁
-- 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 Γ Λ σ
v : σ
L R : ListBlank Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := none, var := v, Tape := Tape.mk' L R })
    (step M { l := none, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })

Tactic:
rfl

Premises used: Turing.TM1.step, StateTransition.FRespects, 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 → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
v : σ
L R : ListBlank Γ
⊢ FRespects (step (tr enc dec M)) (trCfg enc enc0) (trCfg enc enc0 { l := none, var := v, Tape := Tape.mk' L R })
    (step M { l := none, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })

Tactic:
exact rfl

Premises used: 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 → Γ
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 : Cfg Γ Λ σ })
    (step M { l := some l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })

Tactic:
TransGen.head' rfl ?_

Premises used: Relation.TransGen.head', StateTransition.Reaches₁, StateTransition.FRespects, 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 → Γ
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)))
refine :
  ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.normal l₁)) v (trTape enc0 (Tape.mk' L R)))
    (trCfg enc enc0 (stepAux (M l₁) 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 : Cfg Γ Λ σ })
    (step M { l := some l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })

Tactic:
refine TransGen.head' rfl ?_

Premises used: Relation.TransGen.head', 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 → Γ
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)))
rw :
  ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.normal l₁)) v (trTape' enc0 L R)) (trCfg enc enc0 (stepAux (M l₁) v (Tape.mk' L R)))
⊢ ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.normal l₁)) v (trTape enc0 (Tape.mk' L R)))
    (trCfg enc enc0 (stepAux (M l₁) v (Tape.mk' L R)))

Tactic:
rw [trTape_mk']

Premises used: Turing.TM1to1.trTape_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 Γ Λ σ
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)))
⊢ ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.normal l₁)) v (trTape' enc0 L R)) (trCfg enc enc0 (stepAux (M l₁) v (Tape.mk' L R)))

Tactic:
this _ R

Premises used: Turing.TM1to1.tr, StateTransition.Reaches
-- 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 Γ Λ σ
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)))
⊢ ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.normal l₁)) v (trTape' enc0 L R)) (trCfg enc enc0 (stepAux (M l₁) v (Tape.mk' L R)))

Tactic:
exact this _ R
-- 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 Γ Λ σ
v : σ
L R : ListBlank Γ
l₁ : Λ
some :
  ∀ (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 := Option.some l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })
    (step M { l := Option.some l₁, var := v, Tape := Tape.mk' L R : Cfg Γ Λ σ })

Tactic:
suffices ∀ q R, 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))) by
      refine TransGen.head' rfl ?_
      rw [trTape_mk']
      exact this _ R
-- 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 Γ Λ σ
d : Dir
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move Dir.left q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.left q) v (Tape.mk' L R)))
some₁ :
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move Dir.right q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.right q) v (Tape.mk' L R)))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move d q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move d q) v (Tape.mk' L R)))

Tactic:
cases d
-- 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 Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L.tail (ListBlank.cons L.head R)))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L.tail (ListBlank.cons L.head R))))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move Dir.left q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.left q) v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0]

Premises used: Turing.Tape.move_left_mk', Turing.TM1to1.trNormal, Turing.TM1.stepAux, Turing.TM1to1.trTape'_move_left, Turing.TM1to1.stepAux_move, Turing.TM1to1.trTape'_move_right
-- 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 Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 (ListBlank.cons R.head L) R.tail))
    (trCfg enc enc0 (stepAux q v (Tape.move Dir.right (Tape.mk' L R))))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.move Dir.right q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.right q) v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0]

Premises used: Turing.Tape.move_left_mk', Turing.TM1to1.trNormal, Turing.TM1.stepAux, Turing.TM1to1.trTape'_move_left, Turing.TM1to1.stepAux_move, Turing.TM1to1.trTape'_move_right
-- 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 Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 L.tail (ListBlank.cons L.head R)))
    (trCfg enc enc0 (stepAux q v (Tape.mk' L.tail (ListBlank.cons L.head R))))

Tactic:
apply IH
-- 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 Γ Λ σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec q) v (trTape' enc0 (ListBlank.cons R.head L) R.tail))
    (trCfg enc enc0 (stepAux q v (Tape.move Dir.right (Tape.mk' L R))))

Tactic:
apply IH
-- 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 Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M))
    { l := Option.some (Λ'.write (f R.head v) q), var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
    (trCfg enc enc0 (stepAux q v (Tape.write (f (Tape.mk' L R).head v) (Tape.mk' L R))))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.write f q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.write f q) v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]

Premises used: Turing.TM1to1.stepAux_read, Turing.TM1to1.trNormal, Turing.TM1.stepAux
-- 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 Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M))
    { l := some (Λ'.write (f R.head v) q), var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
    (trCfg enc enc0 (stepAux q v (Tape.write (f (Tape.mk' L R).head v) (Tape.mk' L R))))

Tactic:
ReflTransGen.head rfl ?_

Premises used: Relation.ReflTransGen.head, rfl, StateTransition.Reaches
-- 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 Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.write (f R.head v) q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.write (f (Tape.mk' L R).head v) (Tape.mk' L R))))
⊢ Reaches (step (tr enc dec M))
    { l := Option.some (Λ'.write (f R.head v) q), var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
    (trCfg enc enc0 (stepAux q v (Tape.write (f (Tape.mk' L R).head v) (Tape.mk' L R))))

Tactic:
refine ReflTransGen.head rfl ?_

Premises used: Relation.ReflTransGen.head, 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 → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  ∀ (a : Γ) (R : ListBlank Γ),
    ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
      (stepAux (tr enc dec M (Λ'.write (f (ListBlank.cons a R).head v) q)) v (trTape' enc0 L (ListBlank.cons a R)))
      (trCfg enc enc0
        (stepAux q v (Tape.write (f (Tape.mk' L (ListBlank.cons a R)).head v) (Tape.mk' L (ListBlank.cons a R)))))
⊢ ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.write (f R.head v) q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux q v (Tape.write (f (Tape.mk' L R).head v) (Tape.mk' L R))))

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

Premises used: Turing.ListBlank.exists_cons, 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 → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
some :
  ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (trNormal dec q) v
      (trTape' enc0 (ListBlank.cons (f a v) L).tail (ListBlank.cons (ListBlank.cons (f a v) L).head R)))
    (trCfg enc enc0 (stepAux q v (Tape.write (f a v) (Tape.mk' L (ListBlank.cons a R)))))
⊢ ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (tr enc dec M (Λ'.write (f (ListBlank.cons a R).head v) q)) v (trTape' enc0 L (ListBlank.cons a R)))
    (trCfg enc enc0
      (stepAux q v (Tape.write (f (Tape.mk' L (ListBlank.cons a R)).head v) (Tape.mk' L (ListBlank.cons a R)))))

Tactic:
rw [tr, Tape.mk'_head, stepAux_write, ListBlank.head_cons, stepAux_move,
        trTape'_move_left enc0]

Premises used: Turing.TM1to1.tr, Turing.TM1to1.stepAux_write, Turing.ListBlank.head_cons, Turing.Tape.mk'_head, 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 → Γ
M : Λ → Stmt Γ Λ σ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
x : Cfg Γ Λ σ
f : Γ → σ → Γ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ReflTransGen (fun (a b : Cfg Bool (Λ' Γ Λ σ) σ) ↦ b ∈ step (tr enc dec M) a)
    (stepAux (trNormal dec q) v
      (trTape' enc0 (ListBlank.cons (f a v) L).tail (ListBlank.cons (ListBlank.cons (f a v) L).head R)))
    (trCfg enc enc0 (stepAux q v (Tape.write (f a v) (Tape.mk' L (ListBlank.cons a R)))))

Tactic:
simpa using IH ..
-- 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 Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M))
    (stepAux (Stmt.load (fun (x : Bool) (s : σ) ↦ a R.head s) (trNormal dec q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.load a q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux_read dec enc0 encdec]

Premises used: Turing.TM1to1.stepAux_read, Turing.TM1to1.trNormal
-- 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 Γ Λ σ
a : Γ → σ → σ
q : Stmt Γ Λ σ
IH :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M))
    (stepAux (Stmt.load (fun (x : Bool) (s : σ) ↦ a R.head s) (trNormal dec q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.load a q) v (Tape.mk' L R)))

Tactic:
apply IH
-- 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 Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (L 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)))
IH₂ :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M))
    (bif p R.head v then stepAux (trNormal dec q₁) v (trTape' enc0 L R)
    else stepAux (trNormal dec q₂) v (trTape' enc0 L R))
    (trCfg enc enc0 (bif p R.head v then stepAux q₁ v (Tape.mk' L R) else stepAux q₂ v (Tape.mk' L R)))
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.branch p q₁ q₂)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.branch p q₁ q₂) v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, Tape.mk'_head]

Premises used: Turing.TM1to1.stepAux_read, Turing.TM1to1.trNormal, Turing.TM1.stepAux, Turing.Tape.mk'_head
-- 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 Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ) (L 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)))
IH₂ :
  ∀ (v : σ) (L 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)))
v : σ
L R : ListBlank Γ
⊢ Reaches (step (tr enc dec M))
    (bif p R.head v then stepAux (trNormal dec q₁) v (trTape' enc0 L R)
    else stepAux (trNormal dec q₂) v (trTape' enc0 L R))
    (trCfg enc enc0 (bif p R.head v then stepAux q₁ v (Tape.mk' L R) else stepAux q₂ v (Tape.mk' L R)))

Tactic:
grind
-- 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 : Γ → σ → Λ
v : σ
L R : ListBlank Γ
some :
  Reaches (step (tr enc dec M))
    { l := Option.some (Λ'.normal (l R.head v)), var := v, Tape := trTape' enc0 L R : Cfg Bool (Λ' Γ Λ σ) σ }
    { l := Option.map Λ'.normal (Option.some (l (Tape.mk' L R).head v)), var := v, Tape := trTape' enc0 L R }
⊢ Reaches (step (tr enc dec M)) (stepAux (trNormal dec (Stmt.goto l)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.goto l) v (Tape.mk' L R)))

Tactic:
simp only [trNormal, stepAux_read dec enc0 encdec, stepAux, trCfg, trTape_mk']

Premises used: Turing.TM1to1.trTape_mk', Turing.TM1to1.stepAux_read, Turing.TM1to1.trNormal, Turing.TM1.stepAux, Turing.TM1to1.trCfg