Tape as int fun

Cslib.lean

@@ -130,3 +130,4 @@ public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
 public import Cslib.Logics.LinearLogic.CLL.MLL
 public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
 public import Cslib.Logics.Propositional.Defs
+public import Cslib.Logics.Propositional.NaturalDeduction.Basic

Cslib/Computability/Machines/SingleTapeTuring/Basic.lean

@@ -123,24 +123,23 @@ instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance
 /--
 The configurations of a Turing machine consist of:
 an `Option`al state (or none for the halting state),
-and a `BiTape` representing the tape contents.
+and a `BiTape` representing the tape.
 -/
 structure Cfg : Type where
   /-- the state of the TM (or none for the halting state) -/
   state : Option tm.State
-  /-- the BiTape contents -/
+  /-- the BiTape contents and head position -/
   BiTape : BiTape Symbol
 deriving Inhabited
 
 /-- The step function corresponding to a `SingleTapeTM`. -/
-@[simp]
 def step : tm.Cfg → Option tm.Cfg
   | ⟨none, _⟩ =>
     -- If in the halting state, there is no next configuration
     none
   | ⟨some q', t⟩ =>
     -- If in state q', perform look up in the transition function
-    match tm.tr q' t.head with
+    match tm.tr q' t.read with
     -- and enter a new configuration with state q'' (or none for halting)
     -- and tape updated according to the Stmt
     | ⟨⟨wr, dir⟩, q''⟩ => some ⟨q'', (t.write wr).optionMove dir⟩
@@ -152,36 +151,13 @@ This is to ensure that distinct lists map to distinct initial configurations.
 -/
 def initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨some tm.q₀, BiTape.mk₁ s⟩
 
+
 /-- The final configuration corresponding to a list in the output alphabet.
 (We demand that the head halts at the leftmost position of the output.)
 -/
+@[simp]
 def haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) : tm.Cfg := ⟨none, BiTape.mk₁ s⟩
 
-/--
-The space used by a configuration is the space used by its tape.
--/
-def Cfg.space_used (tm : SingleTapeTM Symbol) (cfg : tm.Cfg) : ℕ := cfg.BiTape.space_used
-
-@[scoped grind =]
-lemma Cfg.space_used_initCfg (tm : SingleTapeTM Symbol) (s : List Symbol) :
-    (tm.initCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s
-
-@[scoped grind =]
-lemma Cfg.space_used_haltCfg (tm : SingleTapeTM Symbol) (s : List Symbol) :
-    (tm.haltCfg s).space_used = max 1 s.length := BiTape.space_used_mk₁ s
-
-lemma Cfg.space_used_step {tm : SingleTapeTM Symbol} (cfg cfg' : tm.Cfg)
-    (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by
-  obtain ⟨_ | q, tape⟩ := cfg
-  · simp [step] at hstep
-  · simp only [step] at hstep
-    generalize hM : tm.tr q tape.head = result at hstep
-    obtain ⟨⟨wr, dir⟩, q''⟩ := result
-    cases hstep; cases dir with
-    | none => simp [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM]
-    | some d => simpa [Cfg.space_used, BiTape.optionMove, BiTape.space_used_write, hM] using
-        BiTape.space_used_move (tape.write wr) d
-
 end Cfg
 
 open Cfg
@@ -198,11 +174,45 @@ def TransitionRelation (tm : SingleTapeTM Symbol) (c₁ c₂ : tm.Cfg) : Prop :=
 
 /-- A proof of `tm` outputting `l'` on input `l`. -/
 def Outputs (tm : SingleTapeTM Symbol) (l l' : List Symbol) : Prop :=
-  ReflTransGen tm.TransitionRelation (initCfg tm l) (haltCfg tm l')
+  ReflTransGen tm.TransitionRelation (initCfg tm l) (tm.haltCfg l')
 
 /-- A proof of `tm` outputting `l'` on input `l` in at most `m` steps. -/
 def OutputsWithinTime (tm : SingleTapeTM Symbol) (l l' : List Symbol) (m : ℕ) :=
-  RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (haltCfg tm l') m
+  RelatesWithinSteps tm.TransitionRelation (initCfg tm l) (tm.haltCfg l') m
+
+/-- A single step of `tm` increases the size of the support of the tape by at most one
+(the position written to). -/
+private lemma step_supportSubset {tm : SingleTapeTM Symbol} {cfg cfg' : tm.Cfg}
+    {s : Finset ℤ} (hs : cfg.BiTape.supportSubset s)
+    (hstep : tm.step cfg = some cfg') :
+    ∃ s' : Finset ℤ, s'.card ≤ s.card + 1 ∧ cfg'.BiTape.supportSubset s' := by
+  obtain ⟨_ | q, tape⟩ := cfg
+  · simp [step] at hstep
+  · simp only [step] at hstep
+    cases htr : tm.tr q tape.read with
+    | mk wd q'' =>
+      obtain ⟨wr, dir⟩ := wd
+      simp only [htr] at hstep
+      cases hstep
+      refine ⟨(insert 0 s).image (· + BiTape.optionMoveToInt dir), ?_, ?_⟩
+      · exact Finset.card_image_le.trans <|
+          (Finset.card_insert_le _ _).trans (by omega)
+      · exact BiTape.supportSubset_optionMove _ _ _
+          (BiTape.supportSubset_write_insert _ _ _ hs)
+
+/-- Iterating the support bound: after `n` steps, the support is contained in a finset
+of cardinality at most the initial support's size plus `n`. -/
+private lemma relatesInSteps_supportSubset {tm : SingleTapeTM Symbol}
+    {cfg cfg' : tm.Cfg} {n : ℕ}
+    (h : RelatesInSteps tm.TransitionRelation cfg cfg' n)
+    {s : Finset ℤ} (hs : cfg.BiTape.supportSubset s) :
+    ∃ s' : Finset ℤ, s'.card ≤ s.card + n ∧ cfg'.BiTape.supportSubset s' := by
+  induction h with
+  | refl => exact ⟨s, by omega, hs⟩
+  | tail _ _ _ _ hstep ih =>
+    obtain ⟨s', hsc, hss⟩ := ih
+    obtain ⟨s'', hsc', hss''⟩ := step_supportSubset hss hstep
+    exact ⟨s'', by omega, hss''⟩
 
 /--
 This lemma bounds the size blow-up of the output of a Turing machine.
@@ -214,9 +224,25 @@ is bounded by the output length of the first machine.
 lemma output_length_le_input_length_add_time (tm : SingleTapeTM Symbol) (l l' : List Symbol) (t : ℕ)
     (h : tm.OutputsWithinTime l l' t) :
     l'.length ≤ max 1 l.length + t := by
-  obtain ⟨steps, hsteps_le, hevals⟩ := h
-  grind [hevals.apply_le_apply_add (Cfg.space_used tm)
-      fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep)]
+  obtain ⟨m, hm, hsteps⟩ := h
+  have h_init : (tm.initCfg l).BiTape.supportSubset
+      ((Finset.range l.length).image (Int.ofNat ·)) := by
+    simpa [initCfg] using BiTape.supportSubset_mk₁ l
+  obtain ⟨s', hsc, hss⟩ := relatesInSteps_supportSubset hsteps h_init
+  have h_subset : (Finset.range l'.length).image (Int.ofNat ·) ⊆ s' := by
+    intro x hx
+    simp only [Finset.mem_image, Finset.mem_range] at hx
+    obtain ⟨n, hn, rfl⟩ := hx
+    apply hss
+    simp [BiTape.mk₁, hn]
+  have h_image_card : ((Finset.range l'.length).image (Int.ofNat ·)).card = l'.length := by
+    rw [Finset.card_image_of_injective _ (fun _ _ h => Int.ofNat.inj h)]
+    simp
+  have hcard0 : ((Finset.range l.length).image (Int.ofNat ·)).card ≤ l.length :=
+    Finset.card_image_le.trans (by simp)
+  have h_le : l'.length ≤ s'.card := h_image_card ▸ Finset.card_le_card h_subset
+  omega
+
 
 section Computers
 
@@ -304,7 +330,7 @@ private theorem map_toCompCfg_left_step (hcfg1 : cfg1.state.isSome) :
     | none => grind
     | some q =>
       simp only [step, toCompCfg_left, compComputer]
-      generalize hM : tm1.tr q BiTape.head = result
+      generalize hM : tm1.tr q BiTape.read = result
       obtain ⟨⟨wr, dir⟩, nextState⟩ := result
       #adaptation_note
       /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
@@ -320,7 +346,7 @@ private theorem map_toCompCfg_right_step :
     | none =>
       simp only [step, toCompCfg_right, Option.map_none, compComputer]
     | some q =>
-      generalize hM : tm2.tr q BiTape.head = result
+      generalize hM : tm2.tr q BiTape.read = result
       obtain ⟨⟨wr, dir⟩, nextState⟩ := result
       simp only [compComputer]
       grind [toCompCfg_right, step, compComputer]
@@ -401,7 +427,12 @@ structure TimeComputable (f : List Symbol → List Symbol) where
 def TimeComputable.id : TimeComputable (Symbol := Symbol) id where
   tm := idComputer
   time_bound _ := 1
-  outputsFunInTime _ := ⟨1, le_rfl, RelatesInSteps.single rfl⟩
+  outputsFunInTime a :=
+    ⟨1, le_rfl, RelatesInSteps.single (by
+      change idComputer.step (idComputer.initCfg a) = some (idComputer.haltCfg a)
+      simp only [step, idComputer, initCfg, haltCfg, BiTape.write_read,
+        BiTape.optionMove, BiTape.optionMoveToInt, BiTape.moveInt]
+      ext i; simp)⟩
 
 /--
 Time bounds for `compComputer`.
@@ -449,9 +480,8 @@ def TimeComputable.comp {f g : List Symbol → List Symbol}
     have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
     apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
     refine Nat.add_le_add_left ?_ (hf.time_bound a.length)
-    · apply h_mono
-      -- Use the lemma about output length being bounded by input length + time
-      exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a)
+    apply h_mono
+    exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFunInTime a)
 
 end TimeComputable
 

Cslib/Foundations/Data/BiTape.lean

@@ -9,8 +9,12 @@ module
 public import Cslib.Foundations.Data.StackTape
 public import Mathlib.Computability.TuringMachine.Tape
 public import Mathlib.Data.Finset.Attr
+public import Mathlib.Data.Finset.Range
+public import Mathlib.Data.Finset.Card
+public import Mathlib.Data.Finset.Image
 public import Mathlib.Tactic.SetLike
 public import Mathlib.Algebra.Order.Group.Nat
+public import Mathlib.Tactic.Ring
 
 /-!
 # BiTape: Bidirectionally infinite TM tape representation using StackTape
@@ -40,24 +44,17 @@ will not collide.
 
 namespace Turing
 
-/--
-A structure for bidirectionally-infinite Turing machine tapes
-that eventually take on blank `none` values
--/
+@[ext]
 structure BiTape (Symbol : Type) where
-  /-- The symbol currently under the tape head -/
-  head : Option Symbol
-  /-- The contents to the left of the head -/
-  left : StackTape Symbol
-  /-- The contents to the right of the head -/
-  right : StackTape Symbol
+  /-- the tape contents -/
+  cells : ℤ → Option Symbol
 
 namespace BiTape
 
 variable {Symbol : Type}
 
 /-- The empty `BiTape` -/
-def nil : BiTape Symbol := ⟨none, ∅, ∅⟩
+def nil : BiTape Symbol := ⟨fun _ => none⟩
 
 instance : Inhabited (BiTape Symbol) where
   default := nil
@@ -73,75 +70,78 @@ Given a `List` of `Symbol`s, construct a `BiTape` by mapping the list to `some`
 and laying them out to the right side,
 with the head under the first element of the list if it exists.
 -/
-def mk₁ (l : List Symbol) : BiTape Symbol :=
-  match l with
-  | [] => ∅
-  | h :: t => { head := some h, left := ∅, right := StackTape.map_some t }
+def mk₁ {Symbol : Type} (l : List Symbol) : BiTape Symbol :=
+  { cells
+    | .ofNat n => l[n]?
+    | _ => none }
 
 section Move
 
-/--
-Move the head left by shifting the left StackTape under the head.
--/
-def move_left (t : BiTape Symbol) : BiTape Symbol :=
-  ⟨t.left.head, t.left.tail, StackTape.cons t.head t.right⟩
-
-/--
-Move the head right by shifting the right StackTape under the head.
--/
-def move_right (t : BiTape Symbol) : BiTape Symbol :=
-  ⟨t.right.head, StackTape.cons t.head t.left, t.right.tail⟩
+@[simp, local grind =]
+def optionMoveToInt : Option Dir → ℤ
+  | none => 0
+  | some .left => -1
+  | some .right => 1
 
-/--
-Move the head to the left or right, shifting the tape underneath it.
--/
-def move (t : BiTape Symbol) : Dir → BiTape Symbol
-  | .left => t.move_left
-  | .right => t.move_right
+@[simp, local grind =]
+def moveInt (t : BiTape Symbol) (δ : ℤ) : BiTape Symbol := ⟨ fun i => t.cells (i - δ) ⟩
 
 /--
 Optionally perform a `move`, or do nothing if `none`.
 -/
-def optionMove : BiTape Symbol → Option Dir → BiTape Symbol
-  | t, none => t
-  | t, some d => t.move d
-
-@[simp]
-lemma move_left_move_right (t : BiTape Symbol) : t.move_left.move_right = t := by
-  simp [move_right, move_left]
-
-@[simp]
-lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by
-  simp [move_left, move_right]
+@[simp, local grind =]
+def optionMove (t : BiTape Symbol) (dir : Option Dir) : BiTape Symbol :=
+  t.moveInt (optionMoveToInt dir)
 
 end Move
 
 /--
 Write a value under the head of the `BiTape`.
 -/
-def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a }
+@[local grind =]
+def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol :=
+  ⟨ Function.update t.cells 0 a ⟩
+
+@[local grind =]
+def read (t : BiTape Symbol) : Option Symbol := t.cells 0
+
+@[simp]
+lemma write_read (t : BiTape Symbol) : t.write t.read = t := by simp [write, read]
 
 /--
-The space used by a `BiTape` is the number of symbols
-between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`.
+The cells of `t` are non-blank only at indices in `s`.
 -/
-@[scoped grind]
-def space_used (t : BiTape Symbol) : ℕ := 1 + t.left.length + t.right.length
-
-@[simp, grind =]
-lemma space_used_write (t : BiTape Symbol) (a : Option Symbol) :
-    (t.write a).space_used = t.space_used := by rfl
-
-lemma space_used_mk₁ (l : List Symbol) :
-    (mk₁ l).space_used = max 1 l.length := by
-  cases l with
-  | nil => simp [mk₁, space_used, nil, StackTape.length_nil]
-  | cons h t => simp [mk₁, space_used, StackTape.length_nil, StackTape.length_map_some]; omega
-
-lemma space_used_move (t : BiTape Symbol) (d : Dir) :
-    (t.move d).space_used ≤ t.space_used + 1 := by
-  cases d <;> grind [move_left, move_right, move,
-    space_used, StackTape.length_tail_le, StackTape.length_cons_le]
+def supportSubset (t : BiTape Symbol) (s : Finset ℤ) : Prop :=
+  ∀ i, t.cells i ≠ none → i ∈ s
+
+lemma supportSubset_mk₁ (l : List Symbol) :
+    supportSubset (mk₁ l) ((Finset.range l.length).image (Int.ofNat ·)) := by
+  intro i hi
+  simp only [mk₁] at hi
+  match i with
+  | .ofNat n => grind
+  | .negSucc n => grind
+
+lemma supportSubset_write_insert (t : BiTape Symbol) (a : Option Symbol) (s : Finset ℤ)
+    (hs : supportSubset t s) : supportSubset (t.write a) (insert 0 s) := by
+  intro i hi
+  simp only [write] at hi
+  by_cases h : i = 0
+  · simp [h]
+  · rw [Function.update_of_ne h] at hi
+    exact Finset.mem_insert_of_mem (hs i hi)
+
+lemma supportSubset_moveInt (t : BiTape Symbol) (δ : ℤ) (s : Finset ℤ)
+    (hs : supportSubset t s) :
+    supportSubset (t.moveInt δ) (s.image (· + δ)) := by
+  intro i hi
+  simp only [moveInt] at hi
+  exact Finset.mem_image.mpr ⟨i - δ, hs _ hi, by ring⟩
+
+lemma supportSubset_optionMove (t : BiTape Symbol) (d : Option Dir) (s : Finset ℤ)
+    (hs : supportSubset t s) :
+    supportSubset (t.optionMove d) (s.image (· + optionMoveToInt d)) :=
+  supportSubset_moveInt _ _ _ hs
 
 end BiTape
 

Cslib/Foundations/Data/OmegaSequence/Flatten.lean

@@ -150,7 +150,7 @@ theorem flatten_drop [Inhabited α]
   (flatten_take_drop h_ls n).2
 
 /-- `ls n` is the segement from position `ls.cumLen n` to position `ls.cumLen (n + 1) - 1`
-of ls.flatten` -/
+of `ls.flatten` -/
 @[simp, scoped grind =]
 theorem extract_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0)
     (n : ℕ) : ls.flatten.extract (ls.cumLen n) (ls.cumLen (n + 1)) = ls n := by
@@ -159,6 +159,15 @@ theorem extract_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k
   have h_take := flatten_take h_ls' 1
   grind [extract_eq_drop_take]
 
+/-- Distributivity of "forall" over `flatten`. -/
+theorem forall_flatten_iff [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0)
+    (p : α → Prop) : (∀ n, p (ls.flatten n)) ↔ ∀ k, (ls k).Forall p := by
+  constructor
+  · simp only [List.forall_iff_forall_mem, List.forall_mem_iff_getElem, ← extract_flatten h_ls]
+    grind
+  · have := segment_upper_bound (cumLen_strictMono h_ls)
+    grind [List.forall_iff_forall_mem, flatten_def]
+
 /-- Given an ω-sequence `s` and a function `f : ℕ → ℕ`, `s.toSegs f` is the ω-sequence
 whose `n`-th element is the list `s.extract (f n) (f (n + 1))`.  In all its uses, the
 function `f` will always be assumed to be strictly monotonic with `f 0 = 0`. -/