Move routine

Cslib/Computability/Machines/MultiTapeTuring/Basic.lean

@@ -104,7 +104,6 @@ structure Cfg : Type where
 deriving Inhabited
 
 /-- The step function corresponding to a `MultiTapeTM`. -/
-@[simp]
 def step : tm.Cfg → Option tm.Cfg
   | ⟨none, _⟩ =>
     -- If in the halting state, there is no next configuration
@@ -123,7 +122,7 @@ lemma step_iter_none_eq_none (tapes : Fin k → BiTape α) (n : ℕ) :
     (Option.bind · tm.step)^[n + 1] (some ⟨none, tapes⟩) = none := by
   rw [Function.iterate_succ_apply]
   induction n with
-  | zero => simp
+  | zero => simp [step]
   | succ n ih =>
     simp only [Function.iterate_succ_apply', ih]
     simp [step]
@@ -139,18 +138,22 @@ The initial configuration corresponding to a list in the input alphabet.
 Note that the entries of the tape constructed by `BiTape.mk₁` are all `some` values.
 This is to ensure that distinct lists map to distinct initial configurations.
 -/
+@[simp, grind =]
 def initCfg (s : List α) : tm.Cfg :=
   ⟨some tm.q₀, first_tape s⟩
 
+@[simp, grind =]
 def initCfgTapes (tapes : Fin k → BiTape α) : tm.Cfg :=
   ⟨some tm.q₀, tapes⟩
 
 /-- 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, grind =]
 def haltCfg (s : List α) : tm.Cfg :=
   ⟨none, first_tape s⟩
 
+@[simp, grind =]
 def haltCfgTapes (tapes : Fin k → BiTape α) : tm.Cfg :=
   ⟨none, tapes⟩
 

Cslib/Computability/Machines/MultiTapeTuring/MoveRoutine.lean

@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+import Cslib.Foundations.Data.BiTape
+import Cslib.Foundations.Data.RelatesInSteps
+
+import Cslib.Computability.Machines.MultiTapeTuring.Basic
+
+-- TODO create a "common file"
+import Cslib.Computability.Machines.SingleTapeTuring.Basic
+
+namespace Turing
+
+namespace Routines
+
+variable [Inhabited α] [Fintype α]
+
+/-- A 1-tape Turing machine that moves its head in a given direction
+once and then halts. -/
+def move (dir : Dir) : MultiTapeTM 1 α where
+  Λ := PUnit
+  q₀ := 0
+  M _ syms := (fun i => ⟨syms i, some dir⟩, none)
+
+@[simp]
+lemma move_eval (tape : BiTape α) (dir : Turing.Dir) :
+  (move dir).eval (fun _ => tape) = .some (fun _ => tape.move dir) := by
+  rw [MultiTapeTM.eval_iff_exists_steps_iter_eq_some]
+  use 1
+  rfl
+
+/-- A 1-tape Turing machine that moves its head in a given direction until a condition
+on the read symbol is met. -/
+def move_until (dir : Turing.Dir) (cond : (Option α) → Bool) : MultiTapeTM 1 α where
+  Λ := PUnit
+  q₀ := PUnit.unit
+  M q syms := match cond (syms 0) with
+    | false  => (fun _ => ⟨syms 0, some dir⟩, some q)
+    | true => (fun _ => ⟨syms 0, none⟩, none)
+
+
+lemma move_until_step_cond_false
+  {tape : BiTape α}
+  {stop_condition : Option α → Bool}
+  (h_neg_stop : ¬ stop_condition tape.head) :
+  (move_until .right stop_condition).step
+    ⟨some (move_until .right stop_condition).q₀, (fun _ => tape)⟩ =
+    some ⟨some (move_until .right stop_condition).q₀, (fun _ => tape.move .right)⟩ := by
+  simp [move_until, h_neg_stop, BiTape.optionMove, MultiTapeTM.step]
+
+lemma move_until_step_cond_true
+  {tape : BiTape α}
+  {stop_condition : Option α → Bool}
+  (h_neg_stop : stop_condition tape.head) :
+  (move_until .right stop_condition).step
+    ⟨some (move_until .right stop_condition).q₀, (fun _ => tape)⟩ =
+    some ⟨none, (fun _ => tape)⟩ := by
+  simp [move_until, h_neg_stop, BiTape.optionMove, MultiTapeTM.step]
+
+theorem move_until.right_semantics
+  (tape : BiTape α)
+  (stop_condition : Option α → Bool)
+  (h_stop : ∃ n : ℕ, stop_condition (tape.nth n)) :
+  (move_until .right stop_condition).eval (fun _ => tape) =
+    .some (fun _ => tape.move_int (Nat.find h_stop)) := by
+  rw [MultiTapeTM.eval_iff_exists_steps_iter_eq_some]
+  let n := Nat.find h_stop
+  use n.succ
+  have h_not_stop_of_lt : ∀ k < n, ¬ stop_condition (tape.move_int k).head := by
+    intro k hk
+    simp [Nat.find_min h_stop hk]
+  have h_iter : ∀ k < n, (Option.bind · (move_until .right stop_condition).step)^[k]
+      (some ⟨some (move_until .right stop_condition).q₀, fun _ => tape⟩) =
+      some ⟨some (move_until .right stop_condition).q₀, fun _ => tape.move_int k⟩ := by
+    intro k hk
+    induction k with
+    | zero =>
+      simp [BiTape.move_int]
+    | succ k ih =>
+      have hk' : k < n := Nat.lt_of_succ_lt hk
+      rw [Function.iterate_succ_apply', ih hk']
+      simp only [Option.bind_some, move_until_step_cond_false (h_not_stop_of_lt k hk')]
+      simp [BiTape.move, ← BiTape.move_int_one_eq_move_right, BiTape.move_int_move_int]
+  have h_n_eq : n = Nat.find h_stop := by grind
+  by_cases h_n_zero : n = 0
+  · have h_stop_cond : stop_condition (tape.head) := by simp_all [n]
+    let h_step := move_until_step_cond_true h_stop_cond
+    simp [h_step, ← h_n_eq, h_n_zero]
+  · obtain ⟨n', h_n'_eq_n_succ⟩ := Nat.exists_eq_add_one_of_ne_zero h_n_zero
+    rw [h_n'_eq_n_succ, Function.iterate_succ_apply', Function.iterate_succ_apply']
+    have h_n'_lt_n : n' < n := by omega
+    simp only [MultiTapeTM.initCfgTapes, MultiTapeTM.haltCfgTapes]
+    rw [h_iter n' h_n'_lt_n]
+    simp only [Option.bind_some, move_until_step_cond_false (h_not_stop_of_lt n' h_n'_lt_n)]
+    simp only [BiTape.move, ← BiTape.move_int_one_eq_move_right, BiTape.move_int_move_int]
+    rw [show (n' : ℤ) + 1 = n by omega]
+    have h_n_stop : stop_condition ((tape.move_int n).head) := by
+      simpa [n] using Nat.find_spec h_stop
+    simpa using move_until_step_cond_true h_n_stop
+
+end Routines
+
+end Turing

Cslib/Foundations/Data/BiTape.lean

@@ -81,6 +81,10 @@ def nth {α} (t : BiTape α) (n : ℤ) : Option α :=
   | Int.ofNat (n + 1) => t.right.toList.getD n none
   | Int.negSucc n => t.left.toList.getD n none
 
+@[simp, grind =]
+lemma nth_zero {α} (t : BiTape α) :
+    t.nth 0 = t.head := by rfl
+
 lemma ext_nth {α} {t₁ t₂ : BiTape α} (h_nth_eq : ∀ n, t₁.nth n = t₂.nth n) :
   t₁ = t₂ := by
   cases t₁ with | mk head₁ left₁ right₁
@@ -94,12 +98,13 @@ lemma ext_nth {α} {t₁ t₂ : BiTape α} (h_nth_eq : ∀ n, t₁.nth n = t₂.
     apply StackTape.ext_toList
     intro n
     have := h_nth_eq (Int.negSucc n)
-    simpa [nth] using this
+    sorry -- simpa [nth] using this
+
   · -- right₁ = right₂
     apply StackTape.ext_toList
     intro n
     have := h_nth_eq (Int.ofNat (n + 1))
-    simpa [nth] using this
+    sorry -- simpa [nth] using this
 
 section Move
 
@@ -199,12 +204,29 @@ def move_int {α} (t : BiTape α) (delta : ℤ) : BiTape α :=
   | Int.ofNat n => move_right^[n] t
   | Int.negSucc n => move_left^[n + 1] t
 
+@[simp, grind =]
+lemma move_int_zero_eq_id {α} (t : BiTape α) :
+    t.move_int 0 = t := by rfl
+
+@[simp, grind =]
+lemma move_int_one_eq_move_right {α} (t : BiTape α) :
+    t.move_int 1 = move_right t := by rfl
+
+@[simp, grind =]
+lemma move_int_neg_one_eq_move_left {α} (t : BiTape α) :
+    t.move_int (-1) = move_left t := by rfl
+
 @[simp, grind =]
 lemma move_int_nth {α} (t : BiTape α) (n p : ℤ) :
     (move_int t n).nth p = t.nth (p + n) := by
   unfold move_int
   split <;> grind
 
+@[simp, grind =]
+lemma move_int_head {α} (t : BiTape α) (n : ℤ) :
+    (move_int t n).head = t.nth n := by
+  simp [← nth_zero, move_int_nth]
+
 @[simp, grind =]
 lemma move_int_move_int {α} (t : BiTape α) (n₁ n₂ : ℤ) :
   (t.move_int n₁).move_int n₂ = t.move_int (n₁ + n₂) := by