awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 (Λ' Γ Λ σ) σ
⊢ 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')))
have false : ∀ (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: cases a
Cleared hypotheses: a, f
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 (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')))
⊢ 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 (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')))
have true : ∀ (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 (Bool.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: cases a
Cleared hypotheses: a, f
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 (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')
have rw : stepAux (f (a ::ᵥ Subtype.mk (p := fun (l : List Bool) ↦ l.length = l₂.length) l₂ sorry)) 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₂) sorry)) v
    (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
Tactic: rw [← ListBlank.append, IH]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 (Λ' Γ Λ σ) σ
⊢ 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')
have 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) []) [] sorry)) v
      (Tape.mk' (ListBlank.append (List.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
Cleared hypotheses: l₁, l₂, f
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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')
⊢ 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')
have 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₂ sorry)) 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₂) sorry)) v
      (Tape.mk' (ListBlank.append ((a :: 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
Cleared hypotheses: l₁, l₂, f
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ
⊢ 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 Γ Λ σ })
have 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 Γ Λ σ })
Tactic: obtain ⟨L, R, rfl⟩ := T.exists_mk'
Cleared hypotheses: T
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ
⊢ 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 Γ Λ σ })
have none : 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: rcases l₁ with - | l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ Λ σ })
⊢ 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 Γ Λ σ })
have some : ∀ (l₁ : Λ),
  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: rcases l₁ with - | l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ Λ σ })
have 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)))
Tactic: refine TransGen.head' rfl ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 (Tape.mk' L R)))
    (trCfg enc enc0 (stepAux (M l₁) v (Tape.mk' L R)))
have 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)))
Tactic: rw [trTape_mk']
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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₁ : Λ
⊢ 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 Γ Λ σ })
have 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)))
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
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ
⊢ 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)))
have 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)))
Tactic: cases d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)))
⊢ 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)))
have 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)))
Tactic: cases d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 (Stmt.move Dir.left q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.left q) v (Tape.mk' L R)))
have 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))))
Tactic: simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 (Stmt.move Dir.right q)) v (trTape' enc0 L R))
    (trCfg enc enc0 (stepAux (Stmt.move Dir.right q) v (Tape.mk' L R)))
have 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))))
Tactic: simp only [trNormal, stepAux_move, stepAux,
            Tape.move_left_mk',
            trTape'_move_left enc0, trTape'_move_right enc0]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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)) (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)))
have some : 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: simp only [trNormal, stepAux_read dec enc0 encdec, stepAux]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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))))
have 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))))
Tactic: refine ReflTransGen.head rfl ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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 Γ
⊢ 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))))
have 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)))))
Tactic: obtain ⟨a, R, rfl⟩ := R.exists_cons
Cleared hypotheses: R