Skip to content

refactor(Machines): reuse core List lemmas in transducer kernels #1669

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 1 commit into from
Oct 30, 2026
Merged

refactor(Machines): reuse core List lemmas in transducer kernels #1669

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 4 additions & 11 deletions Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelTransducer.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ module
public import Mathlib.Basic.Finite.Prod
public import Mathlib.Data.Fintype.Option
public import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelZeroSpace
import Mathlib.Basic.Finite.Sum

/-! # Finite-state transducers and their machine semantics

Expand Down Expand Up @@ -69,14 +68,6 @@ public def toTM : MultiTapeTM 0 Symbol (Q × Option Symbol × Bool) :=
{ inputTape := 0, workTapes := Fin.elim0, output := (τ.final q).head?,
state := some (q, (τ.final q).tail.head?, true) }

/-- A word of length at most two is its head followed by the head of its tail. -/
public lemma toList_head?_append {w : List Symbol} (h : w.length ≤ 2) :
w.head?.toList ++ w.tail.head?.toList = w := by
match w, h with
| [], _ => rfl
| [_], _ => rfl
| [_, _], _ => rfl

variable {input : List Symbol}

/-- The configuration of `τ.toTM` in state `st` with the input head at `pos`, having emitted `o`. -/
Expand Down Expand Up @@ -145,7 +136,8 @@ lemma exists_runFrom_halt (q : Q) {i : ℕ} (hi : i ≤ input.length) (o : List
true ⟨input.length + 1, by omega⟩ (o ++ (τ.final q).head?.toList)
refine ⟨1 + u + 1, by omega, ⟨input.length + 1, by omega⟩, ?_⟩
rw [runFrom_add, runFrom_add, runFrom_one, runFrom_one, step_end, hflush, step_halt]
rw [List.drop_length, run_nil, List.append_assoc, toList_head?_append (τ.length_final_le q)]
rw [List.drop_length, run_nil, List.append_assoc, ← List.take_one, List.head?_tail,
← List.take_add_one, List.take_of_length_le (τ.length_final_le q)]
| succ n ih =>
have hi' : i < input.length := by omega
obtain ⟨u₁, hu₁, hflush⟩ := τ.exists_runFrom_flush (input := input) (τ.step q input[i]).1
Expand All @@ -155,7 +147,8 @@ lemma exists_runFrom_halt (q : Q) {i : ℕ} (hi : i ≤ input.length) (o : List
(o ++ (τ.step q input[i]).2) (by omega)
refine ⟨1 + u₁ + u₂, by omega, pos, ?_⟩
rw [runFrom_add, runFrom_add, runFrom_one, step_read _ _ hi', hflush,
List.append_assoc, toList_head?_append (τ.length_step_le _ _), hrest,
List.append_assoc, ← List.take_one, List.head?_tail, ← List.take_add_one,
List.take_of_length_le (τ.length_step_le _ _), hrest,
List.drop_eq_getElem_cons hi', run_cons, List.append_assoc]

/-- `τ.toTM` emits `τ.run τ.q₀ input` on `input`, in `2 * input.length + 3` steps and zero
Expand Down
7 changes: 4 additions & 3 deletions Complexity/Computability/Machines/Turing/MultiTape/Internal/KernelZipTransducer.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ module
public import Complexity.Computability.Machines.Turing.MultiTape.Run
public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame.Basic
public import Mathlib.Data.Fintype.Option
import Complexity.Computability.Machines.Turing.MultiTape.Internal.KernelTransducer
import Mathlib.Basic.Finite.Prod
import Mathlib.Basic.Finite.Sum

Expand Down Expand Up @@ -469,7 +468,8 @@ private lemma seg_zip (q : Q) {r : ℕ} (hr : r ≤ max u.length v.length) (o :
moveInputPosNat_zero (by omega : 2 * u.length + 2 + v.length ≤ (frame u ++ v).length + 1)]
exact cfgAt_congr rfl (by omega)
rw [hu, hv, run_nil_nil]
have hfin := Transducer.toList_head?_append (τ.length_final_le q)
have hfin := (List.take_add_one (l := τ.final q) (i := 1)).symm
rw [List.take_one, ← List.head?_tail, List.take_of_length_le (τ.length_final_le q)] at hfin
rcases hb : (τ.final q).tail.head? with _ | b
· rw [hb, Option.toList_none, List.append_nil] at hfin
rw [hb, Option.map_none] at s₁
Expand Down Expand Up @@ -546,7 +546,8 @@ private lemma seg_zip (q : Q) {r : ℕ} (hr : r ≤ max u.length v.length) (o :
rw [τ.run_of_ne (by simpa [hxdef, hydef, and_comm] using hne), List.tail_drop,
List.tail_drop, List.append_assoc, List.append_assoc,
← List.append_assoc ((τ.step q (y, x)).2.head?.toList),
Transducer.toList_head?_append (τ.length_step_le _ _)]
← List.take_one, List.head?_tail, ← List.take_add_one,
List.take_of_length_le (τ.length_step_le _ _)]
rw [hrun]
exact ((Seg.single (cfgAt_mem_cells (by omega) (by omega)) s₁
(cfgAt_mem_cells (by omega) (by omega))).trans
Expand Down
Loading