feat(MultiTapeTM): redirect input and output through work tapes

Cslib.lean

@@ -49,7 +49,11 @@ public import Cslib.Computability.Languages.SafetyLiveness
 public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Basic
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.ExtendTapes
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape.Defs
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.OutputToWorkTape
 public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents
 public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas
 public import Cslib.Computability.Machines.Turing.SingleTape.Defs
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic

Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape.lean

@@ -0,0 +1,214 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.InputFromWorkTape.Defs
+
+/-! # Correctness of work-tape input substitution -/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM.InputFromWorkTape
+
+variable {k : ℕ} {Symbol State : Type*}
+variable (tm : MultiTapeTM k Symbol State)
+variable {outerInput input : List Symbol} (p : Fin (outerInput.length + 2))
+
+/-- The virtual work-tape position follows the clamped native input-head movement. -/
+private lemma virtualInputPos_move {input : List Symbol}
+    (p : Fin (input.length + 2)) (move : SignType) :
+    virtualInputPos (moveInputPos p move) =
+      virtualInputPos p + (inputMode p).move move := by
+  cases move with
+  | zero => simp [InputMode.move]
+  | neg =>
+      by_cases hleft : p = 0
+      · rw [hleft]
+        simp [inputMode, InputMode.move]
+      · rw [moveInputPos_neg_of_ne_left p hleft]
+        unfold virtualInputPos
+        have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz))
+        by_cases hright : p.val = input.length + 1 <;>
+          simp [inputMode, hleft, hright, InputMode.move] <;> omega
+  | pos =>
+      by_cases hright : p.val = input.length + 1
+      · have hp : p = ⟨input.length + 1, by omega⟩ := Fin.ext hright
+        rw [hp]
+        simp [inputMode, InputMode.move]
+      · rw [moveInputPos_pos_of_ne_right p hright]
+        unfold virtualInputPos
+        by_cases hleft : p = 0 <;>
+          simp [inputMode, hleft, hright, InputMode.move]
+
+/-- The boundary hint selected before a move is left whenever the resulting native position is
+the left boundary. -/
+private lemma nextBoundary_eq_left {input : List Symbol}
+    (p : Fin (input.length + 2)) (move : SignType)
+    (hmove : moveInputPos p move = 0) :
+    (inputMode p).nextBoundary move = .left := by
+  cases move <;>
+    simp_all [inputMode, InputMode.nextBoundary, moveInputPos]
+  split_ifs at hmove <;> simp_all
+
+/-- The boundary hint selected before a move is right whenever the resulting native position is
+the right boundary. -/
+private lemma nextBoundary_eq_right {input : List Symbol}
+    (p : Fin (input.length + 2)) (move : SignType)
+    (hmove : (moveInputPos p move).val = input.length + 1) :
+    (inputMode p).nextBoundary move = .right := by
+  cases move <;>
+    simp_all [inputMode, InputMode.nextBoundary, moveInputPos] <;>
+    split_ifs at * <;> simp_all <;> omega
+
+/-- Classifying the virtual input tape recovers the native input-head mode, provided the
+boundary hint agrees at the two blank boundary cells. -/
+private lemma classifyInput_listTape {input : List Symbol}
+    (p : Fin (input.length + 2)) (boundary : InputBoundary)
+    (hleft : p = 0 → boundary = .left)
+    (hright : p.val = input.length + 1 → boundary = .right) :
+    classifyInput
+      (listTape input (virtualInputPos p)) boundary =
+      inputMode p := by
+  by_cases hp0 : p = 0
+  · simp [hp0, hleft hp0, virtualInputPos, inputMode,
+      classifyInput, InputBoundary.inputMode, listTape]
+    rfl
+  · by_cases hpr : p.val = input.length + 1
+    · simp [virtualInputPos, hpr, hright hpr, inputMode, hp0,
+        classifyInput, InputBoundary.inputMode]
+    · have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => hp0 (Fin.ext hz))
+      have hi : p.val - 1 < input.length := by omega
+      have hv : virtualInputPos p = (p.val - 1 : ℕ) := by
+        unfold virtualInputPos
+        omega
+      simp [hv, classifyInput, inputMode, hp0, hpr, hi]
+
+/-- Classifying the cell reached by a virtual move recovers the native clamped
+input-head mode after that move. -/
+private lemma classifyInput_move {input : List Symbol}
+    (p : Fin (input.length + 2)) (move : SignType) :
+    classifyInput
+      (listTape input
+        (virtualInputPos p + (inputMode p).move move))
+      ((inputMode p).nextBoundary move) =
+      inputMode (moveInputPos p move) := by
+  rw [← virtualInputPos_move p move]
+  apply classifyInput_listTape
+  · exact nextBoundary_eq_left p move
+  · exact nextBoundary_eq_right p move
+
+
+/-- The simulated input symbol is exactly the symbol on the virtual tape. -/
+private lemma embed_inputSymbol (cfg : Cfg k Symbol State input) :
+    (if inputMode cfg.inputPos = .inside then (embed p cfg).workTapeSymbols 0 else none) =
+      cfg.inputSymbol := by
+  simp only [Cfg.workTapeSymbols, embed, Fin.cases_zero]
+  by_cases hleft : cfg.inputPos = 0
+  · simp [inputMode, hleft, Cfg.inputSymbol]
+  · by_cases hright : cfg.inputPos.val = input.length + 1
+    · simp [inputMode, hleft, hright, Cfg.inputSymbol]
+    · have hp : 0 < cfg.inputPos.val := Nat.pos_of_ne_zero (fun hz => hleft (Fin.ext hz))
+      have hi : cfg.inputPos.val - 1 < input.length := by omega
+      have hv : virtualInputPos cfg.inputPos = (cfg.inputPos.val - 1 : ℕ) := by
+        unfold virtualInputPos
+        omega
+      rw [inputSymbolInner (p := cfg.inputPos.val - 1) (by omega) hi]
+      simp [inputMode, hleft, hright, hv, listTape, hi]
+
+/-- Classification restores the native boundary mode and changes no tapes. -/
+lemma step_classifyCfg (cfg : Cfg k Symbol State input) (boundary : InputBoundary)
+    (hmode : classifyInput (listTape input (virtualInputPos cfg.inputPos)) boundary =
+      inputMode cfg.inputPos) :
+    tm.inputFromWorkTape.step (classifyCfg p cfg boundary) = embed p cfg := by
+  cases hs : cfg.state with
+  | none => simp [step, classifyCfg, embed, hs]
+  | some q =>
+    ext i z <;>
+      simp [step, classifyCfg, embed, inputFromWorkTape, hs, Cfg.workTapeSymbols, hmode]
+
+/-- The moving half of a simulated step performs the native tape actions. -/
+lemma step_embed (cfg : Cfg k Symbol State input) (q : State) (hs : cfg.state = some q) :
+    tm.inputFromWorkTape.step (embed p cfg) =
+      classifyCfg p (tm.step cfg)
+        ((inputMode cfg.inputPos).nextBoundary
+          (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove) := by
+  have hwork : (fun i : Fin k => (embed p cfg).workTapeSymbols i.succ) = cfg.workTapeSymbols := by
+    funext i
+    simp [embed, Cfg.workTapeSymbols]
+  unfold step
+  rw [show (embed p cfg).state = some (.run q (inputMode cfg.inputPos)) by
+    simp [embed, hs], hs]
+  simp only [inputFromWorkTape]
+  rw [embed_inputSymbol p cfg, hwork]
+  generalize htr : tm.tr q cfg.inputSymbol cfg.workTapeSymbols = out
+  simp only [htr]
+  apply Cfg.ext
+  · rfl
+  · simp [classifyCfg, embed]
+  · funext i z
+    refine Fin.cases ?_ (fun j => ?_) i
+    · simp [classifyCfg, embed]
+    · cases hw : (out.workActions j).1 <;> simp [classifyCfg, embed, hw]
+  · funext i
+    refine Fin.cases ?_ (fun j => ?_) i
+    · simpa [classifyCfg, embed] using (virtualInputPos_move cfg.inputPos out.inputMove).symm
+    · simp [classifyCfg, embed]
+  · rfl
+
+/-- Every native step is simulated in two steps, including after a native halt. -/
+lemma runFrom_two (cfg : Cfg k Symbol State input) :
+    tm.inputFromWorkTape.runFrom (embed p cfg) 2 = embed p (tm.step cfg) := by
+  cases hs : cfg.state with
+  | none => simp [runFrom, step, embed, hs]
+  | some q =>
+    change tm.inputFromWorkTape.step (tm.inputFromWorkTape.step (embed p cfg)) = _
+    rw [step_embed tm p cfg q hs]
+    apply step_classifyCfg
+    simpa only [step, hs, virtualInputPos_move] using
+      classifyInput_move cfg.inputPos (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).inputMove
+
+/-- The native run is simulated on a work tape with a factor of two in time. -/
+lemma runFrom_embed (cfg : Cfg k Symbol State input) (n : ℕ) :
+    tm.inputFromWorkTape.runFrom (embed p cfg) (2 * n) = embed p (tm.runFrom cfg n) := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [show 2 * (n + 1) = 2 * n + 2 by omega, runFrom_add, ih,
+      runFrom_two, runFrom_succ_eq_step']
+
+/-- Odd simulation steps are classifier configurations. -/
+lemma runFrom_odd (cfg : Cfg k Symbol State input) (n : ℕ) :
+    ∃ boundary, tm.inputFromWorkTape.runFrom (embed p cfg) (2 * n + 1) =
+      classifyCfg p (tm.runFrom cfg (n + 1)) boundary := by
+  rw [runFrom_add, runFrom_embed]
+  cases hs : (tm.runFrom cfg n).state with
+  | none =>
+    refine ⟨.right, ?_⟩
+    change tm.inputFromWorkTape.step (embed p (tm.runFrom cfg n)) = _
+    rw [runFrom_succ_eq_step', step_of_halt hs]
+    simp [step, embed, classifyCfg, hs]
+  | some q =>
+    refine ⟨(inputMode (tm.runFrom cfg n).inputPos).nextBoundary
+      (tm.tr q (tm.runFrom cfg n).inputSymbol (tm.runFrom cfg n).workTapeSymbols).inputMove, ?_⟩
+    change tm.inputFromWorkTape.step (embed p (tm.runFrom cfg n)) = _
+    rw [step_embed tm p _ q hs, runFrom_succ_eq_step']
+
+/-- The initial classifier enters the native initial configuration, also for empty input. -/
+lemma step_init :
+    tm.inputFromWorkTape.step (classifyCfg p (tm.initCfg input) .right) =
+      embed p (tm.initCfg input) := by
+  apply step_classifyCfg
+  cases input <;>
+    simp [classifyInput, inputMode, virtualInputPos, InputBoundary.inputMode, listTape]
+
+/-- A prepared work tape can replace the native input at any real input position. -/
+lemma runFrom_init (n : ℕ) :
+    tm.inputFromWorkTape.runFrom (classifyCfg p (tm.initCfg input) .right) (2 * n + 1) =
+      embed p (tm.runFrom (tm.initCfg input) n) := by
+  rw [runFrom_succ_eq_step, step_init, runFrom_embed]
+
+end Turing.MultiTapeTM.InputFromWorkTape

Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromWorkTape/Defs.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Mathlib.Data.Fintype.Prod
+public import Mathlib.Data.Fintype.Sum
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TapeContents
+public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic
+
+/-!
+# Substituting a work tape for the input tape
+
+The first work tape contains the virtual input. The remaining tapes are the native work tapes.
+A classifier distinguishes the two blank boundaries, preserving native head clamping without
+extending the alphabet. One native step takes two steps, and the real input head stays parked.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM
+
+variable {k : ℕ} {Symbol State : Type*}
+
+/-- Location of the virtual input head. -/
+inductive InputMode
+  | left
+  | inside
+  | right
+deriving DecidableEq
+
+instance : Finite InputMode :=
+  Finite.of_injective (fun | .left => (0 : Fin 3) | .inside => 1 | .right => 2)
+    (by intro a b h; cases a <;> cases b <;> simp_all)
+
+/-- Boundary toward which a virtual input-head move was made. -/
+inductive InputBoundary
+  | left
+  | right
+
+instance : Finite InputBoundary :=
+  Finite.of_injective (fun | .left => true | .right => false)
+    (by intro a b h; cases a <;> cases b <;> simp_all)
+
+/-- Movement of the virtual input head, with outward boundary moves clamped. -/
+def InputMode.move : InputMode → SignType → SignType
+  | .left, .neg => 0
+  | .right, .pos => 0
+  | _, move => move
+
+/-- Boundary to use if the cell reached by a virtual input-head move is blank. -/
+def InputMode.nextBoundary :
+    InputMode → SignType → InputBoundary
+  | _, .neg | .left, .zero => .left
+  | _, _ => .right
+
+/-- Convert a boundary classifier result to an input mode. -/
+def InputBoundary.inputMode : InputBoundary → InputMode
+  | .left => .left
+  | .right => .right
+
+/-- Control state for the work-tape input simulation. -/
+inductive InputState (State : Type*)
+  | run (q : State) (mode : InputMode)
+  | classify (q : State) (boundary : InputBoundary)
+
+instance [Finite State] : Finite (InputState State) := by
+  let := Fintype.ofFinite State
+  let := Fintype.ofFinite InputMode
+  let := Fintype.ofFinite InputBoundary
+  apply Finite.of_injective (fun s : InputState State => match s with
+    | .run q mode => ((q, Sum.inl mode) : State × (InputMode ⊕ InputBoundary))
+    | .classify q boundary => (q, Sum.inr boundary))
+  intro a b h
+  cases a <;> cases b <;> simp_all
+
+/-- Classify the cell reached after a virtual input-head movement. -/
+def classifyInput (cell : Option Symbol) (boundary : InputBoundary) : InputMode :=
+  if cell.isSome then .inside else boundary.inputMode
+
+/-- Use the first work tape as input, and shift native work tapes one index to the right.
+The virtual head starts at cell zero; classification also handles empty input. -/
+def inputFromWorkTape (tm : MultiTapeTM k Symbol State) :
+    MultiTapeTM (k + 1) Symbol (InputState State) where
+  q₀ := .classify tm.q₀ .right
+  tr q _ work := match q with
+    | .run q mode =>
+      let out := tm.tr q (if mode = .inside then work 0 else none) (fun i => work i.succ)
+      ⟨0, Fin.cases (none, mode.move out.inputMove) out.workActions, out.outS,
+        out.q'.map fun q => .classify q (mode.nextBoundary out.inputMove)⟩
+    | .classify q boundary =>
+      ⟨0, fun _ => (none, 0), none, some (.run q (classifyInput (work 0) boundary))⟩
+
+namespace InputFromWorkTape
+
+/-- View a native input-head position as a work-tape position. -/
+def virtualInputPos {input : List Symbol} (p : Fin (input.length + 2)) : ℤ :=
+  p.val - 1
+
+/-- Classify a native input-head position as the left boundary, an input cell, or the right
+boundary. -/
+def inputMode {input : List Symbol}
+    (p : Fin (input.length + 2)) : InputMode :=
+  if p = 0 then .left else if p.val = input.length + 1 then .right else .inside
+
+/-- Embed a native configuration while parking the real input head at `p`. -/
+def embed {outerInput input : List Symbol} (p : Fin (outerInput.length + 2))
+    (cfg : Cfg k Symbol State input) : Cfg (k + 1) Symbol (InputState State) outerInput where
+  state := cfg.state.map fun q => .run q (inputMode cfg.inputPos)
+  inputPos := p
+  workTapes := Fin.cases (listTape input) cfg.workTapes
+  workTapePos := Fin.cases (virtualInputPos cfg.inputPos) cfg.workTapePos
+  output := cfg.output
+
+/-- The classifier configuration between the two halves of a simulated step. -/
+def classifyCfg {outerInput input : List Symbol} (p : Fin (outerInput.length + 2))
+    (cfg : Cfg k Symbol State input) (boundary : InputBoundary) :
+    Cfg (k + 1) Symbol (InputState State) outerInput :=
+  { embed p cfg with state := cfg.state.map fun q => .classify q boundary }
+
+end InputFromWorkTape
+
+end Turing.MultiTapeTM