Proofs for the CSLib multi-tape simulation

Two layers of proof support Complexitylib.Interop.Cslib.MultiTape.

• Generic CSLib facts (namespace Complexity.MultiTape): one step of a running configuration field by field, the input-head arithmetic, and a space bound of k (t + 1) cells.
• The simulation (namespace Complexity.TM): MultiTapeSim relates our configuration to a simulator configuration. TapeSim covers each one-sided tape with its data and marker tapes, and ZoneOK with inputAction_spec covers the input head. One simulator step follows each of our steps (MultiTapeSim.step). After our machine halts, the rewind phase (Rewinding.run) emits the verdict, and toMultiTape_computesFun assembles the time and space bounds.

def Complexity.MultiTape.applyWrite {S : Type u_1} (cells : ℤ → Option S) (pos : ℤ) : Option (Option S) → ℤ → Option S

The effect of an optional write on a CSLib work tape.

Equations

• Complexity.MultiTape.applyWrite cells pos none = cells
• Complexity.MultiTape.applyWrite cells pos (some s) = Function.update cells pos s

@[simp]

theorem Complexity.MultiTape.applyWrite_none {S : Type u_1} (cells : ℤ → Option S) (pos : ℤ) : applyWrite cells pos none = cells

theorem Complexity.MultiTape.step_of_state_eq_some {k : ℕ} {S : Type u_1} {Q : Type u_2} {input : List S} (M : Turing.MultiTapeTM k S Q) {d : Turing.Cfg k S Q input} {q : Q} (h : d.state = some q) : Turing.MultiTapeTM.step d = { state := (M.tr q d.inputSymbol d.workTapeSymbols).state, inputPos := Turing.moveInputPos d.inputPos (M.tr q d.inputSymbol d.workTapeSymbols).inputTape, workTapes := fun (i : Fin k) => applyWrite (d.workTapes i) (d.workTapePos i) ((M.tr q d.inputSymbol d.workTapeSymbols).workTapes i).1, workTapePos := fun (i : Fin k) => d.workTapePos i + ↑((M.tr q d.inputSymbol d.workTapeSymbols).workTapes i).2, output := d.output ++ (M.tr q d.inputSymbol d.workTapeSymbols).output.toList }

One step from a running configuration, field by field.

theorem Complexity.MultiTape.moveInputPos_val {m : ℕ} (p : Fin (m + 2)) (s : SignType) : ↑(Turing.moveInputPos p s) = min (↑↑p + ↑s).toNat (m + 1)

The position reached by an input-head move.

theorem Complexity.MultiTape.inputSymbol_eq_none_iff {k : ℕ} {S : Type u_1} {Q : Type u_2} {input : List S} (d : Turing.Cfg k S Q input) : d.inputSymbol = none ↔ ↑d.inputPos = 0 ∨ ↑d.inputPos = input.length + 1

The input symbol is blank exactly at the two boundary positions.

theorem Complexity.MultiTape.inputSymbol_of_lt {k : ℕ} {S : Type u_1} {Q : Type u_2} {input : List S} (d : Turing.Cfg k S Q input) {p : ℕ} (hpos : ↑d.inputPos = p + 1) (hp : p < input.length) : d.inputSymbol = some input[p]

Inside the input, the input symbol is the corresponding input letter.

theorem Complexity.MultiTape.spaceUsed_le {k : ℕ} {S : Type u_1} {Q : Type u_2} {input : List S} (M : Turing.MultiTapeTM k S Q) (d : Turing.Cfg k S Q input) (t : ℕ) : Turing.MultiTapeTM.spaceUsed d t ≤ k * (t + 1)

Each work head visits at most t + 1 cells in t steps, so a machine with k work tapes uses at most k * (t + 1) cells.

@[simp]

theorem Complexity.TM.Γ.ofCell_toCell (w : Γw) : Γ.ofCell w.toCell = w.toΓ

def Complexity.TM.markTape : ℤ → Option Bool

The marker tape of a simulated tape: a 1 at position 0 and blank elsewhere.

Equations

• Complexity.TM.markTape p = if p = 0 then some true else none

structure Complexity.TM.TapeSim (t : Tape) (pos mpos : ℤ) (cells marks : ℤ → Option Bool) : Prop

The data tape at pos with cells cells and the marker tape at mpos with cells marks simulate our one-sided tape t: both heads at t's head, data cells 1, 2, … equal to t's (CSLib blank read as □), the marker tape unchanged, and ▷ only in cell 0 of t.

• pos : pos = ↑t.head
• mpos : mpos = ↑t.head
• cells (p : ℕ) : 1 ≤ p → Γ.ofCell (cells ↑p) = t.cells p
• marks : marks = markTape
• inv : t.StartInvariant

theorem Complexity.TM.TapeSim.atStart {t : Tape} {pos mpos : ℤ} {cells marks : ℤ → Option Bool} (h : TapeSim t pos mpos cells marks) : decide (marks mpos = some true) = decide (t.head = 0)

theorem Complexity.TM.TapeSim.read {t : Tape} {pos mpos : ℤ} {cells marks : ℤ → Option Bool} (h : TapeSim t pos mpos cells marks) : (if marks mpos = some true then Γ.start else Γ.ofCell (cells pos)) = t.read

theorem Complexity.TM.TapeSim.writeAndMove {t : Tape} {pos mpos : ℤ} {cells marks : ℤ → Option Bool} (h : TapeSim t pos mpos cells marks) (w : Γw) (d : Dir3) : TapeSim (t.writeAndMove w.toΓ d) (pos + ↑(oneSidedMove (decide (t.head = 0)) d)) (mpos + ↑(oneSidedMove (decide (t.head = 0)) d)) (MultiTape.applyWrite cells pos (oneSidedWrite (decide (t.head = 0)) w)) marks

oneSidedWrite and oneSidedMove simulate one write-and-move.

theorem Complexity.TM.TapeSim.move {t : Tape} {pos mpos : ℤ} {cells marks : ℤ → Option Bool} (h : TapeSim t pos mpos cells marks) (d : Dir3) (hd : d = Dir3.left → t.head ≠ 0) : TapeSim (t.move d) (pos + ↑d.toSign) (mpos + ↑d.toSign) cells marks

Moving both heads, other than left from cell 0, keeps a tape simulated.

def Complexity.TM.ZoneOK (N h : ℕ) : InputZone → Prop

The zone flag is consistent with the input head position h on an input of length N.

Equations

• Complexity.TM.ZoneOK N h Complexity.TM.InputZone.left = (h = 0)
• Complexity.TM.ZoneOK N h Complexity.TM.InputZone.inner = (1 ≤ h)
• Complexity.TM.ZoneOK N h Complexity.TM.InputZone.probe = (h ≤ N)

theorem Complexity.TM.atLeft_eq {N h pos : ℕ} {z : InputZone} {sym : Option Bool} (hz : ZoneOK N h z) (hpos : pos = min h (N + 1)) (hsym : sym = none ↔ pos = 0 ∨ pos = N + 1) : z.atLeft sym = decide (h = 0)

The resolved zone says exactly whether the head is on ▷.

theorem Complexity.TM.inputAction_spec {N : ℕ} {t : Tape} {z : InputZone} {pos : Fin (N + 2)} {sym ov : Option Bool} {o : ℤ} (d : Dir3) (hz : ZoneOK N t.head z) (hpos : ↑pos = min t.head (N + 1)) (hsym : sym = none ↔ ↑pos = 0 ∨ ↑pos = N + 1) (ho : o = ↑(t.head - (N + 1))) (hov : ov = some true ↔ t.head ≤ N + 1) : ZoneOK N (t.move d).head (inputAction (z.atLeft sym) sym ov d).2.2 ∧ ↑(Turing.moveInputPos pos (inputAction (z.atLeft sym) sym ov d).1) = min (t.move d).head (N + 1) ∧ o + ↑(inputAction (z.atLeft sym) sym ov d).2.1 = ↑((t.move d).head - (N + 1))

The input bookkeeping of inputAction tracks one input-head move. Here pos is CSLib's clamped input head, o the overshoot counter, sym the input symbol, and ov the counter tape's symbol.

@[simp]

theorem Complexity.TM.tapeLayout_dataIdx {n : ℕ} {α : Type u_1} (u v : Fin (n + 1) → α) (w : α) (i : Fin (n + 1)) : tapeLayout u v w (dataIdx i) = u i

@[simp]

theorem Complexity.TM.tapeLayout_markIdx {n : ℕ} {α : Type u_1} (u v : Fin (n + 1) → α) (w : α) (i : Fin (n + 1)) : tapeLayout u v w (markIdx i) = v i

@[simp]

theorem Complexity.TM.tapeLayout_overIdx {n : ℕ} {α : Type u_1} (u v : Fin (n + 1) → α) (w : α) : tapeLayout u v w overIdx = w

def Complexity.TM.simTape {n : ℕ} {Q : Type} (c : Cfg n Q) : Fin (n + 1) → Tape

Our read-write tapes in the simulator's order: work tapes, then the output tape.

Equations

• Complexity.TM.simTape c i = Fin.lastCases c.output c.work i

@[simp]

theorem Complexity.TM.simTape_castSucc {n : ℕ} {Q : Type} (c : Cfg n Q) (j : Fin n) : simTape c j.castSucc = c.work j

@[simp]

theorem Complexity.TM.simTape_last {n : ℕ} {Q : Type} (c : Cfg n Q) : simTape c (Fin.last n) = c.output

@[reducible, inline]

abbrev Complexity.TM.SimCfg {n : ℕ} (tm : TM n) (x : List Bool) : Type

The simulator's configurations on input x.

Equations

• tm.SimCfg x = Turing.Cfg (Complexity.TM.simTapes n) Bool (Complexity.TM.MultiTapeState tm.Q) x

structure Complexity.TM.MultiTapeSim {n : ℕ} (tm : TM n) (x : List Bool) (c : Cfg n tm.Q) (z : InputZone) (d : tm.SimCfg x) : Prop

The simulator configuration d, with zone flag z, simulates our configuration c on input x.

• state : d.state = some (MultiTapeState.run c.state z)
• zone : ZoneOK x.length c.input.head z
• inputCells : c.input.cells = (Tape.init (List.map Γ.ofBool x)).cells
• inputPos : ↑d.inputPos = min c.input.head (x.length + 1)
• overPos : d.workTapePos overIdx = ↑(c.input.head - (x.length + 1))
• overCells : d.workTapes overIdx = markTape
• tapes (i : Fin (n + 1)) : TapeSim (simTape c i) (d.workTapePos (dataIdx i)) (d.workTapePos (markIdx i)) (d.workTapes (dataIdx i)) (d.workTapes (markIdx i))
• output : d.output = []

theorem Complexity.TM.MultiTapeSim.inputSymbol_eq_none_iff {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (_h : tm.MultiTapeSim x c z d) : Turing.Cfg.inputSymbol d = none ↔ ↑d.inputPos = 0 ∨ ↑d.inputPos = x.length + 1

theorem Complexity.TM.MultiTapeSim.readIn {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) : (if z.atLeft (Turing.Cfg.inputSymbol d) = true then Γ.start else Γ.ofCell (Turing.Cfg.inputSymbol d)) = c.input.read

The simulator reads our input symbol.

theorem Complexity.TM.MultiTapeSim.readOver {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) : Turing.Cfg.workTapeSymbols d overIdx = some true ↔ c.input.head ≤ x.length + 1

The overshoot counter reads 1 exactly when the input head is at most one cell past the input.

theorem Complexity.TM.MultiTapeSim.simRead {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) (i : Fin (n + 1)) : TM.simRead (Turing.Cfg.workTapeSymbols d) i = (simTape c i).read

theorem Complexity.TM.MultiTapeSim.atStart {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) (i : Fin (n + 1)) : decide (Turing.Cfg.workTapeSymbols d (markIdx i) = some true) = decide ((simTape c i).head = 0)

theorem Complexity.TM.MultiTapeSim.step {n : ℕ} {tm : TM n} {x : List Bool} {c c' : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) (hstep : tm.step c = some c') : ∃ (z' : InputZone), tm.MultiTapeSim x c' z' (Turing.MultiTapeTM.step d)

One step of our machine is one step of the simulator.

theorem Complexity.TM.applyWrite_markTape : MultiTape.applyWrite (fun (x : ℤ) => none) 0 (some (some true)) = markTape

A freshly marked marker tape.

theorem Complexity.TM.multiTapeSim_init {n : ℕ} (tm : TM n) (x : List Bool) : tm.MultiTapeSim x (tm.initCfg x) InputZone.left (Turing.MultiTapeTM.step (Turing.MultiTapeTM.initCfg x))

After its marking step, the simulator simulates our initial configuration.

theorem Complexity.TM.MultiTapeSim.reachesIn {n : ℕ} {tm : TM n} {x : List Bool} {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) : ∃ (z' : InputZone), tm.MultiTapeSim x c' z' (Turing.MultiTapeTM.runFrom d t)

A run of our machine is a run of the simulator of the same length.

structure Complexity.TM.Rewinding {n : ℕ} (tm : TM n) (x : List Bool) (t : Tape) (d : tm.SimCfg x) : Prop

The simulator is rewinding its copy t of our output tape.

• state : d.state = some MultiTapeState.rewind
• out : TapeSim t (d.workTapePos (dataIdx (Fin.last n))) (d.workTapePos (markIdx (Fin.last n))) (d.workTapes (dataIdx (Fin.last n))) (d.workTapes (markIdx (Fin.last n)))
• output : d.output = []

structure Complexity.TM.AtVerdict {n : ℕ} (tm : TM n) (x : List Bool) (t : Tape) (d : tm.SimCfg x) : Prop

The simulator is about to read the verdict in cell 1 of its copy t of our output tape.

• state : d.state = some MultiTapeState.verdict
• out : TapeSim t (d.workTapePos (dataIdx (Fin.last n))) (d.workTapePos (markIdx (Fin.last n))) (d.workTapes (dataIdx (Fin.last n))) (d.workTapes (markIdx (Fin.last n)))
• head : t.head = 1
• output : d.output = []

theorem Complexity.TM.MultiTapeSim.halt {n : ℕ} {tm : TM n} {x : List Bool} {c : Cfg n tm.Q} {z : InputZone} {d : tm.SimCfg x} (h : tm.MultiTapeSim x c z d) (hc : c.state = tm.qhalt) : tm.Rewinding x c.output (Turing.MultiTapeTM.step d)

Once our machine halts, the simulator starts rewinding.

theorem Complexity.TM.Rewinding.step_of_ne_zero {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {d : tm.SimCfg x} (h : tm.Rewinding x t d) (h0 : t.head ≠ 0) : tm.Rewinding x (t.move Dir3.left) (Turing.MultiTapeTM.step d)

theorem Complexity.TM.Rewinding.step_of_eq_zero {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {d : tm.SimCfg x} (h : tm.Rewinding x t d) (h0 : t.head = 0) : tm.AtVerdict x (t.move Dir3.right) (Turing.MultiTapeTM.step d)

theorem Complexity.TM.AtVerdict.step {n : ℕ} {tm : TM n} {x : List Bool} {t : Tape} {d : tm.SimCfg x} (h : tm.AtVerdict x t d) : (Turing.MultiTapeTM.step d).state = none ∧ (Turing.MultiTapeTM.step d).output = [decide (t.cells 1 = Γ.one)]

theorem Complexity.TM.Rewinding.run {n : ℕ} {tm : TM n} {x : List Bool} (m : ℕ) {t : Tape} {d : tm.SimCfg x} : tm.Rewinding x t d → t.head = m → (Turing.MultiTapeTM.runFrom d (m + 2)).state = none ∧ (Turing.MultiTapeTM.runFrom d (m + 2)).output = [decide (t.cells 1 = Γ.one)]

The rewind phase from output-head position m halts after m + 2 more steps, emitting the verdict in output cell 1.

theorem Complexity.TM.DecidesInTime.one_le {n : ℕ} {tm : TM n} {L : Language} {f : ℕ → ℕ} (h : tm.DecidesInTime L f) (m : ℕ) : 1 ≤ f m

A decider takes at least one step on every input length: the verdict cell starts blank.

def Complexity.TM.verdictEmb : Bool ↪ List Bool

CSLib's encoding of a Boolean verdict as a one-bit output.

Equations

• Complexity.TM.verdictEmb = { toFun := fun (b : Bool) => [b], inj' := Complexity.TM.verdictEmb._proof_1 }

theorem Complexity.TM.toMultiTape_computesFun {n : ℕ} (tm : TM n) {L : Language} {f : ℕ → ℕ} (hdec : tm.DecidesInTime L f) : tm.toMultiTape.ComputesFunInTimeAndSpace (Function.Embedding.refl (List Bool)) verdictEmb (Turing.MultiTapeTM.indicator L) (fun (x : List Bool) => 2 * f x.length + 4) fun (x : List Bool) => simTapes n * (2 * f x.length + 5)

The simulator decides what tm decides, within time 2 f + 4 and space (2n + 3) (2 f + 5) when tm decides within time f.