From 3e67a9b09049883bbbd3702f4103dde791c073b6 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Fri, 28 Aug 2026 20:15:29 +0300 Subject: [PATCH 01/18] feat(MultiTapeTM): Nondeterministic multi-tape Turing machines A nondeterministic machine replaces the transition function by a transition relation. Configurations and the effect of an action move to a shared `MultiTape/Configuration.lean`; no existing statement changes meaning. A computation path is the list of configurations it passes through together with a proof that they form a chain of steps from the initial configuration to the one it ends at, so `List.IsChainFromTo` carries the whole validity condition. `MultiTapeTM.toNTM` embeds the deterministic machine and `toNTM_computes` shows the embedding preserves computation in bounded time and space. Co-Authored-By: Claude Opus 5 (1M context) --- Cslib.lean | 3 + .../Turing/MultiTape/Configuration.lean | 187 ++++++++++++++++++ .../Turing/MultiTape/Deterministic.lean | 144 ++------------ .../DeterministicToNondeterministic.lean | 107 ++++++++++ .../Turing/MultiTape/Nondeterministic.lean | 144 ++++++++++++++ 5 files changed, 459 insertions(+), 126 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean diff --git a/Cslib.lean b/Cslib.lean index 1d0469a56..23061d3ac 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -46,7 +46,10 @@ public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Languages.SafetyLiveness +public import Cslib.Computability.Machines.Turing.MultiTape.Configuration public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic +public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean new file mode 100644 index 000000000..27ea589ae --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -0,0 +1,187 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Aviv Bar Natan +-/ + +module + +public import Mathlib.Algebra.Order.BigOperators.Group.Finset +public import Mathlib.Algebra.Order.Group.Abs +public import Mathlib.Algebra.Order.Group.Int +public import Mathlib.Data.Finset.Dedup +public import Mathlib.Data.Finset.Max +public import Mathlib.Data.Int.Interval +public import Mathlib.Data.Sign.Defs +public import Cslib.Init + +/-! +# Configurations of Multi-Tape Turing Machines + +Configurations of a multi-tape Turing machine with a read-only input tape, `k` work tapes and one +write-only output tape, together with what a single transition does to one and the space measure +read off a list of them. + +## Design + +Nothing here mentions a machine. A step is described in two parts: an `Action`, recording +which way the input head moves, what is written and where the work heads move, which symbol is +emitted and which state follows; and `Action.apply`, which carries it out on a +configuration. + +The output tape is part of the configuration, so the string emitted along a run can be read off +the configuration the run ends in. + +## Important Declarations + +* `Cfg`: the configuration: the internal state, the tape contents and head positions, and the + output tape +* `Action`: what a machine does in one step +* `Action.apply`: the effect of one action on a configuration +* `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in +* `spaceUsedOfCfgs`: work tape cells touched along a list of configurations +-/ + +@[expose] public section + +namespace Turing + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + +/-- What a machine does in one step. -/ +structure Action (k : ℕ) (Symbol State : Type*) where + /-- The movement (attempt) of the input head. -/ + inputMove : SignType + /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/ + workActions : Fin k → (Option (Option Symbol)) × SignType + /-- An optional symbol to output. -/ + outS : Option Symbol + /-- The successor state or none to halt. -/ + q' : Option State + +/-- +The configurations of a Turing machine is relative to the input of the machine and consist of: +- an `Option`al state (or none for the halting state), +- the position of the input head (shifted by one), +- the contents of the work tape, +- the positions of the work tape heads, +- the contents of the write-only output tape +-/ +@[ext] +structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where + /-- the state of the TM (or none for the halting state) -/ + state : Option State + /-- the position of the input head, shifted by one -/ + inputPos : Fin (input.length + 2) + /-- the work tapes -/ + workTapes : Fin k → ℤ → Option Symbol + /-- the positions of the heads on the work tapes -/ + workTapePos : Fin k → ℤ + /-- the contents of the write-only output tape -/ + output : List Symbol +deriving Inhabited + +/-- Attempt to move the input tape head. +The machine can only read one empty cell outside of the input, +any attempted movement beyond that results in no movement. + +The addition is performed in `ℤ` before clamping. Performing it in `Fin (n + 2)` would wrap an +outward boundary move to the opposite end of the input. -/ +@[scoped grind =] +def moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2) := + let p := ((pos.val : ℤ) + (m.cast : ℤ)).toNat + if h : p < n + 2 then ⟨p, h⟩ else ⟨n + 1, by omega⟩ + +@[simp] +lemma moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) : + moveInputPos pos 0 = pos := by + apply Fin.ext + simp [moveInputPos, pos.isLt] + +@[simp] +lemma moveInputPos_leftBoundary {n : ℕ} : + moveInputPos (0 : Fin (n + 2)) (-1) = 0 := by + apply Fin.ext + simp [moveInputPos] + +@[simp] +lemma moveInputPos_rightBoundary {n : ℕ} : + moveInputPos (⟨n + 1, by omega⟩ : Fin (n + 2)) 1 = ⟨n + 1, by omega⟩ := by + unfold moveInputPos + rw [dite_eq_right (by simp; omega)] + +/-- A left move away from the left input boundary decrements the native input position. -/ +lemma moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) : + moveInputPos p .neg = ⟨p.val - 1, by have := p.isLt; omega⟩ := by + have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => h (Fin.ext hz)) + unfold moveInputPos + apply Fin.ext + rw [dite_eq_left] <;> simp <;> omega + +/-- A right move away from the right input boundary increments the native input position. -/ +lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n + 1) : + moveInputPos p .pos = ⟨p.val + 1, by have := p.isLt; omega⟩ := by + unfold moveInputPos + rw [dite_eq_left] + · apply Fin.ext + simp + · simp + omega + +/-- The symbol currently under the input tape head. -/ +def Cfg.inputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := + if h₁ : cfg.inputPos = 0 then none + else if h₂ : cfg.inputPos = input.length + 1 then none + else input[cfg.inputPos.val - 1]'(by grind) + +@[simp] +lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ) + (h₁ : cfg.inputPos.val = 1 + p) + (h₂ : p < input.length) : + cfg.inputSymbol = some input[p] := by + grind [Cfg.inputSymbol] + +/-- The symbol read by work tape `i`. -/ +def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol := + cfg.workTapes i (cfg.workTapePos i) + +/-- A configuration is halted when it has no state to continue from. -/ +abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none + +/-- The initial configuration for a starting state and an input string. -/ +@[simp] +def Cfg.init (q₀ : State) (input : List Symbol) : Cfg k Symbol State input := + ⟨some q₀, 1, fun _ _ => none, fun _ => 0, []⟩ + +/-- +The effect of an action on a configuration: move the input head, write and move on the work tapes, +append the emitted symbol to the output tape, and go to the successor state. This is the part of a +step that does not depend on how the action was chosen. +-/ +@[simp] +def Action.apply (out : Action k Symbol State) (cfg : Cfg k Symbol State input) : + Cfg k Symbol State input where + state := out.q' + inputPos := moveInputPos cfg.inputPos out.inputMove + workTapes i := match (out.workActions i).1 with + | none => cfg.workTapes i + | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s + workTapePos i := cfg.workTapePos i + (out.workActions i).2 + output := cfg.output ++ out.outS.toList + +/-- A work tape head moves by at most one cell when an action is applied. -/ +lemma workTapePos_apply_le (out : Action k Symbol State) + (cfg : Cfg k Symbol State input) (i : Fin k) : + |(out.apply cfg).workTapePos i - cfg.workTapePos i| ≤ 1 := by + simp only [Action.apply, add_sub_cancel_left, abs_le, SignType.cast] + grind + +/-- The work tape cells visited by the head of tape `i` along a list of configurations. -/ +def visitedOfCfgs (cfgs : List (Cfg k Symbol State input)) (i : Fin k) : Finset ℤ := + (cfgs.map (·.workTapePos i)).toFinset + +/-- The number of work tape cells touched by the heads along a list of configurations. -/ +def spaceUsedOfCfgs (cfgs : List (Cfg k Symbol State input)) : ℕ := + ∑ i, (visitedOfCfgs cfgs i).card + +end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 3d460e45a..9b8ad3feb 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -6,14 +6,10 @@ Authors: Christian Reitwiessner module -public import Mathlib.Data.Finset.Max -public import Mathlib.Data.Int.Interval -public import Mathlib.Algebra.Order.Group.Abs -public import Mathlib.Algebra.Order.Group.Int public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Computability.Language -public import Mathlib.Data.Sign.Defs public import Cslib.Foundations.Data.RelatesInSteps +public import Cslib.Computability.Machines.Turing.MultiTape.Configuration /-! # Deterministic Multi-Tape Turing Machines @@ -67,8 +63,6 @@ the sub-linear space modifications from chapter 2.5 with the following changes: We define a number of structures and concepts related to multi-tape Turing machine computation: * `MultiTapeTM`: the TM itself -* `Cfg`: the configuration of a TM: the internal state, the work tape contents and head positions, - and the output tape * `spaceUsed`: the number of work tape cells touched by the heads until a certain step * `TransitionRelation`: the transition relation from one configuration to the next * `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure @@ -102,17 +96,6 @@ namespace Turing variable {k : ℕ} {State Symbol : Type*} -/-- The output of the transition function. -/ -structure TransitionOut (k : ℕ) (Symbol State : Type*) where - /-- The movement (attempt) of the input head. -/ - inputMove : SignType - /-- Actions on the work tapes: optionally a symbol to write and the head movement. -/ - workActions : Fin k → (Option (Option Symbol)) × SignType - /-- An optional symbol to output. -/ - outS : Option Symbol - /-- The successor state or none to halt. -/ - q' : Option State - /-- A multi-tape Turing machine with `k` work tapes over the alphabet of `Option Symbol` (where `none` is the blank tape symbol). Note that it is not required that `Symbol` or `State` are finite @@ -126,7 +109,7 @@ structure MultiTapeTM (k : ℕ) (Symbol State : Type*) where symbols to a movement for the input head, actions on the work tape, optionally a symbol to output and the successor state -/ tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : - TransitionOut k Symbol State + Action k Symbol State namespace MultiTapeTM @@ -135,115 +118,19 @@ variable {tm : MultiTapeTM k Symbol State} section Cfg /-! -## Configurations of a Turing Machine - -This section defines the configurations of a Turing machine, -the step function that lets the machine transition from one configuration to the next, -the resulting sequence of configurations and the initial configuration. --/ +## Stepping a Turing Machine -/-- -The configurations of a Turing machine is relative to the input of the machine and consist of: -- an `Option`al state (or none for the halting state), -- the position of the input head (shifted by one), -- the contents of the work tape, -- the positions of the work tape heads, -- the contents of the write-only output tape +This section defines the step function that lets the machine transition from one configuration to +the next, and the configuration reached after a number of steps. Configurations themselves are +defined in `Cslib.Computability.Machines.Turing.MultiTape.Configuration`. -/ -@[ext] -structure Cfg (k : ℕ) (Symbol State : Type*) (input : List Symbol) where - /-- the state of the TM (or none for the halting state) -/ - state : Option State - /-- the position of the input head, shifted by one -/ - inputPos : Fin (input.length + 2) - /-- the work tapes -/ - workTapes : Fin k → ℤ → Option Symbol - /-- the positions of the heads on the work tapes -/ - workTapePos : Fin k → ℤ - /-- the contents of the write-only output tape -/ - output : List Symbol -deriving Inhabited - -/-- Attempt to move the input tape head. -The machine can only read one empty cell outside of the input, -any attempted movement beyond that results in no movement. - -The addition is performed in `ℤ` before clamping. Performing it in `Fin (n + 2)` would wrap an -outward boundary move to the opposite end of the input. -/ -@[scoped grind =] -def moveInputPos {n : ℕ} (pos : Fin (n + 2)) (m : SignType) : Fin (n + 2) := - let p := ((pos.val : ℤ) + (m.cast : ℤ)).toNat - if h : p < n + 2 then ⟨p, h⟩ else ⟨n + 1, by omega⟩ - -@[simp] -lemma moveInputPos_zero {n : ℕ} (pos : Fin (n + 2)) : - moveInputPos pos 0 = pos := by - apply Fin.ext - simp [moveInputPos, pos.isLt] - -@[simp] -lemma moveInputPos_leftBoundary {n : ℕ} : - moveInputPos (0 : Fin (n + 2)) (-1) = 0 := by - apply Fin.ext - simp [moveInputPos] - -@[simp] -lemma moveInputPos_rightBoundary {n : ℕ} : - moveInputPos (⟨n + 1, by omega⟩ : Fin (n + 2)) 1 = ⟨n + 1, by omega⟩ := by - unfold moveInputPos - rw [dite_eq_right (by simp; omega)] - -/-- A left move away from the left input boundary decrements the native input position. -/ -lemma moveInputPos_neg_of_ne_left {n : ℕ} (p : Fin (n + 2)) (h : p ≠ 0) : - moveInputPos p .neg = ⟨p.val - 1, by have := p.isLt; omega⟩ := by - have hp : 0 < p.val := Nat.pos_of_ne_zero (fun hz => h (Fin.ext hz)) - unfold moveInputPos - apply Fin.ext - rw [dite_eq_left] <;> simp <;> omega - -/-- A right move away from the right input boundary increments the native input position. -/ -lemma moveInputPos_pos_of_ne_right {n : ℕ} (p : Fin (n + 2)) (h : p.val ≠ n + 1) : - moveInputPos p .pos = ⟨p.val + 1, by have := p.isLt; omega⟩ := by - unfold moveInputPos - rw [dite_eq_left] - · apply Fin.ext - simp - · simp - omega - -/-- The symbol currently under the input tape head. -/ -def Cfg.inputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := - if h₁ : cfg.inputPos = 0 then none - else if h₂ : cfg.inputPos = input.length + 1 then none - else input[cfg.inputPos.val - 1]'(by grind) - -@[simp] -lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ) - (h₁ : cfg.inputPos.val = 1 + p) - (h₂ : p < input.length) : - cfg.inputSymbol = some input[p] := by - grind [Cfg.inputSymbol] - -/-- The symbol read by work tape `i`. -/ -def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol := - cfg.workTapes i (cfg.workTapePos i) /-- The step function corresponding to a `MultiTapeTM`. -/ def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input := match cfg.state with -- in the halting state, we stay at the configuration | none => cfg - | some q => - let {inputMove, workActions, q', outS, ..} := tm.tr q cfg.inputSymbol cfg.workTapeSymbols - { - state := q', - inputPos := moveInputPos cfg.inputPos inputMove, - workTapes i := match (workActions i).1 with - | none => cfg.workTapes i - | some s => Function.update (cfg.workTapes i) (cfg.workTapePos i) s - workTapePos i := (cfg.workTapePos i) + (workActions i).2 - output := cfg.output ++ outS.toList - } + | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg /-- The symbol (optionally) output when executing one step starting from configuration `cfg`. -/ def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := @@ -253,8 +140,7 @@ def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := /-- The initial configuration corresponding to an input string. -/ @[simp] -def initCfg (input : List Symbol) : Cfg k Symbol State input := - ⟨some tm.q₀, 1, fun _ _ => none, fun _ => 0, []⟩ +def initCfg (input : List Symbol) : Cfg k Symbol State input := Cfg.init tm.q₀ input @[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : @@ -305,9 +191,7 @@ lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : unfold step cases hstate : c.state with | none => simp - | some q => - simp only [add_sub_cancel_left, abs_le, SignType.cast] - grind + | some q => exact workTapePos_apply_le _ c i end Cfg @@ -345,6 +229,14 @@ lemma spaceUsedByTape_le_spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) (i tm.spaceUsedByTape cfg t i ≤ tm.spaceUsed cfg t := Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i) +/-- The space used up to step `t` is the space touched by the configurations up to step `t`. -/ +lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : + tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := by + unfold spaceUsed spaceUsedByTape spaceUsedOfCfgs + refine Finset.sum_congr rfl fun i _ => congrArg Finset.card ?_ + ext z + simp [visitedByTapeHead, visitedOfCfgs] + end Space open Cfg @@ -361,7 +253,7 @@ def TransitionRelation (c₁ c₂ : Cfg k Symbol State input) : Prop := tm.step @[simp] lemma step_output (cfg : Cfg k Symbol State input) : (tm.step cfg).output = cfg.output ++ (tm.outputSymbol cfg).toList := by - unfold step outputSymbol + unfold step outputSymbol Action.apply cases cfg.state <;> simp /-- The output does not change after the machine has halted. -/ diff --git a/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean new file mode 100644 index 000000000..b27780794 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean @@ -0,0 +1,107 @@ +/- +Copyright (c) 2026 Aviv Bar Natan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aviv Bar Natan +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic + +/-! +# Deterministic Multi-Tape Turing Machines are Nondeterministic + +Embeds `MultiTapeTM` into `MultiTapeNTM` and shows the embedding preserves computation. + +`toNTM` permits exactly the transition `tr` prescribes: nondeterminism is the possibility of +several, so having exactly one is the special case. A deterministic computation is then witnessed +by the machine's own run. Both models idle once the machine has halted, so that run has exactly +`t` steps for every `t` and its measures match `runFrom` and `spaceUsed` directly, with no +reasoning about the step at which the machine halted. + +## Important Declarations + +* `MultiTapeTM.toNTM`: every deterministic machine is a nondeterministic one +* `MultiTapeTM.toNTMComputationPath`: the machine's own run, as a computation of `toNTM` +* `MultiTapeTM.toNTM_computes`: every deterministic computation is a nondeterministic one +-/ + +@[expose] public section + +namespace Turing + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + +/-- Every deterministic machine is a nondeterministic one whose relation is a singleton. -/ +def MultiTapeTM.toNTM (tm : MultiTapeTM k Symbol State) : MultiTapeNTM k Symbol State where + q₀ := tm.q₀ + Tr q input work out := out = tm.tr q input work + +namespace MultiTapeTM + +variable {tm : MultiTapeTM k Symbol State} {t : ℕ} + +@[simp] +lemma toNTM_initCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) : + tm.toNTM.initCfg input = tm.initCfg input := rfl + +/-- Each step of `tm` is a step of its nondeterministic reading. This holds at a halted +configuration too, where both models idle. -/ +theorem toNTM_step (c : Cfg k Symbol State input) : tm.toNTM.Step c (tm.step c) := by + cases hq : c.state <;> simp [MultiTapeNTM.Step, step, toNTM, hq] + +/-- The configurations the machine passes through form a chain of steps. -/ +lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : + ((List.range (t + 1)).map (tm.runFrom cfg)).IsChain tm.toNTM.Step := by + rw [List.isChain_iff_getElem] + intro i hi + simp only [List.getElem_map, List.getElem_range] + rw [runFrom_succ_eq_step'] + exact toNTM_step _ + +/-- The machine's own run for `t` steps, as a computation of its nondeterministic reading: the +configuration reached after each step. -/ +def toNTMComputationPath (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : + tm.toNTM.ComputationPath input where + cfgs := (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) + last := tm.runFrom (tm.initCfg input) t + isChainFromTo := + { isChain := isChain_map_range _ t + ne_nil := by simp + head_eq := by + rw [List.head_map] + simp [toNTM] + getLast_eq := by + rw [← Option.some_inj, ← List.getLast?_eq_some_getLast, List.range_succ, List.map_append] + simp } + +@[simp] +lemma toNTMComputationPath_time : (tm.toNTMComputationPath input t).time = t := by + simp [MultiTapeNTM.ComputationPath.time, toNTMComputationPath] + +@[simp] +lemma toNTMComputationPath_cfgs : + (tm.toNTMComputationPath input t).cfgs + = (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) := rfl + +@[simp] +lemma toNTMComputationPath_last : + (tm.toNTMComputationPath input t).last = tm.runFrom (tm.initCfg input) t := rfl + +@[simp] +lemma toNTMComputationPath_space : + (tm.toNTMComputationPath input t).space = tm.spaceUsed (tm.initCfg input) t := by + simp [MultiTapeNTM.ComputationPath.space, spaceUsed_eq_spaceUsedOfCfgs] + +/-- Every deterministic computation is a nondeterministic one, witnessed by the machine's own +run. -/ +theorem toNTM_computes {output : List Symbol} {t s : ℕ} + (h : tm.ComputesInTimeAndSpace input output t s) : + tm.toNTM.ComputesInExactTimeAndSpace input output t s := + ⟨tm.toNTMComputationPath input t, by simpa using h.1, by simpa using h.2.1, + toNTMComputationPath_time, toNTMComputationPath_space.trans h.2.2⟩ + +end MultiTapeTM + +end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean new file mode 100644 index 000000000..c0b859135 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -0,0 +1,144 @@ +/- +Copyright (c) 2026 Aviv Bar Natan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aviv Bar Natan +-/ + +module + +public import Mathlib.Data.List.Chain +public import Cslib.Foundations.Data.List.IsChainFromTo +public import Cslib.Computability.Machines.Turing.MultiTape.Configuration + +/-! +# Nondeterministic Multi-Tape Turing Machines + +Defines nondeterministic Turing machines with a read-only input tape, `k` work tapes and one +write-only output tape, and what it means for one to compute an output within a time and space +bound. + +## Design + +Following [Papadimitriou94], chapter 2.7, a nondeterministic machine is a Turing machine whose +transition function is replaced by a transition relation: `Tr q input work action` holds when +`action` is one of the actions permitted in that situation. + +A halted configuration steps to itself, so once a machine has halted it has a run of every length. +A time bound is therefore an upper bound, with no separate account of the step at which it halted. + +The transition relation may be empty at a running configuration, so a machine can get stuck. Every +notion below asks for a computation ending in a halted configuration, so a stuck one is not a +witness. + +## Important Declarations + +* `MultiTapeNTM`: the machine, an initial state and a transition relation +* `Step`: the one-step relation on configurations +* `ComputationPath`: a run of the machine: a series of configurations from the initial one, each + reached from the previous by a step +* `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint +* `Computes`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`: + its instances, whose + bounds all refer to a single computation + +## References + +* [C. Papadimitriou, *Computational Complexity*][Papadimitriou94] +* [M. Sipser, *Introduction to the Theory of Computation*][Sipser2013] +-/ + +@[expose] public section + +namespace Turing + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + +/-- +A nondeterministic multi-tape Turing machine with `k` work tapes over the alphabet of +`Option Symbol` (where `none` is the blank symbol). Neither `Symbol` nor `State` is required to be +finite. +-/ +structure MultiTapeNTM (k : ℕ) (Symbol State : Type*) where + /-- initial state -/ + q₀ : State + /-- transition relation: which combinations of state, current input symbol, tuple of work head + symbols and resulting actions are valid transitions -/ + Tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) + (action : Action k Symbol State) : Prop + +namespace MultiTapeNTM + +variable {ntm : MultiTapeNTM k Symbol State} + +/-- The one-step relation on configurations. A halted configuration steps to itself; a running one +steps by any permitted transition. -/ +@[scoped grind =] +def Step (ntm : MultiTapeNTM k Symbol State) (c₁ c₂ : Cfg k Symbol State input) : Prop := + match c₁.state with + | none => c₂ = c₁ + | some q => + ∃ action, ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols action ∧ c₂ = action.apply c₁ + +/-- A halted configuration steps only to itself. -/ +lemma step_of_halt {c c' : Cfg k Symbol State input} (h : c.Halted) : + ntm.Step c c' ↔ c' = c := by + simp [Step, h] + +/-- The initial configuration corresponding to an input string. -/ +@[simp] +def initCfg (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : + Cfg k Symbol State input := + Cfg.init ntm.q₀ input + +/-- A computation path of `ntm` on `input`: the configurations it passes through, forming a chain +of steps from the initial configuration to the one it ends at. -/ +structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) where + /-- the configurations passed through, starting with the initial one -/ + cfgs : List (Cfg k Symbol State input) + /-- the configuration the path ends at -/ + last : Cfg k Symbol State input + /-- consecutive configurations are joined by a step, from the initial configuration to `last` -/ + isChainFromTo : cfgs.IsChainFromTo ntm.Step (ntm.initCfg input) last + +namespace ComputationPath + +variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} + +/-- The number of steps taken, the time the computation takes. -/ +def time (p : ntm.ComputationPath input) : ℕ := p.cfgs.length - 1 + +/-- The number of work tape cells touched. -/ +def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.cfgs + +end ComputationPath + +/-- `ntm` has a computation on `input` that starts at the initial configuration, halts, emits +`output` and satisfies `P`. The notions below are its instances, so their constraints all refer to +a single computation. -/ +def ComputesSuchThat (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) + (P : ntm.ComputationPath input → Prop) : Prop := + ∃ p : ntm.ComputationPath input, p.last.Halted ∧ p.last.output = output ∧ P p + +/-- `ntm` computes `output` from `input`, with no bound on resources. -/ +def Computes (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) : Prop := + ntm.ComputesSuchThat input output fun _ => True + +/-- `ntm` computes `output` from `input` in exactly `t` steps. -/ +def ComputesInExactTime (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t : ℕ) : + Prop := + ntm.ComputesSuchThat input output fun p => p.time = t + +/-- `ntm` computes `output` from `input` touching exactly `s` work tape cells. -/ +def ComputesInExactSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (s : ℕ) : + Prop := + ntm.ComputesSuchThat input output fun p => p.space = s + +/-- `ntm` computes `output` from `input` in `t` steps and `s` work tape cells, by a single +computation. Nondeterministic analogue of `MultiTapeTM.ComputesInTimeAndSpace`. -/ +def ComputesInExactTimeAndSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) + (t s : ℕ) : Prop := + ntm.ComputesSuchThat input output fun p => p.time = t ∧ p.space = s + +end MultiTapeNTM + +end Turing From f4d0c2044eca5d25d391104790c58b224d5729c8 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 12:59:36 +0300 Subject: [PATCH 02/18] refactor(MultiTapeTM): make the deterministic machine extend the nondeterministic one `MultiTapeTM` now extends `MultiTapeNTM` with a transition function and the requirement that the permitted transitions are exactly the ones it prescribes. A deterministic machine is therefore literally a nondeterministic one rather than something translated into one, and `DeterministicToNondeterministic.lean` is removed. Everything stated of the general machine now applies unchanged: `initCfg` and `ComputesInTimeAndSpace` are no longer defined here, and `Step`, `ComputationPath`, `Computes`, `ComputesInExactTime`, `ComputesInExactSpace` and `ComputesInExactTimeAndSpace` are available on a `MultiTapeTM` directly. What is left is what follows from there being no choice to make. `step_iff` identifies the inherited `Step` with the graph of `step`; from it a computation path can only follow `runFrom`, which is one induction on the path index rather than one per measure, since the output tape lives in the configuration and a path carries no labels. `runPath` supplies a path of every length, and together they give `computesInExactTimeAndSpace_iff_runFrom`, an equivalence where `toNTM_computes` was a one-way implication. `ofTr` builds a machine from an initial state and a transition function and keeps it computable: relation to function needs choice, so `tr` stays data and `Tr_iff` records that the two agree. Co-Authored-By: Claude Opus 5 (1M context) --- Cslib.lean | 1 - .../Turing/MultiTape/Deterministic.lean | 148 +++++++++++++++--- .../DeterministicToNondeterministic.lean | 107 ------------- .../Turing/MultiTape/Nondeterministic.lean | 2 +- 4 files changed, 125 insertions(+), 133 deletions(-) delete mode 100644 Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean diff --git a/Cslib.lean b/Cslib.lean index 23061d3ac..9b3595870 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -48,7 +48,6 @@ public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Languages.SafetyLiveness public import Cslib.Computability.Machines.Turing.MultiTape.Configuration public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic -public import Cslib.Computability.Machines.Turing.MultiTape.DeterministicToNondeterministic public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 9b8ad3feb..c1e3d4ce1 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -9,7 +9,7 @@ module public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Computability.Language public import Cslib.Foundations.Data.RelatesInSteps -public import Cslib.Computability.Machines.Turing.MultiTape.Configuration +public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic /-! # Deterministic Multi-Tape Turing Machines @@ -58,16 +58,23 @@ the sub-linear space modifications from chapter 2.5 with the following changes: and not by a restriction on the transition function. The two definitions are equivalent, but not restricting the transition function makes it easier to define a universal machine. +`MultiTapeTM` extends `MultiTapeNTM` with a transition function and the requirement that the +permitted transitions are exactly the ones it prescribes. `Step`, `ComputationPath` and the +`Computes` notions of the nondeterministic machine therefore apply unchanged, and what this file +adds is what follows from there being no choice to make. + ## Important Declarations We define a number of structures and concepts related to multi-tape Turing machine computation: -* `MultiTapeTM`: the TM itself -* `spaceUsed`: the number of work tape cells touched by the heads until a certain step -* `TransitionRelation`: the transition relation from one configuration to the next +* `MultiTapeTM`: the TM itself, a `MultiTapeNTM` whose transition relation is a function +* `ofTr`: the machine with a given initial state and transition function * `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure -* `ComputesInTimeAndSpace`: a proof that a specific TM computes an output from an input in a certain - number of steps and using a certain number of tape cells +* `TransitionRelation`: the transition relation from one configuration to the next +* `step_iff`: the inherited `Step` is the graph of `step` +* `runPath`: the machine's own run, as a computation path +* `computesInExactTimeAndSpace_iff_runFrom`: the inherited `ComputesInExactTimeAndSpace`, stated + by step index rather than by computation path * `ComputableInTimeAndSpace`: a proof that there is a multi-tape TM that computes a function (on strings) respecting a time and space bound in the input length. * `DecidableInTimeAndSpace`: a proof that a TM decides a language within a certain time @@ -102,14 +109,25 @@ is the blank tape symbol). Note that it is not required that `Symbol` or `State` to keep the definition more general. The restriction will be introduced once we start talking about computability by Turing machines in general. -/ -structure MultiTapeTM (k : ℕ) (Symbol State : Type*) where - /-- initial state -/ - q₀ : State +structure MultiTapeTM (k : ℕ) (Symbol State : Type*) + extends MultiTapeNTM k Symbol State where /-- transition function, mapping a state, the current input symbol and a tuple of work head symbols to a movement for the input head, actions on the work tape, optionally a symbol to output and the successor state -/ tr (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) : Action k Symbol State + /-- the permitted transitions are exactly the one `tr` prescribes -/ + Tr_iff (q : State) (i : Option Symbol) (w : Fin k → Option Symbol) + (action : Action k Symbol State) : Tr q i w action ↔ action = tr q i w + +/-- The deterministic machine with initial state `q₀` and transition function `tr`. -/ +def MultiTapeTM.ofTr (q₀ : State) + (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) : + MultiTapeTM k Symbol State where + q₀ := q₀ + Tr q i w action := action = tr q i w + tr := tr + Tr_iff _ _ _ _ := Iff.rfl namespace MultiTapeTM @@ -138,10 +156,6 @@ def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := | none => none | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).outS -/-- The initial configuration corresponding to an input string. -/ -@[simp] -def initCfg (input : List Symbol) : Cfg k Symbol State input := Cfg.init tm.q₀ input - @[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : tm.step cfg = cfg := by @@ -265,16 +279,102 @@ lemma runFrom_output_eq_of_halt conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] rw [runFrom_add, runFrom_of_halt _ hhalt] -/-- A proof that the Turing machine `tm` on input `input` outputs `output` in at most `t` steps -and uses exactly `s` space. -Note that this does not require the alphabet or state set to be finite. -/ -def ComputesInTimeAndSpace - (tm : MultiTapeTM k Symbol State) - (input output : List Symbol) - (t s : ℕ) : Prop := - (tm.runFrom (tm.initCfg input) t).state = none ∧ - (tm.runFrom (tm.initCfg input) t).output = output ∧ - tm.spaceUsed (tm.initCfg input) t = s +/-! ## Determinism + +`MultiTapeTM` extends `MultiTapeNTM`, so `Step`, `ComputationPath` and the `Computes` notions +already apply to it; only the facts below are specific to having a transition function. They say +that there is no choice to make: `Step` is the graph of `step`, so a computation path can only +follow `runFrom`, and `runPath` shows there is one of every length. +-/ + +/-- `Step` is the relation `step` induces: from each configuration there is exactly one step. -/ +@[simp] +theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := by + cases hq : c.state <;> simp [MultiTapeNTM.Step, step, tm.Tr_iff, hq] + +/-- The configurations the machine passes through form a chain of steps. -/ +lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : + ((List.range (t + 1)).map (tm.runFrom cfg)).IsChain tm.Step := by + rw [List.isChain_iff_getElem] + intro i hi + simp only [List.getElem_map, List.getElem_range] + rw [runFrom_succ_eq_step'] + exact step_iff.mpr rfl + +/-- The machine's own run for `t` steps, as a computation path. -/ +def runPath (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : + tm.ComputationPath input where + cfgs := (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) + last := tm.runFrom (tm.initCfg input) t + isChainFromTo := + { isChain := isChain_map_range _ t + ne_nil := by simp + head_eq := by rw [List.head_map]; simp + getLast_eq := by + rw [← Option.some_inj, ← List.getLast?_eq_some_getLast, List.range_succ, List.map_append] + simp } + +@[simp] +lemma runPath_time (input : List Symbol) (t : ℕ) : (tm.runPath input t).time = t := by + simp [MultiTapeNTM.ComputationPath.time, runPath] + +@[simp] +lemma runPath_last (input : List Symbol) (t : ℕ) : + (tm.runPath input t).last = tm.runFrom (tm.initCfg input) t := rfl + +@[simp] +lemma runPath_space (input : List Symbol) (t : ℕ) : + (tm.runPath input t).space = tm.spaceUsed (tm.initCfg input) t := by + simp [MultiTapeNTM.ComputationPath.space, runPath, spaceUsed_eq_spaceUsedOfCfgs] + +/-- A computation path of `tm` has no choice but to follow `runFrom`. -/ +lemma path_getElem {p : tm.ComputationPath input} (i : ℕ) (h : i < p.cfgs.length) : + p.cfgs[i] = tm.runFrom (tm.initCfg input) i := by + induction i with + | zero => simpa using p.isChainFromTo.getElem_zero + | succ n ih => + have hstep := List.isChain_iff_getElem.mp p.isChainFromTo.isChain n h + rw [step_iff.mp hstep, ih (by omega), ← runFrom_succ_eq_step'] + +/-- A path visiting `t + 1` configurations takes `t` steps. -/ +lemma path_length {p : tm.ComputationPath input} : p.cfgs.length = p.time + 1 := by + have := p.isChainFromTo.length_pos + simp only [MultiTapeNTM.ComputationPath.time] + omega + +lemma path_cfgs {p : tm.ComputationPath input} : + p.cfgs = (List.range (p.time + 1)).map (tm.runFrom (tm.initCfg input)) := by + refine List.ext_getElem (by simp [path_length]) fun i h₁ h₂ => ?_ + simpa using path_getElem i h₁ + +/-- It ends where `tm` is after that many steps. -/ +lemma path_last {p : tm.ComputationPath input} : + p.last = tm.runFrom (tm.initCfg input) p.time := by + have h := p.isChainFromTo.getElem_length_sub_one + rw [path_getElem _ (by have := p.isChainFromTo.length_pos; omega)] at h + exact h.symm + +/-- Its space is the space `tm` uses over the same number of steps. -/ +lemma path_space {p : tm.ComputationPath input} : + p.space = tm.spaceUsed (tm.initCfg input) p.time := by + rw [MultiTapeNTM.ComputationPath.space, path_cfgs, ← spaceUsed_eq_spaceUsedOfCfgs] + +/-- `tm` has exactly one computation path of each length, so `ComputesInExactTimeAndSpace`, +inherited from `MultiTapeNTM`, is the direct statement about `runFrom` and `spaceUsed` at step +`t`. -/ +theorem computesInExactTimeAndSpace_iff_runFrom {input output : List Symbol} {t s : ℕ} : + tm.ComputesInExactTimeAndSpace input output t s ↔ + (tm.runFrom (tm.initCfg input) t).state = none ∧ + (tm.runFrom (tm.initCfg input) t).output = output ∧ + tm.spaceUsed (tm.initCfg input) t = s := by + constructor + · rintro ⟨p, hhalt, hout, rfl, hspace⟩ + rw [path_last] at hhalt hout + rw [path_space] at hspace + exact ⟨hhalt, hout, hspace⟩ + · rintro ⟨hhalt, hout, hspace⟩ + exact ⟨tm.runPath input t, by simpa using hhalt, by simpa using hout, by simp, + by simpa using hspace⟩ /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of length `n` it uses at most `t n` steps and `s n` space. It assumes an embedding function @@ -287,7 +387,7 @@ def ComputesFunInTimeAndSpace (toMachineSymbol : IOSymbol ↪ Symbol) (t s : ℕ → ℕ) : Prop := ∀ input, ∃ t' ≤ t input.length, ∃ s' ≤ s input.length, - ComputesInTimeAndSpace tm (input.map toMachineSymbol) ((f input).map toMachineSymbol) t' s' + tm.ComputesInExactTimeAndSpace (input.map toMachineSymbol) ((f input).map toMachineSymbol) t' s' /-- The main definition of complexity of multi-tape Turing machines: A proof that the function `f` is computable by some multi-tape Turing machine `tm` (with finite diff --git a/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean deleted file mode 100644 index b27780794..000000000 --- a/Cslib/Computability/Machines/Turing/MultiTape/DeterministicToNondeterministic.lean +++ /dev/null @@ -1,107 +0,0 @@ -/- -Copyright (c) 2026 Aviv Bar Natan. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Aviv Bar Natan --/ - -module - -public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic -public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic - -/-! -# Deterministic Multi-Tape Turing Machines are Nondeterministic - -Embeds `MultiTapeTM` into `MultiTapeNTM` and shows the embedding preserves computation. - -`toNTM` permits exactly the transition `tr` prescribes: nondeterminism is the possibility of -several, so having exactly one is the special case. A deterministic computation is then witnessed -by the machine's own run. Both models idle once the machine has halted, so that run has exactly -`t` steps for every `t` and its measures match `runFrom` and `spaceUsed` directly, with no -reasoning about the step at which the machine halted. - -## Important Declarations - -* `MultiTapeTM.toNTM`: every deterministic machine is a nondeterministic one -* `MultiTapeTM.toNTMComputationPath`: the machine's own run, as a computation of `toNTM` -* `MultiTapeTM.toNTM_computes`: every deterministic computation is a nondeterministic one --/ - -@[expose] public section - -namespace Turing - -variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} - -/-- Every deterministic machine is a nondeterministic one whose relation is a singleton. -/ -def MultiTapeTM.toNTM (tm : MultiTapeTM k Symbol State) : MultiTapeNTM k Symbol State where - q₀ := tm.q₀ - Tr q input work out := out = tm.tr q input work - -namespace MultiTapeTM - -variable {tm : MultiTapeTM k Symbol State} {t : ℕ} - -@[simp] -lemma toNTM_initCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) : - tm.toNTM.initCfg input = tm.initCfg input := rfl - -/-- Each step of `tm` is a step of its nondeterministic reading. This holds at a halted -configuration too, where both models idle. -/ -theorem toNTM_step (c : Cfg k Symbol State input) : tm.toNTM.Step c (tm.step c) := by - cases hq : c.state <;> simp [MultiTapeNTM.Step, step, toNTM, hq] - -/-- The configurations the machine passes through form a chain of steps. -/ -lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : - ((List.range (t + 1)).map (tm.runFrom cfg)).IsChain tm.toNTM.Step := by - rw [List.isChain_iff_getElem] - intro i hi - simp only [List.getElem_map, List.getElem_range] - rw [runFrom_succ_eq_step'] - exact toNTM_step _ - -/-- The machine's own run for `t` steps, as a computation of its nondeterministic reading: the -configuration reached after each step. -/ -def toNTMComputationPath (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : - tm.toNTM.ComputationPath input where - cfgs := (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) - last := tm.runFrom (tm.initCfg input) t - isChainFromTo := - { isChain := isChain_map_range _ t - ne_nil := by simp - head_eq := by - rw [List.head_map] - simp [toNTM] - getLast_eq := by - rw [← Option.some_inj, ← List.getLast?_eq_some_getLast, List.range_succ, List.map_append] - simp } - -@[simp] -lemma toNTMComputationPath_time : (tm.toNTMComputationPath input t).time = t := by - simp [MultiTapeNTM.ComputationPath.time, toNTMComputationPath] - -@[simp] -lemma toNTMComputationPath_cfgs : - (tm.toNTMComputationPath input t).cfgs - = (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) := rfl - -@[simp] -lemma toNTMComputationPath_last : - (tm.toNTMComputationPath input t).last = tm.runFrom (tm.initCfg input) t := rfl - -@[simp] -lemma toNTMComputationPath_space : - (tm.toNTMComputationPath input t).space = tm.spaceUsed (tm.initCfg input) t := by - simp [MultiTapeNTM.ComputationPath.space, spaceUsed_eq_spaceUsedOfCfgs] - -/-- Every deterministic computation is a nondeterministic one, witnessed by the machine's own -run. -/ -theorem toNTM_computes {output : List Symbol} {t s : ℕ} - (h : tm.ComputesInTimeAndSpace input output t s) : - tm.toNTM.ComputesInExactTimeAndSpace input output t s := - ⟨tm.toNTMComputationPath input t, by simpa using h.1, by simpa using h.2.1, - toNTMComputationPath_time, toNTMComputationPath_space.trans h.2.2⟩ - -end MultiTapeTM - -end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index c0b859135..43dd000a2 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -134,7 +134,7 @@ def ComputesInExactSpace (ntm : MultiTapeNTM k Symbol State) (input output : Lis ntm.ComputesSuchThat input output fun p => p.space = s /-- `ntm` computes `output` from `input` in `t` steps and `s` work tape cells, by a single -computation. Nondeterministic analogue of `MultiTapeTM.ComputesInTimeAndSpace`. -/ +computation. -/ def ComputesInExactTimeAndSpace (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) (t s : ℕ) : Prop := ntm.ComputesSuchThat input output fun p => p.time = t ∧ p.space = s From f2ac789d255c9424bd57a704d4b537011f04432a Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 14:05:55 +0300 Subject: [PATCH 03/18] refactor(MultiTapeTM): normalise the transition relation away to the function `Tr` is stored but fully determined by `tr`, so making `Tr_iff` a simp lemma lets it normalise away wherever it appears. `step_iff` no longer names it, and `Tr` is now absent from the deterministic file outside the structure itself. Co-Authored-By: Claude Opus 5 (1M context) --- .../Machines/Turing/MultiTape/Deterministic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index c1e3d4ce1..f5ae7ec57 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -120,6 +120,8 @@ structure MultiTapeTM (k : ℕ) (Symbol State : Type*) Tr_iff (q : State) (i : Option Symbol) (w : Fin k → Option Symbol) (action : Action k Symbol State) : Tr q i w action ↔ action = tr q i w +attribute [simp] MultiTapeTM.Tr_iff + /-- The deterministic machine with initial state `q₀` and transition function `tr`. -/ def MultiTapeTM.ofTr (q₀ : State) (tr : State → Option Symbol → (Fin k → Option Symbol) → Action k Symbol State) : @@ -290,7 +292,7 @@ follow `runFrom`, and `runPath` shows there is one of every length. /-- `Step` is the relation `step` induces: from each configuration there is exactly one step. -/ @[simp] theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := by - cases hq : c.state <;> simp [MultiTapeNTM.Step, step, tm.Tr_iff, hq] + cases hq : c.state <;> simp [MultiTapeNTM.Step, step, hq] /-- The configurations the machine passes through form a chain of steps. -/ lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : From 454156d13d690077787fee29b030d6cfce1e3309 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 15:04:25 +0300 Subject: [PATCH 04/18] refactor(MultiTapeTM): keep only deterministic-specific results, generalise the rest Now that a deterministic machine is a nondeterministic one, most of what `Deterministic.lean` carried is either unused or true of any machine. Removed as unreachable: `runFrom_add`, `runFrom_output_eq_of_halt`, `spaceUsedByTape_le_spaceUsed`, `spaceUsed_zero_tapes_eq_zero`, `outputSymbol_of_halt`, `step_output`, `haltsAtStep`, `halting_step_unique` and `not_halts_of_repeat_nonhalt`. Nothing in the library referred to them. `TransitionRelation` was the graph of `step`, which is what the inherited `Step` already is, so it is dropped and `relatesInSteps_iff_runFrom_eq` is stated over `Step`. The space bounds turn out to mention no machine at all: their proofs are cardinality arguments about a list of configurations. `spaceUsedOfCfgs_le` and `spaceUsedOfCfgs_mono` move to `Configuration.lean`, which gives `ComputationPath.space_le` for nondeterministic machines, a bound the library did not have, and leaves `spaceUsed_linear` a corollary rather than its own proof. `visitedByTapeHead` becomes `visitedOfCfgs` at a step index, so there is now one notion of which cells a computation touches, and `spaceUsed_eq_spaceUsedOfCfgs` holds by `rfl`. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Configuration.lean | 19 ++- .../Turing/MultiTape/Deterministic.lean | 128 ++---------------- .../Turing/MultiTape/Nondeterministic.lean | 12 ++ .../Machines/Turing/MultiTape/TapeLemmas.lean | 20 ++- 4 files changed, 48 insertions(+), 131 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean index 27ea589ae..d7a835e03 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -39,7 +39,8 @@ the configuration the run ends in. * `Action`: what a machine does in one step * `Action.apply`: the effect of one action on a configuration * `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in -* `spaceUsedOfCfgs`: work tape cells touched along a list of configurations +* `spaceUsedOfCfgs`: work tape cells touched along a list of configurations, with the bounds + `spaceUsedOfCfgs_le` and `spaceUsedOfCfgs_mono` -/ @[expose] public section @@ -184,4 +185,20 @@ def visitedOfCfgs (cfgs : List (Cfg k Symbol State input)) (i : Fin k) : Finset def spaceUsedOfCfgs (cfgs : List (Cfg k Symbol State input)) : ℕ := ∑ i, (visitedOfCfgs cfgs i).card +/-- Each configuration contributes at most one cell per tape, so space is bounded by length. -/ +theorem spaceUsedOfCfgs_le (cfgs : List (Cfg k Symbol State input)) : + spaceUsedOfCfgs cfgs ≤ k * cfgs.length := by + calc spaceUsedOfCfgs cfgs + ≤ ∑ _i : Fin k, cfgs.length := + Finset.sum_le_sum fun i _ => (List.toFinset_card_le _).trans (by simp) + _ = k * cfgs.length := by simp + +/-- Passing through more configurations touches more cells. -/ +theorem spaceUsedOfCfgs_mono {c d : List (Cfg k Symbol State input)} (h : c.Sublist d) : + spaceUsedOfCfgs c ≤ spaceUsedOfCfgs d := + Finset.sum_le_sum fun i _ => Finset.card_le_card <| by + intro z hz + simp only [visitedOfCfgs, List.mem_toFinset] at hz ⊢ + exact (h.map _).subset hz + end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index f5ae7ec57..4ef47b612 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -69,8 +69,8 @@ We define a number of structures and concepts related to multi-tape Turing machi * `MultiTapeTM`: the TM itself, a `MultiTapeNTM` whose transition relation is a function * `ofTr`: the machine with a given initial state and transition function -* `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure -* `TransitionRelation`: the transition relation from one configuration to the next +* `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure; + the shared `spaceUsedOfCfgs` read at a step index * `step_iff`: the inherited `Step` is the graph of `step` * `runPath`: the machine's own run, as a computation path * `computesInExactTimeAndSpace_iff_runFrom`: the inherited `ComputesInExactTimeAndSpace`, stated @@ -84,7 +84,7 @@ There are two ways to talk about the behaviour of a multi-tape Turing machine, a proven to be equivalent. * `MultiTapeTM.runFrom`: the configuration reached after a given number of execution steps -* `RelatesInSteps tm.TransitionRelation cfg cfg' t`: a proof that `tm` transforms the configuration +* `RelatesInSteps tm.Step cfg cfg' t`: a proof that `tm` transforms the configuration `cfg` into `cfg'` in exactly `t` steps ## References @@ -181,14 +181,6 @@ lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by simp [runFrom, Function.iterate_succ_apply'] -/-- Running `a + b` steps equals running `b` steps from the configuration reached after `a`. -/ -lemma runFrom_add (cfg : Cfg k Symbol State input) (a b : ℕ) : - tm.runFrom cfg (a + b) = tm.runFrom (tm.runFrom cfg a) b := by - unfold runFrom - rw [Nat.add_comm, Function.iterate_add_apply] - -/-- Running from a halting configuration stays at that configuration. -/ -@[simp] lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : tm.runFrom cfg n = cfg := by induction n with @@ -196,12 +188,6 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n | succ d ih => rw [runFrom_succ_eq_step', ih, step_of_halt h] -@[simp] -lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) : - tm.outputSymbol cfg = none := by - simp [outputSymbol, h_halt] - -/-- The work-tape head moves by at most one cell in a single step. -/ lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := by unfold step @@ -217,7 +203,7 @@ section Space /-- The set of positions visited by the head of work tape `i` in the computation starting from configuration `cfg` up to step `t`. -/ def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : Finset ℤ := - (Finset.range (t + 1)).image fun t' => (tm.runFrom cfg t').workTapePos i + visitedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) i /-- The number of work tape cells touched by the head of tape `i` in the computation starting from @@ -232,54 +218,14 @@ The number of work tape cells touched by a computation starting from configurati -/ def spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ := ∑ i, tm.spaceUsedByTape cfg t i -/-- A zero-tape Turing machine uses zero space. -/ -@[simp] -lemma spaceUsed_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h_zero : k = 0) : - tm.spaceUsed cfg t = 0 := by - unfold spaceUsed - subst h_zero - simp - -/-- Each tape's space usage is bounded by the total space used. -/ -lemma spaceUsedByTape_le_spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : - tm.spaceUsedByTape cfg t i ≤ tm.spaceUsed cfg t := - Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i) - /-- The space used up to step `t` is the space touched by the configurations up to step `t`. -/ lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := by - unfold spaceUsed spaceUsedByTape spaceUsedOfCfgs - refine Finset.sum_congr rfl fun i _ => congrArg Finset.card ?_ - ext z - simp [visitedByTapeHead, visitedOfCfgs] + tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := rfl end Space open Cfg -/-- -The `TransitionRelation` corresponding to a `MultiTapeTM k Symbol` -is defined by the `step` function, -which maps a configuration to its next configuration. --/ -@[scoped grind =] -def TransitionRelation (c₁ c₂ : Cfg k Symbol State input) : Prop := tm.step c₁ = c₂ - -/-- One step appends the symbol (optionally) emitted by that step to the output tape. -/ -@[simp] -lemma step_output (cfg : Cfg k Symbol State input) : - (tm.step cfg).output = cfg.output ++ (tm.outputSymbol cfg).toList := by - unfold step outputSymbol Action.apply - cases cfg.state <;> simp - -/-- The output does not change after the machine has halted. -/ -lemma runFrom_output_eq_of_halt - (tm : MultiTapeTM k Symbol State) - (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) - (hhalt : (tm.runFrom cfg τ).state = none) : - (tm.runFrom cfg t).output = (tm.runFrom cfg τ).output := by - conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] - rw [runFrom_add, runFrom_of_halt _ hhalt] /-! ## Determinism @@ -423,74 +369,18 @@ lemma relatesInSteps_iff_runFrom_eq (tm : MultiTapeTM k Symbol State) (cfg₁ cfg₂ : Cfg k Symbol State input) (t : ℕ) : - RelatesInSteps tm.TransitionRelation cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by + RelatesInSteps tm.Step cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by unfold runFrom induction t generalizing cfg₁ cfg₂ with | zero => simp | succ t ih => rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply'] constructor - · grind + · grind [step_iff] · intro h_runFrom use tm.step^[t] cfg₁ - grind - -/-- The Turing machine `tm` halts after exactly `t` steps on input `input` -if its state is `none` at step `t` and non-none at step `t - 1`. -Note that every Turing machine hast to perform at least one step to halt. -/ -def haltsAtStep (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : Bool := - (tm.runFrom (tm.initCfg input) t).state.isNone && - !(tm.runFrom (tm.initCfg input) (t - 1)).state.isNone - -/-- If a Turing machine halts, the time step is uniquely determined. -/ -lemma halting_step_unique - {tm : MultiTapeTM k Symbol State} - {input : List Symbol} - {t₁ t₂ : ℕ} - (h_halts₁ : tm.haltsAtStep input t₁) - (h_halts₂ : tm.haltsAtStep input t₂) : - t₁ = t₂ := by - wlog h : t₁ ≤ t₂ - · exact (this h_halts₂ h_halts₁ (Nat.le_of_not_le h)).symm - obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h - cases d with - | zero => rfl - | succ d => - have halts₁ : (tm.runFrom (tm.initCfg input) t₁).state = none := by - simp [haltsAtStep] at h_halts₁ - exact h_halts₁.left - have halts₂ : (tm.runFrom (tm.initCfg input) (d + t₁)).state ≠ none := by - grind [haltsAtStep, runFrom] - refine absurd ?_ halts₂ - rw [Nat.add_comm, runFrom_add, tm.runFrom_of_halt _ halts₁] - exact halts₁ - -/-- If a deterministic machine repeats a non-halting configuration, it never halts, -because the sequence between the two configurations will loop forever. -Note that this can be applied to two arbitrary and different time steps `t` and `t + Δ` -using `tm.runFrom_add`. -/ -lemma not_halts_of_repeat_nonhalt - (cfg : Cfg k Symbol State input) - (h_not_halt : cfg.state ≠ none) - (t : ℕ) - (heq : tm.runFrom cfg (t + 1) = cfg) : - ∀ t', (tm.runFrom cfg t').state ≠ none := by - intro t' - -- The configuration will repeat every `t + 1` steps. - have hloop : ∀ n, tm.runFrom cfg (n * (t + 1)) = cfg := by - intro n - induction n with - | zero => simp - | succ n ih => - rw [show (n + 1) * (t + 1) = n * (t + 1) + (t + 1) by grind, tm.runFrom_add, ih, heq] - by_contra hnh - -- Assuming the machine halts at step `t'`, it is also halted at step `t' * (t + 1)` - have h₁ : (tm.runFrom cfg (t' * (t + 1))).state = none := by - have hle : t' ≤ t' * (t + 1) := by grind - obtain ⟨tΔ , htΔ⟩ := Nat.exists_eq_add_of_le hle - rw [htΔ, tm.runFrom_add] - simp [hnh] - simp [hloop t', h_not_halt] at h₁ + grind [step_iff] + end MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 43dd000a2..2b27c4563 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -36,6 +36,7 @@ witness. * `Step`: the one-step relation on configurations * `ComputationPath`: a run of the machine: a series of configurations from the initial one, each reached from the previous by a step +* `ComputationPath.space_le`: a machine touches at most `k` cells per step * `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint * `Computes`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`: its instances, whose @@ -110,6 +111,17 @@ def time (p : ntm.ComputationPath input) : ℕ := p.cfgs.length - 1 /-- The number of work tape cells touched. -/ def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.cfgs +/-- A path visiting `t + 1` configurations takes `t` steps. -/ +lemma length_cfgs (p : ntm.ComputationPath input) : p.cfgs.length = p.time + 1 := by + have := p.isChainFromTo.length_pos + simp only [time] + omega + +/-- A machine touches at most `k` cells per step, whether or not it is deterministic. -/ +theorem space_le (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := by + calc p.space ≤ k * p.cfgs.length := spaceUsedOfCfgs_le _ + _ = k * p.time + k := by rw [p.length_cfgs, Nat.mul_succ] + end ComputationPath /-- `ntm` has a computation on `input` that starts at the initial configuration, halts, emits diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 15145637a..8dcabf7e5 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -43,7 +43,7 @@ lemma step_workTapes_eq_of_ne lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by - simp [visitedByTapeHead] + simp [visitedByTapeHead, visitedOfCfgs] lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : (tm.runFrom cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i := @@ -52,7 +52,8 @@ lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : /-- The set of positions visited by a tape head is monotone in the number of steps. -/ lemma visitedByTapeHead_mono (cfg : Cfg k Symbol State input) (i : Fin k) {t t' : ℕ} (h : t ≤ t') : tm.visitedByTapeHead cfg t i ⊆ tm.visitedByTapeHead cfg t' i := by - apply Finset.image_subset_image + intro z hz + rw [mem_visitedByTapeHead] at hz ⊢ grind /-- Starting from configuration `cfg`, every position between the initial head position of tape @@ -119,18 +120,15 @@ lemma content_natAbs_le_spaceUsedByTape /-- The number of cells touched by a single work tape grows by at most one each step. -/ lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : tm.spaceUsedByTape cfg t i ≤ t + 1 := by - calc - tm.spaceUsedByTape cfg t i - _ ≤ (Finset.range (t + 1)).card := Finset.card_image_le - _ = t + 1 := Finset.card_range _ + unfold spaceUsedByTape visitedByTapeHead visitedOfCfgs + exact (List.toFinset_card_le _).trans (by simp) -/-- The space used by a computation is bounded linearly by the number of steps. -/ +/-- The space used by a computation is bounded linearly by the number of steps. This is the +machine-free `spaceUsedOfCfgs_le` read at a step index. -/ lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) : tm.spaceUsed cfg t ≤ k * t + k := by - calc tm.spaceUsed cfg t - = ∑ i, (tm.spaceUsedByTape cfg t i) := by rfl - _ ≤ ∑ i, (t + 1) := Finset.sum_le_sum (fun i _ => tm.spaceUsedByTape_le cfg t i) - _ = k * t + k := by simp [Nat.mul_succ] + rw [spaceUsed_eq_spaceUsedOfCfgs] + exact (spaceUsedOfCfgs_le _).trans (by simp [Nat.mul_succ]) /-- The space used by a single tape is monotone in the number of steps. -/ lemma spaceUsedByTape_mono From c4e0d0f26109ef050f7ff259a4cfc8724c4ab4f5 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 15:35:56 +0300 Subject: [PATCH 05/18] refactor(MultiTape): factor stepping through a shared machine-unaware core `step` and `Step` each carried their own copy of the same case analysis: a halted configuration idles, a running one applies the chosen action. Only the choosing differed, by a function in one case and by a relation in the other. `Cfg.stepWith` and `Cfg.StepWith` move that to `Configuration.lean`, which mentions no machine, and `Cfg.stepWith_iff` states there once that choosing from the graph of a function is choosing its value. Both machines now define stepping in a line, and `step_iff` is that lemma applied. `outputSymbol` is removed. The output tape is part of a configuration, so the symbol a step emits is already recorded in `Cfg.output` and nothing referred to it, leaving the case analysis in exactly one place. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Configuration.lean | 23 +++++++++++++++++++ .../Turing/MultiTape/Deterministic.lean | 21 ++++------------- .../Turing/MultiTape/Nondeterministic.lean | 7 ++---- .../Machines/Turing/MultiTape/TapeLemmas.lean | 2 +- 4 files changed, 31 insertions(+), 22 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean index d7a835e03..18d1e7800 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -38,6 +38,8 @@ the configuration the run ends in. output tape * `Action`: what a machine does in one step * `Action.apply`: the effect of one action on a configuration +* `Cfg.stepWith`, `Cfg.StepWith`: one step, choosing an action by a function or by a relation, + agreeing via `Cfg.stepWith_iff` when the relation is the function's graph * `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in * `spaceUsedOfCfgs`: work tape cells touched along a list of configurations, with the bounds `spaceUsedOfCfgs_le` and `spaceUsedOfCfgs_mono` @@ -170,6 +172,27 @@ def Action.apply (out : Action k Symbol State) (cfg : Cfg k Symbol State input) workTapePos i := cfg.workTapePos i + (out.workActions i).2 output := cfg.output ++ out.outS.toList +/-- One step from `cfg`, choosing an action with `f`. A halted configuration idles. -/ +def Cfg.stepWith (cfg : Cfg k Symbol State input) (f : State → Action k Symbol State) : + Cfg k Symbol State input := + match cfg.state with + | none => cfg + | some q => (f q).apply cfg + +/-- One step from `cfg`, choosing any action permitted by `R`. A halted configuration idles. -/ +def Cfg.StepWith (cfg cfg' : Cfg k Symbol State input) + (R : State → Action k Symbol State → Prop) : Prop := + match cfg.state with + | none => cfg' = cfg + | some q => ∃ a, R q a ∧ cfg' = a.apply cfg + +/-- Choosing from the graph of a function is choosing that function's value: there is exactly one +step. This is what makes a machine deterministic, said without mentioning one. -/ +theorem Cfg.stepWith_iff {cfg cfg' : Cfg k Symbol State input} {f : State → Action k Symbol State} + {R : State → Action k Symbol State → Prop} (h : ∀ q a, R q a ↔ a = f q) : + cfg.StepWith cfg' R ↔ cfg' = cfg.stepWith f := by + cases hq : cfg.state <;> simp [Cfg.StepWith, Cfg.stepWith, hq, h] + /-- A work tape head moves by at most one cell when an action is applied. -/ lemma workTapePos_apply_le (out : Action k Symbol State) (cfg : Cfg k Symbol State input) (i : Fin k) : diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 4ef47b612..1d7c69b55 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -147,22 +147,11 @@ defined in `Cslib.Computability.Machines.Turing.MultiTape.Configuration`. /-- The step function corresponding to a `MultiTapeTM`. -/ def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input := - match cfg.state with - -- in the halting state, we stay at the configuration - | none => cfg - | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).apply cfg + cfg.stepWith fun q => tm.tr q cfg.inputSymbol cfg.workTapeSymbols -/-- The symbol (optionally) output when executing one step starting from configuration `cfg`. -/ -def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := - match cfg.state with - | none => none - | some q => (tm.tr q cfg.inputSymbol cfg.workTapeSymbols).outS - -@[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : tm.step cfg = cfg := by - unfold step - rw [h] + simp [step, Cfg.stepWith, h] /-- The configuration reached by running the Turing machine for `t` steps from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ @@ -190,7 +179,7 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := by - unfold step + unfold step Cfg.stepWith cases hstate : c.state with | none => simp | some q => exact workTapePos_apply_le _ c i @@ -237,8 +226,8 @@ follow `runFrom`, and `runPath` shows there is one of every length. /-- `Step` is the relation `step` induces: from each configuration there is exactly one step. -/ @[simp] -theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := by - cases hq : c.state <;> simp [MultiTapeNTM.Step, step, hq] +theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := + Cfg.stepWith_iff (by simp) /-- The configurations the machine passes through form a chain of steps. -/ lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 2b27c4563..974a1bb7f 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -75,15 +75,12 @@ variable {ntm : MultiTapeNTM k Symbol State} steps by any permitted transition. -/ @[scoped grind =] def Step (ntm : MultiTapeNTM k Symbol State) (c₁ c₂ : Cfg k Symbol State input) : Prop := - match c₁.state with - | none => c₂ = c₁ - | some q => - ∃ action, ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols action ∧ c₂ = action.apply c₁ + c₁.StepWith c₂ fun q action => ntm.Tr q c₁.inputSymbol c₁.workTapeSymbols action /-- A halted configuration steps only to itself. -/ lemma step_of_halt {c c' : Cfg k Symbol State input} (h : c.Halted) : ntm.Step c c' ↔ c' = c := by - simp [Step, h] + simp [Step, Cfg.StepWith, h] /-- The initial configuration corresponding to an input string. -/ @[simp] diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 8dcabf7e5..15ae8bacb 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -35,7 +35,7 @@ lemma step_workTapes_eq_of_ne (z : ℤ) (hz : z ≠ cfg.workTapePos j) : (tm.step cfg).workTapes j z = cfg.workTapes j z := by - unfold step + unfold step Cfg.stepWith cases hst : cfg.state with | none => simp_all | some q => From ef26fccc9c29b8ebcae6265c37d5f47dfca0a264 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 15:51:40 +0300 Subject: [PATCH 06/18] refactor(MultiTape): make stepping reduce by simp rather than by unfolding Marking `Cfg.stepWith` a simp definition, as `Action.apply` beside it already is, lets its two cases fire from a hypothesis on the state. The proofs that reasoned about a step no longer name the internals: `unfold step Cfg.stepWith` becomes `simp [step, hstate]`. Only the function is marked. The relation stays opaque so that `Step` continues to normalise through `step_iff` instead of unfolding into its cases. Co-Authored-By: Claude Opus 5 (1M context) --- .../Machines/Turing/MultiTape/Configuration.lean | 1 + .../Machines/Turing/MultiTape/Deterministic.lean | 7 +++---- .../Machines/Turing/MultiTape/TapeLemmas.lean | 6 +++--- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean index 18d1e7800..cfaa2c8bb 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -173,6 +173,7 @@ def Action.apply (out : Action k Symbol State) (cfg : Cfg k Symbol State input) output := cfg.output ++ out.outS.toList /-- One step from `cfg`, choosing an action with `f`. A halted configuration idles. -/ +@[simp] def Cfg.stepWith (cfg : Cfg k Symbol State input) (f : State → Action k Symbol State) : Cfg k Symbol State input := match cfg.state with diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 1d7c69b55..f737a62cb 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -151,7 +151,7 @@ def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input := lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : tm.step cfg = cfg := by - simp [step, Cfg.stepWith, h] + simp [step, h] /-- The configuration reached by running the Turing machine for `t` steps from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ @@ -179,10 +179,9 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := by - unfold step Cfg.stepWith cases hstate : c.state with - | none => simp - | some q => exact workTapePos_apply_le _ c i + | none => simp [step, hstate] + | some q => simpa [step, hstate] using workTapePos_apply_le _ c i end Cfg diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 15ae8bacb..d040d8af3 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -35,11 +35,11 @@ lemma step_workTapes_eq_of_ne (z : ℤ) (hz : z ≠ cfg.workTapePos j) : (tm.step cfg).workTapes j z = cfg.workTapes j z := by - unfold step Cfg.stepWith cases hst : cfg.state with - | none => simp_all + | none => simp_all [step] | some q => - rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> simp_all + rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> + simp_all [step] lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by From 125e8f82dbc25c7ecb5bfeeed718f5d42b4f0c97 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 16:44:54 +0300 Subject: [PATCH 07/18] refactor(MultiTape): define the space a machine uses as the space of its run `spaceUsed` described the same thing as `ComputationPath.space` and was defined separately. It is now that space, read off the machine's own run. `ComputationPath` gains the configuration it starts from. It was pinned to `initCfg`, but `spaceUsed` and the results about it speak of a run from any configuration, so the path could not express them. `IsChainFromTo` already takes both endpoints; only the start was being fixed. `runPath cfg t` is then the run from `cfg`, `spaceUsed cfg t` is its space, and `visitedByTapeHead` is the cells its configurations touch. The three views of space agree by `rfl`: as a path's space, as a sum over the tapes, and as `spaceUsedOfCfgs` of the configurations passed through. `spaceUsed_linear` and `spaceUsed_mono` follow from the results about any run, `ComputationPath.space_le` and `spaceUsedOfCfgs_mono`, rather than being proved again for the deterministic case. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 110 ++++++++++-------- .../Turing/MultiTape/Nondeterministic.lean | 26 +++-- .../Machines/Turing/MultiTape/TapeLemmas.lean | 13 ++- 3 files changed, 82 insertions(+), 67 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index f737a62cb..4c2998b9d 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -69,10 +69,10 @@ We define a number of structures and concepts related to multi-tape Turing machi * `MultiTapeTM`: the TM itself, a `MultiTapeNTM` whose transition relation is a function * `ofTr`: the machine with a given initial state and transition function +* `runPath`: the machine's own run from a configuration, as a `ComputationPath` * `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure; - the shared `spaceUsedOfCfgs` read at a step index + the space of that run * `step_iff`: the inherited `Step` is the graph of `step` -* `runPath`: the machine's own run, as a computation path * `computesInExactTimeAndSpace_iff_runFrom`: the inherited `ComputesInExactTimeAndSpace`, stated by step index rather than by computation path * `ComputableInTimeAndSpace`: a proof that there is a multi-tape TM that computes a function @@ -185,32 +185,6 @@ lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : end Cfg -section Space -/-! Now we define space usage and add some helper lemmas. -/ - -/-- The set of positions visited by the head of work tape `i` in the computation starting from -configuration `cfg` up to step `t`. -/ -def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : Finset ℤ := - visitedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) i - -/-- -The number of work tape cells touched by the head of tape `i` in the computation starting from -configuration `cfg` up to step `t`. --/ -def spaceUsedByTape (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ := - (tm.visitedByTapeHead cfg t i).card - -/-- -The number of work tape cells touched by a computation starting from configuration -`cfg` up to step `t`. --/ -def spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ := ∑ i, tm.spaceUsedByTape cfg t i - -/-- The space used up to step `t` is the space touched by the configurations up to step `t`. -/ -lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := rfl - -end Space open Cfg @@ -237,11 +211,11 @@ lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : rw [runFrom_succ_eq_step'] exact step_iff.mpr rfl -/-- The machine's own run for `t` steps, as a computation path. -/ -def runPath (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : - tm.ComputationPath input where - cfgs := (List.range (t + 1)).map (tm.runFrom (tm.initCfg input)) - last := tm.runFrom (tm.initCfg input) t +/-- The machine's own run from `cfg` for `t` steps, as a computation path. -/ +def runPath (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : + tm.ComputationPath input cfg where + cfgs := (List.range (t + 1)).map (tm.runFrom cfg) + last := tm.runFrom cfg t isChainFromTo := { isChain := isChain_map_range _ t ne_nil := by simp @@ -251,21 +225,56 @@ def runPath (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : simp } @[simp] -lemma runPath_time (input : List Symbol) (t : ℕ) : (tm.runPath input t).time = t := by - simp [MultiTapeNTM.ComputationPath.time, runPath] +lemma runPath_cfgs (cfg : Cfg k Symbol State input) (t : ℕ) : + (tm.runPath cfg t).cfgs = (List.range (t + 1)).map (tm.runFrom cfg) := rfl + +@[simp] +lemma runPath_last (cfg : Cfg k Symbol State input) (t : ℕ) : + (tm.runPath cfg t).last = tm.runFrom cfg t := rfl @[simp] -lemma runPath_last (input : List Symbol) (t : ℕ) : - (tm.runPath input t).last = tm.runFrom (tm.initCfg input) t := rfl +lemma runPath_time (cfg : Cfg k Symbol State input) (t : ℕ) : (tm.runPath cfg t).time = t := by + simp [MultiTapeNTM.ComputationPath.time] +section Space +/-! Space is read off the machine's own run, so it is the space of a `ComputationPath`. -/ + +/-- The set of positions visited by the head of work tape `i` in the computation starting from +configuration `cfg` up to step `t`. -/ +def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : Finset ℤ := + visitedOfCfgs (tm.runPath cfg t).cfgs i + +/-- +The number of work tape cells touched by the head of tape `i` in the computation starting from +configuration `cfg` up to step `t`. +-/ +def spaceUsedByTape (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ := + (tm.visitedByTapeHead cfg t i).card + +/-- +The number of work tape cells touched by a computation starting from configuration +`cfg` up to step `t`: the space of the machine's own run. +-/ +def spaceUsed (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ := (tm.runPath cfg t).space + +/-- The space used up to step `t` is the space of the run up to step `t`. -/ @[simp] -lemma runPath_space (input : List Symbol) (t : ℕ) : - (tm.runPath input t).space = tm.spaceUsed (tm.initCfg input) t := by - simp [MultiTapeNTM.ComputationPath.space, runPath, spaceUsed_eq_spaceUsedOfCfgs] +lemma runPath_space (cfg : Cfg k Symbol State input) (t : ℕ) : + (tm.runPath cfg t).space = tm.spaceUsed cfg t := rfl + +/-- Space is the sum over the tapes of the cells each head touched. -/ +lemma spaceUsed_eq_sum (cfg : Cfg k Symbol State input) (t : ℕ) : + tm.spaceUsed cfg t = ∑ i, tm.spaceUsedByTape cfg t i := rfl + +/-- The space used up to step `t` is the space touched by the configurations up to step `t`. -/ +lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : + tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := rfl + +end Space /-- A computation path of `tm` has no choice but to follow `runFrom`. -/ -lemma path_getElem {p : tm.ComputationPath input} (i : ℕ) (h : i < p.cfgs.length) : - p.cfgs[i] = tm.runFrom (tm.initCfg input) i := by +lemma path_getElem {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} + (i : ℕ) (h : i < p.cfgs.length) : p.cfgs[i] = tm.runFrom start i := by induction i with | zero => simpa using p.isChainFromTo.getElem_zero | succ n ih => @@ -273,26 +282,27 @@ lemma path_getElem {p : tm.ComputationPath input} (i : ℕ) (h : i < p.cfgs.leng rw [step_iff.mp hstep, ih (by omega), ← runFrom_succ_eq_step'] /-- A path visiting `t + 1` configurations takes `t` steps. -/ -lemma path_length {p : tm.ComputationPath input} : p.cfgs.length = p.time + 1 := by +lemma path_length {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : + p.cfgs.length = p.time + 1 := by have := p.isChainFromTo.length_pos simp only [MultiTapeNTM.ComputationPath.time] omega -lemma path_cfgs {p : tm.ComputationPath input} : - p.cfgs = (List.range (p.time + 1)).map (tm.runFrom (tm.initCfg input)) := by +lemma path_cfgs {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : + p.cfgs = (List.range (p.time + 1)).map (tm.runFrom start) := by refine List.ext_getElem (by simp [path_length]) fun i h₁ h₂ => ?_ simpa using path_getElem i h₁ /-- It ends where `tm` is after that many steps. -/ -lemma path_last {p : tm.ComputationPath input} : - p.last = tm.runFrom (tm.initCfg input) p.time := by +lemma path_last {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : + p.last = tm.runFrom start p.time := by have h := p.isChainFromTo.getElem_length_sub_one rw [path_getElem _ (by have := p.isChainFromTo.length_pos; omega)] at h exact h.symm /-- Its space is the space `tm` uses over the same number of steps. -/ -lemma path_space {p : tm.ComputationPath input} : - p.space = tm.spaceUsed (tm.initCfg input) p.time := by +lemma path_space {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : + p.space = tm.spaceUsed start p.time := by rw [MultiTapeNTM.ComputationPath.space, path_cfgs, ← spaceUsed_eq_spaceUsedOfCfgs] /-- `tm` has exactly one computation path of each length, so `ComputesInExactTimeAndSpace`, @@ -309,7 +319,7 @@ theorem computesInExactTimeAndSpace_iff_runFrom {input output : List Symbol} {t rw [path_space] at hspace exact ⟨hhalt, hout, hspace⟩ · rintro ⟨hhalt, hout, hspace⟩ - exact ⟨tm.runPath input t, by simpa using hhalt, by simpa using hout, by simp, + exact ⟨tm.runPath (tm.initCfg input) t, by simpa using hhalt, by simpa using hout, by simp, by simpa using hspace⟩ /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 974a1bb7f..43d3d8041 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -34,8 +34,8 @@ witness. * `MultiTapeNTM`: the machine, an initial state and a transition relation * `Step`: the one-step relation on configurations -* `ComputationPath`: a run of the machine: a series of configurations from the initial one, each - reached from the previous by a step +* `ComputationPath`: a run of the machine from a given configuration: a series of configurations, + each reached from the previous by a step * `ComputationPath.space_le`: a machine touches at most `k` cells per step * `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint * `Computes`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`: @@ -90,32 +90,34 @@ def initCfg (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : /-- A computation path of `ntm` on `input`: the configurations it passes through, forming a chain of steps from the initial configuration to the one it ends at. -/ -structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) where - /-- the configurations passed through, starting with the initial one -/ +structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) + (start : Cfg k Symbol State input) where + /-- the configurations passed through, starting with `start` -/ cfgs : List (Cfg k Symbol State input) /-- the configuration the path ends at -/ last : Cfg k Symbol State input - /-- consecutive configurations are joined by a step, from the initial configuration to `last` -/ - isChainFromTo : cfgs.IsChainFromTo ntm.Step (ntm.initCfg input) last + /-- consecutive configurations are joined by a step, from `start` to `last` -/ + isChainFromTo : cfgs.IsChainFromTo ntm.Step start last namespace ComputationPath variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} + {start : Cfg k Symbol State input} /-- The number of steps taken, the time the computation takes. -/ -def time (p : ntm.ComputationPath input) : ℕ := p.cfgs.length - 1 +def time (p : ntm.ComputationPath input start) : ℕ := p.cfgs.length - 1 /-- The number of work tape cells touched. -/ -def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.cfgs +def space (p : ntm.ComputationPath input start) : ℕ := spaceUsedOfCfgs p.cfgs /-- A path visiting `t + 1` configurations takes `t` steps. -/ -lemma length_cfgs (p : ntm.ComputationPath input) : p.cfgs.length = p.time + 1 := by +lemma length_cfgs (p : ntm.ComputationPath input start) : p.cfgs.length = p.time + 1 := by have := p.isChainFromTo.length_pos simp only [time] omega /-- A machine touches at most `k` cells per step, whether or not it is deterministic. -/ -theorem space_le (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := by +theorem space_le (p : ntm.ComputationPath input start) : p.space ≤ k * p.time + k := by calc p.space ≤ k * p.cfgs.length := spaceUsedOfCfgs_le _ _ = k * p.time + k := by rw [p.length_cfgs, Nat.mul_succ] @@ -125,8 +127,8 @@ end ComputationPath `output` and satisfies `P`. The notions below are its instances, so their constraints all refer to a single computation. -/ def ComputesSuchThat (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) - (P : ntm.ComputationPath input → Prop) : Prop := - ∃ p : ntm.ComputationPath input, p.last.Halted ∧ p.last.output = output ∧ P p + (P : ntm.ComputationPath input (ntm.initCfg input) → Prop) : Prop := + ∃ p : ntm.ComputationPath input (ntm.initCfg input), p.last.Halted ∧ p.last.output = output ∧ P p /-- `ntm` computes `output` from `input`, with no bound on resources. -/ def Computes (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) : Prop := diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index d040d8af3..8cea567c5 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -16,6 +16,9 @@ This file collects lemmas about the set of positions visited by a work-tape head (`MultiTapeTM.spaceUsedByTape`, `MultiTapeTM.spaceUsed`) and how the tape head positions influence the cells that are modified on a tape. +Those measures are read off the machine's own run, so results that hold of any run come from +`MultiTapeNTM.ComputationPath` rather than being proved again here. + -/ @[expose] public section @@ -123,12 +126,11 @@ lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) unfold spaceUsedByTape visitedByTapeHead visitedOfCfgs exact (List.toFinset_card_le _).trans (by simp) -/-- The space used by a computation is bounded linearly by the number of steps. This is the -machine-free `spaceUsedOfCfgs_le` read at a step index. -/ +/-- The space used by a computation is bounded linearly by the number of steps. This is +`ComputationPath.space_le` read off the machine's own run. -/ lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) : tm.spaceUsed cfg t ≤ k * t + k := by - rw [spaceUsed_eq_spaceUsedOfCfgs] - exact (spaceUsedOfCfgs_le _).trans (by simp [Nat.mul_succ]) + simpa using (tm.runPath cfg t).space_le /-- The space used by a single tape is monotone in the number of steps. -/ lemma spaceUsedByTape_mono @@ -143,6 +145,7 @@ lemma spaceUsedByTape_mono lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) : Monotone (tm.spaceUsed cfg ·) := by intro t t' h - exact Finset.sum_le_sum (fun i _ => spaceUsedByTape_mono tm cfg i h) + simp only [spaceUsed_eq_spaceUsedOfCfgs] + exact spaceUsedOfCfgs_mono ((List.range_sublist.mpr (by omega)).map _) end Turing.MultiTapeTM From 019f248b590633cd54d78b8291ca5281bdaba702 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 17:03:49 +0300 Subject: [PATCH 08/18] refactor(MultiTape): a computation path is a non-empty chain, with both ends read off it The path designated one end and not the other: `start` was a parameter and `last` a field, so the two ends of the same list were described in two different ways. Neither is designated now. A path is a non-empty list of configurations whose consecutive elements are joined by a step, and `start` and `last` are its head and last element. `IsChainFromTo` is no longer needed, since fixing the endpoints was the only thing it added over `IsChain` and non-emptiness. `ComputesSuchThat` asks that a path start at the initial configuration, which the type used to carry. The deterministic side gains `runPath_start` beside `runPath_last`, and the results about a path speak of `p.start` where they spoke of a parameter. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 66 +++++++++---------- .../Turing/MultiTape/Nondeterministic.lean | 48 ++++++++------ 2 files changed, 60 insertions(+), 54 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 4c2998b9d..f1ad67f9e 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -213,24 +213,25 @@ lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : /-- The machine's own run from `cfg` for `t` steps, as a computation path. -/ def runPath (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.ComputationPath input cfg where + tm.ComputationPath input where cfgs := (List.range (t + 1)).map (tm.runFrom cfg) - last := tm.runFrom cfg t - isChainFromTo := - { isChain := isChain_map_range _ t - ne_nil := by simp - head_eq := by rw [List.head_map]; simp - getLast_eq := by - rw [← Option.some_inj, ← List.getLast?_eq_some_getLast, List.range_succ, List.map_append] - simp } + ne_nil := by simp + isChain := isChain_map_range _ t @[simp] lemma runPath_cfgs (cfg : Cfg k Symbol State input) (t : ℕ) : (tm.runPath cfg t).cfgs = (List.range (t + 1)).map (tm.runFrom cfg) := rfl +@[simp] +lemma runPath_start (cfg : Cfg k Symbol State input) (t : ℕ) : + (tm.runPath cfg t).start = cfg := by + simp [MultiTapeNTM.ComputationPath.start, List.head_map] + @[simp] lemma runPath_last (cfg : Cfg k Symbol State input) (t : ℕ) : - (tm.runPath cfg t).last = tm.runFrom cfg t := rfl + (tm.runPath cfg t).last = tm.runFrom cfg t := by + rw [MultiTapeNTM.ComputationPath.last, ← Option.some_inj, ← List.getLast?_eq_some_getLast] + simp [List.range_succ] @[simp] lemma runPath_time (cfg : Cfg k Symbol State input) (t : ℕ) : (tm.runPath cfg t).time = t := by @@ -273,36 +274,33 @@ lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : end Space /-- A computation path of `tm` has no choice but to follow `runFrom`. -/ -lemma path_getElem {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} - (i : ℕ) (h : i < p.cfgs.length) : p.cfgs[i] = tm.runFrom start i := by +lemma path_getElem {p : tm.ComputationPath input} + (i : ℕ) (h : i < p.cfgs.length) : p.cfgs[i] = tm.runFrom p.start i := by induction i with - | zero => simpa using p.isChainFromTo.getElem_zero + | zero => simp [MultiTapeNTM.ComputationPath.start, List.getElem_zero] | succ n ih => - have hstep := List.isChain_iff_getElem.mp p.isChainFromTo.isChain n h + have hstep := List.isChain_iff_getElem.mp p.isChain n h rw [step_iff.mp hstep, ih (by omega), ← runFrom_succ_eq_step'] /-- A path visiting `t + 1` configurations takes `t` steps. -/ -lemma path_length {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : - p.cfgs.length = p.time + 1 := by - have := p.isChainFromTo.length_pos - simp only [MultiTapeNTM.ComputationPath.time] - omega - -lemma path_cfgs {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : - p.cfgs = (List.range (p.time + 1)).map (tm.runFrom start) := by +lemma path_length {p : tm.ComputationPath input} : p.cfgs.length = p.time + 1 := + p.length_cfgs + +lemma path_cfgs {p : tm.ComputationPath input} : + p.cfgs = (List.range (p.time + 1)).map (tm.runFrom p.start) := by refine List.ext_getElem (by simp [path_length]) fun i h₁ h₂ => ?_ simpa using path_getElem i h₁ /-- It ends where `tm` is after that many steps. -/ -lemma path_last {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : - p.last = tm.runFrom start p.time := by - have h := p.isChainFromTo.getElem_length_sub_one - rw [path_getElem _ (by have := p.isChainFromTo.length_pos; omega)] at h - exact h.symm +lemma path_last {p : tm.ComputationPath input} : + p.last = tm.runFrom p.start p.time := by + rw [MultiTapeNTM.ComputationPath.last, List.getLast_eq_getElem, + path_getElem _ (by have := p.length_pos; omega)] + rfl /-- Its space is the space `tm` uses over the same number of steps. -/ -lemma path_space {start : Cfg k Symbol State input} {p : tm.ComputationPath input start} : - p.space = tm.spaceUsed start p.time := by +lemma path_space {p : tm.ComputationPath input} : + p.space = tm.spaceUsed p.start p.time := by rw [MultiTapeNTM.ComputationPath.space, path_cfgs, ← spaceUsed_eq_spaceUsedOfCfgs] /-- `tm` has exactly one computation path of each length, so `ComputesInExactTimeAndSpace`, @@ -314,13 +312,13 @@ theorem computesInExactTimeAndSpace_iff_runFrom {input output : List Symbol} {t (tm.runFrom (tm.initCfg input) t).output = output ∧ tm.spaceUsed (tm.initCfg input) t = s := by constructor - · rintro ⟨p, hhalt, hout, rfl, hspace⟩ - rw [path_last] at hhalt hout - rw [path_space] at hspace + · rintro ⟨p, hstart, hhalt, hout, rfl, hspace⟩ + rw [path_last, hstart] at hhalt hout + rw [path_space, hstart] at hspace exact ⟨hhalt, hout, hspace⟩ · rintro ⟨hhalt, hout, hspace⟩ - exact ⟨tm.runPath (tm.initCfg input) t, by simpa using hhalt, by simpa using hout, by simp, - by simpa using hspace⟩ + exact ⟨tm.runPath (tm.initCfg input) t, by simp, by simpa using hhalt, by simpa using hout, + by simp, by simpa using hspace⟩ /-- A proof that the Turing machine `tm` computes the function `f` such that on all inputs of length `n` it uses at most `t n` steps and `s n` space. It assumes an embedding function diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 43d3d8041..881ced29b 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -7,7 +7,6 @@ Authors: Aviv Bar Natan module public import Mathlib.Data.List.Chain -public import Cslib.Foundations.Data.List.IsChainFromTo public import Cslib.Computability.Machines.Turing.MultiTape.Configuration /-! @@ -34,8 +33,8 @@ witness. * `MultiTapeNTM`: the machine, an initial state and a transition relation * `Step`: the one-step relation on configurations -* `ComputationPath`: a run of the machine from a given configuration: a series of configurations, - each reached from the previous by a step +* `ComputationPath`: a run of the machine: a non-empty list of configurations, each reached from + the previous by a step, with `start` and `last` read off it * `ComputationPath.space_le`: a machine touches at most `k` cells per step * `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint * `Computes`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`: @@ -88,36 +87,44 @@ def initCfg (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : Cfg k Symbol State input := Cfg.init ntm.q₀ input -/-- A computation path of `ntm` on `input`: the configurations it passes through, forming a chain -of steps from the initial configuration to the one it ends at. -/ -structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) - (start : Cfg k Symbol State input) where - /-- the configurations passed through, starting with `start` -/ +/-- A computation path of `ntm` on `input`: the configurations it passes through, forming a +non-empty chain of steps. Neither end is designated; `start` and `last` are read off it. -/ +structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) where + /-- the configurations passed through -/ cfgs : List (Cfg k Symbol State input) - /-- the configuration the path ends at -/ - last : Cfg k Symbol State input - /-- consecutive configurations are joined by a step, from `start` to `last` -/ - isChainFromTo : cfgs.IsChainFromTo ntm.Step start last + /-- a run passes through at least one configuration -/ + ne_nil : cfgs ≠ [] + /-- consecutive configurations are joined by a step -/ + isChain : cfgs.IsChain ntm.Step namespace ComputationPath variable {ntm : MultiTapeNTM k Symbol State} {input : List Symbol} - {start : Cfg k Symbol State input} + +/-- A run passes through at least one configuration. -/ +lemma length_pos (p : ntm.ComputationPath input) : 0 < p.cfgs.length := + List.length_pos_iff.mpr p.ne_nil + +/-- The configuration the run starts from. -/ +def start (p : ntm.ComputationPath input) : Cfg k Symbol State input := p.cfgs.head p.ne_nil + +/-- The configuration the run ends at. -/ +def last (p : ntm.ComputationPath input) : Cfg k Symbol State input := p.cfgs.getLast p.ne_nil /-- The number of steps taken, the time the computation takes. -/ -def time (p : ntm.ComputationPath input start) : ℕ := p.cfgs.length - 1 +def time (p : ntm.ComputationPath input) : ℕ := p.cfgs.length - 1 /-- The number of work tape cells touched. -/ -def space (p : ntm.ComputationPath input start) : ℕ := spaceUsedOfCfgs p.cfgs +def space (p : ntm.ComputationPath input) : ℕ := spaceUsedOfCfgs p.cfgs /-- A path visiting `t + 1` configurations takes `t` steps. -/ -lemma length_cfgs (p : ntm.ComputationPath input start) : p.cfgs.length = p.time + 1 := by - have := p.isChainFromTo.length_pos +lemma length_cfgs (p : ntm.ComputationPath input) : p.cfgs.length = p.time + 1 := by + have := p.length_pos simp only [time] omega /-- A machine touches at most `k` cells per step, whether or not it is deterministic. -/ -theorem space_le (p : ntm.ComputationPath input start) : p.space ≤ k * p.time + k := by +theorem space_le (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := by calc p.space ≤ k * p.cfgs.length := spaceUsedOfCfgs_le _ _ = k * p.time + k := by rw [p.length_cfgs, Nat.mul_succ] @@ -127,8 +134,9 @@ end ComputationPath `output` and satisfies `P`. The notions below are its instances, so their constraints all refer to a single computation. -/ def ComputesSuchThat (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) - (P : ntm.ComputationPath input (ntm.initCfg input) → Prop) : Prop := - ∃ p : ntm.ComputationPath input (ntm.initCfg input), p.last.Halted ∧ p.last.output = output ∧ P p + (P : ntm.ComputationPath input → Prop) : Prop := + ∃ p : ntm.ComputationPath input, p.start = ntm.initCfg input ∧ p.last.Halted ∧ + p.last.output = output ∧ P p /-- `ntm` computes `output` from `input`, with no bound on resources. -/ def Computes (ntm : MultiTapeNTM k Symbol State) (input output : List Symbol) : Prop := From f6e03174b244565b58044e9de1e695409466501a Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 17:05:29 +0300 Subject: [PATCH 09/18] refactor(MultiTape): move the facts about a step to the machine that has steps `workTapePos_step_le` and `step_workTapes_eq_of_ne` were proved for the deterministic machine, but neither uses determinism: a head moves by at most one cell and no cell but the one under it changes because that is what applying an action does. Both are now stated of `Action.apply` in `Configuration.lean` and of `Step` in `Nondeterministic.lean`, so they hold of any machine. The deterministic machine gets them by its own step being one of those steps, which is a line each rather than a proof. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Configuration.lean | 10 +++++++- .../Turing/MultiTape/Deterministic.lean | 17 ++++++++----- .../Turing/MultiTape/Nondeterministic.lean | 24 ++++++++++++++++++- .../Machines/Turing/MultiTape/TapeLemmas.lean | 13 ---------- 4 files changed, 43 insertions(+), 21 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean index cfaa2c8bb..45cde39f1 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -37,7 +37,9 @@ the configuration the run ends in. * `Cfg`: the configuration: the internal state, the tape contents and head positions, and the output tape * `Action`: what a machine does in one step -* `Action.apply`: the effect of one action on a configuration +* `Action.apply`: the effect of one action on a configuration, moving a head by at most one + cell (`workTapePos_apply_le`) and changing no cell but the one under it + (`workTapes_apply_eq_of_ne`) * `Cfg.stepWith`, `Cfg.StepWith`: one step, choosing an action by a function or by a relation, agreeing via `Cfg.stepWith_iff` when the relation is the function's graph * `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in @@ -201,6 +203,12 @@ lemma workTapePos_apply_le (out : Action k Symbol State) simp only [Action.apply, add_sub_cancel_left, abs_le, SignType.cast] grind +/-- An action only changes the cell its head is on, so a cell elsewhere is left alone. -/ +lemma workTapes_apply_eq_of_ne (a : Action k Symbol State) (cfg : Cfg k Symbol State input) + (j : Fin k) (z : ℤ) (hz : z ≠ cfg.workTapePos j) : + (a.apply cfg).workTapes j z = cfg.workTapes j z := by + rcases hw : (a.workActions j).1 <;> simp_all + /-- The work tape cells visited by the head of tape `i` along a list of configurations. -/ def visitedOfCfgs (cfgs : List (Cfg k Symbol State input)) (i : Fin k) : Finset ℤ := (cfgs.map (·.workTapePos i)).toFinset diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index f1ad67f9e..040d100fb 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -177,12 +177,6 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n | succ d ih => rw [runFrom_succ_eq_step', ih, step_of_halt h] -lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : - |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := by - cases hstate : c.state with - | none => simp [step, hstate] - | some q => simpa [step, hstate] using workTapePos_apply_le _ c i - end Cfg @@ -202,6 +196,17 @@ follow `runFrom`, and `runPath` shows there is one of every length. theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := Cfg.stepWith_iff (by simp) +/-- A work tape head moves by at most one cell in a step. Inherited from `MultiTapeNTM`, since +`step` is one of its steps. -/ +lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : + |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := + MultiTapeNTM.workTapePos_step_le (step_iff.mpr rfl) i + +/-- A step changes no work tape cell but the one its head is on. Inherited likewise. -/ +lemma step_workTapes_eq_of_ne (cfg : Cfg k Symbol State input) (j : Fin k) (z : ℤ) + (hz : z ≠ cfg.workTapePos j) : (tm.step cfg).workTapes j z = cfg.workTapes j z := + MultiTapeNTM.workTapes_step_eq_of_ne (step_iff.mpr rfl) j z hz + /-- The configurations the machine passes through form a chain of steps. -/ lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : ((List.range (t + 1)).map (tm.runFrom cfg)).IsChain tm.Step := by diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 881ced29b..3852dda1d 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -32,7 +32,9 @@ witness. ## Important Declarations * `MultiTapeNTM`: the machine, an initial state and a transition relation -* `Step`: the one-step relation on configurations +* `Step`: the one-step relation on configurations, moving a head by at most one cell + (`workTapePos_step_le`) and changing no cell but the one under it + (`workTapes_step_eq_of_ne`) * `ComputationPath`: a run of the machine: a non-empty list of configurations, each reached from the previous by a step, with `start` and `last` read off it * `ComputationPath.space_le`: a machine touches at most `k` cells per step @@ -81,6 +83,26 @@ lemma step_of_halt {c c' : Cfg k Symbol State input} (h : c.Halted) : ntm.Step c c' ↔ c' = c := by simp [Step, Cfg.StepWith, h] +/-- A work tape head moves by at most one cell in a step. -/ +lemma workTapePos_step_le {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (i : Fin k) : + |c'.workTapePos i - c.workTapePos i| ≤ 1 := by + cases hq : c.state with + | none => simp_all [Step, Cfg.StepWith] + | some q => + simp only [Step, Cfg.StepWith, hq] at h + obtain ⟨a, -, rfl⟩ := h + exact workTapePos_apply_le a c i + +/-- A step changes no work tape cell but the one its head is on. -/ +lemma workTapes_step_eq_of_ne {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (j : Fin k) + (z : ℤ) (hz : z ≠ c.workTapePos j) : c'.workTapes j z = c.workTapes j z := by + cases hq : c.state with + | none => simp_all [Step, Cfg.StepWith] + | some q => + simp only [Step, Cfg.StepWith, hq] at h + obtain ⟨a, -, rfl⟩ := h + exact workTapes_apply_eq_of_ne a c j z hz + /-- The initial configuration corresponding to an input string. -/ @[simp] def initCfg (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 8cea567c5..587dfeb4d 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -31,19 +31,6 @@ variable {input : List Symbol} variable {tm : MultiTapeTM k Symbol State} variable {cfg : Cfg k Symbol State input} -/-- If the work tape head is not at position `z`, then the tape does not change there. -/ -lemma step_workTapes_eq_of_ne - (cfg : Cfg k Symbol State input) - (j : Fin k) - (z : ℤ) - (hz : z ≠ cfg.workTapePos j) : - (tm.step cfg).workTapes j z = cfg.workTapes j z := by - cases hst : cfg.state with - | none => simp_all [step] - | some q => - rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> - simp_all [step] - lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by simp [visitedByTapeHead, visitedOfCfgs] From b0e500532b5efb34a5893b1c0c93dc179e293c78 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 17:14:33 +0300 Subject: [PATCH 10/18] refactor(MultiTapeTM): inherit that a halted configuration steps to itself `step_of_halt` was proved twice, once of `Step` and once of `step`. The deterministic one is now the nondeterministic one applied to the machine's own step, so `step_iff` moves up to sit with `step`, where it belongs: it is the fact the rest of the deterministic development rests on. Also restores two `@[simp]` attributes, on `step_of_halt` and `runFrom_of_halt`, that were dropped by mistake when neighbouring declarations were removed. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 040d100fb..8123e9966 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -149,9 +149,17 @@ defined in `Cslib.Computability.Machines.Turing.MultiTape.Configuration`. def step (cfg : Cfg k Symbol State input) : Cfg k Symbol State input := cfg.stepWith fun q => tm.tr q cfg.inputSymbol cfg.workTapeSymbols +/-- `Step` is the relation `step` induces: from each configuration there is exactly one step. +Everything below about a deterministic machine rests on this. -/ +@[simp] +theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := + Cfg.stepWith_iff (by simp) + +/-- A halted configuration steps to itself, inherited from `MultiTapeNTM`. -/ +@[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : - tm.step cfg = cfg := by - simp [step, h] + tm.step cfg = cfg := + (MultiTapeNTM.step_of_halt h).mp (step_iff.mpr rfl) /-- The configuration reached by running the Turing machine for `t` steps from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ @@ -170,6 +178,7 @@ lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by simp [runFrom, Function.iterate_succ_apply'] +@[simp] lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : tm.runFrom cfg n = cfg := by induction n with @@ -191,11 +200,6 @@ that there is no choice to make: `Step` is the graph of `step`, so a computation follow `runFrom`, and `runPath` shows there is one of every length. -/ -/-- `Step` is the relation `step` induces: from each configuration there is exactly one step. -/ -@[simp] -theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := - Cfg.stepWith_iff (by simp) - /-- A work tape head moves by at most one cell in a step. Inherited from `MultiTapeNTM`, since `step` is one of its steps. -/ lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : From b1cdeba1753259c90af7315d9d92d2b40573400b Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 17:25:00 +0300 Subject: [PATCH 11/18] refactor(MultiTapeTM): inherit the facts about a step through one bridge `workTapePos_step_le` and `step_workTapes_eq_of_ne` were restated for the deterministic machine, a line each, only to supply `tm.Step c (tm.step c)` to the general result. That fact is now stated once, as `step_step`, and the general results are applied to it where they are used. A further such result costs nothing. `path_length` was `length_cfgs` under another name and is dropped. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 25 ++++++------------- .../Machines/Turing/MultiTape/TapeLemmas.lean | 4 +-- 2 files changed, 10 insertions(+), 19 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 8123e9966..f4821eef1 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -155,11 +155,17 @@ Everything below about a deterministic machine rests on this. -/ theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := Cfg.stepWith_iff (by simp) +/-- A machine's own step is one of its steps. Applying a result about `MultiTapeNTM.Step` to +this is how the deterministic machine inherits it. -/ +@[simp] +lemma step_step (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) : + tm.Step c (tm.step c) := step_iff.mpr rfl + /-- A halted configuration steps to itself, inherited from `MultiTapeNTM`. -/ @[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : tm.step cfg = cfg := - (MultiTapeNTM.step_of_halt h).mp (step_iff.mpr rfl) + (MultiTapeNTM.step_of_halt h).mp (tm.step_step cfg) /-- The configuration reached by running the Turing machine for `t` steps from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ @@ -200,17 +206,6 @@ that there is no choice to make: `Step` is the graph of `step`, so a computation follow `runFrom`, and `runPath` shows there is one of every length. -/ -/-- A work tape head moves by at most one cell in a step. Inherited from `MultiTapeNTM`, since -`step` is one of its steps. -/ -lemma workTapePos_step_le (c : Cfg k Symbol State input) (i : Fin k) : - |(tm.step c).workTapePos i - c.workTapePos i| ≤ 1 := - MultiTapeNTM.workTapePos_step_le (step_iff.mpr rfl) i - -/-- A step changes no work tape cell but the one its head is on. Inherited likewise. -/ -lemma step_workTapes_eq_of_ne (cfg : Cfg k Symbol State input) (j : Fin k) (z : ℤ) - (hz : z ≠ cfg.workTapePos j) : (tm.step cfg).workTapes j z = cfg.workTapes j z := - MultiTapeNTM.workTapes_step_eq_of_ne (step_iff.mpr rfl) j z hz - /-- The configurations the machine passes through form a chain of steps. -/ lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : ((List.range (t + 1)).map (tm.runFrom cfg)).IsChain tm.Step := by @@ -291,13 +286,9 @@ lemma path_getElem {p : tm.ComputationPath input} have hstep := List.isChain_iff_getElem.mp p.isChain n h rw [step_iff.mp hstep, ih (by omega), ← runFrom_succ_eq_step'] -/-- A path visiting `t + 1` configurations takes `t` steps. -/ -lemma path_length {p : tm.ComputationPath input} : p.cfgs.length = p.time + 1 := - p.length_cfgs - lemma path_cfgs {p : tm.ComputationPath input} : p.cfgs = (List.range (p.time + 1)).map (tm.runFrom p.start) := by - refine List.ext_getElem (by simp [path_length]) fun i h₁ h₂ => ?_ + refine List.ext_getElem (by simp [p.length_cfgs]) fun i h₁ h₂ => ?_ simpa using path_getElem i h₁ /-- It ends where `tm` is after that many steps. -/ diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 587dfeb4d..bfeecb5c0 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -57,7 +57,7 @@ lemma uIcc_workTapePos_subset_visitedByTapeHead | succ t ih => intro z hz have hstep : |(tm.runFrom cfg (t + 1)).workTapePos i - (tm.runFrom cfg t).workTapePos i| ≤ 1 := - runFrom_succ_eq_step' (tm := tm) ▸ tm.workTapePos_step_le _ i + runFrom_succ_eq_step' (tm := tm) ▸ MultiTapeNTM.workTapePos_step_le (tm.step_step _) i have hmono := tm.visitedByTapeHead_mono cfg i (Nat.le_succ t) have hself := tm.mem_visitedByTapeHead_self cfg (t + 1) i grind [Finset.mem_uIcc] @@ -76,7 +76,7 @@ lemma mem_visitedByTapeHead_of_workTapes_ne by_cases hz : z = (tm.runFrom cfg t).workTapePos j · exact hz ▸ tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (tm.mem_visitedByTapeHead_self cfg t j) - · rw [tm.step_workTapes_eq_of_ne _ j z hz] at h + · rw [MultiTapeNTM.workTapes_step_eq_of_ne (tm.step_step _) j z hz] at h exact tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (ih h) /-- Every position visited by the head of tape `i` lies within `spaceUsedByTape … i` of the From f48e9ceb7731ffd8b50b2c9ccfc06646b3f97896 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sat, 29 Aug 2026 19:19:35 +0300 Subject: [PATCH 12/18] refactor(MultiTapeTM): define runFrom by recursion, and drop step_step MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `runFrom` iterated `step` through `Function.iterate`, so reaching the configuration after one more step took a lemma. Defining it by recursion makes `runFrom_zero` and `runFrom_succ_eq_step'` hold by `rfl`, and `runFrom_succ_eq_step`, which peeled a step off the front, is unused and gone. `step_step` was `step_iff.mpr rfl` under a name, and is inlined at its three uses. `step_of_halt` stays. The nondeterministic one is an equivalence about the relation, `Step c c' ↔ c' = c`, which cannot rewrite the term `step cfg`; the deterministic one is the equation that can, which is what makes it useful to `simp`. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 29 ++++++------------- .../Machines/Turing/MultiTape/TapeLemmas.lean | 4 +-- 2 files changed, 11 insertions(+), 22 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index f4821eef1..0937ef519 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -155,34 +155,24 @@ Everything below about a deterministic machine rests on this. -/ theorem step_iff {c c' : Cfg k Symbol State input} : tm.Step c c' ↔ c' = tm.step c := Cfg.stepWith_iff (by simp) -/-- A machine's own step is one of its steps. Applying a result about `MultiTapeNTM.Step` to -this is how the deterministic machine inherits it. -/ -@[simp] -lemma step_step (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) : - tm.Step c (tm.step c) := step_iff.mpr rfl - /-- A halted configuration steps to itself, inherited from `MultiTapeNTM`. -/ @[simp] lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : tm.step cfg = cfg := - (MultiTapeNTM.step_of_halt h).mp (tm.step_step cfg) + (MultiTapeNTM.step_of_halt h).mp (step_iff.mpr rfl) /-- The configuration reached by running the Turing machine for `t` steps from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ -def runFrom (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg +def runFrom (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) : + ℕ → Cfg k Symbol State input + | 0 => cfg + | t + 1 => tm.step (tm.runFrom cfg t) @[simp] -lemma runFrom_zero {cfg : Cfg k Symbol State input} : - tm.runFrom cfg 0 = cfg := by - simp [runFrom] - -lemma runFrom_succ_eq_step {cfg : Cfg k Symbol State input} {t : ℕ} : - tm.runFrom cfg (t + 1) = tm.runFrom (tm.step cfg) t := by - simp [runFrom, Function.iterate_succ_apply] +lemma runFrom_zero {cfg : Cfg k Symbol State input} : tm.runFrom cfg 0 = cfg := rfl lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : - tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by - simp [runFrom, Function.iterate_succ_apply'] + tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := rfl @[simp] lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : @@ -366,15 +356,14 @@ lemma relatesInSteps_iff_runFrom_eq (cfg₁ cfg₂ : Cfg k Symbol State input) (t : ℕ) : RelatesInSteps tm.Step cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by - unfold runFrom induction t generalizing cfg₁ cfg₂ with | zero => simp | succ t ih => - rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply'] + rw [RelatesInSteps.succ_iff, runFrom_succ_eq_step'] constructor · grind [step_iff] · intro h_runFrom - use tm.step^[t] cfg₁ + use tm.runFrom cfg₁ t grind [step_iff] diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index bfeecb5c0..76116d073 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -57,7 +57,7 @@ lemma uIcc_workTapePos_subset_visitedByTapeHead | succ t ih => intro z hz have hstep : |(tm.runFrom cfg (t + 1)).workTapePos i - (tm.runFrom cfg t).workTapePos i| ≤ 1 := - runFrom_succ_eq_step' (tm := tm) ▸ MultiTapeNTM.workTapePos_step_le (tm.step_step _) i + runFrom_succ_eq_step' (tm := tm) ▸ MultiTapeNTM.workTapePos_step_le (step_iff.mpr rfl) i have hmono := tm.visitedByTapeHead_mono cfg i (Nat.le_succ t) have hself := tm.mem_visitedByTapeHead_self cfg (t + 1) i grind [Finset.mem_uIcc] @@ -76,7 +76,7 @@ lemma mem_visitedByTapeHead_of_workTapes_ne by_cases hz : z = (tm.runFrom cfg t).workTapePos j · exact hz ▸ tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (tm.mem_visitedByTapeHead_self cfg t j) - · rw [MultiTapeNTM.workTapes_step_eq_of_ne (tm.step_step _) j z hz] at h + · rw [MultiTapeNTM.workTapes_step_eq_of_ne (step_iff.mpr rfl) j z hz] at h exact tm.visitedByTapeHead_mono cfg j (Nat.le_succ t) (ih h) /-- Every position visited by the head of tape `i` lies within `spaceUsedByTape … i` of the From 2e2d441b2d3e5728ea60b142f1ad5d9242a5769d Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sun, 30 Aug 2026 20:03:47 +0300 Subject: [PATCH 13/18] refactor(MultiTape): move the uniqueness of a run to the machine it is about MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `runFrom` goes back to iterating `step` with `^[·]`. The deterministic file carried four lemmas saying a computation path follows `runFrom`, all in service of `computesInExactTimeAndSpace_iff_runFrom`. What they rest on is not `runFrom` but the uniqueness of a step, so it is stated of `MultiTapeNTM`: a machine whose steps are unique has one run of each length from a given configuration, `ComputationPath.cfgs_eq`. The deterministic file supplies that uniqueness, which `step_iff` gives in a line, and reads the measures off its own run. `path_getElem`, `path_cfgs`, `path_last` and `path_space` are gone. `ComputesInExactTimeAndSpace` was never redefined here: it is the nondeterministic notion, and the theorem states it by step index. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 56 +++++++------------ .../Turing/MultiTape/Nondeterministic.lean | 23 ++++++++ 2 files changed, 42 insertions(+), 37 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 0937ef519..d31e1d151 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -74,7 +74,7 @@ We define a number of structures and concepts related to multi-tape Turing machi the space of that run * `step_iff`: the inherited `Step` is the graph of `step` * `computesInExactTimeAndSpace_iff_runFrom`: the inherited `ComputesInExactTimeAndSpace`, stated - by step index rather than by computation path + by step index rather than by computation path, via `ComputationPath.cfgs_eq` * `ComputableInTimeAndSpace`: a proof that there is a multi-tape TM that computes a function (on strings) respecting a time and space bound in the input length. * `DecidableInTimeAndSpace`: a proof that a TM decides a language within a certain time @@ -163,16 +163,15 @@ lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : /-- The configuration reached by running the Turing machine for `t` steps from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ -def runFrom (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) : - ℕ → Cfg k Symbol State input - | 0 => cfg - | t + 1 => tm.step (tm.runFrom cfg t) +def runFrom (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg @[simp] -lemma runFrom_zero {cfg : Cfg k Symbol State input} : tm.runFrom cfg 0 = cfg := rfl +lemma runFrom_zero {cfg : Cfg k Symbol State input} : tm.runFrom cfg 0 = cfg := by + simp [runFrom] lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : - tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := rfl + tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by + simp [runFrom, Function.iterate_succ_apply'] @[simp] lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : @@ -267,32 +266,6 @@ lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : end Space -/-- A computation path of `tm` has no choice but to follow `runFrom`. -/ -lemma path_getElem {p : tm.ComputationPath input} - (i : ℕ) (h : i < p.cfgs.length) : p.cfgs[i] = tm.runFrom p.start i := by - induction i with - | zero => simp [MultiTapeNTM.ComputationPath.start, List.getElem_zero] - | succ n ih => - have hstep := List.isChain_iff_getElem.mp p.isChain n h - rw [step_iff.mp hstep, ih (by omega), ← runFrom_succ_eq_step'] - -lemma path_cfgs {p : tm.ComputationPath input} : - p.cfgs = (List.range (p.time + 1)).map (tm.runFrom p.start) := by - refine List.ext_getElem (by simp [p.length_cfgs]) fun i h₁ h₂ => ?_ - simpa using path_getElem i h₁ - -/-- It ends where `tm` is after that many steps. -/ -lemma path_last {p : tm.ComputationPath input} : - p.last = tm.runFrom p.start p.time := by - rw [MultiTapeNTM.ComputationPath.last, List.getLast_eq_getElem, - path_getElem _ (by have := p.length_pos; omega)] - rfl - -/-- Its space is the space `tm` uses over the same number of steps. -/ -lemma path_space {p : tm.ComputationPath input} : - p.space = tm.spaceUsed p.start p.time := by - rw [MultiTapeNTM.ComputationPath.space, path_cfgs, ← spaceUsed_eq_spaceUsedOfCfgs] - /-- `tm` has exactly one computation path of each length, so `ComputesInExactTimeAndSpace`, inherited from `MultiTapeNTM`, is the direct statement about `runFrom` and `spaceUsed` at step `t`. -/ @@ -303,8 +276,16 @@ theorem computesInExactTimeAndSpace_iff_runFrom {input output : List Symbol} {t tm.spaceUsed (tm.initCfg input) t = s := by constructor · rintro ⟨p, hstart, hhalt, hout, rfl, hspace⟩ - rw [path_last, hstart] at hhalt hout - rw [path_space, hstart] at hspace + have h : p.cfgs = (tm.runPath (tm.initCfg input) p.time).cfgs := + MultiTapeNTM.ComputationPath.cfgs_eq + (fun h₁ h₂ => (step_iff.mp h₁).trans (step_iff.mp h₂).symm) + (by simpa using hstart) (by simp) + have hlast : p.last = tm.runFrom (tm.initCfg input) p.time := by + rw [MultiTapeNTM.ComputationPath.last]; simp [h] + have hsp : p.space = tm.spaceUsed (tm.initCfg input) p.time := by + rw [MultiTapeNTM.ComputationPath.space, h]; rfl + rw [hlast] at hhalt hout + rw [hsp] at hspace exact ⟨hhalt, hout, hspace⟩ · rintro ⟨hhalt, hout, hspace⟩ exact ⟨tm.runPath (tm.initCfg input) t, by simp, by simpa using hhalt, by simpa using hout, @@ -356,14 +337,15 @@ lemma relatesInSteps_iff_runFrom_eq (cfg₁ cfg₂ : Cfg k Symbol State input) (t : ℕ) : RelatesInSteps tm.Step cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by + unfold runFrom induction t generalizing cfg₁ cfg₂ with | zero => simp | succ t ih => - rw [RelatesInSteps.succ_iff, runFrom_succ_eq_step'] + rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply'] constructor · grind [step_iff] · intro h_runFrom - use tm.runFrom cfg₁ t + use tm.step^[t] cfg₁ grind [step_iff] diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 3852dda1d..939560937 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -38,6 +38,7 @@ witness. * `ComputationPath`: a run of the machine: a non-empty list of configurations, each reached from the previous by a step, with `start` and `last` read off it * `ComputationPath.space_le`: a machine touches at most `k` cells per step +* `ComputationPath.cfgs_eq`: a machine whose steps are unique has one run of each length * `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint * `Computes`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`: its instances, whose @@ -152,6 +153,28 @@ theorem space_le (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := end ComputationPath +/-- A machine whose steps are unique has at most one run of a given length from a given +configuration: the two agree configuration by configuration. -/ +theorem ComputationPath.getElem_eq + (hdet : ∀ {c c' c'' : Cfg k Symbol State input}, ntm.Step c c' → ntm.Step c c'' → c' = c'') + {p q : ntm.ComputationPath input} (hs : p.start = q.start) (i : ℕ) + (h₁ : i < p.cfgs.length) (h₂ : i < q.cfgs.length) : p.cfgs[i] = q.cfgs[i] := by + induction i with + | zero => simpa [ComputationPath.start, List.getElem_zero] using hs + | succ n ih => + have hp := List.isChain_iff_getElem.mp p.isChain n h₁ + have hq := List.isChain_iff_getElem.mp q.isChain n h₂ + rw [ih (by omega) (by omega)] at hp + exact hdet hp hq + +/-- Such a machine has at most one run of a given length from a given configuration. -/ +theorem ComputationPath.cfgs_eq + (hdet : ∀ {c c' c'' : Cfg k Symbol State input}, ntm.Step c c' → ntm.Step c c'' → c' = c'') + {p q : ntm.ComputationPath input} (hs : p.start = q.start) (ht : p.time = q.time) : + p.cfgs = q.cfgs := + List.ext_getElem (by rw [p.length_cfgs, q.length_cfgs, ht]) + fun i h₁ h₂ => ComputationPath.getElem_eq hdet hs i h₁ h₂ + /-- `ntm` has a computation on `input` that starts at the initial configuration, halts, emits `output` and satisfies `P`. The notions below are its instances, so their constraints all refer to a single computation. -/ From bd89f5e02a360408b7049cf502d41014fc706dfe Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sun, 30 Aug 2026 20:14:32 +0300 Subject: [PATCH 14/18] refactor(MultiTape): define runFrom as the end of the machine's run A run is now built rather than described. `ComputationPath.single` is the run of no steps and `ComputationPath.concat` extends one by a step, so the machine's own run is a recursion on the number of steps, and `runFrom` is the configuration it ends in. `spaceUsed` was already the run's space, so both measures are now read off the same object. Uniqueness is stated of the general machine and as an equality of runs, not just of their configurations: a machine whose steps are unique has exactly one run of each length from each configuration, `ComputationPath.eq_of_start_of_time`. That is what removes the existential. `ComputesInExactTimeAndSpace` quantifies over runs, as it must for a machine with a choice; for one without, the run in question is the machine's own, and `computesInExactTimeAndSpace_iff_runFrom` says so with nothing existential left. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 88 +++++++++---------- .../Turing/MultiTape/Nondeterministic.lean | 58 +++++++++++- .../Machines/Turing/MultiTape/TapeLemmas.lean | 8 +- 3 files changed, 102 insertions(+), 52 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index d31e1d151..892c7ae15 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -161,17 +161,27 @@ lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : tm.step cfg = cfg := (MultiTapeNTM.step_of_halt h).mp (step_iff.mpr rfl) -/-- The configuration reached by running the Turing machine for `t` steps from `cfg`. -If the Turing machine halts, it will stay at the halting configuration. -/ -def runFrom (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg +/-- The machine's own run from `cfg` for `t` steps: it does nothing, or takes one more step. -/ +def runPath (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) : + ℕ → tm.ComputationPath input + | 0 => .single cfg + | t + 1 => (tm.runPath cfg t).concat (tm.step (tm.runPath cfg t).last) (step_iff.mpr rfl) + +/-- The configuration reached by running the Turing machine for `t` steps from `cfg`: the one its +run ends in. If the Turing machine halts, it will stay at the halting configuration. -/ +def runFrom (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : + Cfg k Symbol State input := (tm.runPath cfg t).last + +@[simp] +lemma runPath_last (cfg : Cfg k Symbol State input) (t : ℕ) : + (tm.runPath cfg t).last = tm.runFrom cfg t := rfl @[simp] -lemma runFrom_zero {cfg : Cfg k Symbol State input} : tm.runFrom cfg 0 = cfg := by - simp [runFrom] +lemma runFrom_zero {cfg : Cfg k Symbol State input} : tm.runFrom cfg 0 = cfg := rfl lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by - simp [runFrom, Function.iterate_succ_apply'] + simp only [runFrom, runPath, MultiTapeNTM.ComputationPath.concat_last] @[simp] lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : @@ -195,40 +205,29 @@ that there is no choice to make: `Step` is the graph of `step`, so a computation follow `runFrom`, and `runPath` shows there is one of every length. -/ -/-- The configurations the machine passes through form a chain of steps. -/ -lemma isChain_map_range (cfg : Cfg k Symbol State input) (t : ℕ) : - ((List.range (t + 1)).map (tm.runFrom cfg)).IsChain tm.Step := by - rw [List.isChain_iff_getElem] - intro i hi - simp only [List.getElem_map, List.getElem_range] - rw [runFrom_succ_eq_step'] - exact step_iff.mpr rfl - -/-- The machine's own run from `cfg` for `t` steps, as a computation path. -/ -def runPath (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.ComputationPath input where - cfgs := (List.range (t + 1)).map (tm.runFrom cfg) - ne_nil := by simp - isChain := isChain_map_range _ t - +/-- Its run takes `t` steps. -/ @[simp] -lemma runPath_cfgs (cfg : Cfg k Symbol State input) (t : ℕ) : - (tm.runPath cfg t).cfgs = (List.range (t + 1)).map (tm.runFrom cfg) := rfl +lemma runPath_time (cfg : Cfg k Symbol State input) (t : ℕ) : (tm.runPath cfg t).time = t := by + induction t with + | zero => rfl + | succ n ih => simp [runPath, ih] +/-- Its run starts where it was asked to. -/ @[simp] lemma runPath_start (cfg : Cfg k Symbol State input) (t : ℕ) : (tm.runPath cfg t).start = cfg := by - simp [MultiTapeNTM.ComputationPath.start, List.head_map] - -@[simp] -lemma runPath_last (cfg : Cfg k Symbol State input) (t : ℕ) : - (tm.runPath cfg t).last = tm.runFrom cfg t := by - rw [MultiTapeNTM.ComputationPath.last, ← Option.some_inj, ← List.getLast?_eq_some_getLast] - simp [List.range_succ] + induction t with + | zero => rfl + | succ n ih => simp [runPath, ih] -@[simp] -lemma runPath_time (cfg : Cfg k Symbol State input) (t : ℕ) : (tm.runPath cfg t).time = t := by - simp [MultiTapeNTM.ComputationPath.time] +/-- Its run passes through the configurations reached after each step. -/ +lemma runPath_cfgs (cfg : Cfg k Symbol State input) (t : ℕ) : + (tm.runPath cfg t).cfgs = (List.range (t + 1)).map (tm.runFrom cfg) := by + induction t with + | zero => rfl + | succ n ih => + rw [runPath, MultiTapeNTM.ComputationPath.concat_cfgs, ih] + simp [List.range_succ, runFrom_succ_eq_step'] section Space /-! Space is read off the machine's own run, so it is the space of a `ComputationPath`. -/ @@ -262,7 +261,8 @@ lemma spaceUsed_eq_sum (cfg : Cfg k Symbol State input) (t : ℕ) : /-- The space used up to step `t` is the space touched by the configurations up to step `t`. -/ lemma spaceUsed_eq_spaceUsedOfCfgs (cfg : Cfg k Symbol State input) (t : ℕ) : - tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := rfl + tm.spaceUsed cfg t = spaceUsedOfCfgs ((List.range (t + 1)).map (tm.runFrom cfg)) := by + rw [spaceUsed, MultiTapeNTM.ComputationPath.space, runPath_cfgs] end Space @@ -276,17 +276,12 @@ theorem computesInExactTimeAndSpace_iff_runFrom {input output : List Symbol} {t tm.spaceUsed (tm.initCfg input) t = s := by constructor · rintro ⟨p, hstart, hhalt, hout, rfl, hspace⟩ - have h : p.cfgs = (tm.runPath (tm.initCfg input) p.time).cfgs := - MultiTapeNTM.ComputationPath.cfgs_eq + have hp : p = tm.runPath (tm.initCfg input) p.time := + MultiTapeNTM.ComputationPath.eq_of_start_of_time (fun h₁ h₂ => (step_iff.mp h₁).trans (step_iff.mp h₂).symm) (by simpa using hstart) (by simp) - have hlast : p.last = tm.runFrom (tm.initCfg input) p.time := by - rw [MultiTapeNTM.ComputationPath.last]; simp [h] - have hsp : p.space = tm.spaceUsed (tm.initCfg input) p.time := by - rw [MultiTapeNTM.ComputationPath.space, h]; rfl - rw [hlast] at hhalt hout - rw [hsp] at hspace - exact ⟨hhalt, hout, hspace⟩ + rw [hp] at hhalt hout hspace + exact ⟨by simpa using hhalt, by simpa using hout, by simpa using hspace⟩ · rintro ⟨hhalt, hout, hspace⟩ exact ⟨tm.runPath (tm.initCfg input) t, by simp, by simpa using hhalt, by simpa using hout, by simp, by simpa using hspace⟩ @@ -337,15 +332,14 @@ lemma relatesInSteps_iff_runFrom_eq (cfg₁ cfg₂ : Cfg k Symbol State input) (t : ℕ) : RelatesInSteps tm.Step cfg₁ cfg₂ t ↔ tm.runFrom cfg₁ t = cfg₂ := by - unfold runFrom induction t generalizing cfg₁ cfg₂ with | zero => simp | succ t ih => - rw [RelatesInSteps.succ_iff, Function.iterate_succ_apply'] + rw [RelatesInSteps.succ_iff, runFrom_succ_eq_step'] constructor · grind [step_iff] · intro h_runFrom - use tm.step^[t] cfg₁ + use tm.runFrom cfg₁ t grind [step_iff] diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 939560937..55db9b472 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -38,7 +38,9 @@ witness. * `ComputationPath`: a run of the machine: a non-empty list of configurations, each reached from the previous by a step, with `start` and `last` read off it * `ComputationPath.space_le`: a machine touches at most `k` cells per step -* `ComputationPath.cfgs_eq`: a machine whose steps are unique has one run of each length +* `ComputationPath.single`, `ComputationPath.concat`: the runs of no steps and of one more +* `ComputationPath.eq_of_start_of_time`: a machine whose steps are unique has exactly one run of + each length from each configuration * `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint * `Computes`, `ComputesInExactTime`, `ComputesInExactSpace`, `ComputesInExactTimeAndSpace`: its instances, whose @@ -153,6 +155,53 @@ theorem space_le (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := end ComputationPath +/-- The run that does nothing. -/ +def ComputationPath.single {ntm : MultiTapeNTM k Symbol State} (c : Cfg k Symbol State input) : + ntm.ComputationPath input where + cfgs := [c] + ne_nil := by simp + isChain := by simp + +/-- Extend a run by one step at its end. -/ +def ComputationPath.concat (p : ntm.ComputationPath input) (c : Cfg k Symbol State input) + (h : ntm.Step p.last c) : ntm.ComputationPath input where + cfgs := p.cfgs ++ [c] + ne_nil := by simp + isChain := List.isChain_append.mpr ⟨p.isChain, by simp, by + intro x hx y hy + rw [List.getLast?_eq_some_getLast p.ne_nil] at hx + simp only [List.head?_cons, Option.mem_def, Option.some.injEq] at hx hy + subst hx; subst hy + exact h⟩ + +@[simp] lemma ComputationPath.single_cfgs (c : Cfg k Symbol State input) : + (single (ntm := ntm) c).cfgs = [c] := rfl + +@[simp] lemma ComputationPath.single_start (c : Cfg k Symbol State input) : + (single (ntm := ntm) c).start = c := rfl + +@[simp] lemma ComputationPath.single_last (c : Cfg k Symbol State input) : + (single (ntm := ntm) c).last = c := rfl + +@[simp] lemma ComputationPath.single_time (c : Cfg k Symbol State input) : + (single (ntm := ntm) c).time = 0 := rfl + +@[simp] lemma ComputationPath.concat_cfgs (p : ntm.ComputationPath input) (c) (h) : + (p.concat c h).cfgs = p.cfgs ++ [c] := rfl + +@[simp] lemma ComputationPath.concat_last (p : ntm.ComputationPath input) (c) (h) : + (p.concat c h).last = c := by simp [concat, last] + +@[simp] lemma ComputationPath.concat_start (p : ntm.ComputationPath input) (c) (h) : + (p.concat c h).start = p.start := by + simp [concat, start, List.head_append_of_ne_nil p.ne_nil] + +@[simp] lemma ComputationPath.concat_time (p : ntm.ComputationPath input) (c) (h) : + (p.concat c h).time = p.time + 1 := by + have := p.length_pos + simp only [concat, time, List.length_append, List.length_cons, List.length_nil] + omega + /-- A machine whose steps are unique has at most one run of a given length from a given configuration: the two agree configuration by configuration. -/ theorem ComputationPath.getElem_eq @@ -175,6 +224,13 @@ theorem ComputationPath.cfgs_eq List.ext_getElem (by rw [p.length_cfgs, q.length_cfgs, ht]) fun i h₁ h₂ => ComputationPath.getElem_eq hdet hs i h₁ h₂ +/-- Such a machine has exactly one run of a given length from a given configuration. -/ +theorem ComputationPath.eq_of_start_of_time + (hdet : ∀ {c c' c'' : Cfg k Symbol State input}, ntm.Step c c' → ntm.Step c c'' → c' = c'') + {p q : ntm.ComputationPath input} (hs : p.start = q.start) (ht : p.time = q.time) : p = q := by + cases p; cases q; simp_all only [ComputationPath.mk.injEq] + exact cfgs_eq hdet hs ht + /-- `ntm` has a computation on `input` that starts at the initial configuration, halts, emits `output` and satisfies `P`. The notions below are its instances, so their constraints all refer to a single computation. -/ diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 76116d073..80f04bbb1 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -33,7 +33,7 @@ variable {cfg : Cfg k Symbol State input} lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.runFrom cfg t').workTapePos i = z := by - simp [visitedByTapeHead, visitedOfCfgs] + simp [visitedByTapeHead, visitedOfCfgs, runPath_cfgs] lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : (tm.runFrom cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i := @@ -53,7 +53,7 @@ lemma uIcc_workTapePos_subset_visitedByTapeHead Finset.uIcc (cfg.workTapePos i) ((tm.runFrom cfg t).workTapePos i) ⊆ tm.visitedByTapeHead cfg t i := by induction t with - | zero => simpa [runFrom] using tm.mem_visitedByTapeHead_self cfg 0 i + | zero => simpa using tm.mem_visitedByTapeHead_self cfg 0 i | succ t ih => intro z hz have hstep : |(tm.runFrom cfg (t + 1)).workTapePos i - (tm.runFrom cfg t).workTapePos i| ≤ 1 := @@ -70,7 +70,7 @@ lemma mem_visitedByTapeHead_of_workTapes_ne (h : (tm.runFrom cfg t).workTapes j z ≠ cfg.workTapes j z) : z ∈ tm.visitedByTapeHead cfg t j := by induction t with - | zero => exact absurd (by simp [runFrom]) h + | zero => exact absurd (by simp) h | succ t ih => rw [runFrom_succ_eq_step'] at h by_cases hz : z = (tm.runFrom cfg t).workTapePos j @@ -111,7 +111,7 @@ lemma content_natAbs_le_spaceUsedByTape lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : tm.spaceUsedByTape cfg t i ≤ t + 1 := by unfold spaceUsedByTape visitedByTapeHead visitedOfCfgs - exact (List.toFinset_card_le _).trans (by simp) + exact (List.toFinset_card_le _).trans (by simp [MultiTapeNTM.ComputationPath.length_cfgs]) /-- The space used by a computation is bounded linearly by the number of steps. This is `ComputationPath.space_le` read off the machine's own run. -/ From c7b8c52944a4ad262f40ab2f5c681ef606df5fa0 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sun, 30 Aug 2026 20:19:37 +0300 Subject: [PATCH 15/18] feat(MultiTapeTM): give runFrom both descriptions, and run it by the fast one Building the run says what running is; iterating `step` says how to do it. `runFrom_eq_iterate` states they agree, so the `Function.iterate` API is available on `runFrom` again, and a `csimp` lemma has the compiler evaluate it by iteration rather than by building a list of configurations. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Deterministic.lean | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 892c7ae15..beaeaddee 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -70,6 +70,7 @@ We define a number of structures and concepts related to multi-tape Turing machi * `MultiTapeTM`: the TM itself, a `MultiTapeNTM` whose transition relation is a function * `ofTr`: the machine with a given initial state and transition function * `runPath`: the machine's own run from a configuration, as a `ComputationPath` +* `runFrom`: the configuration that run ends in, equal to iterating `step` (`runFrom_eq_iterate`) * `spaceUsed`: the number of tape cells touched by work tape heads, our main space measure; the space of that run * `step_iff`: the inherited `Step` is the graph of `step` @@ -183,6 +184,25 @@ lemma runFrom_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : tm.runFrom cfg (t + 1) = tm.step (tm.runFrom cfg t) := by simp only [runFrom, runPath, MultiTapeNTM.ComputationPath.concat_last] +/-- The run ends where iterating `step` lands. Building the run says what running *is*; iterating +says how to *do* it, and carries the `Function.iterate` API. -/ +theorem runFrom_eq_iterate (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) + (t : ℕ) : tm.runFrom cfg t = tm.step^[t] cfg := by + induction t with + | zero => simp + | succ n ih => + rw [runFrom_succ_eq_step', ih] + exact (Function.iterate_succ_apply' _ _ _).symm + +/-- How `runFrom` is evaluated: iterating `step`, rather than building the run it ends. -/ +def runFromIter (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State input) (t : ℕ) : + Cfg k Symbol State input := tm.step^[t] cfg + +@[csimp] +theorem runFrom_eq_runFromIter : @runFrom = @runFromIter := by + funext k State Symbol input tm cfg t + exact tm.runFrom_eq_iterate cfg t + @[simp] lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : tm.runFrom cfg n = cfg := by From d4ca3f517b6a9b200c31b4c7d3ff539a22f8637c Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sun, 30 Aug 2026 20:32:42 +0300 Subject: [PATCH 16/18] refactor(MultiTape): shorten the chain obligation when extending a run Appending a configuration leaves one thing to check, that the run's last configuration steps to it, which is the hypothesis. Co-Authored-By: Claude Opus 5 (1M context) --- .../Machines/Turing/MultiTape/Nondeterministic.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 55db9b472..cbc8c1598 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -167,12 +167,9 @@ def ComputationPath.concat (p : ntm.ComputationPath input) (c : Cfg k Symbol Sta (h : ntm.Step p.last c) : ntm.ComputationPath input where cfgs := p.cfgs ++ [c] ne_nil := by simp - isChain := List.isChain_append.mpr ⟨p.isChain, by simp, by - intro x hx y hy - rw [List.getLast?_eq_some_getLast p.ne_nil] at hx - simp only [List.head?_cons, Option.mem_def, Option.some.injEq] at hx hy - subst hx; subst hy - exact h⟩ + isChain := by + simpa [List.isChain_append, List.getLast?_eq_some_getLast p.ne_nil, + ComputationPath.last] using ⟨p.isChain, h⟩ @[simp] lemma ComputationPath.single_cfgs (c : Cfg k Symbol State input) : (single (ntm := ntm) c).cfgs = [c] := rfl From 4b7e60ea16476797286d7d99ae5e588f9b958c6b Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sun, 30 Aug 2026 20:42:11 +0300 Subject: [PATCH 17/18] feat(MultiTape): reason about a run by induction on how it was built A run is a list, so proving something of every run meant reasoning about indices. `ComputationPath.induction` gives it the induction of an inductive definition instead: a run is the run of no steps, or one more step on a shorter run. The representation is unchanged, so the list API that `space` and uniqueness rest on still applies; only the way to reason about a run is added. `ComputationPath.reflTransGen`, that a run reaches its last configuration from its first, is the first thing proved that way. `IsChainFromTo` supplied it before the endpoints stopped being part of a run. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Nondeterministic.lean | 29 ++++++++++++++++++- 1 file changed, 28 insertions(+), 1 deletion(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index cbc8c1598..7e0d7bb50 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -38,7 +38,9 @@ witness. * `ComputationPath`: a run of the machine: a non-empty list of configurations, each reached from the previous by a step, with `start` and `last` read off it * `ComputationPath.space_le`: a machine touches at most `k` cells per step -* `ComputationPath.single`, `ComputationPath.concat`: the runs of no steps and of one more +* `ComputationPath.single`, `ComputationPath.concat`: the runs of no steps and of one more, + with `ComputationPath.induction` to reason by cases on the two +* `ComputationPath.reflTransGen`: a run reaches its last configuration from its first * `ComputationPath.eq_of_start_of_time`: a machine whose steps are unique has exactly one run of each length from each configuration * `ComputesSuchThat`: some computation halts, emits a given output and meets a given constraint @@ -199,6 +201,31 @@ def ComputationPath.concat (p : ntm.ComputationPath input) (c : Cfg k Symbol Sta simp only [concat, time, List.length_append, List.length_cons, List.length_nil] omega +/-- Every run is either the run of no steps, or one more step on a shorter run. This gives runs +the induction of an inductive definition while they stay lists. -/ +@[elab_as_elim] +theorem ComputationPath.induction {motive : ntm.ComputationPath input → Prop} + (single : ∀ c, motive (ComputationPath.single c)) + (concat : ∀ (p : ntm.ComputationPath input) c h, motive p → motive (p.concat c h)) + (p : ntm.ComputationPath input) : motive p := by + obtain ⟨cfgs, ne_nil, isChain⟩ := p + induction cfgs using List.reverseRecOn with + | nil => exact absurd rfl ne_nil + | append_singleton l a ih => + rcases eq_or_ne l [] with rfl | hl + · exact single a + · have h : l.IsChain ntm.Step ∧ ntm.Step (l.getLast hl) a := by + simpa [List.isChain_append, List.getLast?_eq_some_getLast hl] using isChain + exact concat ⟨l, hl, h.1⟩ a h.2 (ih hl h.1) + +/-- A run witnesses that its last configuration is reachable from the one it starts at. -/ +theorem ComputationPath.reflTransGen (p : ntm.ComputationPath input) : + Relation.ReflTransGen ntm.Step p.start p.last := by + induction p using ComputationPath.induction with + | single c => simp only [ComputationPath.single_start, ComputationPath.single_last] + exact .refl + | concat p c h ih => simpa using ih.tail (by simpa using h) + /-- A machine whose steps are unique has at most one run of a given length from a given configuration: the two agree configuration by configuration. -/ theorem ComputationPath.getElem_eq From 8b35593358461ca90bee8d97171cdde84ce60b60 Mon Sep 17 00:00:00 2001 From: Aviv Bar Natan Date: Sun, 30 Aug 2026 20:50:10 +0300 Subject: [PATCH 18/18] refactor(MultiTape): collect the tape lemmas, and say what the space bound bounds `workTapePos_step_le` and `workTapes_step_eq_of_ne` are lemmas about what a step does to a tape, so they join the others in `TapeLemmas`, stated of any machine. `space_le` becomes `space_le_linear`, matching `spaceUsed_linear`, which it now proves. Co-Authored-By: Claude Opus 5 (1M context) --- .../Turing/MultiTape/Nondeterministic.lean | 28 ++----------- .../Machines/Turing/MultiTape/TapeLemmas.lean | 39 +++++++++++++++++-- 2 files changed, 38 insertions(+), 29 deletions(-) diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean index 7e0d7bb50..21b4caf37 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean @@ -32,12 +32,10 @@ witness. ## Important Declarations * `MultiTapeNTM`: the machine, an initial state and a transition relation -* `Step`: the one-step relation on configurations, moving a head by at most one cell - (`workTapePos_step_le`) and changing no cell but the one under it - (`workTapes_step_eq_of_ne`) +* `Step`: the one-step relation on configurations * `ComputationPath`: a run of the machine: a non-empty list of configurations, each reached from the previous by a step, with `start` and `last` read off it -* `ComputationPath.space_le`: a machine touches at most `k` cells per step +* `ComputationPath.space_le_linear`: a machine touches at most `k` cells per step * `ComputationPath.single`, `ComputationPath.concat`: the runs of no steps and of one more, with `ComputationPath.induction` to reason by cases on the two * `ComputationPath.reflTransGen`: a run reaches its last configuration from its first @@ -88,26 +86,6 @@ lemma step_of_halt {c c' : Cfg k Symbol State input} (h : c.Halted) : ntm.Step c c' ↔ c' = c := by simp [Step, Cfg.StepWith, h] -/-- A work tape head moves by at most one cell in a step. -/ -lemma workTapePos_step_le {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (i : Fin k) : - |c'.workTapePos i - c.workTapePos i| ≤ 1 := by - cases hq : c.state with - | none => simp_all [Step, Cfg.StepWith] - | some q => - simp only [Step, Cfg.StepWith, hq] at h - obtain ⟨a, -, rfl⟩ := h - exact workTapePos_apply_le a c i - -/-- A step changes no work tape cell but the one its head is on. -/ -lemma workTapes_step_eq_of_ne {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (j : Fin k) - (z : ℤ) (hz : z ≠ c.workTapePos j) : c'.workTapes j z = c.workTapes j z := by - cases hq : c.state with - | none => simp_all [Step, Cfg.StepWith] - | some q => - simp only [Step, Cfg.StepWith, hq] at h - obtain ⟨a, -, rfl⟩ := h - exact workTapes_apply_eq_of_ne a c j z hz - /-- The initial configuration corresponding to an input string. -/ @[simp] def initCfg (ntm : MultiTapeNTM k Symbol State) (input : List Symbol) : @@ -151,7 +129,7 @@ lemma length_cfgs (p : ntm.ComputationPath input) : p.cfgs.length = p.time + 1 : omega /-- A machine touches at most `k` cells per step, whether or not it is deterministic. -/ -theorem space_le (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := by +theorem space_le_linear (p : ntm.ComputationPath input) : p.space ≤ k * p.time + k := by calc p.space ≤ k * p.cfgs.length := spaceUsedOfCfgs_le _ _ = k * p.time + k := by rw [p.length_cfgs, Nat.mul_succ] diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index 80f04bbb1..5b1a5b5a3 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -23,7 +23,36 @@ Those measures are read off the machine's own run, so results that hold of any r @[expose] public section -namespace Turing.MultiTapeTM +namespace Turing + +namespace MultiTapeNTM + +variable {k : ℕ} {State Symbol : Type*} {input : List Symbol} + {ntm : MultiTapeNTM k Symbol State} + +/-- A work tape head moves by at most one cell in a step. -/ +lemma workTapePos_step_le {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (i : Fin k) : + |c'.workTapePos i - c.workTapePos i| ≤ 1 := by + cases hq : c.state with + | none => simp_all [Step, Cfg.StepWith] + | some q => + simp only [Step, Cfg.StepWith, hq] at h + obtain ⟨a, -, rfl⟩ := h + exact workTapePos_apply_le a c i + +/-- A step changes no work tape cell but the one its head is on. -/ +lemma workTapes_step_eq_of_ne {c c' : Cfg k Symbol State input} (h : ntm.Step c c') (j : Fin k) + (z : ℤ) (hz : z ≠ c.workTapePos j) : c'.workTapes j z = c.workTapes j z := by + cases hq : c.state with + | none => simp_all [Step, Cfg.StepWith] + | some q => + simp only [Step, Cfg.StepWith, hq] at h + obtain ⟨a, -, rfl⟩ := h + exact workTapes_apply_eq_of_ne a c j z hz + +end MultiTapeNTM + +namespace MultiTapeTM variable {k : ℕ} variable {State Symbol : Type*} @@ -114,10 +143,10 @@ lemma spaceUsedByTape_le (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) exact (List.toFinset_card_le _).trans (by simp [MultiTapeNTM.ComputationPath.length_cfgs]) /-- The space used by a computation is bounded linearly by the number of steps. This is -`ComputationPath.space_le` read off the machine's own run. -/ +`ComputationPath.space_le_linear` read off the machine's own run. -/ lemma spaceUsed_linear (cfg : Cfg k Symbol State input) (t : ℕ) : tm.spaceUsed cfg t ≤ k * t + k := by - simpa using (tm.runPath cfg t).space_le + simpa using (tm.runPath cfg t).space_le_linear /-- The space used by a single tape is monotone in the number of steps. -/ lemma spaceUsedByTape_mono @@ -135,4 +164,6 @@ lemma spaceUsed_mono (tm : MultiTapeTM k Symbol State) (cfg : Cfg k Symbol State simp only [spaceUsed_eq_spaceUsedOfCfgs] exact spaceUsedOfCfgs_mono ((List.range_sublist.mpr (by omega)).map _) -end Turing.MultiTapeTM +end MultiTapeTM + +end Turing