feat(MultiTapeTM): Some lemmas about Turing machine tapes

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

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

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