Reachability

Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean

@@ -48,7 +48,7 @@ theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} :
       dya_inv ((tapes 1).headD [])) :: (tapes 2)))) := by
   simp [add₀]
   by_cases h : dya_inv ((tapes 0).head?.getD []) = 0
-  · simp [h]; grind
+  · simp [h]
   · grind
 
 /--

Cslib/Computability/Machines/MultiTapeTuring/Basic.lean

@@ -238,6 +238,10 @@ def TransformsTapes
     (tapes tapes' : Fin k → BiTape α) : Prop :=
   ∃ t, tm.TransformsTapesInTime tapes tapes' t
 
+/-- The Turing machine `tm` eventually halts starting from any initial tape configuration. -/
+def haltsOn (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) : Prop :=
+  ∃ tapes', tm.TransformsTapes tapes tapes'
+
 @[scoped grind =]
 lemma relatesInSteps_iff_step_iter_eq_some
     (tm : MultiTapeTM k α)
@@ -294,6 +298,13 @@ public noncomputable def eval (tm : MultiTapeTM k α) (tapes : Fin k → BiTape
     Part (Fin k → BiTape α) :=
   ⟨∃ tapes', tm.TransformsTapes tapes tapes', fun h => h.choose⟩
 
+/--
+Execute the Turing machine `tm` on initial tapes `tapes` given a proof that it always halts
+and thus this yields a total function. -/
+public noncomputable def eval_tot (tm : MultiTapeTM k α) {h : ∀ tapes, tm.haltsOn tapes}
+  (tapes : Fin k → BiTape α) : Fin k → BiTape α :=
+  (tm.eval tapes).get (h tapes)
+
 -- TODO use MultiTapeTM.configurations?
 -- TODO this is a simple consequence of relatesInSteps_iff_configurations_eq_some, maybe not needed.
 lemma configurations_of_transformsTapesInTime

Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean

@@ -31,22 +31,21 @@ lemma copy₁_eval_list {tapes : Fin 2 → List (List α)} :
 A Turing machine that copies the first word on tape `i` to tape `j`.
 If Tape `i` is empty, pushes the empty word to tape `j`.
 -/
-public def copy {k : ℕ} (i j : ℕ)
-  (h_neq : i ≠ j := by decide)
-  (h_i_lt : i < k := by decide)
-  (h_j_lt : j < k := by decide) :
-  MultiTapeTM k (WithSep α) :=
-  copy₁.with_tapes [⟨i, h_i_lt⟩, ⟨j, h_j_lt⟩].get (by intro x y; grind)
+public def copy {k : ℕ}
+  (i j : Fin (k + 2))
+  (h_inj : [i, j].get.Injective := by intro x y; grind) :
+  MultiTapeTM (k + 2) (WithSep α) :=
+  copy₁.with_tapes [i, j].get (by intro x y; grind)
 
 @[simp, grind =]
 public lemma copy_eval_list
-  {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k}
-  {tapes : Fin k → List (List α)} :
-  (copy i j (h_neq := h_neq) (h_i_lt) (h_j_lt)).eval_list tapes = Part.some
-    (Function.update tapes ⟨j, h_j_lt⟩
-      (((tapes ⟨i, h_i_lt⟩).headD []) :: (tapes ⟨j, h_j_lt⟩))) := by
-  have h_inj : [(⟨i, h_i_lt⟩ : Fin k), ⟨j, h_j_lt⟩].get.Injective := by intro x y; grind
-  simp_all [copy]
+  {k : ℕ}
+  (i j : Fin (k + 2))
+  (h_inj : [i, j].get.Injective := by intro x y; grind)
+  {tapes : Fin (k + 2) → List (List α)} :
+  (copy i j h_inj).eval_list tapes = Part.some
+    (Function.update tapes j (((tapes i).headD []) :: (tapes j))) := by
+  simpa [copy] using apply_updates_function_update h_inj
 
 end Routines
 

Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean

@@ -0,0 +1,91 @@
+/-
+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.MultiTapeTuring.Basic
+public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding
+public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
+public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.SuccRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator
+public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator
+
+namespace Turing
+
+namespace Routines
+
+def dec₀ : MultiTapeTM 6 (WithSep OneTwo) :=
+  push 1 [] <;> push 2 [] <;>
+  loop 0 (h_i := by decide) (pop 2 <;> copy 1 2 <;> succ 1) <;>
+  pop 0 <;>
+  copy 2 0 <;>
+  pop 2 <;>
+  pop 1
+
+@[simp]
+lemma inner_eval_iter {r : ℕ} {tapes : Fin 3 → List (List OneTwo)} :
+  (Part.bind · (pop 2 <;> copy 1 2 <;> succ 1).eval_list)^[r] (.some tapes) = Part.some (
+    if r = 0 then
+      tapes
+    else
+      Function.update (Function.update tapes
+        2 ((dya ((dya_inv ((tapes 1).headD [])) + (r - 1))) :: (tapes 2).tail))
+        1 ((dya ((dya_inv ((tapes 1).headD [])) + r)) :: (tapes 1).tail)) := by
+  induction r with
+  | zero => simp
+  | succ r ih =>
+    rw [Function.iterate_succ_apply']
+    simp [ih]
+    grind
+
+@[simp]
+lemma loop_eval_iter {tapes : Fin 6 → List (List OneTwo)} :
+  (loop 0 (h_i := by decide) (pop 2 <;> copy 1 2 <;> succ 1)).eval_list tapes = .some (
+    if dya_inv ((tapes 0).head?.getD []) = 0 then
+      tapes
+    else
+      Function.update (Function.update tapes
+        2 (dya (dya_inv ((tapes 1).head?.getD []) +
+               (dya_inv ((tapes 0).head?.getD []) - 1)) :: (tapes 2).tail))
+        1 (dya (dya_inv ((tapes 1).head?.getD []) +
+                dya_inv ((tapes 0).head?.getD [])) :: (tapes 1).tail)) := by
+  by_cases h : dya_inv ((tapes 0).head?.getD []) = 0
+  · simp [h]
+  · simp [h]; grind
+
+@[simp, grind =]
+lemma dec₀_eval_list {tapes : Fin 6 → List (List OneTwo)} :
+  dec₀.eval_list tapes = .some (Function.update tapes 0
+    ((dya ((dya_inv ((tapes 0).headD [])) - 1)) :: (tapes 0).tail)) := by
+  by_cases h : dya_inv ((tapes 0).head?.getD []) = 0
+  · simp [dec₀, h]; grind
+  · simp [dec₀, h]; grind
+
+/--
+A Turing machine that decrements the dyadic value at the head of tape `i`.
+If the value is zero already, keeps it at zero. If the tape is empty, pushes zero.
+-/
+public def dec {k : ℕ} (i : Fin (k + 6))
+  (aux : Fin (k + 6) := ⟨k + 1, by omega⟩)
+  (h_inj : [i, aux, aux + 1, aux + 2, aux + 3, aux + 4].get.Injective :=
+    by intro x y; grind) :
+  MultiTapeTM (k + 6) (WithSep OneTwo) :=
+  dec₀.with_tapes [i, aux, aux + 1, aux + 2, aux + 3, aux + 4].get h_inj
+
+@[simp, grind =]
+public theorem dec_eval_list {k : ℕ} (i aux : Fin (k + 6))
+  (h_inj : [i, aux, aux + 1, aux + 2, aux + 3, aux + 4].get.Injective)
+  (tapes : Fin (k + 6) → List (List OneTwo)) :
+  (dec i aux h_inj).eval_list tapes = .some (Function.update tapes i
+    ((dya ((dya_inv ((tapes i).headD [])) - 1)) :: (tapes i).tail)) := by
+  simpa [dec] using apply_updates_function_update h_inj
+
+end Routines
+
+end Turing

Cslib/Computability/Machines/MultiTapeTuring/DuplicateRoutine.lean

@@ -0,0 +1,53 @@
+/-
+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.MultiTapeTuring.Basic
+public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding
+public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes
+public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine
+public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator
+
+namespace Turing
+
+namespace Routines
+
+variable [Inhabited α] [Fintype α]
+
+def duplicate₀ : MultiTapeTM 2 (WithSep α) := copy 0 1 <;> copy 1 0 <;> pop 1
+
+@[simp]
+lemma duplicate₀_eval_list {tapes : Fin 2 → List (List α)} :
+  duplicate₀.eval_list tapes = .some (Function.update tapes 0
+    (((tapes 0).headD []) :: (tapes 0))) := by
+  simp [duplicate₀]
+  grind
+
+/--
+A Turing machine that duplicates the head of tape `i` (or pushes the empty word
+if the tape is empty.
+-/
+public def duplicate {k : ℕ} (i : Fin k.succ)
+  (aux : Fin k.succ := ⟨k, by omega⟩)
+  (h_inj : [i, aux].get.Injective := by intro x y; grind) :
+  MultiTapeTM k.succ (WithSep α) :=
+  duplicate₀.with_tapes [i, aux].get h_inj
+
+@[simp, grind =]
+public theorem duplicate_eval_list {k : ℕ} {i : Fin k.succ}
+  (aux : Fin k.succ := ⟨k, by omega⟩)
+  (h_inj : [i, aux].get.Injective)
+  {tapes : Fin k.succ → List (List OneTwo)} :
+  (duplicate i aux h_inj).eval_list tapes = Part.some (Function.update tapes i
+    (((tapes i).headD []) :: (tapes i))) := by
+  simp [duplicate]
+  grind
+
+end Routines
+
+end Turing

Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean

@@ -47,10 +47,11 @@ public def eq {k : ℕ} (q s t : Fin k)
   MultiTapeTM k (WithSep OneTwo) :=
   eq₀.with_tapes [q, s, t].get h_inj
 
+-- TODO why does the linter complain about simp here?
 @[grind =]
-public theorem eq_eval_list {k : ℕ} {q s t : Fin k}
+public theorem eq_eval_list {k : ℕ} {q s t : Fin k.succ}
   (h_inj : [q, s, t].get.Injective)
-  {tapes : Fin k → List (List OneTwo)} :
+  {tapes : Fin k.succ → List (List OneTwo)} :
   (eq q s t).eval_list tapes =
     Part.some (Function.update tapes t ((if (tapes q).headD [] = (tapes s).headD [] then
       [.one]