From 506a894ce504215df6b013376aa905331a69e8b6 Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 1 Aug 2026 23:33:48 +0200 Subject: [PATCH] Some lemmas about Turing machine tapes. --- Cslib.lean | 1 + .../Turing/MultiTape/Deterministic.lean | 115 ++++++++++---- .../Machines/Turing/MultiTape/TapeLemmas.lean | 150 ++++++++++++++++++ 3 files changed, 234 insertions(+), 32 deletions(-) create mode 100644 Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean diff --git a/Cslib.lean b/Cslib.lean index d67431976..ab404a9da 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -41,6 +41,7 @@ public import Cslib.Computability.Languages.OmegaLanguage public import Cslib.Computability.Languages.OmegaRegularLanguage public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic +public import Cslib.Computability.Machines.Turing.MultiTape.TapeLemmas public import Cslib.Computability.Machines.Turing.SingleTape.Defs public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic public import Cslib.Computability.Machines.Turing.SingleTape.NonDeterministic diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean index 9e083b3d0..b7b161762 100644 --- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean +++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean @@ -251,17 +251,43 @@ def outputSymbol (cfg : Cfg k Symbol State input) : Option Symbol := def initCfg (input : List Symbol) : Cfg k Symbol State input := ⟨some tm.q₀, 1, fun _ _ => none, fun _ => 0⟩ +@[simp] +lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) : + tm.step cfg = cfg := by + unfold step + rw [h] + /-- The sequence of configurations of the Turing machine starting from `cfg`. If the Turing machine halts, it will stay at the halting configuration. -/ def configs (cfg : Cfg k Symbol State input) (t : ℕ) : Cfg k Symbol State input := tm.step^[t] cfg -/-- Any number of steps run from a halting configuration results in the same configuration. -/ -@[simp, scoped grind =] -lemma iter_step_eq_of_halt {cfg : Cfg k Symbol State input} {n : ℕ} (h_halt : cfg.state = none) : - tm.step^[n] cfg = cfg := by +@[simp] +lemma configs_zero {cfg : Cfg k Symbol State input} : + tm.configs cfg 0 = cfg := by + simp [configs] + +lemma configs_succ_eq_step {cfg : Cfg k Symbol State input} {t : ℕ} : + tm.configs cfg (t + 1) = tm.configs (tm.step cfg) t := by + simp [configs, Function.iterate_succ_apply] + +lemma configs_succ_eq_step' {cfg : Cfg k Symbol State input} {t : ℕ} : + tm.configs cfg (t + 1) = tm.step (tm.configs cfg t) := by + simp [configs, Function.iterate_succ_apply'] + +/-- Running `a + d` steps equals running `a` steps from the configuration reached after `d`. -/ +lemma configs_add (cfg : Cfg k Symbol State input) (a b : ℕ) : + tm.configs cfg (a + b) = tm.configs (tm.configs cfg a) b := by + unfold configs + rw [Nat.add_comm, Function.iterate_add_apply] + +/-- The sequence of configurations from a halting state is constant. -/ +@[simp] +lemma configs_of_halts (cfg : Cfg k Symbol State input) (h : cfg.state = none) {n : ℕ} : + tm.configs cfg n = cfg := by induction n with | zero => rfl - | succ n ih => rw [Function.iterate_succ_apply', ih, step, h_halt] + | succ d ih => + rw [configs_succ_eq_step', ih, step_of_halt h] @[simp] lemma outputSymbol_of_halt {cfg : Cfg k Symbol State input} (h_halt : cfg.state = none) : @@ -283,12 +309,17 @@ 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 ℤ := + (Finset.range (t + 1)).image fun t' => (tm.configs cfg t').workTapePos 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) : ℕ := - ((List.range (t + 1)).map fun t' => (tm.configs cfg t').workTapePos i).toFinset.card + (tm.visitedByTapeHead cfg t i).card /-- The number of work tape cells touched by a computation starting from configuration @@ -304,23 +335,10 @@ lemma spaceUsed_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h subst h_zero simp -/-- 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 - _ ≤ ((List.range (t + 1)).map _).length := List.toFinset_card_le _ - _ = t + 1 := by simp - -/-- -The space used by a computation is bounded linearly by the number of steps. --/ -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] +/-- 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) end Space @@ -360,11 +378,7 @@ lemma outputString_halt tm.outputString cfg t = [] := by induction t with | zero => simp [outputString] - | succ t ih => - have : tm.configs cfg t = cfg := by - simp [configs, iter_step_eq_of_halt, h_halt] - rw [outputString_succ, ih, this] - simp [outputSymbol, h_halt] + | succ t ih => simp [outputString_succ, ih, h_halt] lemma outputString_add_eq_append (tm : MultiTapeTM k Symbol State) @@ -377,6 +391,16 @@ lemma outputString_add_eq_append rw [show (t₁ + (t + 1)) = (t₁ + t) + 1 by omega] simp [outputString_succ, ih, configs, ← Function.iterate_add_apply, Nat.add_comm] +/-- The output does not change after the machine has halted. -/ +lemma outputString_eq_of_halt + (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k Symbol State input) {τ t : ℕ} (hle : τ ≤ t) + (hhalt : (tm.configs cfg τ).state = none) : + tm.outputString cfg t = tm.outputString cfg τ := by + conv_lhs => rw [← Nat.sub_add_cancel hle, Nat.add_comm] + rw [outputString_add_eq_append, outputString_halt _ _ hhalt] + simp + /-- 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. -/ @@ -466,15 +490,42 @@ lemma halting_step_unique cases d with | zero => rfl | succ d => - have halts₁ : (tm.step^[t₁] (tm.initCfg input)).state = none := by - simp [haltsAtStep, configs] at h_halts₁ + have halts₁ : (tm.configs (tm.initCfg input) t₁).state = none := by + simp [haltsAtStep] at h_halts₁ exact h_halts₁.left - have halts₂ : (tm.step^[d + t₁] (tm.initCfg input)).state ≠ none := by + have halts₂ : (tm.configs (tm.initCfg input) (d + t₁)).state ≠ none := by grind [haltsAtStep, configs] refine absurd ?_ halts₂ - rw [Function.iterate_add_apply, tm.iter_step_eq_of_halt halts₁] + rw [Nat.add_comm, configs_add, tm.configs_of_halts _ 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.configs_add`. -/ +lemma not_halts_of_repeat_nonhalt + (cfg : Cfg k Symbol State input) + (h_not_halt : cfg.state ≠ none) + (t : ℕ) + (heq : tm.configs cfg (t + 1) = cfg) : + ∀ t', (tm.configs cfg t').state ≠ none := by + intro t' + -- The configuration will repeat every `t + 1` steps. + have hloop : ∀ n, tm.configs 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.configs_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.configs 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.configs_add] + simp [hnh] + simp [hloop t', h_not_halt] at h₁ + end MultiTapeTM end Turing diff --git a/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean new file mode 100644 index 000000000..39ec30f56 --- /dev/null +++ b/Cslib/Computability/Machines/Turing/MultiTape/TapeLemmas.lean @@ -0,0 +1,150 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.Turing.MultiTape.Deterministic + +/-! +# Tape head visitation and space-usage lemmas + +This file collects lemmas about the set of positions visited by a work-tape head +(`MultiTapeTM.visitedByTapeHead`) and the resulting space-usage measures +(`MultiTapeTM.spaceUsedByTape`, `MultiTapeTM.spaceUsed`) and how the tape head positions +influence the cells that are modified on a tape. + +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +variable {k : ℕ} +variable {State Symbol : Type*} +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 + unfold step + cases hst : cfg.state with + | none => simp_all + | some q => + rcases hw : ((tm.tr q cfg.inputSymbol cfg.workTapeSymbols).workActions j).1 <;> simp_all + +lemma mem_visitedByTapeHead {t : ℕ} {i : Fin k} {z : ℤ} : + z ∈ tm.visitedByTapeHead cfg t i ↔ ∃ t' < t + 1, (tm.configs cfg t').workTapePos i = z := by + simp [visitedByTapeHead] + +lemma mem_visitedByTapeHead_self (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : + (tm.configs cfg t).workTapePos i ∈ tm.visitedByTapeHead cfg t i := + tm.mem_visitedByTapeHead.mpr ⟨t, by omega, rfl⟩ + +/-- 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 + grind + +/-- Starting from configuration `cfg`, every position between the initial head position of tape +`i` and the one after `t` steps is part of the "visited set" at step `t`. -/ +lemma uIcc_workTapePos_subset_visitedByTapeHead + (cfg : Cfg k Symbol State input) (i : Fin k) (t : ℕ) : + Finset.uIcc (cfg.workTapePos i) ((tm.configs cfg t).workTapePos i) + ⊆ tm.visitedByTapeHead cfg t i := by + induction t with + | zero => simpa [configs] using tm.mem_visitedByTapeHead_self cfg 0 i + | succ t ih => + intro z hz + have hstep : |(tm.configs cfg (t + 1)).workTapePos i - (tm.configs cfg t).workTapePos i| ≤ 1 := + configs_succ_eq_step' (tm := tm) ▸ tm.workTapePos_step_le _ 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] + +/-- If a work tape cell is changed after `t` steps, it must have been visited by the tape head. -/ +lemma mem_visitedByTapeHead_of_workTapes_ne + (j : Fin k) + (t : ℕ) + (z : ℤ) + (h : (tm.configs cfg t).workTapes j z ≠ cfg.workTapes j z) : + z ∈ tm.visitedByTapeHead cfg t j := by + induction t with + | zero => exact absurd (by simp [configs]) h + | succ t ih => + rw [configs_succ_eq_step'] at h + by_cases hz : z = (tm.configs 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 + 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 +head's starting position. -/ +lemma natAbs_le_spaceUsedByTape_of_mem_visited + {i : Fin k} + {z : ℤ} + {t : ℕ} + (hz : z ∈ tm.visitedByTapeHead cfg t i) : + (z - cfg.workTapePos i).natAbs ≤ tm.spaceUsedByTape cfg t i := by + obtain ⟨t', ht', rfl⟩ := tm.mem_visitedByTapeHead.mp hz + have h1 := Finset.card_le_card + ((tm.uIcc_workTapePos_subset_visitedByTapeHead cfg i t').trans + (tm.visitedByTapeHead_mono cfg i (show t' ≤ t by omega))) + rw [Int.card_uIcc] at h1 + unfold spaceUsedByTape + omega + +/-- Every non-blank cell on work tape `i` lies within `spaceUsedByTape … i t` of the origin. -/ +lemma content_natAbs_le_spaceUsedByTape + {i : Fin k} + (t : ℕ) + (z : ℤ) + (h : (tm.configs (tm.initCfg input) t).workTapes i z ≠ none) : + z.natAbs ≤ tm.spaceUsedByTape (tm.initCfg input) t i := by + -- The work tapes start out blank, so any non-blank cell has been visited by the head; the + -- initial head position is `0`, so the displacement bound is a bound on the position itself. + simpa using tm.natAbs_le_spaceUsedByTape_of_mem_visited + (tm.mem_visitedByTapeHead_of_workTapes_ne i t z h) + +/-- 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 _ + +/-- The space used by a computation is bounded linearly by the number of steps. -/ +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] + +/-- The space used by a single tape is monotone in the number of steps. -/ +lemma spaceUsedByTape_mono + (tm : MultiTapeTM k Symbol State) + (cfg : Cfg k Symbol State input) + (i : Fin k) : + Monotone (tm.spaceUsedByTape cfg · i) := by + intro t t' h + exact Finset.card_le_card (tm.visitedByTapeHead_mono cfg i h) + +/-- The total space used is monotone in the number of steps. -/ +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) + +end Turing.MultiTapeTM