awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
have zero : (Tape.move Dir.right)^[0] ((Tape.move Dir.left)^[0] 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]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (goal)
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
⊢ (Tape.move Dir.right)^[i] ((Tape.move Dir.left)^[i] L_1) = L_1
have 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
Tactic: induction i with
  | zero => rfl
  | succ i IH => rw [iterate_succ_apply, iterate_succ_apply', Tape.move_left_right, IH]
Cleared hypotheses: i
-- 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
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ stepAux (write (enc a).toList q) v (trTape' enc0 L (ListBlank.cons b R)) =
    stepAux q v (trTape' enc0 (ListBlank.cons a L) R)
have simp : Eq (α := Cfg Bool (Λ' Γ Λ σ) σ)
  (stepAux (write (enc a).toList q) v
    (Tape.mk' (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) sorry)
      (ListBlank.append (enc b).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) sorry))))
  (stepAux q v
    (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) sorry))
      (R.flatMap (fun (x : Γ) ↦ (enc x).toList) sorry)))
Tactic: simp only [trTape', ListBlank.cons_flatMap]
-- 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
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
a b : Γ
L R : ListBlank Γ
⊢ 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) ⋯)))
have 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')
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)
-- 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
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) []
⊢ 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')
have 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')
Tactic: cases List.length_eq_zero_iff.1 e
Cleared hypotheses: l₂', e
-- 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
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
⊢ 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')
have 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')
Tactic: rcases l₂' with - | ⟨b, l₂'⟩
Cleared hypotheses: l₂', e
-- 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
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')
⊢ 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')
have 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')
Tactic: rcases l₂' with - | ⟨b, l₂'⟩
Cleared hypotheses: l₂', e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.PostTuringMachine (hypothesis)
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
⊢ 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')
have e₁ : l₂'.length = l₂.length
Tactic: simp only [List.length_nil, List.length_cons, Nat.succ_inj, reduceCtorEq] at e
Cleared hypotheses: e
-- 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
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 q v (Tape.mk' (ListBlank.append ((a :: l₂).reverseAux l₁) L') R')
have 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'))
Tactic: rw [List.reverseAux, ← IH (a :: l₁) l₂' e]
-- 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
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
⊢ 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')
have 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')
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]
Cleared hypotheses: l₁, l₂, l₂', e
-- 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
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')
⊢ 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')
have 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')
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]
Cleared hypotheses: l₁, l₂, l₂', e
-- 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
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 (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)
have 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)
Tactic: rw [read, this, stepAux_move, encdec, trTape'_move_left 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 → Γ
inst : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
encdec : ∀ (a : Γ), dec (enc a) = a
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
⊢ stepAux (read dec f) v (trTape' enc0 L R) = stepAux (f R.head) v (trTape' enc0 L R)
have 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)
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]
-- 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
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L R : ListBlank Γ
⊢ ∀ (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)
have 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)
Tactic: obtain ⟨a, R, rfl⟩ := R.exists_cons
Cleared hypotheses: 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 → Γ
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 Γ
⊢ ∀ (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)
have 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) sorry)
        (ListBlank.append (enc a).toList (R.flatMap (fun (x : Γ) ↦ (enc x).toList) sorry))))
    (stepAux (f (enc a)) v
      (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.flatMap (fun (x : Γ) ↦ (enc x).toList.reverse) sorry))
        (R.flatMap (fun (x : Γ) ↦ (enc x).toList) sorry)))
Tactic: simp only [ListBlank.head_cons, ListBlank.tail_cons, trTape', ListBlank.cons_flatMap]
-- 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
f : Γ → Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L : ListBlank Γ
a : Γ
R : ListBlank Γ
⊢ ∀ (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) ⋯)))
have 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')
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
-- 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 (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')
have 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'))
Tactic: trans stepAux (readAux l₂.length fun v ↦ f (a ::ᵥ v)) v
        (Tape.mk' ((L'.append l₁).cons a) (R'.append 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 → Γ
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'))
⊢ 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')
have 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₂) sorry)) 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₂))
-- 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 (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'))
have 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')))
Tactic: dsimp [readAux, 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 → Γ
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 (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')))
have 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')))
Tactic: simp only [ListBlank.head_cons, Tape.move_right_mk', ListBlank.tail_cons]