Utm

Cslib/Computability/Machines/MultiTapeTuring/Data.lean

@@ -18,6 +18,10 @@ public inductive Data where
   /-- A list of data values. -/
   | list : List Data → Data
 
+public abbrev Data.empty : Data := Data.list []
+
+public abbrev Data.cons : Data → Data → Data := fun d ⟨ds⟩ => Data.list (d :: ds)
+
 /-- Extract the list of children from a `Data` value. -/
 @[expose]
 public abbrev Data.toList : Data → List Data
@@ -291,6 +295,11 @@ public lemma Data.atPath_append {d : Data} {path₁ path₂ : List ℕ} :
     cases d with
     | list ds => grind [Data.atPath]
 
+public lemma Data.atPath_isSome_of_cons_isSome {d : Data} {i : ℕ} {path : List ℕ}
+    (h : (d.atPath (i :: path)).isSome) :
+    (d.atPath [i]).isSome := by
+  sorry
+
 @[simp]
 public lemma Data.atPath_get_atPath {d : Data} {path₁ path₂ : List ℕ}
     (h_valid : (d.atPath path₁).isSome) :
@@ -322,6 +331,14 @@ public lemma Data.atPath_dropLast_bind_getLast {d : Data} {path : List ℕ}
     simp [List.dropLast_append_getLast?]]
   simp [Data.atPath_append]
 
+
+@[simp]
+public lemma Data.atPath_take_isSome_of_isSome {d : Data} {path : List ℕ} {n : ℕ}
+    (h_is_some : (d.atPath path).isSome) :
+  (d.atPath (path.take n)).isSome := by
+  sorry
+
+
 public lemma Data.atPath_isSome_of_le_isSome {d : Data} {i₁ i₂ : ℕ}
     (h_le : i₁ ≤ i₂)
     (h_is_some : (d.atPath [i₂]).isSome) :
@@ -473,10 +490,10 @@ public lemma atPath_toData_one_pair {α β : Type*} [StrEnc α] [StrEnc β]
     graph: a list of `(a, f a)` pairs.
     Not registered as an instance to avoid overlap with `Fin k → α`.
     Activate with `letI := StrEnc.ofFunction α β`. -/
-@[reducible]
-public noncomputable def StrEnc.ofFunction (α : Type) (β : Type*)
-    [Fintype α] [StrEnc α] [StrEnc β] : StrEnc (α → β) where
-  toData f := StrEnc.toData (Finset.univ.val.toList.map fun a => (a, f a))
+@[reducible, expose]
+public def StrEnc.ofFunction (α : Type) (β : Type*)
+    [Fintype α] [LinearOrder α] [StrEnc α] [StrEnc β] : StrEnc (α → β) where
+  toData f := StrEnc.toData ((Finset.univ.sort (· ≤ ·)).map fun a => (a, f a))
 
 /-- `StrEnc` instance for any `Encodable` type via its encoding to `ℕ`.
     Not registered as an instance to avoid overlap with specific encodings

Cslib/Computability/Machines/MultiTapeTuring/Routines/Copy.lean

@@ -8,6 +8,7 @@ module
 
 public import Cslib.Computability.Machines.MultiTapeTuring.Routines.Put
 public import Cslib.Computability.Machines.MultiTapeTuring.Routines.Typed
+public import Cslib.Computability.Machines.MultiTapeTuring.Routines.Untyped
 
 namespace Turing
 namespace Routines
@@ -33,5 +34,11 @@ public lemma copyEnc_computes_fun {k : ℕ} {α : Type} [StrEnc α] {i j : Fin k
   simp [copyEnc_eval_struct, h_ne]
   grind
 
+
+-- @[simp, grind .]
+-- public def copyEnc_computes_fun {k : ℕ} {i j : Fin k} (h_ne : i ≠ j) :
+--   ComputesFunctionReadPut (copyEnc i j) i j := by
+--   sorry
+
 end Routines
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/Routines/EvalFun.lean

@@ -0,0 +1,79 @@
+/-
+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.Routines.Put
+public import Cslib.Computability.Machines.MultiTapeTuring.Routines.Typed
+
+namespace Turing
+namespace Routines
+
+/-- If a tape contains the encoding of a function, navigates to the value part belonging
+to a certain input and executes `tm`.
+TODO: Can probably be implemented using find_list. -/
+public def atFunctionValue {k : ℕ} (tm : MultiTapeTM k Char) (f input : Fin k) :
+  MultiTapeTM k Char := sorry
+
+/-- The index of the given value in the sorted list of all values of its type. -/
+public def indexInType {α : Type} [Fintype α] [LinearOrder α] (x : α) : ℕ :=
+  (Finset.univ.sort (· ≤ ·)).idxOf x
+
+public lemma indexInTypeValid {α : Type} [Fintype α] [LinearOrder α] (x : α) :
+  indexInType x < Fintype.card α := by
+  simp [indexInType]
+  sorry
+
+@[simp]
+public lemma atFunctionValue.eval_struct
+    {α β : Type} [StrEnc α] [Fintype α] [LinearOrder α] [StrEnc β]
+    {k : ℕ} (tm : MultiTapeTM k Char) {f input : Fin k}
+    (h_ne : f ≠ input)
+    {views : Fin k → TapeView}
+    {x : α}
+    {function : α → β}
+    (h_input : (views input).current = StrEnc.toData x)
+    (h_f : (views f).current = (StrEnc.ofFunction α β).toData function) :
+    (atFunctionValue tm f input).eval_struct views = (tm.eval_struct
+      (Function.update views f
+        ((views f).appendPath''
+            [indexInType x, 1] (by simp [h_f, function_graph, Data.atPath, indexInTypeValid])))).map
+          fun views' => Function.update views' f ((views' f).parent.parent.setHeadPosOf (views f)) := by
+  sorry
+
+-- @[simp]
+-- public lemma atPath_computes_function {k : ℕ} {path : List ℕ} {i j : Fin k}
+--     {α β γ : Type} [StrEnc α] [StrEnc β] [StrEnc γ]
+--     {tm : MultiTapeTM k Char}
+--     (h_ne : i ≠ j)
+--     (fPath : α → β)
+--     (h_path : ∀ x, ((StrEnc.toData x).atPath path) = some (StrEnc.toData (fPath x)))
+--     (f : β → γ → γ)
+--     (h_tm : computes_function_read_update' tm f i j) :
+--     computes_function_read_update' (atPath path i tm) (fun a => f (fPath a)) i j := by
+--   intro x y views h_views_i h_views_j
+--   have h_d := h_path x
+--   clear h_path
+--   change (atPath path i tm).eval_struct views =
+--     Part.some (Function.update views j (TapeView.ofEnc (f (fPath x) y)))
+--   generalize StrEnc.toData x = d at h_d h_views_i
+--   generalize fPath x = b at h_d ⊢
+--   induction path generalizing d views with
+--   | nil =>
+--     simp only [Data.atPath_nil, Option.some.injEq] at h_d
+--     exact h_tm b y views (by simp [h_views_i, h_d]) h_views_j
+--   | cons n path' ih =>
+--     rw [show n :: path' = [n] ++ path' from rfl, Data.atPath_append] at h_d
+--     obtain ⟨d₁, hd₁, h_tail⟩ := Option.bind_eq_some_iff.mp h_d
+--     have h_valid : ((views i).current.atPath [n]).isSome := by simp [h_views_i, hd₁]
+--     unfold atPath
+--     rw [atElem_eval_struct h_valid]
+--     rw [ih (Function.update views i ((views i).appendPath' n h_valid))
+--         (by simp [h_ne.symm, h_views_j]) d₁ (by simp; grind) h_tail]
+--     simp [h_ne]
+
+end Routines
+end Turing

Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean

@@ -224,9 +224,27 @@ public theorem find_list.computes_fun {k : ℕ} {i j : Fin k}
     ∀ ls : List α, (views i).current = StrEnc.toData ls →
     views j = TapeView.empty →
     (find_list i j tm₁ tm₂ tm₃).eval_struct views = match ls.findIdx? f with
-      | some idx => tm₂.eval_struct (Function.update views i ((views i).appendPath idx (by sorry)))
+      | some idx => tm₂.eval_struct (Function.update views i ((views i).appendPath' idx (by sorry)))
       | none => tm₃.eval_struct views := by
   sorry
 
+-- public theorem find_list.eval_struct {k : ℕ} {i j : Fin k}
+--     (h_neq : i ≠ j)
+--     {tm₁ tm₂ tm₃ : MultiTapeTM k Char}
+--     (halts₁ : AlwaysHaltsOnStruct tm₁)
+--     -- {f : α → Bool}
+--     -- TODO maybe instead of this, we need that tm₁ does not modify tape i.
+--     -- (h_comp₁ : computes_function_read_replace tm₁ f i j)
+--     (views : Fin k → TapeView) :
+--     (find_list i j tm₁ tm₂ tm₃).eval_struct views =
+--       let length := (views i).current.toList.length
+--       let condition := fun (⟨idx, h⟩ : Fin length) => (tm₁.eval_struct_tot halts₁
+--           (Function.update views i ((views i).appendPath' idx (by sorry)))
+--             j).current = StrEnc.toData true
+--       match Fin.find? condition with
+--       | some idx => tm₂.eval_struct (Function.update views i ((views i).appendPath' idx (by sorry)))
+--       | none => tm₃.eval_struct views := by
+--   sorry
+
 end Routines
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean

@@ -28,11 +28,23 @@ public lemma pushList.computes_fun {k : ℕ} {d : Data} {i : Fin k} :
 /-- Prepend the Data element from tape `i` to the list at tape `j` (prepends it). -/
 public def copy_to_list {k : ℕ} (i j : Fin k) : MultiTapeTM k Char := sorry
 
+@[simp]
+public lemma copy_to_list.eval_struct {k : ℕ} {i j : Fin k} (h_ne : i ≠ j)
+  {views : Fin k → TapeView} :
+  (copy_to_list i j).eval_struct views = some
+    (Function.update views j ((views j).pushList (views i).current)) := by
+  sorry
+
 @[simp]
 public lemma copy_to_list.computes_fun {α : Type} [StrEnc α] {k : ℕ} {i j : Fin k} (h_ne : i ≠ j) :
   computes_function_read_push (α := α) (copy_to_list i j) id i j := by
   sorry
 
+@[simp]
+public lemma copy_to_list.computes_fun' {α : Type} [StrEnc α] {k : ℕ} {i j : Fin k} (h_ne : i ≠ j) :
+  computes_function_read_push' (α := α) (copy_to_list i j) id i j := by
+  sorry
+
 /-- Remove the first element from a list encoding on tape `i`.
     Running `popEnc` on an empty list does not modify the tape. -/
 public def popList {k : ℕ} (i : Fin k) : MultiTapeTM k Char := sorry

Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean

@@ -100,6 +100,9 @@ lemma outOfList_inner {k : ℕ} {i : Fin k}
 public lemma outOfList_eval_struct {k : ℕ} {i : Fin k} {views : Fin k → TapeView} :
   (outOfList i).eval_struct views = some (Function.update views i (views i).parent) := by sorry
 
+public lemma outOfList_eval_struct' {k : ℕ} {i : Fin k} :
+  (outOfList i).eval_struct = fun views => .some (Function.update views i (views i).parent) := by sorry
+
 
 /-- Navigate to the `idx`-th element of a `Data.list` encoding on tape `i`.
 Moves past `(` and then skips `idx` Data elements.
@@ -156,6 +159,22 @@ public lemma atElem_computes_function {k : ℕ} {idx : ℕ} {i j : Fin k}
   rw [h_tm (fElem x) y _ (by simp; grind) (by grind)]
   simp [h_ne]
 
+/-- Like atElem, but execute tm₁ if the element exists and tm₂ otherwise. -/
+public def atElem? {k : ℕ} (idx : ℕ) (i : Fin k) (tm₁ tm₂ : MultiTapeTM k Char) :
+  MultiTapeTM k Char := sorry
+
+@[simp]
+public lemma atElem?_eval_struct {k : ℕ} {idx : ℕ} {i : Fin k} {tm₁ tm₂ : MultiTapeTM k Char}
+    {views : Fin k → TapeView} :
+    (atElem? idx i tm₁ tm₂).eval_struct views =
+      if h : ((views i).current.atPath [idx]).isSome then
+        (tm₁.eval_struct
+          (Function.update views i ((views i).appendPath' idx h))).map
+            fun views' => Function.update views' i ((views' i).parent.setHeadPosOf (views i))
+      else
+        (tm₂.eval_struct views) := by
+  sorry
+
 -- TODO this has a double toLeftEnd which is not needed.
 
 /-- Move into the given path, then execute `tm` and then move out again. -/
@@ -197,5 +216,36 @@ public lemma atPath_computes_function {k : ℕ} {path : List ℕ} {i j : Fin k}
     simp [h_ne]
 
 
+/-- Move into the given path, if it exists, then execute `tm₁` and then move out again,
+if it does not exist, execute `tm₂` at the initial position. -/
+public def atPath? {k : ℕ} (path : List ℕ) (i : Fin k) (tm₁ tm₂ : MultiTapeTM k Char) :
+    MultiTapeTM k Char :=
+  match path with
+  | [] => atLeft i tm₁
+  | n :: path' => atElem? n i (atPath? path' i tm₁ (outOfList i ;ₜ tm₂)) tm₂
+
+
+@[simp]
+public lemma atPath?_eval_struct {k : ℕ} {path : List ℕ} {i : Fin k} {tm₁ tm₂ : MultiTapeTM k Char}
+    {views : Fin k → TapeView} :
+    (atPath? path i tm₁ tm₂).eval_struct views =
+      if h : ((views i).current.atPath path).isSome then
+        (tm₁.eval_struct (Function.update views i ((views i).appendPath'' path h))).map
+          fun views' => Function.update views' i
+            (((views' i).parent_n path.length).setHeadPosOf (views i))
+      else
+        (tm₂.eval_struct views) := by
+  induction path generalizing views tm₁ tm₂ with
+  | nil => simp [atPath?]
+  | cons n path' ih =>
+    unfold atPath?
+    by_cases h : ((views i).current.atPath [n]).isSome
+    · simp [h, -TapeView.parent, -TapeView.appendPath', -TapeView.appendPath'']
+      rw [ih]
+      simp
+      sorry
+    · simp [h]
+      sorry -- TODO what is left is the first case which is a contradiction
+
 end Routines
 end Turing

Cslib/Computability/Machines/MultiTapeTuring/Routines/Put.lean

@@ -86,17 +86,17 @@ public theorem clear.eval {i : Fin k} {tapes : Fin k → BiTape Char} {ls : List
 
 /-- Replace the contents of tape `i` by the encoding of `d`. -/
 public def replace {k : ℕ} (d : Data) (i : Fin k) : MultiTapeTM k Char :=
-  clear i;ₜ put d i
+  sorry
+  -- TODO move to the left and then
+  -- clear i;ₜ put d i
 
 @[simp]
-public lemma replace.eval_struct {k : ℕ} {d : Data} {i : Fin k} {views : Fin k → TapeView}
-  (h_data : (views i).path = [])
-  -- TODO remove this condition by skipping to the left end if we are on the right end.
-  (h_left : (views i).headPos = .leftEnd) :
+public lemma replace.eval_struct {k : ℕ} {d : Data} {i : Fin k} {views : Fin k → TapeView} :
   (replace d i).eval_struct views = some (Function.update views i (.ofData d)) := by
-  simp only [MultiTapeTM.eval_struct, replace, MultiTapeTM.seq_eval]
-  rw [clear.eval (ls := (views i).data.enc) (by simp [TapeView.toBiTape, h_data, h_left])]
-  simp [put_eval (old := []), ← TapeView.toBiTape_ofData]
+  sorry
+  -- simp only [MultiTapeTM.eval_struct, replace, MultiTapeTM.seq_eval]
+  -- rw [clear.eval (ls := (views i).data.enc) (by simp [TapeView.toBiTape, h_data, h_left])]
+  -- simp [put_eval (old := []), ← TapeView.toBiTape_ofData]
 
 
 end Routines

Cslib/Computability/Machines/MultiTapeTuring/StructuralMachines.lean

@@ -29,6 +29,18 @@ public def MultiTapeTM.eval_struct
     Part (Fin k → TapeView) :=
   tm.eval (TapeView.toBiTape ∘ views) >>= (TapeView.ofBiTapes? ·)
 
+/-- The Turing machine `tm` eventually halts starting from any initial TapeView and
+the tapes are all a valid encodings of TapeView. -/
+@[expose]
+public def AlwaysHaltsOnStruct (tm : MultiTapeTM k Char) : Prop :=
+  ∀ views, (tm.eval_struct views).Dom
+
+@[expose]
+public def MultiTapeTM.eval_struct_tot
+    (tm : MultiTapeTM k Char) (h_halts : AlwaysHaltsOnStruct tm) (views : Fin k → TapeView) :
+    Fin k → TapeView :=
+  (tm.eval_struct views).get (h_halts views)
+
 -- TODO clean up (AI)
 public theorem MultiTapeTM.eval_of_eval_struct
     {tm : MultiTapeTM k Char} {views views' : Fin k → TapeView}

Cslib/Computability/Machines/MultiTapeTuring/TapeView.lean

@@ -97,6 +97,14 @@ public lemma current_atPath_length_sub_one_isSome_of_non_empty (tv : TapeView)
 @[expose, simp]
 public def parent (tv : TapeView) : TapeView := ⟨tv.data, tv.path.dropLast, tv.headPos, by simp⟩
 
+@[expose]
+public def parent_n (tv : TapeView) (n : ℕ) : TapeView :=
+  ⟨tv.data, tv.path.take (tv.path.length - n), tv.headPos, by simp⟩
+
+@[simp]
+public def parent_zero (tv : TapeView) : parent_n tv 0 = tv := by
+  simp [parent_n]
+
 -- @[simp]
 -- public lemma parent_data (tv : TapeView) : tv.parent.data = tv.data := by
 --   unfold parent
@@ -118,12 +126,20 @@ public def appendPath (tv : TapeView) (idx : ℕ)
     (h : (tv.current.atPath [idx]).isSome) : TapeView :=
   ⟨tv.data, tv.path ++ [idx], tv.headPos, by simpa using h⟩
 
-/-- Like `appendPath` but always sets `headPos` to `.leftEnd`. -/
+/-- Like `appendPath` but always sets `headPos` to `.leftEnd`.
+-- TODO rename to appendToPath or consPath or snocPath -/
 @[expose, simp]
 public def appendPath' (tv : TapeView) (idx : ℕ)
     (h : (tv.current.atPath [idx]).isSome) : TapeView :=
   ⟨tv.data, tv.path ++ [idx], .leftEnd, by simpa using h⟩
 
+
+/-- Like `appendPath` but always sets `headPos` to `.leftEnd`. -/
+@[expose, simp]
+public def appendPath'' (tv : TapeView) (path : List ℕ)
+    (h : (tv.current.atPath path).isSome) : TapeView :=
+  ⟨tv.data, tv.path ++ path, .leftEnd, by simpa using h⟩
+
 /-- Copy the `headPos` from `tv'` into `tv`, keeping all other fields. -/
 @[expose]
 public abbrev setHeadPosOf (tv tv' : TapeView) : TapeView :=
@@ -164,6 +180,13 @@ public lemma toRightEnd_toLeftEnd (tv : TapeView) :
   tv.toRightEnd.toLeftEnd = tv.toLeftEnd := by
   ext <;> simp_all
 
+-- /-- simp lemma that says that `(tv.appendPath' n _).parent = tv.toLeftEnd -/
+-- @[simp]
+-- public lemma parent_appendPath' (tv : TapeView) (idx : ℕ)
+--     (h : (tv.current.atPath [idx]).isSome) :
+--   (tv.appendPath' idx h).parent = tv.toLeftEnd := by
+--   simp [appendPath', parent, toLeftEnd]
+
 /-- The position of the head in the encoded version of the
     `TapeView`. -/
 @[expose]
@@ -675,6 +698,12 @@ public def pushList (d : Data) (tv : TapeView) : TapeView :=
   | ⟨Data.list ds, [], headPos, _⟩ => ⟨Data.list (d :: ds), [], headPos, rfl⟩
   | other => other
 
+@[simp]
+public lemma pushList_ofData {x d : Data} :
+    (TapeView.ofData d).pushList x = TapeView.ofEnc (x :: d.toList) := by
+  simp [pushList, ofData, ofEnc]
+  sorry
+
 @[simp]
 public lemma pushList_list {d : Data} {ds : List Data} {headPos : HeadPos} :
     (TapeView.mk (Data.list ds) [] headPos rfl).pushList d =