From 5ebcb37b43b33bd729fb1f464e5f09345eee86b0 Mon Sep 17 00:00:00 2001 From: crei Date: Thu, 30 Apr 2026 19:17:46 +0200 Subject: [PATCH 1/8] Progress on utm. --- .../Routines/ListIteration.lean | 2 +- .../MultiTapeTuring/Routines/ListOps.lean | 5 + .../Machines/MultiTapeTuring/UniversalTM.lean | 178 +++++++++++++----- Cslib/Foundations/Data/BiTape.lean | 6 + 4 files changed, 143 insertions(+), 48 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean index 2a70a7acb7..dba83fefbd 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean @@ -233,7 +233,7 @@ 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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean index f29857b7a4..92942277d4 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean @@ -33,6 +33,11 @@ public lemma copy_to_list.computes_fun {α : Type} [StrEnc α] {k : ℕ} {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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean index 9dc824fa1b..c3ad7e46a4 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean @@ -15,6 +15,7 @@ public import Cslib.Computability.Machines.MultiTapeTuring.Routines.Eq public import Cslib.Computability.Machines.MultiTapeTuring.Routines.Put public import Cslib.Computability.Machines.MultiTapeTuring.Routines.ListIteration public import Cslib.Computability.Machines.MultiTapeTuring.Routines.Typed +import Mathlib.Order.Interval.Finset.Defs namespace Turing @@ -22,54 +23,27 @@ namespace UniversalTM open Routines -/-- TODO document -/ -public abbrev Var := ℕ +variable [Inhabited Symbol] [Fintype Symbol] [StrEnc Symbol] /-- The cell of a single Turing tape. -/ -public structure TapeCell where - /-- TODO document -/ - c : Option Char - /-- TODO document -/ +public structure TapeCell Symbol where + /-- The symbol in the cell. -/ + c : Option Symbol + /-- If the head is at this cell currently. -/ containsHead : Bool -/-- Cells from `k` Turing tapes combined into one cell. -/ -public structure MultiCell (k : ℕ) where - /-- One cell from each tape. -/ - cells : Vector TapeCell k - /-- Is this the left-most cell (across all tapes)? -/ - isLeftEnd : Bool - /-- Is this the right-most cell (across all tapes)? -/ - isRightEnd : Bool - -public instance : StrEnc TapeCell where +public instance : StrEnc (TapeCell Symbol) where toData cell := StrEnc.toData (cell.c, cell.containsHead) fromData d := do let (c, containsHead) ← StrEnc.fromData d pure { c, containsHead } - fromData_toData := by - intro c - simp + fromData_toData := by simp -public instance (α : Type) [StrEnc α] (k : ℕ) : StrEnc (Vector α k) where - toData v := StrEnc.toData v.toList - fromData d := do - let ls : List α ← StrEnc.fromData d - if h : ls.length = k then - pure ⟨ls.toArray, h⟩ - else - none - fromData_toData := by - intro v - simp [Vector.toList] - -public instance : StrEnc (MultiCell (k : ℕ)) where - toData mc := StrEnc.toData (mc.cells, mc.isLeftEnd, mc.isRightEnd) - fromData d := do - let (cells, isLeftEnd, isRightEnd) <- StrEnc.fromData d - pure { cells, isLeftEnd, isRightEnd } - fromData_toData := by - intro v - simp +omit [Inhabited Symbol] [Fintype Symbol] in +@[simp] +public lemma StrEnc.toData_TapeCell (x : TapeCell Symbol) : + StrEnc.toData x = StrEnc.toData (x.c, x.containsHead) := by + simp [StrEnc.toData] /- Outline of UTM: @@ -98,19 +72,129 @@ while the current state is not None: - extend a list to the right -/ -/-- The encoding of the given tapes as a list of `MultiCell`s. -/ -def encodeTapes (k : ℕ) (tapes : Fin k → BiTape Char) (shifts : Fin k → ℤ) : List (MultiCell k) := - sorry -def getHeadSymbol (k : ℕ) (tapeIdx : ℕ) (mt out aux : Fin k) : MultiTapeTM k Char := - -- Find the cell where the tapeIdx-th tape has the head - find_list mt aux (atPath [0, tapeIdx, 1] mt (copyEnc mt aux)) - -- copy the symbol to out - (atPath [0, tapeIdx, 0] mt (copy_to_list mt out)) +/-- Parameters for encoding a tuple of tapes as a single tape with multiple tracks. -/ +public structure EncodingParams (k : ℕ) where + /-- The encoding start for each tape, relative to the tape head. -/ + start : Fin k → ℤ + /-- The number of cells to encode. -/ + length : ℕ + +/-- The encoding of a tuple of tapes as a list of tuples of `TapeCell`s. +Note that the encoding can only be decoded for some values of `params`. -/ +public def encodeTapes {k : ℕ} (tapes : Fin k → BiTape Symbol) (params : EncodingParams k) : + List (Fin k → TapeCell Symbol) := + List.ofFn (n := params.length) fun p i => + { + c := (tapes i).atPos ((params.start i) + p) + containsHead := (params.start i) + p == 0 + } + +/-- The minimal head positions over all tapes at step `t` starting from initial zero positions. -/ +public def minHeadPos + {k : ℕ} (tm : MultiTapeTM k Symbol) (initialTapes : Fin k → BiTape Symbol) (t : ℕ) : ℤ := + (List.ofFn (tm.headPosition initialTapes t)).min?.getD 0 + +/-- The maximal head positions over all tapes at step `t` starting from initial zero positions. -/ +public def maxHeadPos + {k : ℕ} (tm : MultiTapeTM k Symbol) (initialTapes : Fin k → BiTape Symbol) (t : ℕ) : ℤ := + (List.ofFn (tm.headPosition initialTapes t)).max?.getD 0 + +-- TODO use this sequence of encoding parameters. + +public def encodingParamSequence {k : ℕ} (tm : MultiTapeTM k Symbol) + (initialTapes : Fin k → BiTape Symbol) (t : ℕ) : EncodingParams k := + let headPositions := tm.headPosition initialTapes + -- The min head position over all tapes at a specific step + let minHeadPosAtStep := fun t' => (List.ofFn (headPositions t')).min?.getD 0 + let maxHeadPosAtStep := fun t' => (List.ofFn (headPositions t')).max?.getD 0 + -- The min head position over all tapes and all steps until step t + -- TODO check for off-by-one errors here + let minHeadPosUntil := (List.ofFn (n := t + 1) (fun t' => minHeadPosAtStep t')).min?.getD 0 + let maxHeadPosUntil := (List.ofFn (n := t + 1) (fun t' => maxHeadPosAtStep t')).max?.getD 0 + let length := 1 + (maxHeadPosUntil - minHeadPosUntil).toNat + let start := fun i => (headPositions t i) - minHeadPosUntil + ⟨ start, length ⟩ + +public def updateEncodingParams {k : ℕ} (tm : MultiTapeTM k Symbol) + (params : EncodingParams k) + (cfg : tm.Cfg) : EncodingParams k := sorry + -- match cfg with + -- | ⟨none, _⟩ => (fun _ => 0) + -- | ⟨some q, tapes⟩ => + -- match tm.tr q (fun i => (tapes i).head) with + -- | ⟨stmts, _⟩ => fun i => shifts i + (match (stmts i).movement with + -- | none => 0 + -- | .some .right => 1 + -- | .some .left => -1) + +def getHeadSymbol (k : ℕ) (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := + find_list tapes aux + -- Find the cell where the tapeIdx-th tape has the head + (atPath [tapeIdx, 1] tapes (copyEnc tapes aux)) + -- copy the symbol to out and move back to the start of the list. + (atPath [tapeIdx, 0] tapes (copy_to_list tapes out) ;ₜ outOfList tapes) -- otherwise do nothing (because we know there is a head marker) (noop) +lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : Fin k) + (h_tapes_aux : tapes ≠ aux) + (h_tapes_out : tapes ≠ out) + {t : Fin k' → BiTape Symbol} + {views : Fin k → TapeView} + {params : EncodingParams k'} + (h_tapes : views tapes = .ofEnc (encodeTapes t params)) + (h_aux : views aux = TapeView.empty) + (idx : ℕ) + (h_contains_head : ((encodeTapes t params).findIdx? + (fun c => (c tapeIdx).containsHead)) = some idx) : + ∀ outl : List (Option Symbol), + views out = .ofEnc outl → + (getHeadSymbol k tapeIdx tapes out aux).eval_struct views = .some (Function.update + views out (TapeView.ofEnc ((t tapeIdx).head :: outl))) := by + have h_copyHeadPos : + computes_function_read_update' + (atPath [tapeIdx, 1] tapes (copyEnc tapes aux)) + (fun (tcs : Fin k' → TapeCell Symbol) _ => (tcs tapeIdx).containsHead) + tapes aux := + atPath_computes_function h_tapes_aux + (h_tm := copyEnc_computes_fun h_tapes_aux) + (h_path := by simp) + have h_copySymbol : + computes_function_read_push' + (atPath [tapeIdx, 0] tapes (copy_to_list tapes out)) + (fun (tcs : Fin k' → TapeCell Symbol) => (tcs tapeIdx).c) + tapes out := by + apply atPath_computes_function h_tapes_out + (h_tm := copy_to_list.computes_fun' h_tapes_out) + (h_path := by simp) + + sorry + +-- /-- Copies the symbol the head of tape `i` currently points to, to tape 3. -/ +-- def copyReadSymbol (i : Fin k) : MultiTapeTM 10 Char := +-- find_list 1 4 (atPath [0, i, 1] 1 (copyEnc 1 4)) +-- (atPath [0, i, 0] 1 (copy_to_list 1 4)) +-- (noop) + + +public def utm_step : MultiTapeTM 10 Char := sorry + +/-- Main theorem -/ +public theorem utm_step_semantics + {k : ℕ} (tm : MultiTapeTM k Symbol) + [StrEnc tm.State] -- it is a fintype, so easy to satsify + (cfg : tm.Cfg) + (views : Fin 10 → TapeView) + (params : EncodingParams k) + (h_tapes : views 1 = .ofEnc (encodeTapes cfg.tapes params)) + (h_state : views 2 = .ofEnc cfg.state) : + utm_step.eval_struct views = .some (match tm.step cfg with + | none => views + | some cfg' => Function.update (Function.update views + 1 (.ofEnc (encodeTapes cfg'.tapes (updateEncodingParams tm params cfg)))) + 2 (.ofEnc cfg'.state)) := by sorry end UniversalTM diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 0696bd8990..d39e250170 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -80,6 +80,12 @@ def mk₁ (l : List Symbol) : BiTape Symbol := def mk₂ (l r : List Symbol) : BiTape Symbol := ⟨r.head?, StackTape.map_some l, StackTape.map_some r.tail ⟩ +-- Returns the symbol at a position relative to the current head. -/ +def atPos (t : BiTape Symbol) (i : ℤ) : Option Symbol := match i with + | .ofNat 0 => t.head + | .ofNat (n + 1) => t.right.toList[n]?.getD none + | .negSucc n => t.left.toList[n]?.getD none + section Move /-- From 0d05f71add187822def66a8f1bd34e393271f17f Mon Sep 17 00:00:00 2001 From: crei Date: Thu, 30 Apr 2026 21:07:55 +0200 Subject: [PATCH 2/8] Semantics of copying out the symbols under the head. --- .../MultiTapeTuring/Routines/Navigation.lean | 3 ++ .../Machines/MultiTapeTuring/UniversalTM.lean | 39 ++++++++++++++----- Cslib/Foundations/Data/BiTape.lean | 2 +- 3 files changed, 33 insertions(+), 11 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean index 474cb524a7..add1140836 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean +++ b/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. diff --git a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean index c3ad7e46a4..5c16739ed3 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean @@ -90,6 +90,18 @@ public def encodeTapes {k : ℕ} (tapes : Fin k → BiTape Symbol) (params : Enc containsHead := (params.start i) + p == 0 } + +omit [Inhabited Symbol] [Fintype Symbol] [StrEnc Symbol] in +/-- If a cell in the encoding is marked as containing the head, then its symbol is the +current head symbol of the corresponding tape. -/ +@[simp, grind =] +lemma encodeTapes_getElem_of_containsHead {k : ℕ} + {t : Fin k → BiTape Symbol} {params : EncodingParams k} + {idx : ℕ} (h_idx_lt : idx < (encodeTapes t params).length) {i : Fin k} + (h : (((encodeTapes t params)[idx]'h_idx_lt) i).containsHead) : + ((encodeTapes t params)[idx]'h_idx_lt) i = {c := (t i).head, containsHead := true} := by + simp_all [encodeTapes, BiTape.atPos] + /-- The minimal head positions over all tapes at step `t` starting from initial zero positions. -/ public def minHeadPos {k : ℕ} (tm : MultiTapeTM k Symbol) (initialTapes : Fin k → BiTape Symbol) (t : ℕ) : ℤ := @@ -102,6 +114,7 @@ public def maxHeadPos -- TODO use this sequence of encoding parameters. +/-- The execution sequence of tape encoding parameters. -/ public def encodingParamSequence {k : ℕ} (tm : MultiTapeTM k Symbol) (initialTapes : Fin k → BiTape Symbol) (t : ℕ) : EncodingParams k := let headPositions := tm.headPosition initialTapes @@ -116,6 +129,7 @@ public def encodingParamSequence {k : ℕ} (tm : MultiTapeTM k Symbol) let start := fun i => (headPositions t i) - minHeadPosUntil ⟨ start, length ⟩ +/-- The next tape encoding parameter set given the previous one. -/ public def updateEncodingParams {k : ℕ} (tm : MultiTapeTM k Symbol) (params : EncodingParams k) (cfg : tm.Cfg) : EncodingParams k := sorry @@ -138,6 +152,7 @@ def getHeadSymbol (k : ℕ) (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeT (noop) +omit [Fintype Symbol] [Inhabited Symbol] in lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : Fin k) (h_tapes_aux : tapes ≠ aux) (h_tapes_out : tapes ≠ out) @@ -148,9 +163,9 @@ lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : (h_aux : views aux = TapeView.empty) (idx : ℕ) (h_contains_head : ((encodeTapes t params).findIdx? - (fun c => (c tapeIdx).containsHead)) = some idx) : - ∀ outl : List (Option Symbol), - views out = .ofEnc outl → + (fun c => (c tapeIdx).containsHead)) = some idx) + (outl : List (Option Symbol)) + (h_outl : views out = .ofEnc outl) : (getHeadSymbol k tapeIdx tapes out aux).eval_struct views = .some (Function.update views out (TapeView.ofEnc ((t tapeIdx).head :: outl))) := by have h_copyHeadPos : @@ -169,16 +184,20 @@ lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : apply atPath_computes_function h_tapes_out (h_tm := copy_to_list.computes_fun' h_tapes_out) (h_path := by simp) + unfold getHeadSymbol + rw [find_list.computes_fun h_tapes_aux h_copyHeadPos views + (encodeTapes t params) (by simp [h_tapes]) h_aux] + simp only [h_contains_head, TapeView.appendPath', seq_eval_struct] + obtain ⟨h_idx_lt, h_pred, _⟩ := List.findIdx?_eq_some_iff_getElem.mp h_contains_head + rw [h_copySymbol (encodeTapes t params)[idx] outl _ (by simp [h_tapes, h_idx_lt]) (by grind)] + simp only [Part.bind_some, outOfList_eval_struct, Part.coe_some, Part.some_inj] + rw [encodeTapes_getElem_of_containsHead h_idx_lt h_pred] + simp + grind - sorry - --- /-- Copies the symbol the head of tape `i` currently points to, to tape 3. -/ --- def copyReadSymbol (i : Fin k) : MultiTapeTM 10 Char := --- find_list 1 4 (atPath [0, i, 1] 1 (copyEnc 1 4)) --- (atPath [0, i, 0] 1 (copy_to_list 1 4)) --- (noop) +/-- Execute a single step of the simulated machine. -/ public def utm_step : MultiTapeTM 10 Char := sorry /-- Main theorem -/ diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index d39e250170..727df3055d 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -80,7 +80,7 @@ def mk₁ (l : List Symbol) : BiTape Symbol := def mk₂ (l r : List Symbol) : BiTape Symbol := ⟨r.head?, StackTape.map_some l, StackTape.map_some r.tail ⟩ --- Returns the symbol at a position relative to the current head. -/ +/-- Returns the symbol at a position relative to the current head. -/ def atPos (t : BiTape Symbol) (i : ℤ) : Option Symbol := match i with | .ofNat 0 => t.head | .ofNat (n + 1) => t.right.toList[n]?.getD none From 9a4fa291cf16a5d77749e9c3dbf18b39cfebdb66 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 4 May 2026 22:30:22 +0200 Subject: [PATCH 3/8] Introduce encoding type. --- .../Machines/MultiTapeTuring/UniversalTM.lean | 165 ++++++++++++++++-- Cslib/Foundations/Data/BiTape.lean | 18 ++ Cslib/Foundations/Data/StackTape.lean | 42 +++++ 3 files changed, 212 insertions(+), 13 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean index 5c16739ed3..ccb67413b9 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean @@ -90,6 +90,104 @@ public def encodeTapes {k : ℕ} (tapes : Fin k → BiTape Symbol) (params : Enc containsHead := (params.start i) + p == 0 } +/-- The parameters are such that position `cellPos` of tape `tapeIdx` is part of the encoding. -/ +public def EncodingParams.encodesCell {k : ℕ} (params : EncodingParams k) + (tapeIdx : Fin k) (cellPos : ℤ) : Prop := + (params.start tapeIdx) ≤ cellPos ∧ cellPos - (params.start tapeIdx) < (params.length : ℤ) + +/-- The parameters are suitable to encode all relevant information of the tape. -/ +public def encodesTape {k : ℕ} (params : EncodingParams k) (tapes : Fin k → BiTape Symbol) : Prop := + ∀ idx, + -- the head is encoded + params.encodesCell idx 0 ∧ + -- all non-none cells are encoded + ∀ i, (tapes idx).atPos i ≠ none → params.encodesCell idx i + + +/-- The encoding of tapes generated by `encodeTapes` plus a proof that we properly encoded the tape. -/ +public structure EncodedTapes (k : ℕ) where + /-- The tapes -/ + tapes : Fin k → BiTape Symbol + /-- The encoding params -/ + params : EncodingParams k + /-- The encoding is valid -/ + h_vallid : encodesTape params tapes + +instance (k : ℕ) : StrEnc (EncodedTapes k (Symbol := Symbol)) where + toData enc := StrEnc.toData (encodeTapes enc.tapes enc.params) + fromData _ := none + fromData_toData := by sorry + +/-- The `toData` map for `EncodedTapes` is injective. -/ +lemma EncodedTapes.toData_injective {k : ℕ} : + Function.Injective + (fun enc : EncodedTapes k (Symbol := Symbol) => + StrEnc.toData (encodeTapes enc.tapes enc.params)) := by + intro x y hxy + have henc : encodeTapes x.tapes x.params = encodeTapes y.tapes y.params := + StrEnc.toData_injective _ hxy + -- Lengths agree. + have hlen : x.params.length = y.params.length := by + have := congrArg List.length henc + simpa [encodeTapes] using this + -- Cell-by-cell equality via the encoded list. + have hcell : ∀ (p : ℕ) (hpx : p < x.params.length) (i : Fin k), + (x.tapes i).atPos (x.params.start i + p) = (y.tapes i).atPos (y.params.start i + p) + ∧ ((x.params.start i + (p : ℤ)) == 0) = ((y.params.start i + (p : ℤ)) == 0) := by + intro p hpx i + have hpy : p < y.params.length := hlen ▸ hpx + have hpx' : p < (encodeTapes x.tapes x.params).length := by simpa [encodeTapes] using hpx + have hpy' : p < (encodeTapes y.tapes y.params).length := by simpa [encodeTapes] using hpy + have hget : (encodeTapes x.tapes x.params)[p]'hpx' = + (encodeTapes y.tapes y.params)[p]'hpy' := by + congr 1 + have happ : ((encodeTapes x.tapes x.params)[p]'hpx') i = + ((encodeTapes y.tapes y.params)[p]'hpy') i := congrArg (· i) hget + grind [encodeTapes] + -- Extract `start` equality from the unique head-marked position. + have hstart : x.params.start = y.params.start := by + funext i + obtain ⟨hx_head, _⟩ := x.h_vallid i + set sx := x.params.start i with hsx + set sy := y.params.start i with hsy + have hx_le : sx ≤ 0 := hx_head.1 + have hx_lt : (0 : ℤ) - sx < x.params.length := hx_head.2 + set p : ℕ := (-sx).toNat with hp_def + have hnn : 0 ≤ -sx := by omega + have hp_eq : (p : ℤ) = -sx := by + simp [hp_def, Int.toNat_of_nonneg hnn] + grind + -- Both `params` are equal. + have hparams : x.params = y.params := by + have := EncodingParams.mk.injEq (k := k) x.params.start x.params.length + y.params.start y.params.length + cases hp1 : x.params with + | mk xs xl => + cases hp2 : y.params with + | mk ys yl => + grind + -- Tapes agree on every position. + have htapes : x.tapes = y.tapes := by + funext i + apply BiTape.ext_atPos + intro j + obtain ⟨_, hx_all⟩ := x.h_vallid i + obtain ⟨_, hy_all⟩ := y.h_vallid i + by_cases hx_in : x.params.encodesCell i j + · have hx_le : x.params.start i ≤ j := hx_in.1 + have hx_lt : j - x.params.start i < x.params.length := hx_in.2 + set p : ℕ := (j - x.params.start i).toNat with hp_def + have hnn : 0 ≤ j - x.params.start i := by omega + have hp_eq : (p : ℤ) = j - x.params.start i := by + simp [hp_def, Int.toNat_of_nonneg hnn] + grind + · grind + cases x with | mk xt xp xv => + cases y with | mk yt yp yv => + cases htapes; cases hparams; rfl + +-- TODO continue here: Do we actually need an explicit fromData? +-- Is it enough to prove that toData is injective? omit [Inhabited Symbol] [Fintype Symbol] [StrEnc Symbol] in /-- If a cell in the encoding is marked as containing the head, then its symbol is the @@ -142,6 +240,8 @@ public def updateEncodingParams {k : ℕ} (tm : MultiTapeTM k Symbol) -- | .some .right => 1 -- | .some .left => -1) +/-- Copies the symbol under the head of tape `tapeIdx` from the multi-track tape `tape` to +tape `out` using the auxiliary tape `aux`. -/ def getHeadSymbol (k : ℕ) (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := find_list tapes aux -- Find the cell where the tapeIdx-th tape has the head @@ -154,20 +254,19 @@ def getHeadSymbol (k : ℕ) (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeT omit [Fintype Symbol] [Inhabited Symbol] in lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : Fin k) - (h_tapes_aux : tapes ≠ aux) - (h_tapes_out : tapes ≠ out) - {t : Fin k' → BiTape Symbol} + (h_distinct : [tapes, aux, out].get.Injective) {views : Fin k → TapeView} - {params : EncodingParams k'} - (h_tapes : views tapes = .ofEnc (encodeTapes t params)) + {encodedTapes : EncodedTapes k' (Symbol := Symbol)} + (h_tapes : views tapes = .ofEnc encodedTapes) (h_aux : views aux = TapeView.empty) - (idx : ℕ) - (h_contains_head : ((encodeTapes t params).findIdx? - (fun c => (c tapeIdx).containsHead)) = some idx) (outl : List (Option Symbol)) (h_outl : views out = .ofEnc outl) : (getHeadSymbol k tapeIdx tapes out aux).eval_struct views = .some (Function.update - views out (TapeView.ofEnc ((t tapeIdx).head :: outl))) := by + views out (TapeView.ofEnc ((encodedTapes.tapes tapeIdx).head :: outl))) := by + have h_tapes_aux : tapes ≠ aux := + Function.Injective.ne h_distinct (show (0 : Fin 3) ≠ 1 by decide) + have h_tapes_out : tapes ≠ out := + Function.Injective.ne h_distinct (show (0 : Fin 3) ≠ 2 by decide) have h_copyHeadPos : computes_function_read_update' (atPath [tapeIdx, 1] tapes (copyEnc tapes aux)) @@ -184,18 +283,58 @@ lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : apply atPath_computes_function h_tapes_out (h_tm := copy_to_list.computes_fun' h_tapes_out) (h_path := by simp) + -- Derive the head index and the `findIdx?` equation from the validity of `encodedTapes`. + set idx : ℕ := (-encodedTapes.params.start tapeIdx).toNat with hidx_def + obtain ⟨hhead, _⟩ := encodedTapes.h_vallid tapeIdx + have h_le : encodedTapes.params.start tapeIdx ≤ 0 := hhead.1 + have h_lt : (0 : ℤ) - encodedTapes.params.start tapeIdx < encodedTapes.params.length := hhead.2 + have hnn : 0 ≤ -encodedTapes.params.start tapeIdx := by omega + have h_idx_eq : (idx : ℤ) = -encodedTapes.params.start tapeIdx := by grind + have h_idx_lt : idx < (encodeTapes encodedTapes.tapes encodedTapes.params).length := by + have hlt : (idx : ℤ) < encodedTapes.params.length := by rw [h_idx_eq]; omega + have : idx < encodedTapes.params.length := by exact_mod_cast hlt + simpa [encodeTapes] using this + have h_pred : + (((encodeTapes encodedTapes.tapes encodedTapes.params)[idx]'h_idx_lt) tapeIdx).containsHead = + true := by + have h0 : encodedTapes.params.start tapeIdx + (idx : ℤ) = 0 := by rw [h_idx_eq]; omega + simp [encodeTapes, h0] + have h_contains_head : + (encodeTapes encodedTapes.tapes encodedTapes.params).findIdx? + (fun c => (c tapeIdx).containsHead) = some idx := by + rw [List.findIdx?_eq_some_iff_getElem] + refine ⟨h_idx_lt, h_pred, ?_⟩ + intro j hji + have hjlen : j < (encodeTapes encodedTapes.tapes encodedTapes.params).length := by omega + have hjlen' : j < encodedTapes.params.length := by simpa [encodeTapes] using hjlen + simp only [encodeTapes, List.getElem_ofFn] + intro hbad + have heq0 : encodedTapes.params.start tapeIdx + (j : ℤ) = 0 := by simpa using hbad + have hj_eq : (j : ℤ) = -encodedTapes.params.start tapeIdx := by omega + have : (j : ℤ) = idx := by rw [hj_eq, ← h_idx_eq] + have : j = idx := by exact_mod_cast this + omega unfold getHeadSymbol rw [find_list.computes_fun h_tapes_aux h_copyHeadPos views - (encodeTapes t params) (by simp [h_tapes]) h_aux] + (encodeTapes encodedTapes.tapes encodedTapes.params) + (by simp [h_tapes, StrEnc.toData]) h_aux] simp only [h_contains_head, TapeView.appendPath', seq_eval_struct] - obtain ⟨h_idx_lt, h_pred, _⟩ := List.findIdx?_eq_some_iff_getElem.mp h_contains_head - rw [h_copySymbol (encodeTapes t params)[idx] outl _ (by simp [h_tapes, h_idx_lt]) (by grind)] + rw [h_copySymbol (encodeTapes encodedTapes.tapes encodedTapes.params)[idx] + outl _ + (by simp [h_tapes, StrEnc.toData, h_idx_lt]) + (by simp [Function.update, h_outl, h_tapes_out, h_tapes_out.symm])] simp only [Part.bind_some, outOfList_eval_struct, Part.coe_some, Part.some_inj] rw [encodeTapes_getElem_of_containsHead h_idx_lt h_pred] simp grind - +/-- Copies symbols under the heads of all tapes for `tapeCount` tapes from the multi-track +tape `tapes` to tape `out` using the auxiliary tape `aux`. -/ +def getHeadSymbols (k : ℕ) (tapeCount : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := + match tapeCount with + | 0 => noop + | tapeCount + 1 => + getHeadSymbol k tapeCount tapes out aux ;ₜ getHeadSymbols k tapeCount tapes out aux /-- Execute a single step of the simulated machine. -/ public def utm_step : MultiTapeTM 10 Char := sorry diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 727df3055d..a1bf7d6e13 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -181,4 +181,22 @@ lemma space_used_move (t : BiTape Symbol) (d : Dir) : end BiTape +/-- Extensionality for `BiTape` via `atPos`: two tapes that agree at every position are equal. -/ +lemma BiTape.ext_atPos {t1 t2 : BiTape Symbol} + (h : ∀ i : ℤ, t1.atPos i = t2.atPos i) : t1 = t2 := by + obtain ⟨h1, l1, r1⟩ := t1 + obtain ⟨h2, l2, r2⟩ := t2 + have hh : h1 = h2 := by simpa [BiTape.atPos] using h 0 + have hl : l1 = l2 := by + apply StackTape.toList_ext_getElem?_getD + intro k + have := h (.negSucc k) + simpa [BiTape.atPos] using this + have hr : r1 = r2 := by + apply StackTape.toList_ext_getElem?_getD + intro k + have := h (.ofNat (k + 1)) + simpa [BiTape.atPos] using this + subst hh; subst hl; subst hr; rfl + end Turing diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 868a5c9131..098eaf5171 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -197,6 +197,48 @@ lemma length_nil : (nil : StackTape Symbol).length = 0 := by grind end Length +/-- Two `StackTape`s are equal iff their underlying lists agree at every position +under `getD none`. -/ +lemma toList_ext_getElem?_getD {l1 l2 : StackTape Symbol} + (h : ∀ k : ℕ, l1.toList[k]?.getD (none : Option Symbol) = l2.toList[k]?.getD none) : + l1 = l2 := by + obtain ⟨xs, hx⟩ := l1 + obtain ⟨ys, hy⟩ := l2 + suffices h' : xs = ys by cases h'; rfl + -- Helper: if a no-trailing-none list `l` has any cell agreeing with `none` past its + -- last index `l.length - 1`, the agreement must come from the *other* list having + -- an element at that index whose value is `some none`, contradicting its invariant. + -- Conclude lengths equal, then pointwise equality. + have aux : ∀ {as bs : List (Option Symbol)}, + as.getLast? ≠ some none → bs.getLast? ≠ some none → + (∀ k : ℕ, as[k]?.getD (none : Option Symbol) = bs[k]?.getD none) → + as.length ≤ bs.length → as = bs := by + intro as bs ha hb hk hle + rcases Nat.lt_or_eq_of_le hle with hlt | heq + · exfalso + have hpos : 0 < bs.length := by omega + have hne : bs ≠ [] := fun hnil => by simp [hnil] at hpos + have hkey := hk (bs.length - 1) + have h1 : as[bs.length - 1]? = none := List.getElem?_eq_none (by omega) + have h2 : bs[bs.length - 1]? = some (bs.getLast hne) := by + rw [List.getElem?_eq_getElem (by omega), List.getLast_eq_getElem] + rw [h1, h2] at hkey + simp at hkey + apply hb + rw [List.getLast?_eq_some_getLast hne, hkey] + · apply List.ext_getElem heq + intro k h1 h2 + have := hk k + rw [List.getElem?_eq_getElem h1, List.getElem?_eq_getElem h2] at this + simpa using this + have hxlast : xs.getLast? ≠ some none := by + have := toList_getLast?_ne_some_none ⟨xs, hx⟩; simpa using this + have hylast : ys.getLast? ≠ some none := by + have := toList_getLast?_ne_some_none ⟨ys, hy⟩; simpa using this + rcases Nat.le_total xs.length ys.length with hle | hle + · exact aux hxlast hylast h hle + · exact (aux hylast hxlast (fun k => (h k).symm) hle).symm + end StackTape end Turing From 17fcdb90eac836ce564ff8ff4eb3d88e3848c588 Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 5 May 2026 12:18:35 +0200 Subject: [PATCH 4/8] fix merge. --- .../Machines/MultiTapeTuring/UniversalTM.lean | 88 ++----------------- Cslib/Foundations/Data/BiTape.lean | 18 ---- Cslib/Foundations/Data/StackTape.lean | 42 --------- 3 files changed, 6 insertions(+), 142 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean index 9facc91a17..3a1156225d 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean @@ -38,9 +38,6 @@ public instance : StrEnc (TapeCell Symbol) where public instance (α : Type) [StrEnc α] (k : ℕ) : StrEnc (Vector α k) where toData v := StrEnc.toData v.toList -public instance : StrEnc (MultiCell (k : ℕ)) where - toData mc := StrEnc.toData (mc.cells, mc.isLeftEnd, mc.isRightEnd) - /- Outline of UTM: while the current state is not None: @@ -82,7 +79,7 @@ public def encodeTapes {k : ℕ} (tapes : Fin k → BiTape Symbol) (params : Enc List (Fin k → TapeCell Symbol) := List.ofFn (n := params.length) fun p i => { - c := (tapes i).atPos ((params.start i) + p) + c := (tapes i).get ((params.start i) + p) containsHead := (params.start i) + p == 0 } @@ -97,7 +94,7 @@ public def encodesTape {k : ℕ} (params : EncodingParams k) (tapes : Fin k → -- the head is encoded params.encodesCell idx 0 ∧ -- all non-none cells are encoded - ∀ i, (tapes idx).atPos i ≠ none → params.encodesCell idx i + ∀ i, (tapes idx).get i ≠ none → params.encodesCell idx i /-- The encoding of tapes generated by `encodeTapes` plus a proof that we properly encoded the tape. -/ @@ -111,79 +108,6 @@ public structure EncodedTapes (k : ℕ) where instance (k : ℕ) : StrEnc (EncodedTapes k (Symbol := Symbol)) where toData enc := StrEnc.toData (encodeTapes enc.tapes enc.params) - fromData _ := none - fromData_toData := by sorry - -/-- The `toData` map for `EncodedTapes` is injective. -/ -lemma EncodedTapes.toData_injective {k : ℕ} : - Function.Injective - (fun enc : EncodedTapes k (Symbol := Symbol) => - StrEnc.toData (encodeTapes enc.tapes enc.params)) := by - intro x y hxy - have henc : encodeTapes x.tapes x.params = encodeTapes y.tapes y.params := - StrEnc.toData_injective _ hxy - -- Lengths agree. - have hlen : x.params.length = y.params.length := by - have := congrArg List.length henc - simpa [encodeTapes] using this - -- Cell-by-cell equality via the encoded list. - have hcell : ∀ (p : ℕ) (hpx : p < x.params.length) (i : Fin k), - (x.tapes i).atPos (x.params.start i + p) = (y.tapes i).atPos (y.params.start i + p) - ∧ ((x.params.start i + (p : ℤ)) == 0) = ((y.params.start i + (p : ℤ)) == 0) := by - intro p hpx i - have hpy : p < y.params.length := hlen ▸ hpx - have hpx' : p < (encodeTapes x.tapes x.params).length := by simpa [encodeTapes] using hpx - have hpy' : p < (encodeTapes y.tapes y.params).length := by simpa [encodeTapes] using hpy - have hget : (encodeTapes x.tapes x.params)[p]'hpx' = - (encodeTapes y.tapes y.params)[p]'hpy' := by - congr 1 - have happ : ((encodeTapes x.tapes x.params)[p]'hpx') i = - ((encodeTapes y.tapes y.params)[p]'hpy') i := congrArg (· i) hget - grind [encodeTapes] - -- Extract `start` equality from the unique head-marked position. - have hstart : x.params.start = y.params.start := by - funext i - obtain ⟨hx_head, _⟩ := x.h_vallid i - set sx := x.params.start i with hsx - set sy := y.params.start i with hsy - have hx_le : sx ≤ 0 := hx_head.1 - have hx_lt : (0 : ℤ) - sx < x.params.length := hx_head.2 - set p : ℕ := (-sx).toNat with hp_def - have hnn : 0 ≤ -sx := by omega - have hp_eq : (p : ℤ) = -sx := by - simp [hp_def, Int.toNat_of_nonneg hnn] - grind - -- Both `params` are equal. - have hparams : x.params = y.params := by - have := EncodingParams.mk.injEq (k := k) x.params.start x.params.length - y.params.start y.params.length - cases hp1 : x.params with - | mk xs xl => - cases hp2 : y.params with - | mk ys yl => - grind - -- Tapes agree on every position. - have htapes : x.tapes = y.tapes := by - funext i - apply BiTape.ext_atPos - intro j - obtain ⟨_, hx_all⟩ := x.h_vallid i - obtain ⟨_, hy_all⟩ := y.h_vallid i - by_cases hx_in : x.params.encodesCell i j - · have hx_le : x.params.start i ≤ j := hx_in.1 - have hx_lt : j - x.params.start i < x.params.length := hx_in.2 - set p : ℕ := (j - x.params.start i).toNat with hp_def - have hnn : 0 ≤ j - x.params.start i := by omega - have hp_eq : (p : ℤ) = j - x.params.start i := by - simp [hp_def, Int.toNat_of_nonneg hnn] - grind - · grind - cases x with | mk xt xp xv => - cases y with | mk yt yp yv => - cases htapes; cases hparams; rfl - --- TODO continue here: Do we actually need an explicit fromData? --- Is it enough to prove that toData is injective? omit [Inhabited Symbol] [Fintype Symbol] [StrEnc Symbol] in /-- If a cell in the encoding is marked as containing the head, then its symbol is the @@ -194,7 +118,7 @@ lemma encodeTapes_getElem_of_containsHead {k : ℕ} {idx : ℕ} (h_idx_lt : idx < (encodeTapes t params).length) {i : Fin k} (h : (((encodeTapes t params)[idx]'h_idx_lt) i).containsHead) : ((encodeTapes t params)[idx]'h_idx_lt) i = {c := (t i).head, containsHead := true} := by - simp_all [encodeTapes, BiTape.atPos] + simp_all [encodeTapes, BiTape.get] /-- The minimal head positions over all tapes at step `t` starting from initial zero positions. -/ public def minHeadPos @@ -270,7 +194,7 @@ lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : tapes aux := atPath_computes_function h_tapes_aux (h_tm := copyEnc_computes_fun h_tapes_aux) - (h_path := by simp) + (h_path := by simp [StrEnc.toData]) have h_copySymbol : computes_function_read_push' (atPath [tapeIdx, 0] tapes (copy_to_list tapes out)) @@ -278,7 +202,7 @@ lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : tapes out := by apply atPath_computes_function h_tapes_out (h_tm := copy_to_list.computes_fun' h_tapes_out) - (h_path := by simp) + (h_path := by simp [StrEnc.toData]) -- Derive the head index and the `findIdx?` equation from the validity of `encodedTapes`. set idx : ℕ := (-encodedTapes.params.start tapeIdx).toNat with hidx_def obtain ⟨hhead, _⟩ := encodedTapes.h_vallid tapeIdx @@ -318,7 +242,7 @@ lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : rw [h_copySymbol (encodeTapes encodedTapes.tapes encodedTapes.params)[idx] outl _ (by simp [h_tapes, StrEnc.toData, h_idx_lt]) - (by simp [Function.update, h_outl, h_tapes_out, h_tapes_out.symm])] + (by simp [Function.update, h_outl, h_tapes_out.symm])] simp only [Part.bind_some, outOfList_eval_struct, Part.coe_some, Part.some_inj] rw [encodeTapes_getElem_of_containsHead h_idx_lt h_pred] simp diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 6270d3b4bb..3274d2fcaa 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -270,22 +270,4 @@ lemma space_used_move (t : BiTape Symbol) (d : Dir) : end BiTape -/-- Extensionality for `BiTape` via `atPos`: two tapes that agree at every position are equal. -/ -lemma BiTape.ext_atPos {t1 t2 : BiTape Symbol} - (h : ∀ i : ℤ, t1.atPos i = t2.atPos i) : t1 = t2 := by - obtain ⟨h1, l1, r1⟩ := t1 - obtain ⟨h2, l2, r2⟩ := t2 - have hh : h1 = h2 := by simpa [BiTape.atPos] using h 0 - have hl : l1 = l2 := by - apply StackTape.toList_ext_getElem?_getD - intro k - have := h (.negSucc k) - simpa [BiTape.atPos] using this - have hr : r1 = r2 := by - apply StackTape.toList_ext_getElem?_getD - intro k - have := h (.ofNat (k + 1)) - simpa [BiTape.atPos] using this - subst hh; subst hl; subst hr; rfl - end Turing diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 2d79d47d56..4bff37a325 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -233,48 +233,6 @@ lemma length_nil : (nil : StackTape Symbol).length = 0 := by grind end Length -/-- Two `StackTape`s are equal iff their underlying lists agree at every position -under `getD none`. -/ -lemma toList_ext_getElem?_getD {l1 l2 : StackTape Symbol} - (h : ∀ k : ℕ, l1.toList[k]?.getD (none : Option Symbol) = l2.toList[k]?.getD none) : - l1 = l2 := by - obtain ⟨xs, hx⟩ := l1 - obtain ⟨ys, hy⟩ := l2 - suffices h' : xs = ys by cases h'; rfl - -- Helper: if a no-trailing-none list `l` has any cell agreeing with `none` past its - -- last index `l.length - 1`, the agreement must come from the *other* list having - -- an element at that index whose value is `some none`, contradicting its invariant. - -- Conclude lengths equal, then pointwise equality. - have aux : ∀ {as bs : List (Option Symbol)}, - as.getLast? ≠ some none → bs.getLast? ≠ some none → - (∀ k : ℕ, as[k]?.getD (none : Option Symbol) = bs[k]?.getD none) → - as.length ≤ bs.length → as = bs := by - intro as bs ha hb hk hle - rcases Nat.lt_or_eq_of_le hle with hlt | heq - · exfalso - have hpos : 0 < bs.length := by omega - have hne : bs ≠ [] := fun hnil => by simp [hnil] at hpos - have hkey := hk (bs.length - 1) - have h1 : as[bs.length - 1]? = none := List.getElem?_eq_none (by omega) - have h2 : bs[bs.length - 1]? = some (bs.getLast hne) := by - rw [List.getElem?_eq_getElem (by omega), List.getLast_eq_getElem] - rw [h1, h2] at hkey - simp at hkey - apply hb - rw [List.getLast?_eq_some_getLast hne, hkey] - · apply List.ext_getElem heq - intro k h1 h2 - have := hk k - rw [List.getElem?_eq_getElem h1, List.getElem?_eq_getElem h2] at this - simpa using this - have hxlast : xs.getLast? ≠ some none := by - have := toList_getLast?_ne_some_none ⟨xs, hx⟩; simpa using this - have hylast : ys.getLast? ≠ some none := by - have := toList_getLast?_ne_some_none ⟨ys, hy⟩; simpa using this - rcases Nat.le_total xs.length ys.length with hle | hle - · exact aux hxlast hylast h hle - · exact (aux hylast hxlast (fun k => (h k).symm) hle).symm - end StackTape end Turing From c7394a158425f66460500d75df25c45866964772 Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 5 May 2026 13:57:04 +0200 Subject: [PATCH 5/8] Simplify proof. --- .../Machines/MultiTapeTuring/UniversalTM.lean | 64 +++++++++---------- 1 file changed, 31 insertions(+), 33 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean index 3a1156225d..e3dbe212d0 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean @@ -89,7 +89,7 @@ public def EncodingParams.encodesCell {k : ℕ} (params : EncodingParams k) (params.start tapeIdx) ≤ cellPos ∧ cellPos - (params.start tapeIdx) < (params.length : ℤ) /-- The parameters are suitable to encode all relevant information of the tape. -/ -public def encodesTape {k : ℕ} (params : EncodingParams k) (tapes : Fin k → BiTape Symbol) : Prop := +public def EncodingParams.encodesTape {k : ℕ} (params : EncodingParams k) (tapes : Fin k → BiTape Symbol) : Prop := ∀ idx, -- the head is encoded params.encodesCell idx 0 ∧ @@ -104,7 +104,7 @@ public structure EncodedTapes (k : ℕ) where /-- The encoding params -/ params : EncodingParams k /-- The encoding is valid -/ - h_vallid : encodesTape params tapes + h_valid : params.encodesTape tapes instance (k : ℕ) : StrEnc (EncodedTapes k (Symbol := Symbol)) where toData enc := StrEnc.toData (encodeTapes enc.tapes enc.params) @@ -173,7 +173,7 @@ def getHeadSymbol (k : ℕ) (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeT omit [Fintype Symbol] [Inhabited Symbol] in -lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : Fin k) +lemma getHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : Fin k) (h_distinct : [tapes, aux, out].get.Injective) {views : Fin k → TapeView} {encodedTapes : EncodedTapes k' (Symbol := Symbol)} @@ -203,48 +203,31 @@ lemma geatHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : apply atPath_computes_function h_tapes_out (h_tm := copy_to_list.computes_fun' h_tapes_out) (h_path := by simp [StrEnc.toData]) + unfold getHeadSymbol + rw [find_list.computes_fun h_tapes_aux h_copyHeadPos views + (encodeTapes encodedTapes.tapes encodedTapes.params) + (by simp [h_tapes, StrEnc.toData]) h_aux] + obtain ⟨⟨headValid1, headValid2⟩, _⟩ := encodedTapes.h_valid tapeIdx + simp at headValid2 -- Derive the head index and the `findIdx?` equation from the validity of `encodedTapes`. - set idx : ℕ := (-encodedTapes.params.start tapeIdx).toNat with hidx_def - obtain ⟨hhead, _⟩ := encodedTapes.h_vallid tapeIdx - have h_le : encodedTapes.params.start tapeIdx ≤ 0 := hhead.1 - have h_lt : (0 : ℤ) - encodedTapes.params.start tapeIdx < encodedTapes.params.length := hhead.2 - have hnn : 0 ≤ -encodedTapes.params.start tapeIdx := by omega - have h_idx_eq : (idx : ℤ) = -encodedTapes.params.start tapeIdx := by grind + let idx_z := -encodedTapes.params.start tapeIdx + let idx := idx_z.toNat + have h_idx_eq : (idx : ℤ) = idx_z := by simp_all [idx, idx_z] have h_idx_lt : idx < (encodeTapes encodedTapes.tapes encodedTapes.params).length := by - have hlt : (idx : ℤ) < encodedTapes.params.length := by rw [h_idx_eq]; omega - have : idx < encodedTapes.params.length := by exact_mod_cast hlt - simpa [encodeTapes] using this + simp_all [encodeTapes, idx, idx_z] have h_pred : (((encodeTapes encodedTapes.tapes encodedTapes.params)[idx]'h_idx_lt) tapeIdx).containsHead = true := by - have h0 : encodedTapes.params.start tapeIdx + (idx : ℤ) = 0 := by rw [h_idx_eq]; omega - simp [encodeTapes, h0] - have h_contains_head : - (encodeTapes encodedTapes.tapes encodedTapes.params).findIdx? + simp [encodeTapes, h_idx_eq, idx_z] + have h_contains_head : (encodeTapes encodedTapes.tapes encodedTapes.params).findIdx? (fun c => (c tapeIdx).containsHead) = some idx := by rw [List.findIdx?_eq_some_iff_getElem] - refine ⟨h_idx_lt, h_pred, ?_⟩ - intro j hji - have hjlen : j < (encodeTapes encodedTapes.tapes encodedTapes.params).length := by omega - have hjlen' : j < encodedTapes.params.length := by simpa [encodeTapes] using hjlen - simp only [encodeTapes, List.getElem_ofFn] - intro hbad - have heq0 : encodedTapes.params.start tapeIdx + (j : ℤ) = 0 := by simpa using hbad - have hj_eq : (j : ℤ) = -encodedTapes.params.start tapeIdx := by omega - have : (j : ℤ) = idx := by rw [hj_eq, ← h_idx_eq] - have : j = idx := by exact_mod_cast this - omega - unfold getHeadSymbol - rw [find_list.computes_fun h_tapes_aux h_copyHeadPos views - (encodeTapes encodedTapes.tapes encodedTapes.params) - (by simp [h_tapes, StrEnc.toData]) h_aux] + grind [encodeTapes] simp only [h_contains_head, TapeView.appendPath', seq_eval_struct] rw [h_copySymbol (encodeTapes encodedTapes.tapes encodedTapes.params)[idx] outl _ (by simp [h_tapes, StrEnc.toData, h_idx_lt]) (by simp [Function.update, h_outl, h_tapes_out.symm])] - simp only [Part.bind_some, outOfList_eval_struct, Part.coe_some, Part.some_inj] - rw [encodeTapes_getElem_of_containsHead h_idx_lt h_pred] simp grind @@ -256,6 +239,21 @@ def getHeadSymbols (k : ℕ) (tapeCount : ℕ) (tapes out aux : Fin k) : MultiTa | tapeCount + 1 => getHeadSymbol k tapeCount tapes out aux ;ₜ getHeadSymbols k tapeCount tapes out aux +omit [Fintype Symbol] [Inhabited Symbol] in +lemma getHeadSymbols.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : Fin k) + (h_distinct : [tapes, aux, out].get.Injective) + {views : Fin k → TapeView} + {encodedTapes : EncodedTapes k' (Symbol := Symbol)} + (h_tapes : views tapes = .ofEnc encodedTapes) + (h_aux : views aux = TapeView.empty) + (outl : List (Option Symbol)) + (h_outl : views out = .ofEnc outl) : + (getHeadSymbols k tk' tapes out aux).eval_struct views = .some (Function.update + -- FIx the next line, we should get all the head symbols. + views out (TapeView.ofEnc ((encodedTapes.tapes tapeIdx).head :: outl))) := by + -- prove by induction, after k'' steps, we het the last k'' head symbols on the output tape. + sorry + /-- Execute a single step of the simulated machine. -/ public def utm_step : MultiTapeTM 10 Char := sorry From c2c110156cde6adc5a9ee024289a4b0f0151e2dd Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 5 May 2026 18:45:52 +0200 Subject: [PATCH 6/8] Semantics of getHeadSymbols. --- .../Machines/MultiTapeTuring/UniversalTM.lean | 37 ++++++++++++++++--- 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean index e3dbe212d0..edba57fdeb 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean @@ -240,7 +240,7 @@ def getHeadSymbols (k : ℕ) (tapeCount : ℕ) (tapes out aux : Fin k) : MultiTa getHeadSymbol k tapeCount tapes out aux ;ₜ getHeadSymbols k tapeCount tapes out aux omit [Fintype Symbol] [Inhabited Symbol] in -lemma getHeadSymbols.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : Fin k) +lemma getHeadSymbols.semantics {k k' : ℕ} (tapes out aux : Fin k) (h_distinct : [tapes, aux, out].get.Injective) {views : Fin k → TapeView} {encodedTapes : EncodedTapes k' (Symbol := Symbol)} @@ -248,11 +248,36 @@ lemma getHeadSymbols.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : (h_aux : views aux = TapeView.empty) (outl : List (Option Symbol)) (h_outl : views out = .ofEnc outl) : - (getHeadSymbols k tk' tapes out aux).eval_struct views = .some (Function.update - -- FIx the next line, we should get all the head symbols. - views out (TapeView.ofEnc ((encodedTapes.tapes tapeIdx).head :: outl))) := by - -- prove by induction, after k'' steps, we het the last k'' head symbols on the output tape. - sorry + (getHeadSymbols k k' tapes out aux).eval_struct views = .some (Function.update + views out (TapeView.ofEnc + ((List.ofFn (fun i : Fin k' => (encodedTapes.tapes i).head)) ++ outl))) := by + have h_tapes_out : tapes ≠ out := + Function.Injective.ne h_distinct (show (0 : Fin 3) ≠ 2 by decide) + have h_aux_out : aux ≠ out := + Function.Injective.ne h_distinct (show (1 : Fin 3) ≠ 2 by decide) + suffices h : ∀ (tc : ℕ) (h_le : tc ≤ k') {views : Fin k → TapeView} + (outl : List (Option Symbol)), + views tapes = .ofEnc encodedTapes → views aux = TapeView.empty → + views out = .ofEnc outl → + (getHeadSymbols k tc tapes out aux).eval_struct views = .some (Function.update + views out (TapeView.ofEnc ((List.ofFn (fun i : Fin tc => + (encodedTapes.tapes (Fin.castLE h_le i)).head)) ++ outl))) by + simpa using h k' (le_refl _) outl h_tapes h_aux h_outl + intro tc h_le views outl h_tapes h_aux h_outl + induction tc generalizing views outl with + | zero => + simp [getHeadSymbols, noop.eval_struct, ← h_outl] + | succ tc ih => + unfold getHeadSymbols + rw [seq_eval_struct, + getHeadSymbol.semantics ⟨tc, h_le⟩ tapes out aux h_distinct h_tapes h_aux outl h_outl] + simp only [Part.bind_some] + rw [ih (by omega) ((encodedTapes.tapes ⟨tc, h_le⟩).head :: outl) + (by grind) (by grind) (by simp)] + congr 1 + rw [Function.update_idem, List.ofFn_succ' (n := tc) + (f := fun i : Fin (tc+1) => (encodedTapes.tapes (Fin.castLE h_le i)).head)] + simp [Fin.castLE] /-- Execute a single step of the simulated machine. -/ public def utm_step : MultiTapeTM 10 Char := sorry From ecf5daada3e4109def150ac9448d9288003049c9 Mon Sep 17 00:00:00 2001 From: crei Date: Thu, 7 May 2026 13:16:58 +0200 Subject: [PATCH 7/8] Semantics of provideTransitionInput --- .../Machines/MultiTapeTuring/Data.lean | 25 +++++-- .../MultiTapeTuring/Routines/Copy.lean | 7 ++ .../Routines/ListIteration.lean | 18 +++++ .../MultiTapeTuring/Routines/ListOps.lean | 7 ++ .../MultiTapeTuring/Routines/Navigation.lean | 47 +++++++++++++ .../MultiTapeTuring/Routines/Put.lean | 16 ++--- .../MultiTapeTuring/StructuralMachines.lean | 12 ++++ .../Machines/MultiTapeTuring/TapeView.lean | 31 ++++++++- .../Machines/MultiTapeTuring/UniversalTM.lean | 66 ++++++++++++++++--- 9 files changed, 207 insertions(+), 22 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Data.lean b/Cslib/Computability/Machines/MultiTapeTuring/Data.lean index 9d794f421b..db061c94ed 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Data.lean +++ b/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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Copy.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/Copy.lean index a56ae7cc8e..f4141bf96c 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Copy.lean +++ b/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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean index 92933b649e..c8862ae255 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListIteration.lean @@ -228,5 +228,23 @@ public theorem find_list.computes_fun {k : ℕ} {i j : Fin k} | 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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean index 92942277d4..7ac8547a6d 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Routines/ListOps.lean @@ -28,6 +28,13 @@ 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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean index add1140836..494edd5159 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Routines/Navigation.lean @@ -159,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. -/ @@ -200,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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Put.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/Put.lean index f9839ef413..ae7d79adb4 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Routines/Put.lean +++ b/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 diff --git a/Cslib/Computability/Machines/MultiTapeTuring/StructuralMachines.lean b/Cslib/Computability/Machines/MultiTapeTuring/StructuralMachines.lean index 52630f6adc..efbd03f792 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/StructuralMachines.lean +++ b/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} diff --git a/Cslib/Computability/Machines/MultiTapeTuring/TapeView.lean b/Cslib/Computability/Machines/MultiTapeTuring/TapeView.lean index 92f9e9d2f8..691fb2ad19 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/TapeView.lean +++ b/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 = diff --git a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean index edba57fdeb..b4ba090840 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/UniversalTM.lean @@ -160,9 +160,31 @@ public def updateEncodingParams {k : ℕ} (tm : MultiTapeTM k Symbol) -- | .some .right => 1 -- | .some .left => -1) +-- TODO: Can we describe the semantics of getHeadSymbol on Data itself? +-- This way, we could maybe use Data-based lemmas only and thus +-- unconditional simp lemmas. One problem might be that the atPath +-- combinator does not work in all cases. +-- Solution: We define `ifHasElem idx tm\₁tm\2`. Using this, define `atPath` to only do +-- something if the path exists. +-- then find_list compares to `StrEnc.toData true` - if nothing was executed, +-- it is false. +-- So the discriminator in the list search is `d.atPath [tapeIdx, 1] == some (StrEnc.toData true)` +-- which is equivalent to `(tcs tapeIdx).containsHead` if `d = StrEnc.toData tcs` + +/-- Copies the symbol under the head of tape `tapeIdx` from the multi-track tape `tape` to +tape `out` using the auxiliary tape `aux`. -/ +def getHeadSymbol_v2 {k : ℕ} (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := + find_list tapes aux + -- Find the cell where the tapeIdx-th tape has the head + (atPath? [tapeIdx, 1] tapes (copyEnc tapes aux) noop) + -- copy the symbol to out and move back to the start of the list. + (atPath? [tapeIdx, 0] tapes (copy_to_list tapes out) noop ;ₜ outOfList tapes) + -- otherwise do nothing (because we know there is a head marker) + (noop) + /-- Copies the symbol under the head of tape `tapeIdx` from the multi-track tape `tape` to tape `out` using the auxiliary tape `aux`. -/ -def getHeadSymbol (k : ℕ) (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := +def getHeadSymbol {k : ℕ} (tapeIdx : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := find_list tapes aux -- Find the cell where the tapeIdx-th tape has the head (atPath [tapeIdx, 1] tapes (copyEnc tapes aux)) @@ -181,7 +203,7 @@ lemma getHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : F (h_aux : views aux = TapeView.empty) (outl : List (Option Symbol)) (h_outl : views out = .ofEnc outl) : - (getHeadSymbol k tapeIdx tapes out aux).eval_struct views = .some (Function.update + (getHeadSymbol tapeIdx tapes out aux).eval_struct views = .some (Function.update views out (TapeView.ofEnc ((encodedTapes.tapes tapeIdx).head :: outl))) := by have h_tapes_aux : tapes ≠ aux := Function.Injective.ne h_distinct (show (0 : Fin 3) ≠ 1 by decide) @@ -192,7 +214,13 @@ lemma getHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : F (atPath [tapeIdx, 1] tapes (copyEnc tapes aux)) (fun (tcs : Fin k' → TapeCell Symbol) _ => (tcs tapeIdx).containsHead) tapes aux := - atPath_computes_function h_tapes_aux + atPath_computes_function + (α := Fin k' → TapeCell Symbol) + (β := Bool) + (γ := Bool) + (tm := copyEnc tapes aux) + (path := [tapeIdx, 1]) + h_tapes_aux (h_tm := copyEnc_computes_fun h_tapes_aux) (h_path := by simp [StrEnc.toData]) have h_copySymbol : @@ -233,11 +261,11 @@ lemma getHeadSymbol.semantics {k k' : ℕ} (tapeIdx : Fin k') (tapes out aux : F /-- Copies symbols under the heads of all tapes for `tapeCount` tapes from the multi-track tape `tapes` to tape `out` using the auxiliary tape `aux`. -/ -def getHeadSymbols (k : ℕ) (tapeCount : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := +def getHeadSymbols {k : ℕ} (tapeCount : ℕ) (tapes out aux : Fin k) : MultiTapeTM k Char := match tapeCount with | 0 => noop | tapeCount + 1 => - getHeadSymbol k tapeCount tapes out aux ;ₜ getHeadSymbols k tapeCount tapes out aux + getHeadSymbol tapeCount tapes out aux ;ₜ getHeadSymbols tapeCount tapes out aux omit [Fintype Symbol] [Inhabited Symbol] in lemma getHeadSymbols.semantics {k k' : ℕ} (tapes out aux : Fin k) @@ -248,7 +276,7 @@ lemma getHeadSymbols.semantics {k k' : ℕ} (tapes out aux : Fin k) (h_aux : views aux = TapeView.empty) (outl : List (Option Symbol)) (h_outl : views out = .ofEnc outl) : - (getHeadSymbols k k' tapes out aux).eval_struct views = .some (Function.update + (getHeadSymbols k' tapes out aux).eval_struct views = .some (Function.update views out (TapeView.ofEnc ((List.ofFn (fun i : Fin k' => (encodedTapes.tapes i).head)) ++ outl))) := by have h_tapes_out : tapes ≠ out := @@ -259,14 +287,13 @@ lemma getHeadSymbols.semantics {k k' : ℕ} (tapes out aux : Fin k) (outl : List (Option Symbol)), views tapes = .ofEnc encodedTapes → views aux = TapeView.empty → views out = .ofEnc outl → - (getHeadSymbols k tc tapes out aux).eval_struct views = .some (Function.update + (getHeadSymbols tc tapes out aux).eval_struct views = .some (Function.update views out (TapeView.ofEnc ((List.ofFn (fun i : Fin tc => (encodedTapes.tapes (Fin.castLE h_le i)).head)) ++ outl))) by simpa using h k' (le_refl _) outl h_tapes h_aux h_outl intro tc h_le views outl h_tapes h_aux h_outl induction tc generalizing views outl with - | zero => - simp [getHeadSymbols, noop.eval_struct, ← h_outl] + | zero => simp [getHeadSymbols, h_outl] | succ tc ih => unfold getHeadSymbols rw [seq_eval_struct, @@ -279,6 +306,27 @@ lemma getHeadSymbols.semantics {k k' : ℕ} (tapes out aux : Fin k) (f := fun i : Fin (tc+1) => (encodedTapes.tapes (Fin.castLE h_le i)).head)] simp [Fin.castLE] +def provideTransitionInput {k : ℕ} (tapeCount : ℕ) + (state tapes out aux : Fin k) : MultiTapeTM k Char := + replace Data.empty out ;ₜ getHeadSymbols tapeCount tapes out aux ;ₜ copy_to_list state out + +-- states, tapes, out, aux: 1 2 3 4 +omit [Fintype Symbol] [Inhabited Symbol] in +lemma provideTransitionInput.semantics {k' : ℕ} + {views : Fin 5 → TapeView} + {encodedTapes : EncodedTapes k' (Symbol := Symbol)} + (h_tapes : views 2 = .ofEnc encodedTapes) + (h_aux : views 4 = TapeView.empty) : + (provideTransitionInput k' 1 2 3 4).eval_struct views = .some (Function.update + views 3 (TapeView.ofEnc ((views 1).current :: + List.ofFn fun i : Fin k' => StrEnc.toData (encodedTapes.tapes i).head))) := by + simp only [provideTransitionInput, seq_eval_struct, replace.eval_struct, + Part.coe_some, Part.bind_some] + rw [getHeadSymbols.semantics (encodedTapes := encodedTapes) (Symbol := Symbol) 2 3 4 (by decide) + (by simp [h_tapes]) (by simp [h_aux]) [] (by simp [StrEnc.toData])] + simp + congr + /-- Execute a single step of the simulated machine. -/ public def utm_step : MultiTapeTM 10 Char := sorry From e24da877213e27dfdacd9b88d480ed128d28e6e5 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 11 May 2026 11:51:45 +0200 Subject: [PATCH 8/8] eval fun --- .../MultiTapeTuring/Routines/EvalFun.lean | 79 +++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 Cslib/Computability/Machines/MultiTapeTuring/Routines/EvalFun.lean diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Routines/EvalFun.lean b/Cslib/Computability/Machines/MultiTapeTuring/Routines/EvalFun.lean new file mode 100644 index 0000000000..d2d3618541 --- /dev/null +++ b/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