diff --git a/Cslib.lean b/Cslib.lean index 6c20dd086..5c649af37 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -60,6 +60,8 @@ 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.Plumbing.Sequential +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes 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 index 78237a5b5..a366358b5 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean @@ -156,6 +156,18 @@ def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Sy /-- 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 same configuration in a different control state, possibly of a different state type. -/ +@[simps] def Cfg.withState (cfg : Cfg k Symbol State input) + {State' : Type*} (q : Option State') : Cfg k Symbol State' input := + ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩ + +/-- Remap the (optional) state of a configuration through `φ`, leaving the input head, the work +tapes, the work-tape heads and the output alone. This is the shape of embedding used to place a +sub-machine's configurations into a larger machine built from it. -/ +@[simps] def Cfg.mapState {State' : Type*} (φ : Option State → Option State') + (c : Cfg k Symbol State input) : Cfg k Symbol State' input := + ⟨φ c.state, c.inputPos, c.workTapes, c.workTapePos, c.output⟩ + /-- 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 := diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 602953c79..a587e2771 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -191,6 +191,26 @@ lemma runFrom_of_halt (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n tm.runFrom cfg n = cfg := Function.iterate_fixed (step_of_halt h) n +/-- Nothing changes after the machine has halted. -/ +lemma runFrom_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 = tm.runFrom cfg τ := by + conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] + rw [runFrom_add, runFrom_of_halt _ hhalt] + +/-- Every halted run has a first halting time no later than the supplied one. -/ +lemma exists_minimal_halting_time + (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k Symbol State input) (t : ℕ) + (hhalt : (tm.runFrom cfg t).state = none) : + ∃ u ≤ t, (tm.runFrom cfg u).state = none ∧ ∀ s < u, (tm.runFrom cfg s).state ≠ none := by + classical + have hex : ∃ n, (tm.runFrom cfg n).state = none := ⟨t, hhalt⟩ + exact ⟨Nat.find hex, Nat.find_min' hex hhalt, Nat.find_spec hex, + fun s hs => Nat.find_min hex hs⟩ + @[simp] lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) : tm.outputSymbol cfg = none := by diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean new file mode 100644 index 000000000..d5370bda1 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean @@ -0,0 +1,176 @@ +/- +Copyright (c) 2026 Christian Reitwiessner and Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes + +/-! +# Sequential composition of machines on shared tapes + +`seq tm₀ tm₁` behaves like `tm₀` until `tm₀` would halt, at which point it continues as `tm₁`, +started in its initial state on the tapes as `tm₀` left them. The state space is +`State₀ ⊕ State₁`, and the *halting transition* of the first phase is mapped to the initial state +of the second, so the handoff costs no extra step. + +At the specification level this is `transformsTapes_seq`: transformations compose, with the time +and space bounds adding. The postcondition of `TransformsTapes` is what makes the proof direct: +the first machine halts in a full `wordsCfg`, which is exactly a starting configuration for the +second. + +## Main results + +* `Turing.MultiTapeTM.seq`: the composed machine. +* `Turing.MultiTapeTM.transformsTapes_seq`: transformations compose, bounds adding. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State₀ State₁ : Type*} {input : List Symbol} + +/-- The sequential composition of `tm₀` and `tm₁`: it behaves like `tm₀` until `tm₀` would halt, +at which point it switches to the initial state of `tm₁` and behaves like `tm₁`. The switch is +folded into the halting transition of `tm₀`, so it costs no step. -/ +def seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) : + MultiTapeTM k Symbol (State₀ ⊕ State₁) where + q₀ := .inl tm₀.q₀ + tr q inp work := + match q with + | .inl q₀ => + let a := tm₀.tr q₀ inp work + { a with state := some (a.state.elim (.inr tm₁.q₀) .inl) } + | .inr q₁ => + let a := tm₁.tr q₁ inp work + { a with state := a.state.map .inr } + +variable {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁} + +namespace Sequential + +/-- A configuration of the first phase: a configuration of `tm₀`, with a halted state mapped to +the initial state of the second phase. Under this map, the whole first phase of `seq` mirrors the +run of `tm₀`, *including* its halting step. -/ +def leftCfg (tm₁ : MultiTapeTM k Symbol State₁) (cfg : Cfg k Symbol State₀ input) : + Cfg k Symbol (State₀ ⊕ State₁) input := + cfg.mapState (fun st => some (st.elim (.inr tm₁.q₀) .inl)) + +/-- A configuration of the second phase. Under this map, the second phase of `seq` mirrors the +run of `tm₁`. -/ +def rightCfg (cfg : Cfg k Symbol State₁ input) : + Cfg k Symbol (State₀ ⊕ State₁) input := + cfg.mapState (Option.map .inr) + +lemma step_leftCfg (cfg : Cfg k Symbol State₀ input) (h : cfg.state ≠ none) : + (tm₀.seq tm₁).step (leftCfg tm₁ cfg) = leftCfg tm₁ (tm₀.step cfg) := by + obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp h + have h1 : (leftCfg tm₁ cfg).state = some (Sum.inl q : State₀ ⊕ State₁) := by + simp [leftCfg, Cfg.mapState, hq] + simp only [step, h1, hq] + rfl + +lemma step_rightCfg (cfg : Cfg k Symbol State₁ input) : + (tm₀.seq tm₁).step (rightCfg cfg) = rightCfg (tm₁.step cfg) := by + cases hq : cfg.state with + | none => + have h1 : (rightCfg (State₀ := State₀) cfg).state = none := by simp [rightCfg, Cfg.mapState, hq] + simp only [step, h1, hq] + | some q => + have h1 : (rightCfg (State₀ := State₀) cfg).state = some (Sum.inr q : State₀ ⊕ State₁) := by + simp [rightCfg, hq] + simp only [step, h1, hq] + rfl + +/-- The second phase of `seq` mirrors the run of `tm₁`. -/ +lemma runFrom_rightCfg (cfg : Cfg k Symbol State₁ input) (n : ℕ) : + (tm₀.seq tm₁).runFrom (rightCfg cfg) n = rightCfg (tm₁.runFrom cfg n) := + runFrom_comm_of_step rightCfg (fun c => step_rightCfg c) cfg n + +/-- While `tm₀` is running, `seq` mirrors it. -/ +lemma runFrom_leftCfg (cfg : Cfg k Symbol State₀ input) (n : ℕ) + (h : ∀ m < n, (tm₀.runFrom cfg m).state ≠ none) : + (tm₀.seq tm₁).runFrom (leftCfg tm₁ cfg) n = leftCfg tm₁ (tm₀.runFrom cfg n) := by + induction n with + | zero => rfl + | succ n ih => + rw [runFrom_succ_eq_step', runFrom_succ_eq_step', ih fun m hm => h m (by omega), + step_leftCfg _ (h n (by omega))] + +@[simp] +lemma workTapePos_leftCfg (cfg : Cfg k Symbol State₀ input) : + (leftCfg tm₁ cfg).workTapePos = cfg.workTapePos := rfl + +@[simp] +lemma workTapePos_rightCfg (cfg : Cfg k Symbol State₁ input) : + (rightCfg (State₀ := State₀) cfg).workTapePos = cfg.workTapePos := rfl + +end Sequential + +open Sequential in +/-- **Sequential composition of transformations.** If the postcondition of the first +transformation implies the precondition of the second, the composed machine performs the two +transformations one after the other, with the time and space bounds adding. -/ +theorem transformsTapes_seq + {P₀ P₁ : (input : List Symbol) → (Fin k → List Symbol) → Prop} + {Q₀ Q₁ : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop} + {t₀ s₀ t₁ s₁ : ℕ} + (h₀ : TransformsTapes tm₀ P₀ Q₀ t₀ s₀) (h₁ : TransformsTapes tm₁ P₁ Q₁ t₁ s₁) + (hmid : ∀ input ws ws', P₀ input ws → Q₀ input ws ws' → P₁ input ws') : + TransformsTapes (tm₀.seq tm₁) P₀ + (fun input ws ws'' => ∃ ws', Q₀ input ws ws' ∧ Q₁ input ws' ws'') + (t₀ + t₁) (s₀ + s₁) := by + intro input ws out hP₀ + obtain ⟨ws', hrun₀, hQ₀, hspace₀⟩ := h₀ input ws out hP₀ + obtain ⟨ws'', hrun₁, hQ₁, hspace₁⟩ := h₁ input ws' out (hmid input ws ws' hP₀ hQ₀) + -- the first halting time of the first machine, which may be earlier than `t₀` + obtain ⟨u, hu, huhalt, huactive⟩ := exists_minimal_halting_time tm₀ + (wordsCfg input (some tm₀.q₀) ws out) t₀ (by simp [hrun₀]) + have hu_run : tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) u = + wordsCfg input none ws' out := by + rw [← runFrom_eq_of_halt tm₀ _ hu huhalt, hrun₀] + -- the first phase mirrors the first machine, ending in the handoff configuration + have hleft : ∀ m ≤ u, (tm₀.seq tm₁).runFrom (wordsCfg input (some (tm₀.seq tm₁).q₀) ws out) m + = leftCfg tm₁ (tm₀.runFrom (wordsCfg input (some tm₀.q₀) ws out) m) := by + intro m hm + have : wordsCfg (State := State₀ ⊕ State₁) input (some (tm₀.seq tm₁).q₀) ws out = + leftCfg tm₁ (wordsCfg input (some tm₀.q₀) ws out) := rfl + rw [this, runFrom_leftCfg _ m fun r hr => + huactive r (by omega)] + -- the handoff configuration is the second machine's start, seen through the right embedding + have hhandoff : (tm₀.seq tm₁).runFrom (wordsCfg input (some (tm₀.seq tm₁).q₀) ws out) u = + rightCfg (wordsCfg input (some tm₁.q₀) ws' out) := by + rw [hleft u le_rfl, hu_run] + rfl + -- the second phase mirrors the second machine + have hright : ∀ n, (tm₀.seq tm₁).runFrom (wordsCfg input (some (tm₀.seq tm₁).q₀) ws out) (u + n) + = rightCfg (tm₁.runFrom (wordsCfg input (some tm₁.q₀) ws' out) n) := by + intro n + rw [runFrom_add, hhandoff, runFrom_rightCfg] + -- the composition is done after `u + t₁` steps and then simply stays put until `t₀ + t₁` + have hrun : (tm₀.seq tm₁).runFrom (wordsCfg input (some (tm₀.seq tm₁).q₀) ws out) (u + t₁) + = wordsCfg input none ws'' out := by + rw [hright t₁, hrun₁] + rfl + have hhalt : ((tm₀.seq tm₁).runFrom (wordsCfg input (some (tm₀.seq tm₁).q₀) ws out) + (u + t₁)).state = none := by + rw [hrun] + rfl + have hle : u + t₁ ≤ t₀ + t₁ := by omega + refine ⟨ws'', ?_, ⟨ws', hQ₀, hQ₁⟩, ?_⟩ + · rw [runFrom_eq_of_halt _ _ hle hhalt, hrun] + · rw [spaceUsed_eq_of_halt _ hle hhalt] + refine le_trans (spaceUsed_add_le _ _ _) (Nat.add_le_add ?_ ?_) + · -- the first phase visits what the first machine visits + refine le_trans (le_of_eq (spaceUsed_eq_of_workTapePos _ _ u fun m hm => ?_)) + (le_trans (spaceUsed_mono tm₀ _ hu) hspace₀) + rw [hleft m hm, workTapePos_leftCfg] + · -- the second phase visits what the second machine visits + rw [hhandoff] + refine le_trans (le_of_eq (spaceUsed_eq_of_workTapePos _ _ t₁ fun m hm => ?_)) hspace₁ + rw [runFrom_rightCfg, workTapePos_rightCfg] + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TransformsTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TransformsTapes.lean new file mode 100644 index 000000000..cb018275a --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/TransformsTapes.lean @@ -0,0 +1,178 @@ +/- +Copyright (c) 2026 Christian Reitwiessner and Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas + +/-! +# Machines as transformers of tape words + +The interface through which combinators use machines: a machine reads words from its work tapes +and leaves words on them. A combinator composing such machines talks about words only, never about +individual cells, head positions or the set of tapes a machine has touched. + +Configurations are described by *equalities*: `wordsCfg input q ws out` is the configuration whose +work tape `i` holds exactly the word `ws i` (contents `tapeOfList (ws i)`, head at the start), with +the input head at the start of the input and output `out`. A specification +`TransformsTapes tm P Q t s` says: started on word-holding tapes satisfying `P`, after exactly `t` +steps the machine sits in the halted *normal form* `wordsCfg input none ws' out` (every head reset +to its initial position, tapes blank outside their words, output untouched), with the new words +related to the old ones by `Q` and using at most `s` work-tape cells. The machine may halt earlier +than `t`; since a halted machine stays put and stops visiting new cells, running on to `t` costs +nothing, so a fixed step count loses no generality and spares every composition an existential. +Requiring this normal form is what lets specifications compose by rewriting: the halting +configuration of one machine is already a valid start for the next, so which words survived a step +is read off the equation, not re-established cell by cell. + +## Main definitions + +* `Turing.MultiTapeTM.tapeOfList`: the tape holding exactly a given word. +* `Turing.MultiTapeTM.wordsCfg`: the configuration whose tapes hold given words. +* `Turing.MultiTapeTM.TransformsTapes`: the specification format described above. +* `Turing.MultiTapeTM.nop`: the machine that does nothing. + +## Main results + +* `Turing.MultiTapeTM.TransformsTapes.imp`: strengthen the precondition, weaken the postcondition + and raise the bounds. +* `Turing.MultiTapeTM.transformsTapes_nop`: `nop` leaves every word as it was, the first machine of + the interface and the check that the format is inhabited as intended. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} {Symbol State : Type*} {input : List Symbol} + +/-- A tape containing exactly the symbols of `xs` at positions `0, ..., xs.length - 1`. -/ +def tapeOfList (xs : List Symbol) : ℤ → Option Symbol + | .ofNat n => xs[n]? + | .negSucc _ => none + +@[simp] +lemma tapeOfList_ofNat (xs : List Symbol) (n : ℕ) : tapeOfList xs n = xs[n]? := rfl + +@[simp] +lemma tapeOfList_negSucc (xs : List Symbol) (n : ℕ) : + tapeOfList xs (.negSucc n) = none := rfl + +/-- Appending one symbol writes precisely the cell after the existing word. -/ +lemma tapeOfList_append_single (xs : List Symbol) (x : Symbol) : + tapeOfList (xs ++ [x]) = Function.update (tapeOfList xs) (xs.length : ℤ) (some x) := by + funext z + cases z with + | negSucc n => simp [tapeOfList] + | ofNat n => grind [tapeOfList] + +/-- The blank tape holds the empty word. -/ +@[simp] +lemma tapeOfList_nil : tapeOfList ([] : List Symbol) = fun _ => none := by + funext z + cases z <;> simp + +/-- The cell at position `0` holds the first symbol of the word. -/ +lemma tapeOfList_zero (xs : List Symbol) : tapeOfList xs 0 = xs.head? := by + have h : (0 : ℤ) = ((0 : ℕ) : ℤ) := rfl + rw [h, tapeOfList_ofNat] + cases xs <;> rfl + +/-- The configuration whose work tape `i` holds exactly the word `ws i` with its head at the +start, whose input head is at the start of the input, in state `q` with output `out`. -/ +@[simps] +def wordsCfg (input : List Symbol) (q : Option State) + (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input := + ⟨q, 1, fun i => tapeOfList (ws i), fun _ => 0, out⟩ + +/-- Remapping the state of a `wordsCfg` remaps its state and leaves the words alone. -/ +@[simp] +lemma mapState_wordsCfg {State' : Type*} (φ : Option State → Option State') + (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : + (wordsCfg input q ws out).mapState φ = wordsCfg input (φ q) ws out := rfl + +/-- The initial configuration is the word configuration with blank tapes and no output. -/ +lemma initCfg_eq_wordsCfg (tm : MultiTapeTM k Symbol State) (input : List Symbol) : + tm.initCfg input = wordsCfg input (some tm.q₀) (fun _ => []) [] := by + refine Cfg.ext rfl rfl ?_ rfl rfl + funext i + simp [Cfg.init, wordsCfg] + +/-- `TransformsTapes tm P Q t s`: started in its initial state on tapes holding words `ws` that +satisfy the precondition `P`, the machine is halted after exactly `t` steps in the configuration +whose tapes hold words `ws'` with `Q input ws ws'`, having used at most `s` work-tape cells. The +machine is free to halt before step `t`, because it then stays in that configuration. + +The bounds are numbers; a specification whose bounds depend on the data is a *family* +`∀ j, TransformsTapes tm (P j) (Q j) (t j) (s j)` over one fixed machine. -/ +def TransformsTapes (tm : MultiTapeTM k Symbol State) + (P : (input : List Symbol) → (Fin k → List Symbol) → Prop) + (Q : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop) + (t s : ℕ) : Prop := + ∀ (input : List Symbol) (ws : Fin k → List Symbol) (out : List Symbol), P input ws → + ∃ ws', + tm.runFrom (wordsCfg input (some tm.q₀) ws out) t = wordsCfg input none ws' out ∧ + Q input ws ws' ∧ + tm.spaceUsed (wordsCfg input (some tm.q₀) ws out) t ≤ s + +/-- A `TransformsTapes` statement can be read with a stronger precondition, a weaker postcondition +and larger bounds. -/ +theorem TransformsTapes.imp {tm : MultiTapeTM k Symbol State} + {P P' : (input : List Symbol) → (Fin k → List Symbol) → Prop} + {Q Q' : (input : List Symbol) → (Fin k → List Symbol) → (Fin k → List Symbol) → Prop} + {t s t' s' : ℕ} (h : TransformsTapes tm P Q t s) + (hP : ∀ input ws, P' input ws → P input ws) + (hQ : ∀ input ws ws', P' input ws → Q input ws ws' → Q' input ws ws') + (ht : t ≤ t') (hs : s ≤ s') : + TransformsTapes tm P' Q' t' s' := by + intro input ws out hP' + obtain ⟨ws', hrun, hQ'', hspace⟩ := h input ws out (hP input ws hP') + -- the machine is halted at step `t`, so running on to `t'` changes neither tapes nor space + have hhalt : (tm.runFrom (wordsCfg input (some tm.q₀) ws out) t).state = none := by + rw [hrun] + rfl + refine ⟨ws', ?_, hQ input ws ws' hP' hQ'', ?_⟩ + · rw [runFrom_eq_of_halt tm _ ht hhalt, hrun] + · rw [spaceUsed_eq_of_halt _ ht hhalt] + exact hspace.trans hs + +section Nop + +/-- The machine that does nothing: it halts on its first step, leaving the configuration +unchanged. -/ +def nop (k : ℕ) (Symbol : Type*) : MultiTapeTM k Symbol Unit where + q₀ := () + tr _ _ _ := { inputTape := 0, workTapes := fun _ => (none, 0), output := none, state := none } + +/-- A single step of `nop` halts and leaves the words alone. -/ +@[simp] +lemma step_nop (ws : Fin k → List Symbol) (out : List Symbol) : + (nop k Symbol).step (wordsCfg input (some ()) ws out) = wordsCfg input none ws out := by + refine Cfg.ext rfl ?_ ?_ ?_ ?_ <;> + simp [step, nop, Action.apply, wordsCfg, SignType.cast] + +/-- `nop` reaches its halting configuration after exactly one step. -/ +@[simp] +lemma runFrom_nop_one (ws : Fin k → List Symbol) (out : List Symbol) : + (nop k Symbol).runFrom (wordsCfg input (some ()) ws out) 1 = wordsCfg input none ws out := by + rw [runFrom_succ_eq_step', runFrom_zero, step_nop] + +/-- **The machine that does nothing** halts in one step, leaving every word as it was. Its heads +never move, so it visits one cell per tape. This is the first machine of the interface: it checks +that the specification format is inhabited exactly as intended. -/ +theorem transformsTapes_nop (k : ℕ) (Symbol : Type*) : + TransformsTapes (nop k Symbol) (fun _ _ => True) (fun _ ws ws' => ws' = ws) 1 k := by + intro input ws out _ + -- the heads never move, so each tape touches only the single cell `0` + refine ⟨ws, runFrom_nop_one ws out, rfl, + spaceUsed_le_of_workTapePos_const _ 1 fun m hm => ?_⟩ + rcases (by omega : m = 0 ∨ m = 1) with rfl | rfl + · rw [runFrom_zero] + · rw [runFrom_nop_one]; funext i; simp only [wordsCfg_workTapePos] + +end Nop + +end Turing.MultiTapeTM diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean index fcf67a3d0..e3db9a32c 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -171,4 +171,89 @@ lemma exists_spaceUsedByTape_max (cfg : Cfg k Symbol State input) {s : ℕ} exact ⟨Finset.univ.sup T, fun t i => (hT i t).trans (tm.spaceUsedByTape_mono cfg i (Finset.le_sup (Finset.mem_univ i)))⟩ + +/-- Every position the head takes up to step `t` lies in `S`, so the whole visited set does. This +is `Finset.image_subset_iff` for the visited set, and the workhorse behind the space bounds +below. -/ +lemma visitedByTapeHead_subset (cfg : Cfg k Symbol State input) {t : ℕ} {i : Fin k} {S : Finset ℤ} + (h : ∀ m ≤ t, (tm.runFrom cfg m).workTapePos i ∈ S) : + tm.visitedByTapeHead cfg t i ⊆ S := + Finset.image_subset_iff.mpr fun m hm => h m (Nat.lt_succ_iff.mp (Finset.mem_range.mp hm)) + +/-- A set containing every position of a head bounds the space used by its tape. -/ +lemma spaceUsedByTape_le_card (cfg : Cfg k Symbol State input) {t : ℕ} {i : Fin k} {S : Finset ℤ} + (h : ∀ m ≤ t, (tm.runFrom cfg m).workTapePos i ∈ S) : + tm.spaceUsedByTape cfg t i ≤ S.card := + Finset.card_le_card (tm.visitedByTapeHead_subset cfg h) + +/-- A head that never moves uses a single cell. -/ +lemma spaceUsedByTape_le_one (cfg : Cfg k Symbol State input) {t : ℕ} {i : Fin k} + (h : ∀ m ≤ t, (tm.runFrom cfg m).workTapePos i = cfg.workTapePos i) : + tm.spaceUsedByTape cfg t i ≤ 1 := by + simpa using tm.spaceUsedByTape_le_card cfg (S := {cfg.workTapePos i}) + fun m hm => by simp [h m hm] + +/-- The cells a run visits are the ones visited by its two halves. -/ +lemma visitedByTapeHead_add (cfg : Cfg k Symbol State input) (a b : ℕ) (i : Fin k) : + tm.visitedByTapeHead cfg (a + b) i = + tm.visitedByTapeHead cfg a i ∪ tm.visitedByTapeHead (tm.runFrom cfg a) b i := by + ext z + simp only [mem_visitedByTapeHead, Finset.mem_union] + constructor + · rintro ⟨r, hr, rfl⟩ + rcases Nat.lt_or_ge r (a + 1) with h | h + · exact Or.inl ⟨r, h, rfl⟩ + · exact Or.inr ⟨r - a, by omega, + by rw [← runFrom_add, show a + (r - a) = r from by omega]⟩ + · rintro (⟨r, hr, rfl⟩ | ⟨r, hr, rfl⟩) + · exact ⟨r, by omega, rfl⟩ + · exact ⟨a + r, by omega, by rw [runFrom_add]⟩ + +/-- Splitting a run into two phases can only overcount the cells it visits, since the two phases +may revisit each other's cells. -/ +lemma spaceUsed_add_le (cfg : Cfg k Symbol State input) (a b : ℕ) : + tm.spaceUsed cfg (a + b) ≤ tm.spaceUsed cfg a + tm.spaceUsed (tm.runFrom cfg a) b := by + rw [spaceUsed, spaceUsed, spaceUsed, ← Finset.sum_add_distrib] + refine Finset.sum_le_sum fun i _ => ?_ + rw [spaceUsedByTape, visitedByTapeHead_add] + exact Finset.card_union_le _ _ + +/-- Space usage only depends on where the work-tape heads are at each step, so two runs whose head +positions agree use the same space. This is what lets a machine be replaced by a simulation of +it. -/ +lemma spaceUsed_eq_of_workTapePos {State' : Type*} {input' : List Symbol} + {tm' : MultiTapeTM k Symbol State'} (cfg : Cfg k Symbol State input) + (cfg' : Cfg k Symbol State' input') (t : ℕ) + (h : ∀ m ≤ t, (tm.runFrom cfg m).workTapePos = (tm'.runFrom cfg' m).workTapePos) : + tm.spaceUsed cfg t = tm'.spaceUsed cfg' t := by + refine Finset.sum_congr rfl fun i _ => congrArg Finset.card (Finset.image_congr fun m hm => ?_) + exact congrFun (h m (Nat.lt_succ_iff.mp (Finset.mem_range.mp hm))) i + +/-- After the machine has halted the heads no longer move, so the visited set stops growing. -/ +lemma visitedByTapeHead_eq_of_halt (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) + (hhalt : (tm.runFrom cfg τ).state = none) (i : Fin k) : + tm.visitedByTapeHead cfg t i = tm.visitedByTapeHead cfg τ i := by + refine Finset.Subset.antisymm (visitedByTapeHead_subset cfg fun m hm => ?_) + (tm.visitedByTapeHead_mono cfg i hle) + rcases Nat.le_total m τ with h | h + · exact mem_visitedByTapeHead.mpr ⟨m, by omega, rfl⟩ + · rw [runFrom_eq_of_halt tm cfg h hhalt] + exact tm.mem_visitedByTapeHead_self cfg τ i + +/-- After the machine has halted the heads no longer move, so the space usage stops growing. -/ +lemma spaceUsed_eq_of_halt (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) + (hhalt : (tm.runFrom cfg τ).state = none) : + tm.spaceUsed cfg t = tm.spaceUsed cfg τ := + Finset.sum_congr rfl fun i _ => + congrArg Finset.card (tm.visitedByTapeHead_eq_of_halt cfg hle hhalt i) + +/-- A run that never moves a work-tape head visits one cell per tape. -/ +lemma spaceUsed_le_of_workTapePos_const (cfg : Cfg k Symbol State input) (u : ℕ) + (h : ∀ m ≤ u, (tm.runFrom cfg m).workTapePos = cfg.workTapePos) : + tm.spaceUsed cfg u ≤ k := by + have hcard : ∀ i ∈ Finset.univ, tm.spaceUsedByTape cfg u i ≤ 1 := + fun i _ => tm.spaceUsedByTape_le_one cfg fun m hm => congrFun (h m hm) i + simpa [spaceUsed] using Finset.sum_le_card_nsmul _ _ 1 hcard + + end Turing.MultiTapeTM