From 5f433ff882776d54d3a19434bea82b2f84ee6ea5 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 17 Apr 2026 16:26:39 -0400 Subject: [PATCH 1/2] feat(Computability/MultiTapeTM): input/output tape predicates + head-position bound Adds read-only input and write-only output tape abstractions for multi-tape Turing machines, plus a proof that the input-tape head position stays within [-1, |input|] across reachable configurations. - StackTape/BiTape: migrated `*_nil` lemmas into BiTape, extended StackTape API used by the new invariants. - MultiTapeTM.HasInputTape / HasOutputTape: predicates characterising read-only input and write-only output tapes. - HeadBoundInvariantAt: Prop-valued structure carrying the position bound, canonical-tape equality, and left/right reachability chains; .initCfg and .step lemmas prove inductivity. - HasInputTape.step_tape0_decompose: factors a step through its predecessor state, eliminating `change`-tactic gymnastics in invariant-preservation proofs. - head_position_bounded: quantitative head-position bound derived from the invariant via iter_step. --- Cslib.lean | 1 + .../Machines/MultiTapeTuring/Basic.lean | 609 +++++++++++++++++- .../Computability/Machines/TuringCommon.lean | 100 +++ Cslib/Foundations/Data/BiTape.lean | 16 + Cslib/Foundations/Data/BiTape/Canonical.lean | 179 +++++ Cslib/Foundations/Data/RelatesInSteps.lean | 11 + Cslib/Foundations/Data/StackTape.lean | 42 ++ 7 files changed, 954 insertions(+), 4 deletions(-) create mode 100644 Cslib/Foundations/Data/BiTape/Canonical.lean diff --git a/Cslib.lean b/Cslib.lean index 626aadd72..dd2edcdcb 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -50,6 +50,7 @@ public import Cslib.Foundations.Control.Monad.Free public import Cslib.Foundations.Control.Monad.Free.Effects public import Cslib.Foundations.Control.Monad.Free.Fold public import Cslib.Foundations.Data.BiTape +public import Cslib.Foundations.Data.BiTape.Canonical public import Cslib.Foundations.Data.DecidableEqZero public import Cslib.Foundations.Data.FinFun.Basic public import Cslib.Foundations.Data.FinFun.Update diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean index 91ee0c781..4f6e8a712 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Copyright (c) 2026 Christian Reitwiessner, Sam Schlesinger. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Christian Reitwiessner +Authors: Christian Reitwiessner, Sam Schlesinger -/ module @@ -9,6 +9,7 @@ module public import Mathlib.Data.Part public import Mathlib.Data.Fintype.Defs public import Cslib.Foundations.Data.BiTape +public import Cslib.Foundations.Data.BiTape.Canonical public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Computability.Machines.TuringCommon public import Mathlib.Algebra.Order.BigOperators.Group.Finset @@ -52,12 +53,26 @@ There are multiple ways to talk about the behaviour of a multi-tape Turing machi * `MultiTapeTM.eval`: executes a TM on initial tapes `tapes` and returns the resulting tapes if it eventually halts +For machines with designated input and output tapes: + +* `MultiTapeTM.HasInputTape`: tape `0` is write-preserving, with a syntactic head-bound + condition that rules out two consecutive same-direction off-end moves +* `MultiTapeTM.HasOutputTape`: in a machine with at least two tapes, the last tape is write-only + (`Stmt.IsWriteOnly` on every transition) + +The syntactic finite-control reachability machinery underpinning head-boundedness lives in +`Cslib.Computability.Machines.TuringCommon` (`MovesOffBlankInDir`, `MoveThenStays`, +`IsBoundedInDirectionOnTape`). + ## TODOs * Define sequential composition of multi-tape Turing machines. -* Define different kinds of tapes (input-only, output-only, oracle, etc) and how they influence - how space is counted. +* Define oracle tapes, and refine space accounting to discount read-only input and write-only + output tapes from the working-space charge. * Define the notion of a multi-tape Turing machine computing a function. +* Provide a `Decidable` instance for `IsBoundedInDirectionOnTape` (the existential over reads is + finite when `Symbol` is `Fintype`, and the reachability relation is finite on a finite state + set). -/ @@ -90,6 +105,62 @@ structure MultiTapeTM k Symbol [Inhabited Symbol] [Fintype Symbol] where namespace MultiTapeTM +/-! +## Designated input and output tapes + +By convention we reserve tape index `0` for a two-way read-only *input* tape and, for +machines with at least two tapes, the last tape index for a write-only *output* tape. The +predicates `HasInputTape` and `HasOutputTape` assert these roles as syntactic properties of +the machine's transition function, so they can be checked without reasoning about the +dynamics of any particular computation. + +For the two-way read-only input tape we combine *write-preservation* (tape `0` is never +modified) with a syntactic head-bound condition (`IsBoundedInDirectionOnTape`, defined in +`TuringCommon`): once the head steps off the input in some direction, no chain of stay-moves +on the blank can lead to another off-end step in the same direction. + +This suffices to prove a quantitative `±1` bound on the head position over arbitrary traces +from `initCfg`: see `HasInputTape.head_position_bounded`. +-/ + +section InputOutputTape + +variable [Inhabited Symbol] [Fintype Symbol] + +/-- +`tm` has a *write-preserving, head-bounded input tape* at tape index `0`. This bundles two +conditions on the transition function: + +* *read-preservation*: every transition writes back the symbol it read on tape `0`, so tape + `0` is never modified (see `HasInputTape.step_tape0_eq_optionMove`); +* *syntactic head-bound in both directions* (`IsBoundedInDirectionOnTape`): if the head on + tape `0` steps off an end of the input in some direction, no chain of stay-moves on the + blank can lead to another off-end step in the same direction. + +The semantic upshot is captured trace-level by `HasInputTape.head_position_bounded`: +along any trace from `initCfg s` with nonempty input, tape `0`'s content matches some +`canonicalInputTape s p` with `p ∈ [-1, s.length]`. +-/ +structure HasInputTape {k : ℕ} (tm : MultiTapeTM (k + 1) Symbol) : Prop where + /-- Every transition writes back the symbol it read on tape `0`. -/ + readPreserving : ∀ q reads, ((tm.tr q reads).1 0).IsReadPreserving (reads 0) + /-- Once the head steps left off the input, no chain of stay-moves on the blank can lead + to another left step on the blank. -/ + leftBounded : IsBoundedInDirectionOnTape tm.tr 0 .left + /-- Once the head steps right off the input, no chain of stay-moves on the blank can lead + to another right step on the blank. -/ + rightBounded : IsBoundedInDirectionOnTape tm.tr 0 .right + +/-- +`tm` has a write-only output tape at the last tape index, distinct from tape `0`: on every +transition, the stmt produced on the last tape either writes a blank and stays put or +writes a non-blank symbol and moves the head right. +-/ +def HasOutputTape {k : ℕ} (tm : MultiTapeTM (k + 2) Symbol) : Prop := + ∀ q reads, ((tm.tr q reads).1 (Fin.last (k + 1))).IsWriteOnly + +end InputOutputTape + section Cfg /-! @@ -345,4 +416,534 @@ lemma eval_eq_some_iff_transformsTapes end MultiTapeTM +/-! +## Bridge lemmas: syntactic tape predicates ⇒ semantic invariants + +These lemmas show that the syntactic predicates `HasInputTape` and `HasOutputTape` deliver +the semantic guarantees they are intended to capture, by step-by-step inspection of the +underlying `BiTape` operations. +-/ + +namespace MultiTapeTM + +variable [Inhabited Symbol] [Fintype Symbol] + +/-! ### Decomposing a step + +Auxiliary lemmas that extract the state and tape components of `tm.step cfg = some cfg'` +in terms of the transition function `tm.tr`. +-/ + +/-- The state component of `tm.step cfg` is `(tm.tr q ...).2` when `cfg.state = some q`. -/ +lemma step_state_eq {k : ℕ} {tm : MultiTapeTM k Symbol} {cfg cfg' : tm.Cfg} {q : tm.State} + (h_state : cfg.state = some q) (h_step : tm.step cfg = some cfg') : + (tm.tr q fun i => (cfg.tapes i).head).2 = cfg'.state := by + obtain ⟨_ | _, _⟩ := cfg <;> grind [step] + +/-- The tape component of `tm.step cfg` on tape `i` is the result of applying the `i`-th +`Stmt` of the transition function to `cfg.tapes i`, when `cfg.state = some q`. -/ +lemma step_tapes_eq {k : ℕ} {tm : MultiTapeTM k Symbol} {cfg cfg' : tm.Cfg} {q : tm.State} + (h_state : cfg.state = some q) (h_step : tm.step cfg = some cfg') (i : Fin k) : + cfg'.tapes i = + ((cfg.tapes i).write ((tm.tr q fun i => (cfg.tapes i).head).1 i).symbol).optionMove + ((tm.tr q fun i => (cfg.tapes i).head).1 i).movement := by + obtain ⟨_ | _, _⟩ := cfg <;> grind [step] + +/-! ### Read-only input tape -/ + +/-- +**Step decomposition for an input-tape step.** A step from `cfg` to `cfg'` factors through +the predecessor state `q` (witnessed by `cfg.state = some q`) and specifies the tape-`0` +movement explicitly: `cfg'.tapes 0` is `cfg.tapes 0` under `optionMove` with the direction +dictated by `tm.tr q`. The intermediate `tm.step ⟨some q, cfg.tapes⟩ = some cfg'` form is +handy for feeding `MoveThenStaysOnBlank.move`, whose constructor destructures `cfg`. +-/ +lemma HasInputTape.step_tape0_decompose + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (h_input : tm.HasInputTape) + {cfg cfg' : tm.Cfg} (h_step : tm.step cfg = some cfg') : + ∃ q : tm.State, cfg.state = some q ∧ + tm.step ⟨some q, cfg.tapes⟩ = some cfg' ∧ + cfg'.tapes 0 = (cfg.tapes 0).optionMove + ((tm.tr q fun i => (cfg.tapes i).head).1 0).movement := by + obtain ⟨_ | q, tapes⟩ := cfg + · simp [step] at h_step + refine ⟨q, rfl, h_step, ?_⟩ + have h_pre : ((tm.tr q fun i => (tapes i).head).1 0).symbol = (tapes 0).head := + h_input.readPreserving q (fun i => (tapes i).head) + rw [step_tapes_eq rfl h_step 0, h_pre, BiTape.write_head] + +/-- +A single step of a TM with a designated input tape leaves tape `0` unchanged up to head +movement: the new tape `0` is obtained from the old one by some `optionMove`, and no symbol +on it has changed. +-/ +lemma HasInputTape.step_tape0_eq_optionMove + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (h_input : tm.HasInputTape) + {cfg cfg' : tm.Cfg} (h_step : tm.step cfg = some cfg') : + ∃ m : Option Dir, cfg'.tapes 0 = (cfg.tapes 0).optionMove m := by + obtain ⟨_, _, _, h_tape0⟩ := h_input.step_tape0_decompose h_step + exact ⟨_, h_tape0⟩ + +/-! ### Write-only output tape -/ + +/-- +`OutputTapeContents tape out` says that `tape` is in the canonical shape of a write-only +output tape containing the emitted word `out`: the head is on the first blank cell after +the output, there is nothing to its right, and the left stack stores `out` in reverse +order because the nearest cell to the head is the most recently written symbol. +-/ +def OutputTapeContents (tape : BiTape Symbol) (out : List Symbol) : Prop := + tape.head = none ∧ tape.left = StackTape.map_some out.reverse ∧ tape.right = ∅ + +omit [Inhabited Symbol] [Fintype Symbol] in +@[simp] +lemma outputTapeContents_nil : OutputTapeContents (BiTape.nil : BiTape Symbol) [] := by + simp [OutputTapeContents, BiTape.nil] + +/-- +If the output tape is in canonical output shape before a step, it is in canonical output +shape after the step. The output word either stays the same (blank/stay transition) or +extends by the non-blank symbol written by this step. +-/ +lemma HasOutputTape.step_outputTapeContents + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {cfg cfg' : tm.Cfg} {out : List Symbol} (h_step : tm.step cfg = some cfg') + (h_contents : OutputTapeContents (cfg.tapes (Fin.last (k + 1))) out) : + ∃ out' : List Symbol, + OutputTapeContents (cfg'.tapes (Fin.last (k + 1))) out' ∧ + (out' = out ∨ ∃ a, out' = out ++ [a]) := by + obtain ⟨_ | q, tapes⟩ := cfg + · simp [step] at h_step + obtain ⟨_, h_left, h_right⟩ := h_contents + have h_left' : (tapes (Fin.last (k + 1))).left = StackTape.map_some out.reverse := h_left + have h_right' : (tapes (Fin.last (k + 1))).right = ∅ := h_right + rw [step_tapes_eq rfl h_step (Fin.last (k + 1))] + rcases h_output q (fun i => (tapes i).head) with ⟨h_sym, h_mov⟩ | ⟨h_some, h_mov⟩ + · refine ⟨out, ?_, .inl rfl⟩ + simp [OutputTapeContents, h_sym, h_mov, BiTape.optionMove, BiTape.write, h_left', h_right'] + · obtain ⟨a, h_sym⟩ := Option.isSome_iff_exists.mp h_some + refine ⟨out ++ [a], ?_, .inr ⟨a, rfl⟩⟩ + simp [OutputTapeContents, h_sym, h_mov, BiTape.optionMove, BiTape.write, BiTape.move, + BiTape.move_right, h_left', h_right', List.reverse_append] + +/-- +**Trace-level output-content invariant.** Along any chain of step transitions from a +canonical output tape, the final output tape is canonical for some emitted word. +-/ +lemma HasOutputTape.relatesInSteps_outputTapeContents + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {cfg cfg' : tm.Cfg} {t : ℕ} {out : List Symbol} + (h_rel : Relation.RelatesInSteps tm.TransitionRelation cfg cfg' t) + (h_contents : OutputTapeContents (cfg.tapes (Fin.last (k + 1))) out) : + ∃ out' : List Symbol, + OutputTapeContents (cfg'.tapes (Fin.last (k + 1))) out' := by + exact h_rel.invariant + (P := fun c => ∃ out, OutputTapeContents (c.tapes (Fin.last (k + 1))) out) + (fun h_step h => + let ⟨out, h_contents⟩ := h + let ⟨out', h_contents', _⟩ := h_output.step_outputTapeContents h_step h_contents + ⟨out', h_contents'⟩) + ⟨out, h_contents⟩ + +/-- +Starting from a blank output tape, any reachable output tape is canonical for some emitted +word: the head is blank, the right stack is empty, and the left stack is that word in +reverse. +-/ +lemma HasOutputTape.relatesInSteps_outputTapeContents_of_nil + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {cfg cfg' : tm.Cfg} {t : ℕ} + (h_rel : Relation.RelatesInSteps tm.TransitionRelation cfg cfg' t) + (h_nil : cfg.tapes (Fin.last (k + 1)) = BiTape.nil) : + ∃ out : List Symbol, + OutputTapeContents (cfg'.tapes (Fin.last (k + 1))) out := by + have h_contents : OutputTapeContents (cfg.tapes (Fin.last (k + 1))) [] := by + rw [h_nil] + exact outputTapeContents_nil + exact h_output.relatesInSteps_outputTapeContents h_rel h_contents + +/-- +**Output-content invariant at `TransformsTapes`.** If the output tape starts in canonical +shape, then on any final tapes `tm` transforms them into, the output tape is again +canonical for some emitted word. +-/ +lemma HasOutputTape.transformsTapes_outputTapeContents + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {tapes tapes' : Fin (k + 2) → BiTape Symbol} {out : List Symbol} + (h_trans : tm.TransformsTapes tapes tapes') + (h_contents : OutputTapeContents (tapes (Fin.last (k + 1))) out) : + ∃ out' : List Symbol, + OutputTapeContents (tapes' (Fin.last (k + 1))) out' := by + obtain ⟨_, h_rel⟩ := h_trans + exact h_output.relatesInSteps_outputTapeContents h_rel h_contents + +/-- +**Output-content invariant at `TransformsTapes`, blank initial output case.** +-/ +lemma HasOutputTape.transformsTapes_outputTapeContents_of_nil + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {tapes tapes' : Fin (k + 2) → BiTape Symbol} + (h_trans : tm.TransformsTapes tapes tapes') + (h_nil : tapes (Fin.last (k + 1)) = BiTape.nil) : + ∃ out : List Symbol, + OutputTapeContents (tapes' (Fin.last (k + 1))) out := by + obtain ⟨_, h_rel⟩ := h_trans + exact h_output.relatesInSteps_outputTapeContents_of_nil h_rel h_nil + +/-- +**Output-content invariant at `eval`.** If `tm.eval tapes = some tapes'` and the output tape +starts in canonical shape, then the final output tape is canonical for some emitted word. +-/ +lemma HasOutputTape.eval_outputTapeContents + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {tapes tapes' : Fin (k + 2) → BiTape Symbol} {out : List Symbol} + (h_eval : tm.eval tapes = .some tapes') + (h_contents : OutputTapeContents (tapes (Fin.last (k + 1))) out) : + ∃ out' : List Symbol, + OutputTapeContents (tapes' (Fin.last (k + 1))) out' := + h_output.transformsTapes_outputTapeContents (eval_eq_some_iff_transformsTapes.mp h_eval) + h_contents + +/-- +**Output-content invariant at `eval`, blank initial output case.** +-/ +lemma HasOutputTape.eval_outputTapeContents_of_nil + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {tapes tapes' : Fin (k + 2) → BiTape Symbol} + (h_eval : tm.eval tapes = .some tapes') + (h_nil : tapes (Fin.last (k + 1)) = BiTape.nil) : + ∃ out : List Symbol, + OutputTapeContents (tapes' (Fin.last (k + 1))) out := + h_output.transformsTapes_outputTapeContents_of_nil (eval_eq_some_iff_transformsTapes.mp h_eval) + h_nil + +/-- +If the output tape's right `StackTape` is empty before a step, it is empty after the step. +This is a weaker projection of `HasOutputTape.step_outputTapeContents` that does not assume +the current head cell is blank or that the left stack contains only symbols. +-/ +lemma HasOutputTape.step_right_empty + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {cfg cfg' : tm.Cfg} (h_step : tm.step cfg = some cfg') + (h_right : (cfg.tapes (Fin.last (k + 1))).right = ∅) : + (cfg'.tapes (Fin.last (k + 1))).right = ∅ := by + obtain ⟨_ | q, tapes⟩ := cfg + · simp [step] at h_step + have h_right' : (tapes (Fin.last (k + 1))).right = ∅ := h_right + rw [step_tapes_eq rfl h_step (Fin.last (k + 1))] + rcases h_output q (fun i => (tapes i).head) with ⟨h_sym, h_mov⟩ | ⟨_, h_mov⟩ + · simpa [h_sym, h_mov, BiTape.optionMove, BiTape.write] using h_right' + · simp [h_mov, BiTape.optionMove, BiTape.write, BiTape.move, BiTape.move_right, h_right'] + +/-- +**Trace-level output invariant.** Along any chain of step transitions starting from a +configuration whose output tape has empty `right` `StackTape`, the output tape's `right` +remains empty. Use `HasOutputTape.relatesInSteps_outputTapeContents` when the stronger +canonical output shape is needed. +-/ +lemma HasOutputTape.relatesInSteps_right_empty + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {cfg cfg' : tm.Cfg} {t : ℕ} + (h_rel : Relation.RelatesInSteps tm.TransitionRelation cfg cfg' t) + (h_right : (cfg.tapes (Fin.last (k + 1))).right = ∅) : + (cfg'.tapes (Fin.last (k + 1))).right = ∅ := + h_rel.invariant (P := fun c => (c.tapes (Fin.last (k + 1))).right = ∅) + h_output.step_right_empty h_right + +/-- +**Output invariant at `TransformsTapes`.** If the output tape's right `StackTape` is empty +on the initial tapes, then on any final tapes `tm` transforms them into, the output tape's +right is again empty. +-/ +lemma HasOutputTape.transformsTapes_right_empty + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {tapes tapes' : Fin (k + 2) → BiTape Symbol} + (h_trans : tm.TransformsTapes tapes tapes') + (h_right : (tapes (Fin.last (k + 1))).right = ∅) : + (tapes' (Fin.last (k + 1))).right = ∅ := by + obtain ⟨_, h_rel⟩ := h_trans + exact h_output.relatesInSteps_right_empty h_rel h_right + +/-- +**Output invariant at `eval`.** If `tm.eval tapes = some tapes'` and the output tape's right +`StackTape` starts empty, then the output tape's right is empty on `tapes'`. +-/ +lemma HasOutputTape.eval_right_empty + {k : ℕ} {tm : MultiTapeTM (k + 2) Symbol} (h_output : tm.HasOutputTape) + {tapes tapes' : Fin (k + 2) → BiTape Symbol} + (h_eval : tm.eval tapes = .some tapes') + (h_right : (tapes (Fin.last (k + 1))).right = ∅) : + (tapes' (Fin.last (k + 1))).right = ∅ := + h_output.transformsTapes_right_empty (eval_eq_some_iff_transformsTapes.mp h_eval) h_right + +/-! ### Trace-level head boundedness on the input tape + +The syntactic predicate `IsBoundedInDirectionOnTape` is phrased on the *finite control* — it +forbids certain reachability patterns in the state graph. To show this rules out actual +computation trajectories that drift off the input, we lift the syntactic chain `MoveThenStays` +to a configuration-level chain `MoveThenStaysOnBlank` and prove that any semantic trace of +the right shape produces a syntactic reachability witness, after which +`IsBoundedInDirectionOnTape` rules out the bad continuation. +-/ + +/-- +A configuration trajectory of the form +`⟨some q₁, _⟩ →[move-d on tape i] cfg₂ →[stay-on-blank-on-tape-i]* cfg`, +parameterized by the starting state `q₁`, the ending state `q₂`, and the ending +configuration `cfg`, whose tapes are inspectable. +-/ +inductive MoveThenStaysOnBlank + {k : ℕ} (tm : MultiTapeTM k Symbol) (i : Fin k) (d : Dir) : + tm.State → tm.State → tm.Cfg → Prop where + /-- Single move-`d` step from `q₁`: the resulting configuration is the witness. -/ + | move {q₁ q₂ : tm.State} {tapes₁ : Fin k → BiTape Symbol} {cfg₂ : tm.Cfg} + (h_step : tm.step ⟨some q₁, tapes₁⟩ = some cfg₂) + (h_state : cfg₂.state = some q₂) + (h_mov : ((tm.tr q₁ fun i => (tapes₁ i).head).1 i).movement = some d) : + MoveThenStaysOnBlank tm i d q₁ q₂ cfg₂ + /-- Extend an existing chain by a stay-on-blank step on tape `i`. -/ + | stay {q₁ q₂ q₃ : tm.State} {cfg₂ cfg₃ : tm.Cfg} + (h_prev : MoveThenStaysOnBlank tm i d q₁ q₂ cfg₂) + (h_blank : (cfg₂.tapes i).head = none) + (h_step : tm.step cfg₂ = some cfg₃) + (h_state : cfg₃.state = some q₃) + (h_no_mov : ((tm.tr q₂ fun i => (cfg₂.tapes i).head).1 i).movement = none) : + MoveThenStaysOnBlank tm i d q₁ q₃ cfg₃ + +/-- The state of the witness configuration of a chain matches its second state parameter. -/ +lemma MoveThenStaysOnBlank.cfg_state_eq + {k : ℕ} {tm : MultiTapeTM k Symbol} {i : Fin k} {d : Dir} + {q₁ q₂ : tm.State} {cfg : tm.Cfg} + (h : MoveThenStaysOnBlank tm i d q₁ q₂ cfg) : + cfg.state = some q₂ := by + induction h with + | move _ h_state _ => exact h_state + | stay _ _ _ h_state _ => exact h_state + +/-- +A semantic chain is a witness of the syntactic chain on its endpoint states. +-/ +lemma MoveThenStaysOnBlank.moveThenStays + {k : ℕ} {tm : MultiTapeTM k Symbol} {i : Fin k} {d : Dir} + {q₁ q₂ : tm.State} {cfg : tm.Cfg} + (h_chain : MoveThenStaysOnBlank tm i d q₁ q₂ cfg) : + MoveThenStays tm.tr i d q₁ q₂ := by + induction h_chain with + | move h_step h_state h_mov => + refine .move _ _ _ h_mov ?_ + rw [step_state_eq rfl h_step, h_state] + | stay h_prev h_blank h_step h_state h_no_mov ih => + refine .stay _ _ _ ih _ h_blank h_no_mov ?_ + rw [step_state_eq h_prev.cfg_state_eq h_step, h_state] + +end MultiTapeTM + +namespace IsBoundedInDirectionOnTape + +variable [Inhabited Symbol] [Fintype Symbol] + +/-- +**Trace-level boundedness.** Given `IsBoundedInDirectionOnTape tm.tr i d`, no actual +computation trace matching the "move-`d` on tape `i`, then stay-on-blank-on-tape-`i`*" +pattern can end in a state that would move the head further in direction `d` on a blank. + +Iterating this gives that the head on tape `i` does not perform two consecutive +direction-`d` moves separated by stay-moves on the blank. The quantitative `±1`-cell +bound on the head position over arbitrary traces is `HasInputTape.head_position_bounded`. +-/ +lemma not_movesOffBlankInDir_of_chain + {k : ℕ} {tm : MultiTapeTM k Symbol} {i : Fin k} {d : Dir} + (h_bound : IsBoundedInDirectionOnTape tm.tr i d) + {q₁ q₂ : tm.State} {cfg : tm.Cfg} + (h_chain : MultiTapeTM.MoveThenStaysOnBlank tm i d q₁ q₂ cfg) : + ¬ MovesOffBlankInDir tm.tr i d q₂ := + h_bound q₁ q₂ h_chain.moveThenStays + +end IsBoundedInDirectionOnTape + +/-! ### Quantitative head-position bound on the input tape + +We promote the qualitative chain-level boundedness to a quantitative `±1` bound on the +tape-`0` head position over arbitrary traces from `initCfg s` (with non-empty input). +The position is read off the `BiTape` geometry via `canonicalInputTape s p`, the unique +shape of tape `0` after the head has moved to integer position `p` relative to the +start of the input (see `Cslib.Foundations.Data.BiTape.Canonical`). +-/ + +namespace MultiTapeTM + +variable [Inhabited Symbol] [Fintype Symbol] + +/-! ### Head-boundedness invariant -/ + +/-- +**Head-boundedness invariant at position `p`.** For a configuration `cfg` along a trace +from `initCfg s` of a TM with a designated input tape, tape `0` of `cfg` is in canonical +shape `canonicalInputTape s p` for some integer position `p ∈ [-1, s.length]`. +-/ +structure HeadBoundInvariantAt {k : ℕ} (tm : MultiTapeTM (k + 1) Symbol) (s : List Symbol) + (cfg : tm.Cfg) (p : ℤ) : Prop where + /-- `p` is at least `-1` (one cell left of the input). -/ + pos_lower : -1 ≤ p + /-- `p` is at most `s.length` (one cell right of the last input symbol). -/ + pos_upper : p ≤ (s.length : ℤ) + /-- Tape `0` is in canonical shape at integer position `p`. -/ + tape_eq : cfg.tapes 0 = canonicalInputTape s p + +/-- +**Strong head-boundedness invariant.** Extends `HeadBoundInvariantAt` with chain witnesses +at the endpoints: when the machine is not halted and the head sits one cell past an end of +the input, a move-stay-blank chain witness records the inbound direction. This is what +threads `IsBoundedInDirectionOnTape` through the inductive step preservation; user-facing +results expose only the underlying `HeadBoundInvariantAt`. +-/ +structure HeadBoundInvariantAt.Strong {k : ℕ} (tm : MultiTapeTM (k + 1) Symbol) + (s : List Symbol) (cfg : tm.Cfg) (p : ℤ) : Prop + extends HeadBoundInvariantAt tm s cfg p where + /-- Chain witness at the left endpoint. -/ + chain_left : ∀ q, cfg.state = some q → p = -1 → + ∃ q₀, MoveThenStaysOnBlank tm 0 .left q₀ q cfg + /-- Chain witness at the right endpoint. -/ + chain_right : ∀ q, cfg.state = some q → p = (s.length : ℤ) → + ∃ q₀, MoveThenStaysOnBlank tm 0 .right q₀ q cfg + +/-- +**Trace-level invariant.** Either the input is empty (in which case tape `0` is forced to +`BiTape.nil` throughout the trace and any canonical position coincides with `nil`), or +some position `p ∈ [-1, s.length]` witnesses the strong invariant. The disjunction handles +empty and nonempty input uniformly along traces. +-/ +def HeadBoundInvariantForInput {k : ℕ} (tm : MultiTapeTM (k + 1) Symbol) (s : List Symbol) + (cfg : tm.Cfg) : Prop := + s = [] ∧ cfg.tapes 0 = BiTape.nil ∨ ∃ p : ℤ, HeadBoundInvariantAt.Strong tm s cfg p + +/-- The initial configuration satisfies the strong head-boundedness invariant at `p = 0`, +provided the input is nonempty. -/ +lemma HeadBoundInvariantAt.Strong.initCfg + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} {s : List Symbol} (h_pos : 0 < s.length) : + HeadBoundInvariantAt.Strong tm s (tm.initCfg s) 0 where + pos_lower := by omega + pos_upper := Int.natCast_nonneg _ + tape_eq := show BiTape.mk₁ s = _ from (canonicalInputTape_zero s).symm + chain_left _ _ h := absurd h (by omega) + chain_right _ _ h := absurd h (by exact_mod_cast h_pos.ne) + +/-- The initial configuration satisfies the trace-level invariant for any input. -/ +lemma HeadBoundInvariantForInput.initCfg + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (s : List Symbol) : + HeadBoundInvariantForInput tm s (tm.initCfg s) := by + by_cases h_pos : 0 < s.length + · exact .inr ⟨0, .initCfg h_pos⟩ + · have hs : s = [] := List.length_eq_zero_iff.mp (by omega) + subst hs + exact .inl ⟨rfl, rfl⟩ + +/-- **Step preservation of the strong head-boundedness invariant.** A single step of a TM +with an input tape preserves the strong invariant: the head position advances by at most +one cell and stays within `[-1, s.length]`; endpoint chain witnesses are maintained by +extending via `stay` or constructed fresh via `move`; an attempt to step past an endpoint +is ruled out by `IsBoundedInDirectionOnTape.not_movesOffBlankInDir_of_chain`. -/ +lemma HeadBoundInvariantAt.Strong.step + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (h_input : tm.HasInputTape) + {s : List Symbol} {cfg cfg' : tm.Cfg} {p : ℤ} + (h_inv : HeadBoundInvariantAt.Strong tm s cfg p) (h_step : tm.step cfg = some cfg') : + ∃ p' : ℤ, HeadBoundInvariantAt.Strong tm s cfg' p' := by + obtain ⟨q, h_state_q, h_step_q, h_tape0⟩ := h_input.step_tape0_decompose h_step + have h_head_eq : (cfg.tapes 0).head = none ↔ (p = -1 ∨ p = (s.length : ℤ)) := by + rw [h_inv.tape_eq]; exact canonicalInputTape_head_eq_none_iff h_inv.pos_lower h_inv.pos_upper + cases hm : ((tm.tr q fun i => (cfg.tapes i).head).1 0).movement with + | none => + refine ⟨p, ⟨h_inv.pos_lower, h_inv.pos_upper, ?_⟩, ?_, ?_⟩ + · rw [h_tape0, hm]; exact h_inv.tape_eq + · intro q' hq' hp_neg_one + have h_blank : (cfg.tapes 0).head = none := h_head_eq.mpr (Or.inl hp_neg_one) + obtain ⟨q₀, h_chain⟩ := h_inv.chain_left q h_state_q hp_neg_one + exact ⟨q₀, MoveThenStaysOnBlank.stay h_chain h_blank h_step hq' hm⟩ + · intro q' hq' hp_len + have h_blank : (cfg.tapes 0).head = none := h_head_eq.mpr (Or.inr hp_len) + obtain ⟨q₀, h_chain⟩ := h_inv.chain_right q h_state_q hp_len + exact ⟨q₀, MoveThenStaysOnBlank.stay h_chain h_blank h_step hq' hm⟩ + | some d => + cases d with + | right => + by_cases hp_eq : p = (s.length : ℤ) + · exfalso + have h_blank : (cfg.tapes 0).head = none := h_head_eq.mpr (Or.inr hp_eq) + obtain ⟨q₀, h_chain⟩ := h_inv.chain_right q h_state_q hp_eq + exact IsBoundedInDirectionOnTape.not_movesOffBlankInDir_of_chain + h_input.rightBounded h_chain ⟨fun i => (cfg.tapes i).head, h_blank, hm⟩ + · have hp_lt : p < (s.length : ℤ) := by have := h_inv.pos_upper; omega + have hp_lo := h_inv.pos_lower + refine ⟨p + 1, ⟨by omega, by omega, ?_⟩, ?_, ?_⟩ + · rw [h_tape0, hm, h_inv.tape_eq] + exact canonicalInputTape_move_right hp_lo hp_lt + · intro _ _ hp_neg_one; exfalso; omega + · intro q' hq' _ + exact ⟨q, MoveThenStaysOnBlank.move h_step_q hq' hm⟩ + | left => + by_cases hp_eq : p = -1 + · exfalso + have h_blank : (cfg.tapes 0).head = none := h_head_eq.mpr (Or.inl hp_eq) + obtain ⟨q₀, h_chain⟩ := h_inv.chain_left q h_state_q hp_eq + exact IsBoundedInDirectionOnTape.not_movesOffBlankInDir_of_chain + h_input.leftBounded h_chain ⟨fun i => (cfg.tapes i).head, h_blank, hm⟩ + · have hp_nn : 0 ≤ p := by have := h_inv.pos_lower; omega + have hp_hi := h_inv.pos_upper + refine ⟨p - 1, ⟨by omega, by omega, ?_⟩, ?_, ?_⟩ + · rw [h_tape0, hm, h_inv.tape_eq] + exact canonicalInputTape_move_left hp_nn hp_hi + · intro q' hq' _ + exact ⟨q, MoveThenStaysOnBlank.move h_step_q hq' hm⟩ + · intro _ _ hp_len; exfalso; omega + +/-- A step of an input-tape-preserving TM keeps `BiTape.nil` on tape `0`. -/ +private lemma HasInputTape.step_tape0_nil {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} + (h_input : tm.HasInputTape) {cfg cfg' : tm.Cfg} + (h_tape : cfg.tapes 0 = BiTape.nil) (h_step : tm.step cfg = some cfg') : + cfg'.tapes 0 = BiTape.nil := by + obtain ⟨m, h_m⟩ := h_input.step_tape0_eq_optionMove h_step + rw [h_m, h_tape, BiTape.optionMove_nil] + +/-- **Step preservation of the trace-level invariant.** -/ +lemma HeadBoundInvariantForInput.step + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (h_input : tm.HasInputTape) + {s : List Symbol} {cfg cfg' : tm.Cfg} + (h_inv : HeadBoundInvariantForInput tm s cfg) (h_step : tm.step cfg = some cfg') : + HeadBoundInvariantForInput tm s cfg' := by + rcases h_inv with ⟨h_empty, h_nil⟩ | ⟨_, h_strong⟩ + · exact .inl ⟨h_empty, h_input.step_tape0_nil h_nil h_step⟩ + · exact .inr (h_strong.step h_input h_step) + +/-- The trace-level invariant is preserved along any chain of step transitions. -/ +lemma HeadBoundInvariantForInput.relatesInSteps + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (h_input : tm.HasInputTape) + {s : List Symbol} {cfg cfg' : tm.Cfg} {t : ℕ} + (h_inv : HeadBoundInvariantForInput tm s cfg) + (h_rel : Relation.RelatesInSteps tm.TransitionRelation cfg cfg' t) : + HeadBoundInvariantForInput tm s cfg' := + h_rel.invariant (fun h_step h => h.step h_input h_step) h_inv + +/-- The trace-level invariant projects to a position bound + canonical tape match. -/ +lemma HeadBoundInvariantForInput.exists_pos {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} + {s : List Symbol} {cfg : tm.Cfg} (h_inv : HeadBoundInvariantForInput tm s cfg) : + ∃ p : ℤ, -1 ≤ p ∧ p ≤ (s.length : ℤ) ∧ cfg.tapes 0 = canonicalInputTape s p := by + rcases h_inv with ⟨h_empty, h_nil⟩ | ⟨p, h_strong⟩ + · subst h_empty + refine ⟨0, by omega, by simp, ?_⟩ + rw [canonicalInputTape_nil]; exact h_nil + · exact ⟨p, h_strong.pos_lower, h_strong.pos_upper, h_strong.tape_eq⟩ + +/-- **Quantitative head-position bound.** Every configuration reachable from `initCfg s` +in `t` steps has its tape-`0` content in canonical shape `canonicalInputTape s p` for some +integer position `p ∈ [-1, s.length]`. In particular, the head on tape `0` stays within +one cell of the input region throughout the trace. -/ +theorem HasInputTape.head_position_bounded + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (h_input : tm.HasInputTape) + {s : List Symbol} {cfg' : tm.Cfg} {t : ℕ} + (h_rel : Relation.RelatesInSteps tm.TransitionRelation (tm.initCfg s) cfg' t) : + ∃ p : ℤ, -1 ≤ p ∧ p ≤ (s.length : ℤ) ∧ cfg'.tapes 0 = canonicalInputTape s p := + ((HeadBoundInvariantForInput.initCfg s).relatesInSteps h_input h_rel).exists_pos + +end MultiTapeTM + end Turing diff --git a/Cslib/Computability/Machines/TuringCommon.lean b/Cslib/Computability/Machines/TuringCommon.lean index 60d063663..2cdff20ef 100644 --- a/Cslib/Computability/Machines/TuringCommon.lean +++ b/Cslib/Computability/Machines/TuringCommon.lean @@ -6,6 +6,7 @@ Authors: Bolton Bailey, Pim Spelier, Daan van Gent module +public import Cslib.Init public import Mathlib.Computability.TuringMachine.Tape @[expose] public section @@ -25,4 +26,103 @@ deriving Inhabited instance inhabitedStmt : Inhabited (Stmt Symbol) := inferInstance +namespace Stmt + +variable {Symbol : Type} + +/-- +A `Stmt` is *write-only* if it either writes a blank and stays put, or writes a non-blank +symbol and moves the head right. + +A transition function that produces only write-only `Stmt`s on a given tape implements a +"write-only output tape" in the sense of Arora–Barak when started from a blank output +tape: the head remains on the first blank cell after the output, and the tape content to +the left of the head is the reverse of the sequence of non-blank writes. + +Note that the "write a blank, move right" case is deliberately excluded: on a write-only +output tape, blanks only appear in cells the head has not yet visited. Admitting blank +writes would break the "left of the head is the reverse of the emitted output" reading. +-/ +def IsWriteOnly (s : Stmt Symbol) : Prop := + (s.symbol = none ∧ s.movement = none) ∨ + (s.symbol.isSome ∧ s.movement = some .right) + +/-- +A `Stmt` is *read-preserving with respect to the currently read symbol `r`* if it writes +back exactly what it read. The head is free to move in either direction (or stay). + +A transition function that produces only read-preserving `Stmt`s on a given tape never +modifies that tape. This is the syntactic half of the classical "two-way read-only input +tape" condition; the complementary *boundedness* property—that the head stays within the +input region plus at most one cell on either side—cannot be stated purely on the +transition function (a transition reading a blank cannot distinguish the left blank from +the right blank) and is left to a separate predicate. +-/ +def IsReadPreserving (r : Option Symbol) (s : Stmt Symbol) : Prop := + s.symbol = r + +end Stmt + +/-! ## Syntactic predicates on multi-tape transition functions + +These predicates characterise reachability patterns in the finite control of a transition +function `tr` of the multi-tape shape, independently of any wrapping machine structure. +They are used to phrase head-boundedness of designated input tapes syntactically. +-/ + +variable {State Symbol : Type} {k : ℕ} + +/-- +State `q` is *harmful in direction `d`* on tape index `i` of transition function `tr` if some +transition from `q` reads a blank on tape `i` and moves the head on tape `i` in direction `d`. + +These are the states whose firing would step the head one cell further past an end of the +input region. +-/ +def MovesOffBlankInDir + (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State)) + (i : Fin k) (d : Dir) (q : State) : Prop := + ∃ reads, reads i = none ∧ ((tr q reads).1 i).movement = some d + +/-- +`MoveThenStays tr i d q q'` holds if `q'` is reachable from `q` by a tape-`i` trajectory +of the form `q →[move in direction d] q₁ →[stay while reading blank]* q'`. + +The initial transition's read is unconstrained — the head may have been on an input cell +before stepping out to the blank — but every subsequent transition keeps the head fixed at +the blank, hence reads blank on tape `i` and produces no movement on tape `i`. +-/ +inductive MoveThenStays + (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State)) + (i : Fin k) (d : Dir) : State → State → Prop where + /-- Single move in direction `d`, with no constraint on the read. -/ + | move (q q' : State) (reads : Fin k → Option Symbol) + (h_mov : ((tr q reads).1 i).movement = some d) + (h_next : (tr q reads).2 = some q') : + MoveThenStays tr i d q q' + /-- Extend an existing chain by a stay-move while reading blank on tape `i`. -/ + | stay (q q' q'' : State) + (h_prev : MoveThenStays tr i d q q') + (reads : Fin k → Option Symbol) + (h_reads : reads i = none) + (h_mov : ((tr q' reads).1 i).movement = none) + (h_next : (tr q' reads).2 = some q'') : + MoveThenStays tr i d q q'' + +/-- +Transition function `tr` is *bounded in direction `d`* on tape `i` if no chain of the form +"move in direction `d`, then stay-on-blank repeatedly, then move in direction `d` again" +exists. Equivalently: no harmful state in direction `d` is reachable via a post-`d`-move +stay-on-blank chain. + +This is the syntactic condition we use to keep the head within the input region (plus one +cell on either side): once the head steps off the input in direction `d`, it cannot step +further in direction `d` without returning first. The condition is finitary — both the +reachability relation and the existential in `MovesOffBlankInDir` range over finite types. +-/ +def IsBoundedInDirectionOnTape + (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State)) + (i : Fin k) (d : Dir) : Prop := + ∀ q q', MoveThenStays tr i d q q' → ¬ MovesOffBlankInDir tr i d q' + end Turing diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index ba7160556..5fb13607c 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -44,6 +44,7 @@ namespace Turing A structure for bidirectionally-infinite Turing machine tapes that eventually take on blank `none` values -/ +@[ext] structure BiTape (Symbol : Type) where /-- The symbol currently under the tape head -/ head : Option Symbol @@ -114,6 +115,18 @@ lemma move_left_move_right (t : BiTape Symbol) : t.move_left.move_right = t := b lemma move_right_move_left (t : BiTape Symbol) : t.move_right.move_left = t := by simp [move_left, move_right] +@[simp] +lemma move_left_nil : (nil : BiTape Symbol).move_left = nil := rfl + +@[simp] +lemma move_right_nil : (nil : BiTape Symbol).move_right = nil := rfl + +@[simp] +lemma optionMove_nil (m : Option Dir) : (nil : BiTape Symbol).optionMove m = nil := by + cases m with + | none => rfl + | some d => cases d <;> rfl + end Move /-- @@ -121,6 +134,9 @@ Write a value under the head of the `BiTape`. -/ def write (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol := { t with head := a } +@[simp] +lemma write_head (t : BiTape Symbol) : t.write t.head = t := rfl + /-- The space used by a `BiTape` is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the `BiTape`. diff --git a/Cslib/Foundations/Data/BiTape/Canonical.lean b/Cslib/Foundations/Data/BiTape/Canonical.lean new file mode 100644 index 000000000..248ad6606 --- /dev/null +++ b/Cslib/Foundations/Data/BiTape/Canonical.lean @@ -0,0 +1,179 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Sam Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Sam Schlesinger +-/ + +module + +public import Cslib.Foundations.Data.BiTape +public import Mathlib.Data.List.TakeDrop + +@[expose] public section + +/-! +# Canonical input-tape shapes for `BiTape` + +The canonical `BiTape` configuration for an input list `s` with the head at integer position +`p` relative to the start of the input. Used by the multi-tape Turing machine head-position +bound to characterise tape `0`'s shape along a trace. + +* `canonicalInputTapeNat s n` — the shape when the head sits at natural-number position `n`. +* `canonicalInputTape s p` — the integer-indexed version, with `p = -1` representing "one + cell left of the input" and `p ≥ 0` delegating to `canonicalInputTapeNat`. + +The basic move-right / move-left / head / zero / nil lemmas collected here are what the +Turing-machine invariant uses to step the head back and forth within `[-1, s.length]`. +-/ + +namespace Turing + +open StackTape + +variable {Symbol : Type} + +/-- +The canonical `BiTape` configuration for an input tape containing `s`, with the head at +natural number position `n` (i.e. `0` is the start of the input). + +For `n < s.length`, the head reads `some s[n]`; for `n ≥ s.length`, the head reads +`none` and the tape has `s.reverse` on the left. +-/ +def canonicalInputTapeNat (s : List Symbol) (n : ℕ) : BiTape Symbol where + head := s[n]? + left := StackTape.map_some (s.take n).reverse + right := StackTape.map_some (s.drop (n + 1)) + +/-- +The canonical `BiTape` shape of the input tape at integer position `p`, with `p = -1` +representing "one cell left of the input" (a blank cell with `s` to the right) and +`p ≥ 0` delegating to `canonicalInputTapeNat`. + +The head-position bound theorem shows that traces from `initCfg s` only produce tapes +matching `canonicalInputTape s p` for `-1 ≤ p ≤ s.length`. +-/ +def canonicalInputTape (s : List Symbol) (p : ℤ) : BiTape Symbol := + if 0 ≤ p then canonicalInputTapeNat s p.toNat + else ⟨none, ∅, StackTape.map_some s⟩ + +@[simp] +lemma canonicalInputTape_ofNat (s : List Symbol) (n : ℕ) : + canonicalInputTape s (n : ℤ) = canonicalInputTapeNat s n := by + simp [canonicalInputTape] + +@[simp] +lemma canonicalInputTape_neg_one (s : List Symbol) : + canonicalInputTape s (-1) = ⟨none, ∅, StackTape.map_some s⟩ := rfl + +@[simp] +lemma canonicalInputTapeNat_zero (s : List Symbol) : + canonicalInputTapeNat s 0 = BiTape.mk₁ s := by + cases s <;> simp [canonicalInputTapeNat, BiTape.mk₁, BiTape.nil] + +@[simp] +lemma canonicalInputTape_zero (s : List Symbol) : + canonicalInputTape s 0 = BiTape.mk₁ s := + (canonicalInputTape_ofNat s 0).trans (canonicalInputTapeNat_zero s) + +/-- One-step move-right on the canonical configuration at natural-number position `n`, +when still within the input region. -/ +lemma canonicalInputTapeNat_move_right {s : List Symbol} {n : ℕ} (h : n < s.length) : + (canonicalInputTapeNat s n).move_right = canonicalInputTapeNat s (n + 1) := by + simp only [canonicalInputTapeNat, BiTape.move_right] + have h_take : s.take (n + 1) = s.take n ++ [s[n]] := (List.take_concat_get' s n h).symm + have h_get : s[n]? = some s[n] := List.getElem?_eq_getElem h + ext + · -- head: (map_some (s.drop (n+1))).head = s[n+1]? + rw [StackTape.head_map_some, List.head?_drop] + · -- left: cons s[n]? (map_some (s.take n).reverse) = map_some (s.take (n+1)).reverse + rw [h_get, h_take, List.reverse_append, List.reverse_singleton, List.singleton_append, + StackTape.map_some_cons] + · -- right: (map_some (s.drop (n+1))).tail = map_some (s.drop (n+2)) + rw [StackTape.tail_map_some, List.tail_drop] + +/-- One-step move-left on the canonical configuration at natural-number position `n + 1`, +when still within the input region. -/ +lemma canonicalInputTapeNat_move_left {s : List Symbol} {n : ℕ} (h : n < s.length) : + (canonicalInputTapeNat s (n + 1)).move_left = canonicalInputTapeNat s n := by + simp only [canonicalInputTapeNat, BiTape.move_left] + have h_take : s.take (n + 1) = s.take n ++ [s[n]] := (List.take_concat_get' s n h).symm + have h_get : s[n]? = some s[n] := List.getElem?_eq_getElem h + ext + · -- head: (map_some (s.take (n+1)).reverse).head = s[n]? + rw [h_take, List.reverse_append, List.reverse_singleton, List.singleton_append, + StackTape.head_map_some_cons, h_get] + · -- left: (map_some (s.take (n+1)).reverse).tail = map_some (s.take n).reverse + rw [StackTape.tail_map_some, h_take, List.reverse_append, List.reverse_singleton, + List.singleton_append, List.tail_cons] + · -- right: cons s[n+1]? (map_some (s.drop (n+1+1))) = map_some (s.drop (n+1)) + -- `cases h_drop : s.drop (n+1)` rewrites `s.drop (n+1)` on the RHS + cases h_drop : s.drop (n + 1) with + | nil => + have h1 : s.length ≤ n + 1 := List.drop_eq_nil_iff.mp h_drop + have h_head : s[n + 1]? = none := List.getElem?_eq_none (by omega) + have h_drop2 : s.drop (n + 1 + 1) = [] := List.drop_eq_nil_iff.mpr (by omega) + rw [h_head, h_drop2] + rfl + | cons a rest => + have h_head : s[n + 1]? = some a := by + rw [← List.head?_drop, h_drop]; rfl + have h_drop2 : s.drop (n + 1 + 1) = rest := by + rw [← List.tail_drop, h_drop]; rfl + rw [h_head, h_drop2] + exact (StackTape.map_some_cons a rest).symm + +/-- One-step move-right on the integer-indexed canonical configuration, staying within +`[-1, s.length]`. -/ +lemma canonicalInputTape_move_right {s : List Symbol} {p : ℤ} + (h_lo : -1 ≤ p) (h_hi : p < (s.length : ℤ)) : + (canonicalInputTape s p).move_right = canonicalInputTape s (p + 1) := by + by_cases hp_nn : 0 ≤ p + · simp only [canonicalInputTape, if_pos hp_nn, if_pos (show (0 : ℤ) ≤ p + 1 by omega), + show (p + 1).toNat = p.toNat + 1 from by omega] + exact canonicalInputTapeNat_move_right (by omega) + · obtain rfl : p = -1 := by omega + rw [show (-1 : ℤ) + 1 = 0 from rfl, canonicalInputTape_neg_one, canonicalInputTape_zero] + cases s with + | nil => rfl + | cons a t => + simp [BiTape.mk₁, BiTape.move_right] + +/-- One-step move-left on the integer-indexed canonical configuration, staying within +`[0, s.length]` (with the result going to `[-1, s.length - 1]`). -/ +lemma canonicalInputTape_move_left {s : List Symbol} {p : ℤ} + (h_lo : 0 ≤ p) (h_hi : p ≤ (s.length : ℤ)) : + (canonicalInputTape s p).move_left = canonicalInputTape s (p - 1) := by + by_cases hp_pos : 0 < p + · have hp_pred : (p - 1).toNat + 1 = p.toNat := by omega + simp only [canonicalInputTape, if_pos hp_pos.le, if_pos (show (0 : ℤ) ≤ p - 1 by omega)] + rw [← hp_pred] + exact canonicalInputTapeNat_move_left (by omega) + · obtain rfl : p = 0 := by omega + rw [show (0 : ℤ) - 1 = -1 from rfl, canonicalInputTape_zero, canonicalInputTape_neg_one] + cases s with + | nil => rfl + | cons a t => + simp [BiTape.mk₁, BiTape.move_left] + +/-- Characterization of when the head of a canonical configuration is blank (inside the +valid range `[-1, s.length]`). -/ +lemma canonicalInputTape_head_eq_none_iff {s : List Symbol} {p : ℤ} + (h_lo : -1 ≤ p) (h_hi : p ≤ (s.length : ℤ)) : + (canonicalInputTape s p).head = none ↔ p = -1 ∨ p = s.length := by + by_cases hp_nn : 0 ≤ p + · have hp_cast : (p.toNat : ℤ) = p := Int.toNat_of_nonneg hp_nn + simp only [canonicalInputTape, if_pos hp_nn, canonicalInputTapeNat, + List.getElem?_eq_none_iff] + omega + · obtain rfl : p = -1 := by omega + simp + +/-- With empty input, every integer position collapses to the empty bi-tape. This makes the +empty-input branch of `HasInputTape.head_position_bounded` trivial: every reachable tape-`0` +configuration is `BiTape.nil`, which equals `canonicalInputTape [] p` for any `p`. -/ +lemma canonicalInputTape_nil (p : ℤ) : + canonicalInputTape ([] : List Symbol) p = BiTape.nil := by + unfold canonicalInputTape + split_ifs <;> simp [canonicalInputTapeNat, BiTape.nil] + +end Turing diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean index 052e52c98..1ac6252f5 100644 --- a/Cslib/Foundations/Data/RelatesInSteps.lean +++ b/Cslib/Foundations/Data/RelatesInSteps.lean @@ -120,6 +120,17 @@ lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} : · rintro ⟨t', h_red, h_steps⟩ exact h_steps.head a t' b n h_red +/-- +A predicate preserved by every step of `r` is preserved along any chain of `r`-steps. +-/ +lemma RelatesInSteps.invariant {a b : α} {n : ℕ} {P : α → Prop} + (h_step : ∀ {x y}, r x y → P x → P y) (h_rel : RelatesInSteps r a b n) : + P a → P b := by + induction h_rel with + | refl => exact id + | tail _ _ _ _ h₂ ih => exact fun ha => h_step h₂ (ih ha) + + /-- If `h : α → ℕ` increases by at most 1 on each step of `r`, then the value of `h` at the output is at most `h` at the input plus the number of steps. diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index f495d897a..3a2f60e9c 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -88,6 +88,12 @@ def cons (x : Option Symbol) (xs : StackTape Symbol) : StackTape Symbol := @[simp, scoped grind =] lemma cons_none_nil_toList : (cons none (nil : StackTape Symbol)).toList = [] := by grind +@[simp, scoped grind =] +lemma cons_none_nil : cons none (nil : StackTape Symbol) = nil := rfl + +@[simp, scoped grind =] +lemma cons_none_empty : cons none (∅ : StackTape Symbol) = ∅ := rfl + @[simp, scoped grind =] lemma cons_some_toList (a : Symbol) (l : StackTape Symbol) : (cons (some a) l).toList = some a :: l.toList := by simp only [cons] @@ -99,6 +105,9 @@ def tail (l : StackTape Symbol) : StackTape Symbol := | [] => nil | hd :: t => ⟨t, by grind⟩ +@[simp] +lemma tail_nil : (nil : StackTape Symbol).tail = nil := rfl + /-- Get the first element of the `StackTape`. -/ @[scoped grind] def head (l : StackTape Symbol) : Option Symbol := @@ -106,6 +115,12 @@ def head (l : StackTape Symbol) : Option Symbol := | [] => none | h :: _ => h +@[simp, scoped grind =] +lemma head_nil : (nil : StackTape Symbol).head = none := rfl + +@[simp, scoped grind =] +lemma head_empty : (∅ : StackTape Symbol).head = none := rfl + lemma eq_iff (l1 l2 : StackTape Symbol) : l1 = l2 ↔ l1.head = l2.head ∧ l1.tail = l2.tail := by constructor @@ -142,6 +157,33 @@ lemma cons_head_tail (l : StackTape Symbol) : @[scoped grind] def map_some (l : List Symbol) : StackTape Symbol := ⟨l.map some, by simp⟩ +@[simp, scoped grind =] +lemma map_some_nil : (map_some [] : StackTape Symbol) = ∅ := rfl + +@[simp, scoped grind =] +lemma map_some_cons (a : Symbol) (l : List Symbol) : + map_some (a :: l) = cons (some a) (map_some l) := by + cases l <;> simp [map_some, cons] + +@[simp, scoped grind =] +lemma head_map_some_nil : (map_some [] : StackTape Symbol).head = none := rfl + +@[simp, scoped grind =] +lemma head_map_some_cons (a : Symbol) (l : List Symbol) : + (map_some (a :: l) : StackTape Symbol).head = some a := rfl + +@[simp, scoped grind =] +lemma head_map_some (l : List Symbol) : + (map_some l : StackTape Symbol).head = l.head? := by + cases l <;> rfl + +@[simp, scoped grind =] +lemma tail_map_some (l : List Symbol) : + (map_some l : StackTape Symbol).tail = map_some l.tail := by + cases l with + | nil => rfl + | cons a t => cases t <;> simp [map_some, tail] + section Length /-- The length of the `StackTape` is the number of elements up to the last non-`none` element -/ From 697ee60e830d01813a1c9b8789453cef6cc6eef9 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 21 Apr 2026 16:52:02 -0400 Subject: [PATCH 2/2] Address multi-tape input review comments --- .../Machines/MultiTapeTuring/Basic.lean | 73 +++++++-- .../Computability/Machines/TuringCommon.lean | 13 +- Cslib/Foundations/Data/BiTape.lean | 68 ++++++++ Cslib/Foundations/Data/BiTape/Canonical.lean | 149 ++++++++---------- Cslib/Foundations/Data/StackTape.lean | 15 +- 5 files changed, 210 insertions(+), 108 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean index 4f6e8a712..38446d782 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean @@ -143,7 +143,7 @@ along any trace from `initCfg s` with nonempty input, tape `0`'s content matches -/ structure HasInputTape {k : ℕ} (tm : MultiTapeTM (k + 1) Symbol) : Prop where /-- Every transition writes back the symbol it read on tape `0`. -/ - readPreserving : ∀ q reads, ((tm.tr q reads).1 0).IsReadPreserving (reads 0) + readPreserving : IsReadPreservingOnTape tm.tr 0 /-- Once the head steps left off the input, no chain of stay-moves on the blank can lead to another left step on the blank. -/ leftBounded : IsBoundedInDirectionOnTape tm.tr 0 .left @@ -496,7 +496,6 @@ def OutputTapeContents (tape : BiTape Symbol) (out : List Symbol) : Prop := tape.head = none ∧ tape.left = StackTape.map_some out.reverse ∧ tape.right = ∅ omit [Inhabited Symbol] [Fintype Symbol] in -@[simp] lemma outputTapeContents_nil : OutputTapeContents (BiTape.nil : BiTape Symbol) [] := by simp [OutputTapeContents, BiTape.nil] @@ -707,6 +706,7 @@ inductive MoveThenStaysOnBlank (h_blank : (cfg₂.tapes i).head = none) (h_step : tm.step cfg₂ = some cfg₃) (h_state : cfg₃.state = some q₃) + (h_write : ((tm.tr q₂ fun i => (cfg₂.tapes i).head).1 i).symbol = none) (h_no_mov : ((tm.tr q₂ fun i => (cfg₂.tapes i).head).1 i).movement = none) : MoveThenStaysOnBlank tm i d q₁ q₃ cfg₃ @@ -718,7 +718,7 @@ lemma MoveThenStaysOnBlank.cfg_state_eq cfg.state = some q₂ := by induction h with | move _ h_state _ => exact h_state - | stay _ _ _ h_state _ => exact h_state + | stay _ _ _ h_state _ _ => exact h_state /-- A semantic chain is a witness of the syntactic chain on its endpoint states. @@ -732,8 +732,8 @@ lemma MoveThenStaysOnBlank.moveThenStays | move h_step h_state h_mov => refine .move _ _ _ h_mov ?_ rw [step_state_eq rfl h_step, h_state] - | stay h_prev h_blank h_step h_state h_no_mov ih => - refine .stay _ _ _ ih _ h_blank h_no_mov ?_ + | stay h_prev h_blank h_step h_state h_write h_no_mov ih => + refine .stay _ _ _ ih _ h_blank h_write h_no_mov ?_ rw [step_state_eq h_prev.cfg_state_eq h_step, h_state] end MultiTapeTM @@ -777,9 +777,9 @@ variable [Inhabited Symbol] [Fintype Symbol] /-! ### Head-boundedness invariant -/ /-- -**Head-boundedness invariant at position `p`.** For a configuration `cfg` along a trace -from `initCfg s` of a TM with a designated input tape, tape `0` of `cfg` is in canonical -shape `canonicalInputTape s p` for some integer position `p ∈ [-1, s.length]`. +**Head-boundedness invariant at position `p`.** For a configuration `cfg` tracked by the +input-tape invariant, tape `0` is in canonical shape `canonicalInputTape s p` for some +integer position `p ∈ [-1, s.length]`. -/ structure HeadBoundInvariantAt {k : ℕ} (tm : MultiTapeTM (k + 1) Symbol) (s : List Symbol) (cfg : tm.Cfg) (p : ℤ) : Prop where @@ -828,6 +828,22 @@ lemma HeadBoundInvariantAt.Strong.initCfg chain_left _ _ h := absurd h (by omega) chain_right _ _ h := absurd h (by exact_mod_cast h_pos.ne) +/-- +An arbitrary configuration satisfies the strong head-boundedness invariant when tape `0` +already has canonical input shape and the head starts strictly inside the input region. +The endpoint chain witnesses are vacuous in this case. +-/ +lemma HeadBoundInvariantAt.Strong.of_head_inside + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} {s : List Symbol} {cfg : tm.Cfg} {p : ℤ} + (h_lo : 0 ≤ p) (h_hi : p < (s.length : ℤ)) + (h_tape : cfg.tapes 0 = canonicalInputTape s p) : + HeadBoundInvariantAt.Strong tm s cfg p where + pos_lower := by omega + pos_upper := by omega + tape_eq := h_tape + chain_left _ _ h := absurd h (by omega) + chain_right _ _ h := absurd h (by omega) + /-- The initial configuration satisfies the trace-level invariant for any input. -/ lemma HeadBoundInvariantForInput.initCfg {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (s : List Symbol) : @@ -851,6 +867,9 @@ lemma HeadBoundInvariantAt.Strong.step obtain ⟨q, h_state_q, h_step_q, h_tape0⟩ := h_input.step_tape0_decompose h_step have h_head_eq : (cfg.tapes 0).head = none ↔ (p = -1 ∨ p = (s.length : ℤ)) := by rw [h_inv.tape_eq]; exact canonicalInputTape_head_eq_none_iff h_inv.pos_lower h_inv.pos_upper + have h_write_of_blank (h_blank : (cfg.tapes 0).head = none) : + ((tm.tr q fun i => (cfg.tapes i).head).1 0).symbol = none := by + rw [h_input.readPreserving q (fun i => (cfg.tapes i).head), h_blank] cases hm : ((tm.tr q fun i => (cfg.tapes i).head).1 0).movement with | none => refine ⟨p, ⟨h_inv.pos_lower, h_inv.pos_upper, ?_⟩, ?_, ?_⟩ @@ -858,11 +877,13 @@ lemma HeadBoundInvariantAt.Strong.step · intro q' hq' hp_neg_one have h_blank : (cfg.tapes 0).head = none := h_head_eq.mpr (Or.inl hp_neg_one) obtain ⟨q₀, h_chain⟩ := h_inv.chain_left q h_state_q hp_neg_one - exact ⟨q₀, MoveThenStaysOnBlank.stay h_chain h_blank h_step hq' hm⟩ + exact ⟨q₀, MoveThenStaysOnBlank.stay h_chain h_blank h_step hq' + (h_write_of_blank h_blank) hm⟩ · intro q' hq' hp_len have h_blank : (cfg.tapes 0).head = none := h_head_eq.mpr (Or.inr hp_len) obtain ⟨q₀, h_chain⟩ := h_inv.chain_right q h_state_q hp_len - exact ⟨q₀, MoveThenStaysOnBlank.stay h_chain h_blank h_step hq' hm⟩ + exact ⟨q₀, MoveThenStaysOnBlank.stay h_chain h_blank h_step hq' + (h_write_of_blank h_blank) hm⟩ | some d => cases d with | right => @@ -872,11 +893,11 @@ lemma HeadBoundInvariantAt.Strong.step obtain ⟨q₀, h_chain⟩ := h_inv.chain_right q h_state_q hp_eq exact IsBoundedInDirectionOnTape.not_movesOffBlankInDir_of_chain h_input.rightBounded h_chain ⟨fun i => (cfg.tapes i).head, h_blank, hm⟩ - · have hp_lt : p < (s.length : ℤ) := by have := h_inv.pos_upper; omega - have hp_lo := h_inv.pos_lower + · have hp_lo := h_inv.pos_lower + have hp_hi := h_inv.pos_upper refine ⟨p + 1, ⟨by omega, by omega, ?_⟩, ?_, ?_⟩ · rw [h_tape0, hm, h_inv.tape_eq] - exact canonicalInputTape_move_right hp_lo hp_lt + exact canonicalInputTape_move_right · intro _ _ hp_neg_one; exfalso; omega · intro q' hq' _ exact ⟨q, MoveThenStaysOnBlank.move h_step_q hq' hm⟩ @@ -887,11 +908,11 @@ lemma HeadBoundInvariantAt.Strong.step obtain ⟨q₀, h_chain⟩ := h_inv.chain_left q h_state_q hp_eq exact IsBoundedInDirectionOnTape.not_movesOffBlankInDir_of_chain h_input.leftBounded h_chain ⟨fun i => (cfg.tapes i).head, h_blank, hm⟩ - · have hp_nn : 0 ≤ p := by have := h_inv.pos_lower; omega + · have hp_lo := h_inv.pos_lower have hp_hi := h_inv.pos_upper refine ⟨p - 1, ⟨by omega, by omega, ?_⟩, ?_, ?_⟩ · rw [h_tape0, hm, h_inv.tape_eq] - exact canonicalInputTape_move_left hp_nn hp_hi + exact canonicalInputTape_move_left · intro q' hq' _ exact ⟨q, MoveThenStaysOnBlank.move h_step_q hq' hm⟩ · intro _ _ hp_len; exfalso; omega @@ -933,6 +954,22 @@ lemma HeadBoundInvariantForInput.exists_pos {k : ℕ} {tm : MultiTapeTM (k + 1) rw [canonicalInputTape_nil]; exact h_nil · exact ⟨p, h_strong.pos_lower, h_strong.pos_upper, h_strong.tape_eq⟩ +/-- +**Quantitative head-position bound from an arbitrary inside-start configuration.** If tape +`0` starts in canonical input shape with the head inside the input, every reachable +configuration keeps tape `0` within one cell of the input region. +-/ +theorem HasInputTape.head_position_bounded_from_cfg + {k : ℕ} {tm : MultiTapeTM (k + 1) Symbol} (h_input : tm.HasInputTape) + {s : List Symbol} {cfg cfg' : tm.Cfg} {p : ℤ} {t : ℕ} + (h_lo : 0 ≤ p) (h_hi : p < (s.length : ℤ)) + (h_tape : cfg.tapes 0 = canonicalInputTape s p) + (h_rel : Relation.RelatesInSteps tm.TransitionRelation cfg cfg' t) : + ∃ p' : ℤ, -1 ≤ p' ∧ p' ≤ (s.length : ℤ) ∧ + cfg'.tapes 0 = canonicalInputTape s p' := by + exact (HeadBoundInvariantForInput.relatesInSteps h_input + (Or.inr ⟨p, HeadBoundInvariantAt.Strong.of_head_inside h_lo h_hi h_tape⟩) h_rel).exists_pos + /-- **Quantitative head-position bound.** Every configuration reachable from `initCfg s` in `t` steps has its tape-`0` content in canonical shape `canonicalInputTape s p` for some integer position `p ∈ [-1, s.length]`. In particular, the head on tape `0` stays within @@ -942,7 +979,11 @@ theorem HasInputTape.head_position_bounded {s : List Symbol} {cfg' : tm.Cfg} {t : ℕ} (h_rel : Relation.RelatesInSteps tm.TransitionRelation (tm.initCfg s) cfg' t) : ∃ p : ℤ, -1 ≤ p ∧ p ≤ (s.length : ℤ) ∧ cfg'.tapes 0 = canonicalInputTape s p := - ((HeadBoundInvariantForInput.initCfg s).relatesInSteps h_input h_rel).exists_pos + by + by_cases h_pos : 0 < s.length + · exact h_input.head_position_bounded_from_cfg (p := 0) (by omega) (by omega) + (canonicalInputTape_zero s).symm h_rel + · exact ((HeadBoundInvariantForInput.initCfg s).relatesInSteps h_input h_rel).exists_pos end MultiTapeTM diff --git a/Cslib/Computability/Machines/TuringCommon.lean b/Cslib/Computability/Machines/TuringCommon.lean index 2cdff20ef..ee80cf2e5 100644 --- a/Cslib/Computability/Machines/TuringCommon.lean +++ b/Cslib/Computability/Machines/TuringCommon.lean @@ -72,6 +72,15 @@ They are used to phrase head-boundedness of designated input tapes syntactically variable {State Symbol : Type} {k : ℕ} +/-- +A transition function is *read-preserving on tape `i`* if every transition writes back the +symbol read on tape `i`. +-/ +def IsReadPreservingOnTape + (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State)) + (i : Fin k) : Prop := + ∀ q reads, ((tr q reads).1 i).symbol = reads i + /-- State `q` is *harmful in direction `d`* on tape index `i` of transition function `tr` if some transition from `q` reads a blank on tape `i` and moves the head on tape `i` in direction `d`. @@ -90,7 +99,8 @@ of the form `q →[move in direction d] q₁ →[stay while reading blank]* q'`. The initial transition's read is unconstrained — the head may have been on an input cell before stepping out to the blank — but every subsequent transition keeps the head fixed at -the blank, hence reads blank on tape `i` and produces no movement on tape `i`. +the blank, hence reads blank on tape `i`, writes the blank back, and produces no movement +on tape `i`. -/ inductive MoveThenStays (tr : State → (Fin k → Option Symbol) → ((Fin k → Stmt Symbol) × Option State)) @@ -105,6 +115,7 @@ inductive MoveThenStays (h_prev : MoveThenStays tr i d q q') (reads : Fin k → Option Symbol) (h_reads : reads i = none) + (h_write : ((tr q' reads).1 i).symbol = none) (h_mov : ((tr q' reads).1 i).movement = none) (h_next : (tr q' reads).2 = some q'') : MoveThenStays tr i d q q'' diff --git a/Cslib/Foundations/Data/BiTape.lean b/Cslib/Foundations/Data/BiTape.lean index 5fb13607c..d918f2e0a 100644 --- a/Cslib/Foundations/Data/BiTape.lean +++ b/Cslib/Foundations/Data/BiTape.lean @@ -7,6 +7,7 @@ Authors: Bolton Bailey module public import Cslib.Foundations.Data.StackTape +public import Mathlib.Algebra.Group.End public import Mathlib.Computability.TuringMachine.Tape public import Mathlib.Data.Finset.Attr public import Mathlib.Tactic.SetLike @@ -127,6 +128,73 @@ lemma optionMove_nil (m : Option Dir) : (nil : BiTape Symbol).optionMove m = nil | none => rfl | some d => cases d <;> rfl +/-- The right-move equivalence, with inverse `move_left`. -/ +def moveEquiv : Equiv.Perm (BiTape Symbol) where + toFun := move_right + invFun := move_left + left_inv := move_right_move_left + right_inv := move_left_move_right + +/-- Move the head by an integer amount of cells: positive values move right, negative +values move left. -/ +def move_int (t : BiTape Symbol) (delta : ℤ) : BiTape Symbol := + (moveEquiv ^ delta) t + +@[simp] +lemma move_int_zero_eq_id (t : BiTape Symbol) : + t.move_int 0 = t := by + simp [move_int] + +@[simp] +lemma move_int_one_eq_move_right (t : BiTape Symbol) : + t.move_int 1 = t.move_right := by + simp [move_int, moveEquiv] + +@[simp] +lemma move_int_neg_one_eq_move_left (t : BiTape Symbol) : + t.move_int (-1) = t.move_left := by + simp [move_int, moveEquiv] + +@[simp] +lemma move_int_move_right (t : BiTape Symbol) (delta : ℤ) : + (t.move_int delta).move_right = t.move_int (delta + 1) := by + change moveEquiv ((moveEquiv ^ delta) t) = (moveEquiv ^ (delta + 1)) t + rw [← Equiv.Perm.mul_apply, ← zpow_one_add, add_comm] + +@[simp] +lemma move_int_move_left (t : BiTape Symbol) (delta : ℤ) : + (t.move_int delta).move_left = t.move_int (delta - 1) := by + change (moveEquiv (Symbol := Symbol))⁻¹ ((moveEquiv ^ delta) t) = + (moveEquiv ^ (delta - 1)) t + rw [← Equiv.Perm.mul_apply, ← zpow_neg_one, ← zpow_add] + rw [show -1 + delta = delta - 1 by omega] + +@[simp] +lemma move_int_move_int (t : BiTape Symbol) (delta₁ delta₂ : ℤ) : + (t.move_int delta₁).move_int delta₂ = t.move_int (delta₁ + delta₂) := by + change (moveEquiv ^ delta₂) ((moveEquiv ^ delta₁) t) = + (moveEquiv ^ (delta₁ + delta₂)) t + rw [← Equiv.Perm.mul_apply, ← zpow_add, add_comm] + +@[simp] +lemma move_int_nil (delta : ℤ) : (nil : BiTape Symbol).move_int delta = nil := by + cases delta with + | ofNat n => + induction n with + | zero => simp + | succ n ih => + rw [show Int.ofNat (n + 1) = (Int.ofNat n : ℤ) + 1 by + simp [Int.natCast_succ]] + rw [← move_int_move_right, ih, move_right_nil] + | negSucc n => + induction n with + | zero => simp + | succ n ih => + rw [show Int.negSucc (n + 1) = Int.negSucc n - 1 by + rw [Int.negSucc_eq, Int.negSucc_eq] + omega] + rw [← move_int_move_left, ih, move_left_nil] + end Move /-- diff --git a/Cslib/Foundations/Data/BiTape/Canonical.lean b/Cslib/Foundations/Data/BiTape/Canonical.lean index 248ad6606..16702146a 100644 --- a/Cslib/Foundations/Data/BiTape/Canonical.lean +++ b/Cslib/Foundations/Data/BiTape/Canonical.lean @@ -18,9 +18,8 @@ The canonical `BiTape` configuration for an input list `s` with the head at inte `p` relative to the start of the input. Used by the multi-tape Turing machine head-position bound to characterise tape `0`'s shape along a trace. -* `canonicalInputTapeNat s n` — the shape when the head sits at natural-number position `n`. -* `canonicalInputTape s p` — the integer-indexed version, with `p = -1` representing "one - cell left of the input" and `p ≥ 0` delegating to `canonicalInputTapeNat`. +* `canonicalInputTapeNat s n` — the tape obtained by moving right `n` cells from `mk₁ s`. +* `canonicalInputTape s p` — the tape obtained by moving by integer offset `p` from `mk₁ s`. The basic move-right / move-left / head / zero / nil lemmas collected here are what the Turing-machine invariant uses to step the head back and forth within `[-1, s.length]`. @@ -37,49 +36,59 @@ The canonical `BiTape` configuration for an input tape containing `s`, with the natural number position `n` (i.e. `0` is the start of the input). For `n < s.length`, the head reads `some s[n]`; for `n ≥ s.length`, the head reads -`none` and the tape has `s.reverse` on the left. +`none`. -/ -def canonicalInputTapeNat (s : List Symbol) (n : ℕ) : BiTape Symbol where +def canonicalInputTapeNat (s : List Symbol) (n : ℕ) : BiTape Symbol := + (BiTape.mk₁ s).move_int n + +/-- Closed form for canonical natural positions while the head is at most one cell past +the input. This is private because the public API is movement-based. -/ +private def canonicalInputTapeNatClosed (s : List Symbol) (n : ℕ) : BiTape Symbol where head := s[n]? left := StackTape.map_some (s.take n).reverse right := StackTape.map_some (s.drop (n + 1)) /-- -The canonical `BiTape` shape of the input tape at integer position `p`, with `p = -1` -representing "one cell left of the input" (a blank cell with `s` to the right) and -`p ≥ 0` delegating to `canonicalInputTapeNat`. +The canonical `BiTape` shape of the input tape at integer position `p`, obtained by moving +by `p` cells from `BiTape.mk₁ s`. -The head-position bound theorem shows that traces from `initCfg s` only produce tapes -matching `canonicalInputTape s p` for `-1 ≤ p ≤ s.length`. +The head-position bound theorem shows that the input-tape invariant only needs positions +in the range `-1 ≤ p ≤ s.length`. -/ def canonicalInputTape (s : List Symbol) (p : ℤ) : BiTape Symbol := - if 0 ≤ p then canonicalInputTapeNat s p.toNat - else ⟨none, ∅, StackTape.map_some s⟩ + (BiTape.mk₁ s).move_int p @[simp] lemma canonicalInputTape_ofNat (s : List Symbol) (n : ℕ) : - canonicalInputTape s (n : ℤ) = canonicalInputTapeNat s n := by - simp [canonicalInputTape] + canonicalInputTape s (n : ℤ) = canonicalInputTapeNat s n := rfl @[simp] lemma canonicalInputTape_neg_one (s : List Symbol) : - canonicalInputTape s (-1) = ⟨none, ∅, StackTape.map_some s⟩ := rfl + canonicalInputTape s (-1) = ⟨none, ∅, StackTape.map_some s⟩ := by + rw [canonicalInputTape, BiTape.move_int_neg_one_eq_move_left] + cases s <;> simp [BiTape.mk₁, BiTape.move_left, BiTape.nil] @[simp] lemma canonicalInputTapeNat_zero (s : List Symbol) : canonicalInputTapeNat s 0 = BiTape.mk₁ s := by - cases s <;> simp [canonicalInputTapeNat, BiTape.mk₁, BiTape.nil] + simp [canonicalInputTapeNat] @[simp] lemma canonicalInputTape_zero (s : List Symbol) : - canonicalInputTape s 0 = BiTape.mk₁ s := - (canonicalInputTape_ofNat s 0).trans (canonicalInputTapeNat_zero s) + canonicalInputTape s 0 = BiTape.mk₁ s := by + simp [canonicalInputTape] + +@[simp] +private lemma canonicalInputTapeNatClosed_zero (s : List Symbol) : + canonicalInputTapeNatClosed s 0 = BiTape.mk₁ s := by + cases s <;> simp [canonicalInputTapeNatClosed, BiTape.mk₁, BiTape.nil] /-- One-step move-right on the canonical configuration at natural-number position `n`, when still within the input region. -/ -lemma canonicalInputTapeNat_move_right {s : List Symbol} {n : ℕ} (h : n < s.length) : - (canonicalInputTapeNat s n).move_right = canonicalInputTapeNat s (n + 1) := by - simp only [canonicalInputTapeNat, BiTape.move_right] +private lemma canonicalInputTapeNatClosed_move_right {s : List Symbol} {n : ℕ} + (h : n < s.length) : + (canonicalInputTapeNatClosed s n).move_right = canonicalInputTapeNatClosed s (n + 1) := by + simp only [canonicalInputTapeNatClosed, BiTape.move_right] have h_take : s.take (n + 1) = s.take n ++ [s[n]] := (List.take_concat_get' s n h).symm have h_get : s[n]? = some s[n] := List.getElem?_eq_getElem h ext @@ -91,69 +100,38 @@ lemma canonicalInputTapeNat_move_right {s : List Symbol} {n : ℕ} (h : n < s.le · -- right: (map_some (s.drop (n+1))).tail = map_some (s.drop (n+2)) rw [StackTape.tail_map_some, List.tail_drop] -/-- One-step move-left on the canonical configuration at natural-number position `n + 1`, -when still within the input region. -/ -lemma canonicalInputTapeNat_move_left {s : List Symbol} {n : ℕ} (h : n < s.length) : +/-- One-step move-right on the canonical configuration at natural-number position `n`. -/ +lemma canonicalInputTapeNat_move_right {s : List Symbol} {n : ℕ} : + (canonicalInputTapeNat s n).move_right = canonicalInputTapeNat s (n + 1) := by + rw [canonicalInputTapeNat, canonicalInputTapeNat, BiTape.move_int_move_right] + simp [Int.natCast_succ] + +/-- One-step move-left on the canonical configuration at natural-number position `n + 1`. -/ +lemma canonicalInputTapeNat_move_left {s : List Symbol} {n : ℕ} : (canonicalInputTapeNat s (n + 1)).move_left = canonicalInputTapeNat s n := by - simp only [canonicalInputTapeNat, BiTape.move_left] - have h_take : s.take (n + 1) = s.take n ++ [s[n]] := (List.take_concat_get' s n h).symm - have h_get : s[n]? = some s[n] := List.getElem?_eq_getElem h - ext - · -- head: (map_some (s.take (n+1)).reverse).head = s[n]? - rw [h_take, List.reverse_append, List.reverse_singleton, List.singleton_append, - StackTape.head_map_some_cons, h_get] - · -- left: (map_some (s.take (n+1)).reverse).tail = map_some (s.take n).reverse - rw [StackTape.tail_map_some, h_take, List.reverse_append, List.reverse_singleton, - List.singleton_append, List.tail_cons] - · -- right: cons s[n+1]? (map_some (s.drop (n+1+1))) = map_some (s.drop (n+1)) - -- `cases h_drop : s.drop (n+1)` rewrites `s.drop (n+1)` on the RHS - cases h_drop : s.drop (n + 1) with - | nil => - have h1 : s.length ≤ n + 1 := List.drop_eq_nil_iff.mp h_drop - have h_head : s[n + 1]? = none := List.getElem?_eq_none (by omega) - have h_drop2 : s.drop (n + 1 + 1) = [] := List.drop_eq_nil_iff.mpr (by omega) - rw [h_head, h_drop2] - rfl - | cons a rest => - have h_head : s[n + 1]? = some a := by - rw [← List.head?_drop, h_drop]; rfl - have h_drop2 : s.drop (n + 1 + 1) = rest := by - rw [← List.tail_drop, h_drop]; rfl - rw [h_head, h_drop2] - exact (StackTape.map_some_cons a rest).symm - -/-- One-step move-right on the integer-indexed canonical configuration, staying within -`[-1, s.length]`. -/ -lemma canonicalInputTape_move_right {s : List Symbol} {p : ℤ} - (h_lo : -1 ≤ p) (h_hi : p < (s.length : ℤ)) : + rw [canonicalInputTapeNat, canonicalInputTapeNat, BiTape.move_int_move_left] + simp [Int.natCast_succ] + +private lemma canonicalInputTapeNat_eq_closed_of_le {s : List Symbol} {n : ℕ} + (h : n ≤ s.length) : + canonicalInputTapeNat s n = canonicalInputTapeNatClosed s n := by + induction n with + | zero => rw [canonicalInputTapeNat_zero, canonicalInputTapeNatClosed_zero] + | succ n ih => + have hn_le : n ≤ s.length := Nat.le_trans (Nat.le_succ n) h + have hn_lt : n < s.length := Nat.lt_of_succ_le h + rw [← canonicalInputTapeNat_move_right, ih hn_le] + exact canonicalInputTapeNatClosed_move_right hn_lt + +/-- One-step move-right on the integer-indexed canonical configuration. -/ +lemma canonicalInputTape_move_right {s : List Symbol} {p : ℤ} : (canonicalInputTape s p).move_right = canonicalInputTape s (p + 1) := by - by_cases hp_nn : 0 ≤ p - · simp only [canonicalInputTape, if_pos hp_nn, if_pos (show (0 : ℤ) ≤ p + 1 by omega), - show (p + 1).toNat = p.toNat + 1 from by omega] - exact canonicalInputTapeNat_move_right (by omega) - · obtain rfl : p = -1 := by omega - rw [show (-1 : ℤ) + 1 = 0 from rfl, canonicalInputTape_neg_one, canonicalInputTape_zero] - cases s with - | nil => rfl - | cons a t => - simp [BiTape.mk₁, BiTape.move_right] - -/-- One-step move-left on the integer-indexed canonical configuration, staying within -`[0, s.length]` (with the result going to `[-1, s.length - 1]`). -/ -lemma canonicalInputTape_move_left {s : List Symbol} {p : ℤ} - (h_lo : 0 ≤ p) (h_hi : p ≤ (s.length : ℤ)) : + simp [canonicalInputTape] + +/-- One-step move-left on the integer-indexed canonical configuration. -/ +lemma canonicalInputTape_move_left {s : List Symbol} {p : ℤ} : (canonicalInputTape s p).move_left = canonicalInputTape s (p - 1) := by - by_cases hp_pos : 0 < p - · have hp_pred : (p - 1).toNat + 1 = p.toNat := by omega - simp only [canonicalInputTape, if_pos hp_pos.le, if_pos (show (0 : ℤ) ≤ p - 1 by omega)] - rw [← hp_pred] - exact canonicalInputTapeNat_move_left (by omega) - · obtain rfl : p = 0 := by omega - rw [show (0 : ℤ) - 1 = -1 from rfl, canonicalInputTape_zero, canonicalInputTape_neg_one] - cases s with - | nil => rfl - | cons a t => - simp [BiTape.mk₁, BiTape.move_left] + simp [canonicalInputTape] /-- Characterization of when the head of a canonical configuration is blank (inside the valid range `[-1, s.length]`). -/ @@ -162,8 +140,10 @@ lemma canonicalInputTape_head_eq_none_iff {s : List Symbol} {p : ℤ} (canonicalInputTape s p).head = none ↔ p = -1 ∨ p = s.length := by by_cases hp_nn : 0 ≤ p · have hp_cast : (p.toNat : ℤ) = p := Int.toNat_of_nonneg hp_nn - simp only [canonicalInputTape, if_pos hp_nn, canonicalInputTapeNat, - List.getElem?_eq_none_iff] + have hp_le : p.toNat ≤ s.length := by omega + rw [← hp_cast, canonicalInputTape_ofNat, + canonicalInputTapeNat_eq_closed_of_le hp_le] + simp only [canonicalInputTapeNatClosed, List.getElem?_eq_none_iff] omega · obtain rfl : p = -1 := by omega simp @@ -173,7 +153,6 @@ empty-input branch of `HasInputTape.head_position_bounded` trivial: every reacha configuration is `BiTape.nil`, which equals `canonicalInputTape [] p` for any `p`. -/ lemma canonicalInputTape_nil (p : ℤ) : canonicalInputTape ([] : List Symbol) p = BiTape.nil := by - unfold canonicalInputTape - split_ifs <;> simp [canonicalInputTapeNat, BiTape.nil] + simp [canonicalInputTape, BiTape.mk₁] end Turing diff --git a/Cslib/Foundations/Data/StackTape.lean b/Cslib/Foundations/Data/StackTape.lean index 3a2f60e9c..658bb5802 100644 --- a/Cslib/Foundations/Data/StackTape.lean +++ b/Cslib/Foundations/Data/StackTape.lean @@ -85,16 +85,16 @@ def cons (x : Option Symbol) (xs : StackTape Symbol) : StackTape Symbol := | none, ⟨hd :: tl, hl⟩ => ⟨none :: hd :: tl, by grind⟩ | some a, ⟨l, hl⟩ => ⟨some a :: l, by grind⟩ -@[simp, scoped grind =] +@[simp] lemma cons_none_nil_toList : (cons none (nil : StackTape Symbol)).toList = [] := by grind -@[simp, scoped grind =] +@[simp] lemma cons_none_nil : cons none (nil : StackTape Symbol) = nil := rfl -@[simp, scoped grind =] +@[simp] lemma cons_none_empty : cons none (∅ : StackTape Symbol) = ∅ := rfl -@[simp, scoped grind =] +@[simp] lemma cons_some_toList (a : Symbol) (l : StackTape Symbol) : (cons (some a) l).toList = some a :: l.toList := by simp only [cons] @@ -136,7 +136,9 @@ lemma head_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).head = o | none => cases l with | mk toList hl => cases toList <;> grind - | some a => grind + | some a => + cases l with | mk toList hl => + simp [cons, head] @[simp] lemma tail_cons (o : Option Symbol) (l : StackTape Symbol) : (cons o l).tail = l := by @@ -204,7 +206,8 @@ lemma length_cons_none (l : StackTape Symbol) : @[scoped grind =] lemma length_cons_some (a : Symbol) (l : StackTape Symbol) : (cons (some a) l).length = l.length + 1 := by - grind + cases l with | mk toList hl => + simp [length, cons] lemma length_cons_le (o : Option Symbol) (l : StackTape Symbol) : (cons o l).length ≤ l.length + 1 := by