refactor(MultiTape): remove the deterministic space measures

Cslib/Computability/Machines/Turing/MultiTape/ConfigBound.lean

@@ -30,8 +30,8 @@ The results are layered, from the purely combinatorial to the machine-specific:
 * `MultiTapeTM.encard_fitsIn_le` is a counting statement about the type `Storage` alone and does
   not mention Turing machines: a memory whose non-blank cells and heads stay within per-tape
   windows of total size `s` can hold at most `storageBound Symbol State k s` different values.
-* `MultiTapeTM.storage_fitsIn` is the geometric input: the storage reached after `t` steps stays
-  within the windows given by the space used up to step `t`.
+* `MultiTapeNTM.ComputationPath.storage_fitsIn` is the geometric input: the storage at the end of a
+  computation path stays within the windows given by the per-tape space of the path.
 * `MultiTapeTM.encard_storages_le` combines the two: a machine bounded by space `s` passes through
   at most `storageBound Symbol State k s` storages *during its whole run*, no matter how long it
   runs and how long its input is. This is the form needed for arguments below logarithmic space,
@@ -62,8 +62,9 @@ alphabet exponent.
 We lose a factor of `2 * k` by simplifying the windows to `[-sᵢ, sᵢ]` instead of the actually used
 area, but this is absorbed by the `O(s)` exponent in the final bound.
 
-The windows for a whole run are available because a machine that is space-bounded at every point in
-time attains its per-tape space usage at a single step (`MultiTapeTM.exists_spaceUsedByTape_max`).
+The windows for a whole run are available because the computation paths of a deterministic
+machine are prefixes of one another, so the one visiting the most cells contains the windows of
+every other (`MultiTapeNTM.ComputationPath.spaceUsedByTape_le_of_space_le`).
 -/
 
 @[expose] public section
@@ -247,63 +248,58 @@ def Cfg.core (c : Cfg k Symbol State input) :
     Fin (input.length + 2) × Storage Symbol State k :=
   (c.inputPos, c.storage)
 
-/-- `step` never reads the output tape, so the core of the next configuration is determined by the
-core of the current one. -/
-lemma core_step_eq_of_core_eq {c₁ c₂ : Cfg k Symbol State input} (h : c₁.core = c₂.core) :
-    (tm.step c₁).core = (tm.step c₂).core := by
-  rcases c₁ with ⟨q₁, i₁, w₁, p₁, out₁⟩
-  rcases c₂ with ⟨q₂, i₂, w₂, p₂, out₂⟩
-  simp only [Cfg.core, Cfg.storage, Prod.mk.injEq, Storage.mk.injEq] at h
-  obtain ⟨rfl, rfl, rfl, rfl⟩ := h
-  cases q₁ with
-  | none => rw [MultiTapeTM.step_of_halt rfl, MultiTapeTM.step_of_halt rfl]; rfl
-  | some q => rw [MultiTapeTM.step_of_state rfl, MultiTapeTM.step_of_state rfl]; rfl
-
 /-! ## The storages and cores of a space-bounded run
 
 These are the main results giving upper bounds on the number of storages and configuration cores
 reachable in bounded space.
 -/
 
-namespace MultiTapeTM
+namespace MultiTapeNTM
 
-/-- The storage reached after `t` steps fits in the windows given by the per-tape space usage up
-to step `t`. -/
-lemma storage_fitsIn (t : ℕ) :
-    (tm.runFrom (tm.initCfg input) t).storage.FitsIn (tm.spaceUsedByTape (tm.initCfg input) t) := by
-  constructor
-  · intro j
-    simpa [Cfg.storage] using tm.natAbs_le_spaceUsedByTape_of_mem_visited
-      (tm.mem_visitedByTapeHead_self (tm.initCfg input) t j)
-  · intro j
-    exact content_natAbs_le_spaceUsedByTape t
+/-- The storage at the end of a computation path fits in the windows given by its per-tape space:
+the tapes start blank, with every head at `0`. -/
+lemma ComputationPath.storage_fitsIn {ntm : MultiTapeNTM k Symbol State}
+    (p : ntm.ComputationPath input) : p.last.storage.FitsIn p.spaceUsedByTape := by
+  refine ⟨fun j => ?_, fun j z hz => ?_⟩
+  · simpa [Cfg.storage, p.head_eq, Cfg.init, ComputationPath.spaceUsedByTape] using
+      RunPath.natAbs_le_spaceUsedByTape_of_mem_visited p.toRunPath
+        ((RunPath.mem_visitedByTapeHead _).mpr ⟨_, RelSeries.last_mem _, rfl⟩)
+  · simpa [p.head_eq, Cfg.init, ComputationPath.spaceUsedByTape] using
+      RunPath.natAbs_le_spaceUsedByTape_of_mem_visited p.toRunPath
+        (RunPath.mem_visitedByTapeHead_of_workTapes_ne _
+          (by simpa [p.head_eq, Cfg.init, Cfg.storage] using hz))
+
+end MultiTapeNTM
+
+namespace MultiTapeTM
 
 /-- A machine that uses at most `s` cells of work-tape space at every point in time passes through
 at most `storageBound Symbol State k s` different storages during its whole run — independently of
 the length of the input and of how long it runs. -/
 theorem encard_storages_le [Fintype Symbol] [Fintype State] {s : ℕ}
-    (hs : ∀ t, tm.space (tm.initCfg input) t ≤ s) :
-    (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard
+    (hs : tm.RunsInSpace input s) :
+    (Set.range fun p : tm.ComputationPath input => p.last.storage).encard
       ≤ storageBound Symbol State k s := by
-  obtain ⟨T, hT⟩ := tm.exists_spaceUsedByTape_max (tm.initCfg input) hs
-  refine le_trans (Set.encard_le_encard ?_) (encard_fitsIn_le (hs T))
-  rintro _ ⟨t, rfl⟩
-  exact Storage.FitsIn_mono (fun i => hT t i) (tm.storage_fitsIn t)
+  -- every storage fits in the windows of a computation path visiting the most cells
+  obtain ⟨p, hp⟩ := hs.exists_space_max
+  refine le_trans (Set.encard_le_encard ?_) (encard_fitsIn_le (hs p))
+  rintro _ ⟨q, rfl⟩
+  exact Storage.FitsIn_mono (q.spaceUsedByTape_le_of_space_le (hp q)) q.storage_fitsIn
 
 /-- The number of configuration cores that a machine bounded by space `s` can reach is at most
 `(n + 2) * storageBound Symbol State k s`, where `n` is the length of the input. -/
 theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ}
-    (hs : ∀ t, tm.space (tm.initCfg input) t ≤ s) :
-    (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
+    (hs : tm.RunsInSpace input s) :
+    (Set.range fun p : tm.ComputationPath input => p.last.core).encard
       ≤ (input.length + 2) * storageBound Symbol State k s := by
-  calc (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
+  calc (Set.range fun p : tm.ComputationPath input => p.last.core).encard
       ≤ ((Set.univ : Set (Fin (input.length + 2)))
-          ×ˢ (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage)).encard := by
+          ×ˢ (Set.range fun p : tm.ComputationPath input => p.last.storage)).encard := by
         apply Set.encard_le_encard
-        rintro _ ⟨t, rfl⟩
-        exact ⟨Set.mem_univ _, t, rfl⟩
+        rintro _ ⟨p, rfl⟩
+        exact ⟨Set.mem_univ _, p, rfl⟩
     _ = (Set.univ : Set (Fin (input.length + 2))).encard
-          * (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard := Set.encard_prod
+          * (Set.range fun p : tm.ComputationPath input => p.last.storage).encard := Set.encard_prod
     _ ≤ (input.length + 2) * storageBound Symbol State k s := by
         refine mul_le_mul' ?_ (tm.encard_storages_le hs)
         simp [Set.encard_univ, ENat.card_eq_coe_fintype_card]
@@ -312,8 +308,8 @@ theorem encard_cores_le [Fintype Symbol] [Fintype State] {s : ℕ}
 passes through is at most `2 ^ (O(s))`, with constants depending only on the machine. -/
 theorem encard_storages_le_pow [Finite Symbol] [Finite State] :
     ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ),
-      (∀ t, tm.space (tm.initCfg input) t ≤ s) →
-      (Set.range fun t => (tm.runFrom (tm.initCfg input) t).storage).encard ≤ a * 2 ^ (c * s) := by
+      tm.RunsInSpace input s →
+      (Set.range fun p : tm.ComputationPath input => p.last.storage).encard ≤ a * 2 ^ (c * s) := by
   have : Fintype Symbol := Fintype.ofFinite Symbol
   have : Fintype State := Fintype.ofFinite State
   obtain ⟨a, c, hpow⟩ := storageBound_le_pow (Symbol := Symbol) (State := State) (k := k)
@@ -325,8 +321,8 @@ is at most `(n + 2) * 2 ^ (O(s))`, with constants depending only on the machine
 input. -/
 theorem encard_cores_le_pow [Finite Symbol] [Finite State] :
     ∃ a c : ℕ, ∀ (input : List Symbol) (s : ℕ),
-      (∀ t, tm.space (tm.initCfg input) t ≤ s) →
-      (Set.range fun t => (tm.runFrom (tm.initCfg input) t).core).encard
+      tm.RunsInSpace input s →
+      (Set.range fun p : tm.ComputationPath input => p.last.core).encard
         ≤ (input.length + 2) * a * 2 ^ (c * s) := by
   have : Fintype Symbol := Fintype.ofFinite Symbol
   have : Fintype State := Fintype.ofFinite State

Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean

@@ -34,7 +34,6 @@ We define a number of structures and concepts related to multi-tape Turing machi
 * `step`, `runFrom`: the successor configuration and iteration of this function
 * `MultiTapeNTM.RunPath.ofDeterministic`, `MultiTapeNTM.ComputationPath.ofDeterministic`:
     paths of a given length from an arbitrary or initial configuration
-* `space`: the space of the path of the first `t` steps from a configuration
 * `Computes`: the machine halts with the given output on an input
 * `ComputesInTimeAndSpace`: the machine produces an output within the shared resource bounds
 * `ComputesFunInTimeAndSpace`: function computation with the shared time and space bounds
@@ -225,6 +224,32 @@ lemma ComputationPath.eq_ofDeterministic (p : tm.ComputationPath input) :
   congr 1
   exact (RunPath.eq_ofDeterministic p).trans (by rw [hp]; rfl)
 
+/-- Deterministic run paths from the same configuration are prefixes of one another: the shorter one
+is the longer one, cut at its length. -/
+lemma RunPath.eq_take {p q : tm.RunPath input} (hhead : p.head = q.head) (h : p.length ≤ q.length) :
+    p = q.take ⟨p.length, Nat.lt_succ_of_le h⟩ := by
+  refine p.eq_ofDeterministic.trans ((eq_ofDeterministic (q.take _)).trans ?_).symm
+  rw [RelSeries.head_take, hhead]
+  rfl
+
+/-- The computation paths of a deterministic machine are prefixes of one another, so a path visiting
+at most as many cells as another visits at most as many on each tape. -/
+lemma ComputationPath.spaceUsedByTape_le_of_space_le (p : tm.ComputationPath input)
+    {q : tm.ComputationPath input} (h : p.space ≤ q.space) :
+    p.spaceUsedByTape ≤ q.spaceUsedByTape := by
+  -- a shorter path is a prefix of a longer one, so it visits fewer cells on each tape
+  have hmono {p q : tm.ComputationPath input} (h : p.time ≤ q.time) :
+      p.spaceUsedByTape ≤ q.spaceUsedByTape := fun i => by
+    change RunPath.spaceUsedByTape p.toRunPath i ≤ RunPath.spaceUsedByTape q.toRunPath i
+    rw [RunPath.eq_take (by rw [p.head_eq, q.head_eq]) h]
+    exact Finset.card_le_card (RunPath.visitedByTapeHead_take_subset _ _ i)
+  rcases le_total p.time q.time with hpq | hqp
+  · exact hmono hpq
+  -- a longer `p` visits no more cells than `q`, so it visits exactly those of `q`
+  have h : ∑ j, p.spaceUsedByTape j ≤ ∑ j, q.spaceUsedByTape j := h
+  exact fun i => ((Finset.sum_eq_sum_iff_of_le fun j _ => hmono hqp j).mp
+    (le_antisymm (Finset.sum_le_sum fun j _ => hmono hqp j) h) i (Finset.mem_univ i)).ge
+
 /-- A step-preserving map sends the path of `t` steps from `cfg` to the path of `t` steps from the
 image of `cfg`. -/
 lemma RunPath.map_ofDeterministic {k' : ℕ} {State' : Type*} {input' : List Symbol}
@@ -281,48 +306,6 @@ lemma runsInTime_of_halted {input : List Symbol} {t : ℕ}
   rw [computationPath_last_eq_runFrom p, runFrom_eq_of_halt _ _ hp h]
   exact h
 
-/-- 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
-  cases hstate : c.state with
-  | none => simp [step_of_halt hstate]
-  | some q => rw [step_of_state hstate]; exact workTapePos_apply_le _ c i
-
-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`. -/
-noncomputable def visitedByTapeHead (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    Finset ℤ :=
-  Finset.univ.image fun n : Fin (t + 1) => (tm.runFrom cfg n).workTapePos i
-
-/--
-The number of work tape cells visited by the head of tape `i` in the computation starting from
-configuration `cfg` up to step `t`.
--/
-noncomputable def spaceUsedByTape (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) : ℕ :=
-  (tm.visitedByTapeHead cfg t i).card
-
-/-- The number of work tape cells visited in the first `t` steps from `cfg`: the space of the path
-of these steps. -/
-noncomputable abbrev space (cfg : Cfg k Symbol State input) (t : ℕ) : ℕ :=
-  (MultiTapeNTM.RunPath.ofDeterministic tm cfg t).space
-
-/-- A zero-tape Turing machine uses zero space. -/
-@[simp]
-lemma space_zero_tapes_eq_zero (cfg : Cfg k Symbol State input) (t : ℕ) (h_zero : k = 0) :
-    tm.space cfg t = 0 := by
-  subst h_zero
-  simp [MultiTapeNTM.RunPath.space]
-
-/-- Each tape's space usage is bounded by the total space used. -/
-lemma spaceUsedByTape_le_space (cfg : Cfg k Symbol State input) (t : ℕ) (i : Fin k) :
-    tm.spaceUsedByTape cfg t i ≤ tm.space cfg t :=
-  Finset.single_le_sum (fun _ _ => Nat.zero_le _) (Finset.mem_univ i)
-
-end Space
-
 /-- In `t` steps the input head moves at most `t` positions to the right. -/
 lemma inputPos_runFrom_le (tm : MultiTapeTM k Symbol State)
     (cfg : Cfg k Symbol State input) (t : ℕ) :

Cslib/Computability/Machines/Turing/MultiTape/Space.lean

@@ -8,6 +8,7 @@ module
 
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 public import Mathlib.Data.Int.Interval
+public import Mathlib.Order.Lattice.Nat
 public import Cslib.Computability.Machines.Turing.MultiTape.Nondeterministic
 
 /-!
@@ -98,6 +99,25 @@ lemma space_le_of_subset {p q : ntm.RunPath input} (h : ∀ c ∈ q, c ∈ p) :
     let ⟨n, hn⟩ := h c hc
     hn ▸ Finset.mem_image_of_mem _ (Finset.mem_univ n)
 
+/-- A path visits exactly the head positions of its configurations. -/
+@[simp]
+lemma mem_visitedByTapeHead (p : ntm.RunPath input) {i : Fin k} {z : ℤ} :
+    z ∈ p.visitedByTapeHead i ↔ ∃ c ∈ p, c.workTapePos i = z := by
+  simp [visitedByTapeHead, RelSeries.mem_def]
+
+/-- A prefix of a path visits only cells that the path visits. -/
+lemma visitedByTapeHead_take_subset (p : ntm.RunPath input) (j : Fin (p.length + 1)) (i : Fin k) :
+    visitedByTapeHead (p.take j) i ⊆ p.visitedByTapeHead i :=
+  Finset.image_subset_iff.mpr fun n _ =>
+    p.mem_visitedByTapeHead.mpr ⟨_, ⟨Fin.castLE j.isLt n, rfl⟩, rfl⟩
+
+/-- Extending a path by a configuration visits its head positions as well. -/
+lemma visitedByTapeHead_snoc (p : ntm.RunPath input) (c : Cfg k Symbol State input)
+    (h : ntm.Step p.last c) (i : Fin k) :
+    visitedByTapeHead (p.snoc c h) i = insert (c.workTapePos i) (p.visitedByTapeHead i) := by
+  ext z
+  simp [RelSeries.mem_snoc, or_and_right, exists_or, eq_comm, or_comm]
+
 /-! ### Windows -/
 
 /-- Every head stays within the window `[-s, s]` along the path. -/
@@ -140,6 +160,10 @@ lemma space_map_le (p : ntm.RunPath input) (f : (ntm.stepRel input).Hom (ntm'.st
 
 end RunPath
 
+/-- The number of positions visited by the head of work tape `i` along a computation path. -/
+def ComputationPath.spaceUsedByTape (p : ntm.ComputationPath input) (i : Fin k) : ℕ :=
+  RunPath.spaceUsedByTape p.toRunPath i
+
 /-- The number of work tape cells visited along a computation path. -/
 def ComputationPath.space (p : ntm.ComputationPath input) : ℕ := RunPath.space p.toRunPath
 
@@ -153,6 +177,16 @@ lemma RunsInSpace.mono {s s' : ℕ} (h : ntm.RunsInSpace input s) (hs : s ≤ s'
     ntm.RunsInSpace input s' :=
   fun p ↦ (h p).trans hs
 
+/-- A machine running in space `s` has a computation path visiting the most cells. -/
+lemma RunsInSpace.exists_space_max {s : ℕ} (hs : ntm.RunsInSpace input s) :
+    ∃ p : ntm.ComputationPath input, ∀ q : ntm.ComputationPath input, q.space ≤ p.space := by
+  have hne : (Set.range fun p : ntm.ComputationPath input => p.space).Nonempty :=
+    ⟨_, ⟨.singleton _ (ntm.initCfg input), rfl⟩, rfl⟩
+  have hbdd : BddAbove (Set.range fun p : ntm.ComputationPath input => p.space) :=
+    ⟨s, by rintro _ ⟨p, rfl⟩; exact hs p⟩
+  obtain ⟨p, hp⟩ := Nat.sSup_mem hne hbdd
+  exact ⟨p, fun q => (le_csSup hbdd ⟨q, rfl⟩).trans_eq hp.symm⟩
+
 /-- A machine without work tapes satisfies every space bound. -/
 @[simp]
 lemma runsInSpace_zero_tapes (ntm : MultiTapeNTM 0 Symbol State) (input : List Symbol) (s : ℕ) :