From e8c772bb87cdd415b4981c748a2c42faee2b1b2b Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Tue, 13 Jan 2026 19:39:39 -0800 Subject: [PATCH 01/13] add files --- .../Machines/SingleTapeTuring/Basic.lean | 998 ++++++++++++++++++ .../Semantics/ReductionSystem/Basic.lean | 12 + 2 files changed, 1010 insertions(+) create mode 100644 Cslib/Computability/Machines/SingleTapeTuring/Basic.lean diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean new file mode 100644 index 00000000..fb9e7ab2 --- /dev/null +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -0,0 +1,998 @@ +/- +Copyright (c) 2025 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey +-/ + +module + +public import Cslib.Computability.Automata.Acceptors.Acceptor +public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor +public import Cslib.Foundations.Data.OmegaSequence.InfOcc +public import Cslib.Foundations.Semantics.ReductionSystem.Basic +public import Mathlib.Algebra.Polynomial.Eval.Defs +public import Mathlib.Computability.PostTuringMachine +public import Mathlib.Computability.TuringMachine + + +namespace Turing + +/-- +List of option values that don't end with none +-/ +structure OList (α : Type) where + (asList : List (Option α)) + -- The list can be empty (i.e. none), but if it is not empty, the last element is not (some) none + (h : asList.getLast? ≠ some none) + +def OList.empty {α} : OList α := { asList := [], h := by simp } + +def OList.map_some {α} (l : List α) : OList α := { asList := l.map some, h := by simp } + +instance {α : Type} : Inhabited (OList α) where + default := OList.empty + + +def OList.length {α} (l : OList α) : ℕ := l.asList.length + +def OList.cons {α} : Option α -> OList α -> OList α +| none, l => { asList := [], h := by simp } +| some a, l => { + asList := some a :: l.asList, + h := by + cases hl : l.asList with + | nil => simp + | cons hd tl => + simp only [List.getLast?_cons_cons] + rw [← hl] + exact l.h + } + +def OList.tail {α} (l : OList α) : OList α := + match hl : l.asList with + | [] => OList.empty + | hd :: t => { asList := t, h := by + match t with + | [] => simp + | hd' :: t' => + have lh := l.h + rw [hl] at lh + simp only [List.getLast?_cons_cons] at lh + have := l.h + rw [hl, List.getLast?_cons_cons] at this + exact this + } + +def OList.head {α} (l : OList α) : Option α := + match l.asList with + | [] => none + | h :: _ => h + +lemma OList.length_tail_le {α} (l : OList α) : l.tail.length ≤ l.length := by + unfold tail length + split + · simp [empty] + · next heq => simp [heq] + +lemma OList.length_cons_none {α} (l : OList α) : (OList.cons none l).length = 0 := by + simp [cons, length, empty] + +lemma OList.length_cons_some {α} (a : α) (l : OList α) : + (OList.cons (some a) l).length = l.length + 1 := by + simp [cons, length] + +lemma OList.length_cons_le {α} (o : Option α) (l : OList α) : + (OList.cons o l).length ≤ l.length + 1 := by + cases o with + | none => simp [length_cons_none] + | some a => simp [length_cons_some] + +lemma OList.length_map_some {α} (l : List α) : (OList.map_some l).length = l.length := by + simp [map_some, length] + +lemma OList.length_empty {α} : (OList.empty : OList α).length = 0 := by + simp [empty, length] + +/-- +I find this more convenient than mathlib's Tape type, +because that requires the type tobe inhabited, +and it is easy to confuse a list representing one thing with a list representing another, +if the representations are the same except for a sequence of default values at the end. + +The head of the machine is the current symbol under the tape head. +We do not assume here, but could add, that the ends of the tape are never none. +The move function should guarantee this, so that two tapes are equal +even if one has written none to the side +-/ +structure OTape (α : Type) where + (head : Option α) + (left : OList α) + (right : OList α) +deriving Inhabited + +def OTape.mk₁ (l : List Bool) : OTape Bool := + match l with + | [] => { head := none, left := OList.empty, right := OList.empty } + | h :: t => { head := some h, left := OList.empty, right := OList.map_some t } + +-- TODO incorrect, we must delete blanks from the ends, refactor out OList +def OTape.move {α} : Turing.OTape α → Dir → Turing.OTape α + | t, .left => + match t.left, t.head, t.right with + | l, h, r => { head := l.head, left := l.tail, right := OList.cons h r } + | t, .right => + match t.left, t.head, t.right with + | l, h, r => { head := r.head, left := OList.cons h l, right := r.tail } + + +def OTape.move? {α} : Turing.OTape α → Option Dir → Turing.OTape α + | t, none => t + | t, some d => t.move d + +def OTape.write {α} : Turing.OTape α → Option α → Turing.OTape α + | t, a => { t with head := a } + +open Classical in +noncomputable def ListBlank.space_used {α} [Inhabited α] (l : ListBlank α) : ℕ := + Nat.find (p := fun n => ∀ i > n, l.nth i = default) + (l.inductionOn (fun xs => ⟨xs.length, fun i hi => by + change (ListBlank.mk xs).nth i = default + rw [ListBlank.nth_mk] + exact List.getI_eq_default xs (Nat.le_of_lt hi)⟩)) + +/-- +The space used by a OTape is the number of symbols +between and including the head, and leftmost and rightmost non-blank symbols on the OTape +-/ +noncomputable def OTape.space_used {α} [Inhabited α] (t : Turing.OTape α) : ℕ := + 1 + t.left.length + t.right.length + +lemma OTape.space_used_write {α} [Inhabited α] (t : Turing.OTape α) (a : Option α) : + (t.write a).space_used = t.space_used := by + rfl + +lemma OTape.space_used_mk₁ (l : List Bool) : + (OTape.mk₁ l).space_used = max 1 l.length := by + cases l with + | nil => + simp [mk₁, space_used, OList.length_empty] + | cons h t => + simp [mk₁, space_used, OList.length_empty, OList.length_map_some] + omega + +open Classical in +lemma ListBlank.nth_ge_space_used {α} [Inhabited α] (l : ListBlank α) (i : ℕ) + (hi : i > l.space_used) : l.nth i = default := by + unfold space_used at hi + have H : ∃ n, ∀ i > n, l.nth i = default := l.inductionOn (fun xs => ⟨xs.length, fun i hi => + (ListBlank.nth_mk xs i).symm ▸ List.getI_eq_default xs (Nat.le_of_lt hi)⟩) + have h := Nat.find_spec H + exact h i hi + +open Classical in +lemma ListBlank.space_used_cons_le {α} [Inhabited α] (a : α) (l : ListBlank α) : + (l.cons a).space_used ≤ l.space_used + 1 := by + unfold space_used + apply Nat.find_le + intro i hi + cases i with + | zero => omega + | succ i => + rw [ListBlank.nth_succ, ListBlank.tail_cons] + exact ListBlank.nth_ge_space_used l i (by unfold space_used; omega) + +open Classical in +lemma ListBlank.space_used_tail_le {α} [Inhabited α] (l : ListBlank α) : + l.tail.space_used ≤ l.space_used := by + unfold space_used + apply Nat.find_le + intro i hi + rw [← ListBlank.nth_succ] + exact ListBlank.nth_ge_space_used l (i + 1) (by unfold space_used; omega) + +lemma OTape.space_used_move {α} [Inhabited α] (t : Turing.OTape α) (d : Dir) : + (t.move d).space_used ≤ t.space_used + 1 := by + cases d with + | left => + simp only [move, space_used] + have h1 := OList.length_tail_le t.left + have h2 := OList.length_cons_le t.head t.right + omega + | right => + simp only [move, space_used] + have h1 := OList.length_cons_le t.head t.left + have h2 := OList.length_tail_le t.right + omega + +namespace BinTM0 + +/-- A Turing machine "statement" is just a command to move + left or right, and write a symbol on the OTape. -/ +def Stmt := (Option Bool) × Option (Dir) +deriving Inhabited + +end BinTM0 + +/-- A TM0 over the alphabet of Option Bool (none is blank OTape symbol). -/ +structure BinTM0 where + /-- type of state labels -/ + (Λ : Type) + /-- finiteness of the state type -/ + [FintypeΛ : Fintype Λ] + /-- Initial state -/ + (q₀ : Λ) + /-- Transition function, mapping a state and a head symbol + to a Stmt to invoke, and optionally a new state (none for halt) -/ + (M : Λ → (Option Bool) → (Turing.BinTM0.Stmt × Option Λ)) + + +namespace BinTM0 + +section + +variable (tm : BinTM0) + +instance : Inhabited tm.Λ := + ⟨tm.q₀⟩ + +instance : Fintype tm.Λ := + tm.FintypeΛ + +instance inhabitedStmt : Inhabited (Stmt) := inferInstance + +/-- The type of configurations (functions) corresponding to this TM. -/ +structure Cfg : Type where + /-- the state of the TM (or none for the halting state) -/ + state : Option tm.Λ + /-- the OTape contents, which -/ + OTape : OTape (Bool) +deriving Inhabited + +/-- The step function corresponding to this TM. -/ +@[simp] +def step : tm.Cfg → Option tm.Cfg := + fun ⟨q, t⟩ => + match q with + -- If in the halting state, there is no next configuration + | none => none + -- If in state q' + | some q' => + -- Look up the transition function + match tm.M q' t.head with + | ⟨(wr, dir), q''⟩ => + -- enter a new configuration + some ⟨ + -- With state q'' (or none for halting) + q'', + -- And OTape updated according to the Stmt + (t.write wr).move? dir⟩ +end + +/-- The initial configuration corresponding to a list in the input alphabet. -/ +def initCfg (tm : BinTM0) (s : List Bool) : tm.Cfg := ⟨some tm.q₀, OTape.mk₁ s⟩ + +/-- The final configuration corresponding to a list in the output alphabet. +(We demand that the head halts at the leftmost position of the output.) +-/ +def haltCfg (tm : BinTM0) (s : List (Bool)) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ + +/-- +The `ReductionSystem` corresponding to a `BinTM0` is defined by the `step` function, +which maps a configuration to its next configuration if it exists. +-/ +def ReductionSystem (tm : BinTM0) : Cslib.ReductionSystem (tm.Cfg) := + { Red := fun cfg cfg' => tm.step cfg = some cfg' } +-- TODO use this, rather than the current setup + + +noncomputable def Cfg.space_used (tm : BinTM0) (cfg : tm.Cfg) : ℕ := + cfg.OTape.space_used + +open Classical in +lemma ListBlank.space_used_mk_nil {α} [Inhabited α] : + (ListBlank.mk ([] : List α)).space_used = 0 := by + unfold ListBlank.space_used + rw [Nat.find_eq_zero] + intro i hi + rw [ListBlank.nth_mk] + exact List.getI_nil i + +-- Helper lemma for space_used of a ListBlank created from a list +open Classical in +lemma ListBlank.space_used_mk {α} [Inhabited α] (l : List α) : + (ListBlank.mk l).space_used ≤ l.length := by + unfold ListBlank.space_used + apply Nat.find_le + intro i hi + rw [ListBlank.nth_mk] + exact List.getI_eq_default l (Nat.le_of_lt hi) + +-- /-- The space_used of a OTape created from a list +-- equals the maximum of 1 and the list length -/ +-- lemma OTape.space_used_mk₁ {α} [Inhabited α] (l : List α) : +-- (OTape.mk₁ l).space_used = max 1 l.length := by +-- unfold OTape.mk₁ OTape.mk₂ OTape.mk' OTape.space_used +-- simp only [ListBlank.space_used_mk_nil, add_zero, ListBlank.tail_mk] +-- cases l with +-- | nil => +-- simp [ListBlank.space_used_mk_nil] +-- | cons h t => +-- simp only [List.tail_cons, List.length_cons, le_add_iff_nonneg_left, zero_le, sup_of_le_right] +-- rw [add_comm] +-- simp only [Nat.add_right_cancel_iff] +-- sorry + +lemma Cfg.space_used_initCfg (tm : BinTM0) (s : List Bool) : + (tm.initCfg s).space_used = max 1 s.length := by + simp [initCfg, Cfg.space_used, OTape.space_used_mk₁] + +lemma Cfg.space_used_haltCfg (tm : BinTM0) (s : List Bool) : + (tm.haltCfg s).space_used = max 1 s.length := by + simp [haltCfg, Cfg.space_used, OTape.space_used_mk₁] + +lemma Cfg.space_used_step {tm : BinTM0} (cfg cfg' : tm.Cfg) + (hstep : tm.step cfg = some cfg') : + cfg'.space_used ≤ cfg.space_used + 1 := by + unfold Cfg.space_used + cases cfg with | mk state tape => + cases state with + | none => simp [step] at hstep + | some q => + simp only [step] at hstep + generalize hM : tm.M q tape.head = result at hstep + obtain ⟨⟨wr, dir⟩, q''⟩ := result + simp only at hstep + cases hstep + cases dir with + | none => + simp only [OTape.move?] + rw [OTape.space_used_write] + omega + | some d => + simp only [OTape.move?] + have h1 := OTape.space_used_move (tape.write wr) d + rw [OTape.space_used_write] at h1 + exact h1 + +/-- `f` eventually reaches `b` when repeatedly evaluated on `a`, in exactly `steps` steps. -/ +def EvalsToInTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (steps : ℕ) : Prop := + (· >>= f)^[steps] a = b + +/-- Reflexivity of `EvalsTo` in 0 steps. -/ +lemma EvalsToInTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : EvalsToInTime f a (some a) 0 := + rfl + +/-- Transitivity of `EvalsTo` in the sum of the numbers of steps. -/ +@[trans] +lemma EvalsToInTime.trans {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (c : Option σ) + (steps₁ steps₂ : ℕ) + (h₁ : EvalsToInTime f a b steps₁) + (h₂ : EvalsToInTime f b c steps₂) : + EvalsToInTime f a c (steps₂ + steps₁) := by + simp_all only [EvalsToInTime, Option.bind_eq_bind] + rw [Function.iterate_add_apply, h₁, h₂] + +/-- If we evaluate to some state in n+1 steps, there is an intermediate state + that we reach in n steps, and then one more step reaches the final state. -/ +lemma EvalsToInTime.succ_decompose {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) + (n : ℕ) (h : EvalsToInTime f a (some b) (n + 1)) : + ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := by + set c' := (· >>= f)^[n] (some a) with hc' + simp only [EvalsToInTime, Option.bind_eq_bind] at h hc' ⊢ + rw [Function.iterate_succ_apply'] at h + -- h : (· >>= f) ((· >>= f)^[n] (some a)) = some b + -- This means (· >>= f)^[n] (some a) >>= f = some b + -- So (· >>= f)^[n] (some a) = some c for some c with f c = some b + rw [<-hc'] at h + revert h hc' + cases c' with + | none => + grind + | some c => + intros h hc' + use c + grind + +lemma EvalsToInTime.succ_iff {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) + (n : ℕ) : + EvalsToInTime f a (some b) (n + 1) ↔ + ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := by + constructor + · exact EvalsToInTime.succ_decompose f a b n + · intro ⟨c, hc_eval, hc_step⟩ + simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_succ_apply'] at hc_eval ⊢ + simp only [hc_eval, Option.bind_some, hc_step] + +theorem Turing.BinTM0.EvalsToInTime.congr.extracted_1_2.{u_2, u_1} + {σ : Type u_1} {σ' : Type u_2} (f : σ → Option σ) + (f' : σ' → Option σ') (g : σ → σ') + (hg : ∀ (x : σ), Option.map g (f x) = f' (g x)) (n : ℕ) (a : σ) : + (Option.map g ((flip Option.bind f)^[n] (some a))).bind f' = + ((flip Option.bind f)^[n] (some a)).bind fun a ↦ f' (g a) := by + induction n with + | zero => simp + | succ n ih => + simp only [Function.iterate_succ_apply, flip, Option.bind_some, <- hg] at ih ⊢ + grind + + + + + +/-- +If `f` is homomorphic to `f'` via `g`, then if `f` evals to `b` from `a` in `steps` steps, +then `f'` evals to `g b` from `g a` in `steps` steps. +-/ +lemma EvalsToInTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') + (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) + (a : σ) (b : Option σ) + (steps : ℕ) + (h : EvalsToInTime f a b steps) : EvalsToInTime f' (g a) (Option.map g b) steps := by + induction steps generalizing a b with + | zero => + simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq] at h ⊢ + subst h + rfl + | succ n ih => + simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_succ_apply', + forall_eq'] at h ih ⊢ + subst h + rw [ih] + clear ih + simp only [Option.map_bind, Function.comp_apply, hg] + exact Turing.BinTM0.EvalsToInTime.congr.extracted_1_2 f f' g hg n a + +/-- +If `h : σ → ℕ` increases by at most 1 on each step of `f`, +then the value of `h` at the output after `steps` steps is at most `h` at the input plus `steps`. +-/ +lemma EvalsToInTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) + (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) + (a : σ) (b : σ) + (steps : ℕ) + (hevals : EvalsToInTime f a b steps) : + h b ≤ h a + steps := by + induction steps generalizing a b with + | zero => + simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq, Option.some.injEq, + add_zero] at hevals ⊢ + subst hevals + exact Nat.le_refl (h a) + | succ n ih => + rw [EvalsToInTime.succ_iff] at hevals + obtain ⟨c, hevals_n, h_step_eq⟩ := hevals + specialize ih a c hevals_n + specialize h_step c b h_step_eq + omega + + +-- m -> step_bound +/-- `f` eventually reaches `b` in at most `m` steps when repeatedly +evaluated on `a`. -/ +def EvalsToWithinTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (m : ℕ) : Prop := + ∃ steps ≤ m, EvalsToInTime f a b steps + +/-- Reflexivity of `EvalsToWithinTime` in 0 steps. -/ +def EvalsToWithinTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : + EvalsToWithinTime f a (some a) 0 := by + use 0 + exact if_false_right.mp rfl + +/-- Transitivity of `EvalsToWithinTime` in the sum of the numbers of steps. -/ +@[trans] +def EvalsToWithinTime.trans {σ : Type*} (f : σ → Option σ) (m₁ : ℕ) (m₂ : ℕ) (a : σ) (b : σ) + (c : Option σ) (h₁ : EvalsToWithinTime f a b m₁) (h₂ : EvalsToWithinTime f b c m₂) : + EvalsToWithinTime f a c (m₂ + m₁) := by + obtain ⟨steps₁, hsteps₁, hevals₁⟩ := h₁ + obtain ⟨steps₂, hsteps₂, hevals₂⟩ := h₂ + use steps₂ + steps₁ + constructor + · omega + · exact EvalsToInTime.trans f a b c steps₁ steps₂ hevals₁ hevals₂ + +def EvalsToWithinTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') + (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) + (a : σ) (b : Option σ) + (m : ℕ) + (h : EvalsToWithinTime f a b m) : EvalsToWithinTime f' (g a) (Option.map g b) m := by + obtain ⟨steps, hsteps, hevals⟩ := h + use steps + constructor + · exact hsteps + · exact EvalsToInTime.map f f' g hg a b steps hevals + +/-- +Monotonicity of `EvalsToWithinTime` in the time bound. +-/ +def EvalsToWithinTime.mono_time {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) + {m₁ m₂ : ℕ} (h : EvalsToWithinTime f a b m₁) (hm : m₁ ≤ m₂) : EvalsToWithinTime f a b m₂ := by + obtain ⟨steps, hsteps, hevals⟩ := h + use steps + simp_all only + simp + omega + +lemma EvalsToWithinTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) + (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) + (a : σ) (b : σ) + (m : ℕ) + (hevals : EvalsToWithinTime f a (some b) m) : + h b ≤ h a + m := by + obtain ⟨steps, hsteps, hevals_steps⟩ := hevals + have := EvalsToInTime.small_change f h h_step a b steps hevals_steps + omega + +/-- A proof of tm outputting l' when given l. -/ +def OutputsInTime (tm : BinTM0) (l : List (Bool)) (l' : Option (List (Bool))) := + EvalsToInTime tm.step (initCfg tm l) ((Option.map (haltCfg tm)) l') + +/-- A proof of tm outputting l' when given l in at most m steps. -/ +def OutputsWithinTime (tm : BinTM0) (l : List (Bool)) (l' : Option (List (Bool))) + (m : ℕ) := + EvalsToWithinTime tm.step (initCfg tm l) ((Option.map (haltCfg tm)) l') m + +-- /-- A (bundled TM0) Turing machine +-- with input alphabet equivalent to `Γ₀` and output alphabet equivalent to `Γ₁`. +-- TODO this is something of a holdover, might get rid +-- -/ +-- structure ComputableAux (Γ₀ Γ₁ : Type) where +-- /-- the underlying bundled TM0 -/ +-- tm : BinTM0 +-- /-- the input alphabet is equivalent to `Γ₀` -/ +-- inputAlphabet : Bool ≃ Γ₀ +-- /-- the output alphabet is equivalent to `Γ₁` -/ +-- outputAlphabet : Bool ≃ Γ₁ + +/-- A Turing machine + a proof it outputsInTime `f`. -/ +structure Computable (f : List Bool → List Bool) where + /-- the underlying bundled TM0 -/ + tm : BinTM0 + steps : ℕ + /-- a proof this machine outputsInTime `f` -/ + outputsFun : + ∀ a, + OutputsInTime tm ((a)) + (Option.some (((f a)))) + steps + +/-- A Turing machine + a time function + +a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ +structure ComputableInTime (f : List Bool → List Bool) where + /-- the underlying bundled TM0 -/ + tm : BinTM0 + /-- a time function -/ + time : ℕ → ℕ + /-- proof this machine outputsInTime `f` in at most `time(input.length)` steps -/ + outputsFun : + ∀ a, + tm.OutputsWithinTime + ((a)) + (Option.some (((f a)))) + (time ( a).length) + +/-- A Turing machine + a polynomial time function + +a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ +structure ComputableInPolyTime (f : List Bool → List Bool) where + /-- the underlying bundled TM0 -/ + tm : BinTM0 + /-- a polynomial time function -/ + time : Polynomial ℕ + /-- proof that this machine outputsInTime `f` in at most `time(input.length)` steps -/ + outputsFun : + ∀ a, + OutputsWithinTime tm (( a)) + (Option.some (((f a)))) + (time.eval ( a).length) + +-- /-- A forgetful map, forgetting the time bound on the number of steps. -/ +-- def ComputableInTime.toComputable {α β : Type} {ea : BinEncoding α} {eb : BinEncoding β} +-- {f : α → β} (h : ComputableInTime ea eb f) : Computable ea eb f := +-- ⟨h.tm, fun a => OutputsWithinTime.toOutputsInTime (h.outputsFun a)⟩ + +/-- A forgetful map, forgetting that the time function is polynomial. -/ +def ComputableInPolyTime.toComputableInTime {f : List Bool → List Bool} (h : ComputableInPolyTime f) : + ComputableInTime f := + ⟨h.tm, fun n => h.time.eval n, h.outputsFun⟩ + +open Turing.TM0.Stmt + +/-- A Turing machine computing the identity. -/ +def idComputer : BinTM0 where + Λ := PUnit + q₀ := PUnit.unit + M := fun _ b => ⟨(b, none), none⟩ + +noncomputable section + +/-- A proof that the identity map on α is computable in polytime. -/ +def ComputableInPolyTime.id : + @ComputableInPolyTime id where + tm := idComputer + time := 1 + outputsFun x := by + use 1 + simp only [Polynomial.eval_one, le_refl, id_eq, Option.map_some, true_and] + simp only [EvalsToInTime, initCfg, haltCfg, idComputer, + Function.iterate_succ, Function.iterate_zero, Function.comp_apply, id_eq] + congr 1 + + + -- { steps := 1 + -- evals_in_steps := rfl + -- steps_le_m := by simp only [Polynomial.eval_one, le_refl] } + +-- instance inhabitedComputableInPolyTime : +-- Inhabited (ComputableInPolyTime (default : BinEncoding Bool) default id) := +-- ⟨idComputableInPolyTime Computability.inhabitedBinEncoding.default⟩ + +-- instance inhabitedOutputsWithinTime : +-- Inhabited +-- (OutputsWithinTime (idComputer finEncodingBoolBool) +-- (List.map (Equiv.cast rfl).invFun [false]) +-- (some (List.map (Equiv.cast rfl).invFun [false])) (Polynomial.eval 1 1)) := +-- ⟨(idComputableInPolyTime finEncodingBoolBool).outputsFun false⟩ + +-- instance inhabitedOutputsInTime : +-- Inhabited +-- (OutputsInTime (idComputer finEncodingBoolBool) (List.map (Equiv.cast rfl).invFun [false]) +-- (some (List.map (Equiv.cast rfl).invFun [false]))) := +-- ⟨OutputsWithinTime.toOutputsInTime Turing.inhabitedOutputsWithinTime.default⟩ + +-- instance inhabitedEvalsToWithinTime : +-- Inhabited (EvalsToWithinTime (fun _ : Unit => some ⟨⟩) ⟨⟩ (some ⟨⟩) 0) := +-- ⟨EvalsToWithinTime.refl _ _⟩ + +-- instance inhabitedTM0EvalsToInTime : +-- Inhabited (EvalsToInTime (fun _ : Unit => some ⟨⟩) ⟨⟩ (some ⟨⟩)) := +-- ⟨EvalsTo.refl _ _⟩ + +/-- A proof that the identity map on α is computable in time. -/ +def ComputableInTime.id : + @ComputableInTime id := + ComputableInPolyTime.toComputableInTime <| ComputableInPolyTime.id + +-- instance inhabitedComputableInTime : +-- Inhabited (ComputableInTime finEncodingBoolBool finEncodingBoolBool id) := +-- ⟨idComputableInTime Computability.inhabitedBinEncoding.default⟩ + +-- /-- A proof that the identity map on α is computable. -/ +-- def idComputable {α : Type} (ea : BinEncoding α) : @Computable α α ea ea id := +-- ComputableInTime.toComputable <| ComputableInTime.id ea + +-- instance inhabitedComputable : +-- Inhabited (Computable finEncodingBoolBool finEncodingBoolBool id) := +-- ⟨idComputable Computability.inhabitedBinEncoding.default⟩ + +-- instance inhabitedComputableAux : Inhabited (ComputableAux Bool Bool) := +-- ⟨(default : Computable finEncodingBoolBool finEncodingBoolBool id).toComputableAux⟩ + +def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) + (hg : ComputableInTime g) : + BinTM0 := + { + Λ := hf.tm.Λ ⊕ hg.tm.Λ + q₀ := Sum.inl hf.tm.q₀ + M := fun q h => + match q with + -- If we are in the first machine's states, run that machine + | Sum.inl ql => match hf.tm.M ql (h) with + -- The action should be the same, and the state should either be the corresponding state + -- in the first machine, or transition to the start state of the second machine if halting + | (ql', stmt) => (ql', + match stmt with + -- If it halts, transition to the start state of the second machine + | none => some (Sum.inr hg.tm.q₀) + -- Otherwise continue as normal + | _ => Option.map Sum.inl stmt) + -- If we are in the second machine's states, run that machine + | Sum.inr qr => + match hg.tm.M qr (h) with + -- The action should be the same, and the state should be the corresponding state + -- in the second machine, or halting if the second machine halts + | (qr', stmt) => (qr', + match stmt with + -- If it halts, transition to the halting state + | none => none + -- Otherwise continue as normal + | _ => Option.map Sum.inr stmt) + } + +lemma compComputer_q₀_eq (f : List Bool → List Bool) (g : List Bool → List Bool) + (hf : ComputableInTime f) + (hg : ComputableInTime g) : + (compComputer hf hg).q₀ = Sum.inl hf.tm.q₀ := + rfl + +/-- Lift a config over a tm to a config over the comp -/ +def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) + (hg : ComputableInTime g) + (cfg : hf.tm.Cfg) : + (compComputer hf hg).Cfg := + { + state := Option.map Sum.inl cfg.state + OTape := cfg.OTape + } + +def liftCompCfg_right{f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) + (hg : ComputableInTime g) + (cfg : hg.tm.Cfg) : + (compComputer hf hg).Cfg := + { + state := Option.map Sum.inr cfg.state + OTape := cfg.OTape + } + +theorem map_liftCompCfg_left_step + {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) (hg : ComputableInTime g) + (x : hf.tm.Cfg) + (hx : ∀ cfg, hf.tm.step x = some cfg → cfg.state.isSome) : + Option.map (liftCompCfg_left hf hg) (hf.tm.step x) = + (compComputer hf hg).step (liftCompCfg_left hf hg x) := by + cases x with + | mk state OTape => + cases state with + | none => + -- x is already in halting state, step returns none on both sides + simp only [step, liftCompCfg_left, Option.map_none, compComputer] + | some q => + simp only [step, liftCompCfg_left, compComputer, Option.map_some] + -- Get the transition result + generalize hM : hf.tm.M q OTape.head = result + obtain ⟨⟨wr, dir⟩, nextState⟩ := result + simp only + -- Case on whether the next state is none (halting) or some + cases nextState with + | none => + -- The first machine halts, but hx says the result has state.isSome + simp only [step, hM] at hx + have := hx ⟨none, (OTape.write wr).move? dir⟩ rfl + simp at this + | some q' => + -- Normal step case - both sides produce the lifted config + simp only [hM, Option.map_some, liftCompCfg_left] + +/-- Helper lemma: liftCompCfg_right commutes with step for the second machine -/ +theorem map_liftCompCfg_right_step + {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) (hg : ComputableInTime g) + (x : hg.tm.Cfg) : + Option.map (liftCompCfg_right hf hg) (hg.tm.step x) = + (compComputer hf hg).step (liftCompCfg_right hf hg x) := by + cases x with + | mk state OTape => + cases state with + | none => + simp only [step, liftCompCfg_right, Option.map_none, compComputer] + | some q => + simp only [step, liftCompCfg_right, compComputer, Option.map_some] + generalize hM : hg.tm.M q OTape.head = result + obtain ⟨⟨wr, dir⟩, nextState⟩ := result + cases nextState with + | none => simp only [hM, Option.map_some, liftCompCfg_right, Option.map_none] + | some q' => simp only [hM, Option.map_some, liftCompCfg_right] + +/-- When the first machine would halt, the composed machine transitions to the second machine -/ +theorem comp_transition_to_right {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) (hg : ComputableInTime g) + (tp : OTape (Bool)) + (q : hf.tm.Λ) + (hM : (hf.tm.M q tp.head).2 = none) : + (compComputer hf hg).step { state := some (Sum.inl q), OTape := tp } = + some { state := some (Sum.inr hg.tm.q₀), + OTape := (tp.write (hf.tm.M q tp.head).1.1).move? (hf.tm.M q tp.head).1.2 } := by + simp only [step, compComputer, hM] + generalize hfM_eq : hf.tm.M q tp.head = result + obtain ⟨⟨wr, dir⟩, nextState⟩ := result + simp only [hfM_eq] + +/-- Helper: lifting to Sum.inl and transitioning to Sum.inr on halt -/ +def liftCompCfg_left_or_right {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) + (hg : ComputableInTime g) + (cfg : hf.tm.Cfg) : + (compComputer hf hg).Cfg := + match cfg.state with + | some q => { state := some (Sum.inl q), OTape := cfg.OTape } + | none => { state := some (Sum.inr hg.tm.q₀), OTape := cfg.OTape } + +/-- The lifting function commutes with step, converting halt to transition -/ +theorem map_liftCompCfg_left_or_right_step + {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) (hg : ComputableInTime g) + (x : hf.tm.Cfg) + (hx : x.state.isSome) : + Option.map (liftCompCfg_left_or_right hf hg) (hf.tm.step x) = + (compComputer hf hg).step (liftCompCfg_left_or_right hf hg x) := by + cases x with + | mk state OTape => + cases state with + | none => simp at hx + | some q => + simp only [step, liftCompCfg_left_or_right, compComputer] + generalize hM : hf.tm.M q OTape.head = result + obtain ⟨⟨wr, dir⟩, nextState⟩ := result + cases nextState with + | none => simp only [hM, Option.map_some, liftCompCfg_left_or_right] + | some q' => simp only [hM, Option.map_some, liftCompCfg_left_or_right] + +/-- General simulation: if the first machine goes from cfg to halt, the composed machine + goes from lifted cfg to Sum.inr hg.tm.q₀ -/ +theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) (hg : ComputableInTime g) + (cfg : hf.tm.Cfg) + (hcfg : cfg.state.isSome) + (haltCfg : hf.tm.Cfg) + -- (haltCfg_state : haltCfg.state = none) + (steps : ℕ) + (h : EvalsToInTime hf.tm.step cfg (some haltCfg) steps) : + EvalsToInTime (compComputer hf hg).step + (liftCompCfg_left_or_right hf hg cfg) + (some (liftCompCfg_left_or_right hf hg haltCfg)) + steps := by + -- Proof by induction on steps. + -- Key insight: liftCompCfg_left_or_right maps: + -- { state := some q, OTape } -> { state := some (Sum.inl q), OTape } + -- { state := none, OTape } -> { state := some (Sum.inr hg.tm.q₀), OTape } + -- For non-halting configs, the composed machine simulates exactly. + -- When the first machine halts, the composed machine transitions to Sum.inr hg.tm.q₀. + induction steps generalizing cfg haltCfg with + | zero => + simp only [EvalsToInTime, Option.bind_eq_bind, step, Function.iterate_zero, id_eq, + Option.some.injEq] at h ⊢ + rw [h] + | succ n ih => + -- Use the decomposition lemma: cfg evals to some intermediate c in n steps, + -- and then c steps to haltCfg + -- obtain ⟨c, hc_n, hc_step⟩ := EvalsToInTime.succ_decompose hf.tm.step cfg haltCfg n h + rw [EvalsToInTime.succ_iff] at h ⊢ + obtain ⟨c, hc_n, hc_step⟩ := h + use liftCompCfg_left_or_right hf hg c + constructor + · apply ih + · exact hcfg + · exact hc_n + · cases c with + | mk state OTape => + cases state with + | none => + simp_all + | some q => + rw [← map_liftCompCfg_left_or_right_step hf hg ⟨some q, OTape⟩ (by simp)] + simp only [hc_step, Option.map_some] + + +/-- +Simulation for the first phase of the composed computer. +When the first machine runs from start to halt, the composed machine +runs from start (with Sum.inl state) to Sum.inr hg.tm.q₀ (the start of the second phase). +This takes the same number of steps because the halt transition becomes a transition to the +second machine. +-/ +theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) (hg : ComputableInTime g) + (a : List Bool) + (hf_outputsFun : + EvalsToWithinTime hf.tm.step + { state := some hf.tm.q₀, OTape := OTape.mk₁ ( a) } + (some { state := none, OTape := OTape.mk₁ ( (f a)) }) + (hf.time ( a).length)) : + EvalsToWithinTime (compComputer hf hg).step + { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ ( a) } + (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ ( (f a)) }) + (hf.time ( a).length) := by + obtain ⟨steps, hsteps_le, hsteps_eval⟩ := hf_outputsFun + use steps + constructor + · exact hsteps_le + · have := comp_left_simulation_general hf hg + { state := some hf.tm.q₀, OTape := OTape.mk₁ ( a) } + (by simp) + { state := none, OTape := OTape.mk₁ ( (f a)) } + steps + hsteps_eval + simp only [liftCompCfg_left_or_right] at this + exact this + +/-- Simulation lemma for the second machine in the composed computer -/ +theorem comp_right_simulation + {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) (hg : ComputableInTime g) + (x : hg.tm.Cfg) (y : Option hg.tm.Cfg) (m : ℕ) + (h : EvalsToWithinTime hg.tm.step x y m) : + EvalsToWithinTime (compComputer hf hg).step + (liftCompCfg_right hf hg x) + (Option.map (liftCompCfg_right hf hg) y) + m := by + exact EvalsToWithinTime.map hg.tm.step (compComputer hf hg).step + (liftCompCfg_right hf hg) (map_liftCompCfg_right_step hf hg) x y m h + + + + +lemma output_length_le_input_length_add_time (tm : BinTM0) (l l' : List Bool) (t : ℕ) + (h : tm.OutputsWithinTime l (some l') t) : + l'.length ≤ max 1 l.length + t := by + unfold OutputsWithinTime at h + obtain ⟨steps, hsteps_le, hevals⟩ := h + replace hevals := hevals.small_change + specialize hevals (Cfg.space_used tm) + simp only [Cfg.space_used_initCfg, Cfg.space_used_haltCfg] at hevals + suffices l'.length ≤ max 1 l.length + steps + by omega + specialize hevals fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep) + omega + +/-- +A composition for ComputableInTime. + +If f and g are computed by turing machines M₁ and M₂ +then we can construct a turing machine M which computes g ∘ f by first running M₁ +and then, when M₁ halts, transitioning to the start state of M₂ and running M₂. + +This results in time bounded by the amount of time taken by M₁ plus the maximum time taken by M₂ on +inputs of length of the maximum output length of M₁ for that input size (which is itself bounded by +the time taken by M₁). + +Note that we require the time function of the second machine to be monotone; +this is to ensure that if the first machine returns an output +which is shorter than the maximum possible length of output for that input size, +then the time bound for the second machine still holds for that shorter input to the second machine. + +TODO refactor out the definition of the composed TM. +Prove separately that it +evals to the intermediate state from the start state and +then from the intermediate state to the final state. +-/ +def ComputableInTime.comp + {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) + (hg : ComputableInTime g) + (h_mono : Monotone hg.time) : + (ComputableInTime (g ∘ f)) where + tm := compComputer hf hg + time l := (hf.time l) + hg.time (max 1 l + hf.time l) + outputsFun a := by + have hf_outputsFun := hf.outputsFun a + have hg_outputsFun := hg.outputsFun (f a) + simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, + Option.map_some, haltCfg] at hg_outputsFun hf_outputsFun ⊢ + -- The computer evals a to f a in time hf.time ( a) + have h_a_evalsTo_f_a : + EvalsToWithinTime (compComputer hf hg).step + { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ ( a) } + (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ ( ((f a))) }) + (hf.time ( a).length) := + comp_left_simulation hf hg a hf_outputsFun + have h_f_a_evalsTo_g_f_a : + EvalsToWithinTime (compComputer hf hg).step + { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ ( ((f a))) } + (some { state := none, OTape := OTape.mk₁ ( ((g (f a)))) }) + (hg.time ( ((f a))).length) := by + -- Use the simulation lemma for the second machine + have := comp_right_simulation hf hg + { state := some hg.tm.q₀, OTape := OTape.mk₁ ( (f a)) } + (some { state := none, OTape := OTape.mk₁ ( (g (f a))) }) + (hg.time ( (f a)).length) + hg_outputsFun + simp only [liftCompCfg_right, Option.map_some] at this + exact this + have h_a_evalsTo_g_f_a := + EvalsToWithinTime.trans + (compComputer hf hg).step _ _ _ _ _ h_a_evalsTo_f_a h_f_a_evalsTo_g_f_a + apply EvalsToWithinTime.mono_time _ _ _ h_a_evalsTo_g_f_a + nth_rw 1 [← add_comm] + apply add_le_add + · omega + · apply h_mono + -- Use the lemma about output length being bounded by input length + time + exact output_length_le_input_length_add_time hf.tm _ _ _ (hf.outputsFun a) + +end + +end BinTM0 + +end Turing diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 5aad8a38..1c85c16d 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -50,6 +50,18 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b) end MultiStep +section Timed + +/-! ## Timed reductions -/ + +/-- Given a reduction system `rs` on `Term`, returns a reduction system on `Term × ℕ` +where the second component of the pair represents the number of steps taken. -/ +def Timed (rs : ReductionSystem Term) : ReductionSystem (Term × ℕ) := + { Red := fun ⟨t, n⟩ ⟨t', n'⟩ => rs.Red t t' ∧ n' = n + 1 } + +end Timed + + open Lean Elab Meta Command Term -- thank you to Kyle Miller for this: From efa68803a0e1f56c7d868daba74b2d8fdb3f1678 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Tue, 13 Jan 2026 21:34:08 -0800 Subject: [PATCH 02/13] refactor --- .../Machines/SingleTapeTuring/Basic.lean | 269 +++--------------- Cslib/Foundations/Data/OList.lean | 98 +++++++ Cslib/Foundations/Data/OTape.lean | 120 ++++++++ 3 files changed, 262 insertions(+), 225 deletions(-) create mode 100644 Cslib/Foundations/Data/OList.lean create mode 100644 Cslib/Foundations/Data/OTape.lean diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index fb9e7ab2..cf195ff1 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -6,203 +6,20 @@ Authors: Bolton Bailey module +-- TODO golf imports public import Cslib.Computability.Automata.Acceptors.Acceptor public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor public import Cslib.Foundations.Data.OmegaSequence.InfOcc +public import Cslib.Foundations.Data.OTape public import Cslib.Foundations.Semantics.ReductionSystem.Basic public import Mathlib.Algebra.Polynomial.Eval.Defs public import Mathlib.Computability.PostTuringMachine public import Mathlib.Computability.TuringMachine +@[expose] public section -namespace Turing - -/-- -List of option values that don't end with none --/ -structure OList (α : Type) where - (asList : List (Option α)) - -- The list can be empty (i.e. none), but if it is not empty, the last element is not (some) none - (h : asList.getLast? ≠ some none) - -def OList.empty {α} : OList α := { asList := [], h := by simp } - -def OList.map_some {α} (l : List α) : OList α := { asList := l.map some, h := by simp } - -instance {α : Type} : Inhabited (OList α) where - default := OList.empty - - -def OList.length {α} (l : OList α) : ℕ := l.asList.length - -def OList.cons {α} : Option α -> OList α -> OList α -| none, l => { asList := [], h := by simp } -| some a, l => { - asList := some a :: l.asList, - h := by - cases hl : l.asList with - | nil => simp - | cons hd tl => - simp only [List.getLast?_cons_cons] - rw [← hl] - exact l.h - } - -def OList.tail {α} (l : OList α) : OList α := - match hl : l.asList with - | [] => OList.empty - | hd :: t => { asList := t, h := by - match t with - | [] => simp - | hd' :: t' => - have lh := l.h - rw [hl] at lh - simp only [List.getLast?_cons_cons] at lh - have := l.h - rw [hl, List.getLast?_cons_cons] at this - exact this - } - -def OList.head {α} (l : OList α) : Option α := - match l.asList with - | [] => none - | h :: _ => h - -lemma OList.length_tail_le {α} (l : OList α) : l.tail.length ≤ l.length := by - unfold tail length - split - · simp [empty] - · next heq => simp [heq] - -lemma OList.length_cons_none {α} (l : OList α) : (OList.cons none l).length = 0 := by - simp [cons, length, empty] - -lemma OList.length_cons_some {α} (a : α) (l : OList α) : - (OList.cons (some a) l).length = l.length + 1 := by - simp [cons, length] - -lemma OList.length_cons_le {α} (o : Option α) (l : OList α) : - (OList.cons o l).length ≤ l.length + 1 := by - cases o with - | none => simp [length_cons_none] - | some a => simp [length_cons_some] - -lemma OList.length_map_some {α} (l : List α) : (OList.map_some l).length = l.length := by - simp [map_some, length] - -lemma OList.length_empty {α} : (OList.empty : OList α).length = 0 := by - simp [empty, length] - -/-- -I find this more convenient than mathlib's Tape type, -because that requires the type tobe inhabited, -and it is easy to confuse a list representing one thing with a list representing another, -if the representations are the same except for a sequence of default values at the end. - -The head of the machine is the current symbol under the tape head. -We do not assume here, but could add, that the ends of the tape are never none. -The move function should guarantee this, so that two tapes are equal -even if one has written none to the side --/ -structure OTape (α : Type) where - (head : Option α) - (left : OList α) - (right : OList α) -deriving Inhabited - -def OTape.mk₁ (l : List Bool) : OTape Bool := - match l with - | [] => { head := none, left := OList.empty, right := OList.empty } - | h :: t => { head := some h, left := OList.empty, right := OList.map_some t } - --- TODO incorrect, we must delete blanks from the ends, refactor out OList -def OTape.move {α} : Turing.OTape α → Dir → Turing.OTape α - | t, .left => - match t.left, t.head, t.right with - | l, h, r => { head := l.head, left := l.tail, right := OList.cons h r } - | t, .right => - match t.left, t.head, t.right with - | l, h, r => { head := r.head, left := OList.cons h l, right := r.tail } - - -def OTape.move? {α} : Turing.OTape α → Option Dir → Turing.OTape α - | t, none => t - | t, some d => t.move d - -def OTape.write {α} : Turing.OTape α → Option α → Turing.OTape α - | t, a => { t with head := a } - -open Classical in -noncomputable def ListBlank.space_used {α} [Inhabited α] (l : ListBlank α) : ℕ := - Nat.find (p := fun n => ∀ i > n, l.nth i = default) - (l.inductionOn (fun xs => ⟨xs.length, fun i hi => by - change (ListBlank.mk xs).nth i = default - rw [ListBlank.nth_mk] - exact List.getI_eq_default xs (Nat.le_of_lt hi)⟩)) - -/-- -The space used by a OTape is the number of symbols -between and including the head, and leftmost and rightmost non-blank symbols on the OTape --/ -noncomputable def OTape.space_used {α} [Inhabited α] (t : Turing.OTape α) : ℕ := - 1 + t.left.length + t.right.length - -lemma OTape.space_used_write {α} [Inhabited α] (t : Turing.OTape α) (a : Option α) : - (t.write a).space_used = t.space_used := by - rfl - -lemma OTape.space_used_mk₁ (l : List Bool) : - (OTape.mk₁ l).space_used = max 1 l.length := by - cases l with - | nil => - simp [mk₁, space_used, OList.length_empty] - | cons h t => - simp [mk₁, space_used, OList.length_empty, OList.length_map_some] - omega - -open Classical in -lemma ListBlank.nth_ge_space_used {α} [Inhabited α] (l : ListBlank α) (i : ℕ) - (hi : i > l.space_used) : l.nth i = default := by - unfold space_used at hi - have H : ∃ n, ∀ i > n, l.nth i = default := l.inductionOn (fun xs => ⟨xs.length, fun i hi => - (ListBlank.nth_mk xs i).symm ▸ List.getI_eq_default xs (Nat.le_of_lt hi)⟩) - have h := Nat.find_spec H - exact h i hi -open Classical in -lemma ListBlank.space_used_cons_le {α} [Inhabited α] (a : α) (l : ListBlank α) : - (l.cons a).space_used ≤ l.space_used + 1 := by - unfold space_used - apply Nat.find_le - intro i hi - cases i with - | zero => omega - | succ i => - rw [ListBlank.nth_succ, ListBlank.tail_cons] - exact ListBlank.nth_ge_space_used l i (by unfold space_used; omega) - -open Classical in -lemma ListBlank.space_used_tail_le {α} [Inhabited α] (l : ListBlank α) : - l.tail.space_used ≤ l.space_used := by - unfold space_used - apply Nat.find_le - intro i hi - rw [← ListBlank.nth_succ] - exact ListBlank.nth_ge_space_used l (i + 1) (by unfold space_used; omega) - -lemma OTape.space_used_move {α} [Inhabited α] (t : Turing.OTape α) (d : Dir) : - (t.move d).space_used ≤ t.space_used + 1 := by - cases d with - | left => - simp only [move, space_used] - have h1 := OList.length_tail_le t.left - have h2 := OList.length_cons_le t.head t.right - omega - | right => - simp only [move, space_used] - have h1 := OList.length_cons_le t.head t.left - have h2 := OList.length_tail_le t.right - omega +namespace Turing namespace BinTM0 @@ -317,7 +134,8 @@ lemma ListBlank.space_used_mk {α} [Inhabited α] (l : List α) : -- | nil => -- simp [ListBlank.space_used_mk_nil] -- | cons h t => --- simp only [List.tail_cons, List.length_cons, le_add_iff_nonneg_left, zero_le, sup_of_le_right] +-- simp only [List.tail_cons, List.length_cons, le_add_iff_nonneg_left, zero_le, +-- sup_of_le_right] -- rw [add_comm] -- simp only [Nat.add_right_cancel_iff] -- sorry @@ -551,8 +369,8 @@ structure Computable (f : List Bool → List Bool) where /-- a proof this machine outputsInTime `f` -/ outputsFun : ∀ a, - OutputsInTime tm ((a)) - (Option.some (((f a)))) + OutputsInTime tm a + (Option.some (f a)) steps /-- A Turing machine + a time function + @@ -566,9 +384,9 @@ structure ComputableInTime (f : List Bool → List Bool) where outputsFun : ∀ a, tm.OutputsWithinTime - ((a)) - (Option.some (((f a)))) - (time ( a).length) + a + (Option.some (f a)) + (time a.length) /-- A Turing machine + a polynomial time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ @@ -580,9 +398,9 @@ structure ComputableInPolyTime (f : List Bool → List Bool) where /-- proof that this machine outputsInTime `f` in at most `time(input.length)` steps -/ outputsFun : ∀ a, - OutputsWithinTime tm (( a)) - (Option.some (((f a)))) - (time.eval ( a).length) + OutputsWithinTime tm a + (Option.some (f a)) + (time.eval a.length) -- /-- A forgetful map, forgetting the time bound on the number of steps. -/ -- def ComputableInTime.toComputable {α β : Type} {ea : BinEncoding α} {eb : BinEncoding β} @@ -590,7 +408,8 @@ structure ComputableInPolyTime (f : List Bool → List Bool) where -- ⟨h.tm, fun a => OutputsWithinTime.toOutputsInTime (h.outputsFun a)⟩ /-- A forgetful map, forgetting that the time function is polynomial. -/ -def ComputableInPolyTime.toComputableInTime {f : List Bool → List Bool} (h : ComputableInPolyTime f) : +def ComputableInPolyTime.toComputableInTime {f : List Bool → List Bool} + (h : ComputableInPolyTime f) : ComputableInTime f := ⟨h.tm, fun n => h.time.eval n, h.outputsFun⟩ @@ -647,7 +466,7 @@ def ComputableInPolyTime.id : -- ⟨EvalsTo.refl _ _⟩ /-- A proof that the identity map on α is computable in time. -/ -def ComputableInTime.id : +def ComputableInTime.id : @ComputableInTime id := ComputableInPolyTime.toComputableInTime <| ComputableInPolyTime.id @@ -706,7 +525,7 @@ lemma compComputer_q₀_eq (f : List Bool → List Bool) (g : List Bool → List /-- Lift a config over a tm to a config over the comp -/ def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) + (hf : ComputableInTime f) (hg : ComputableInTime g) (cfg : hf.tm.Cfg) : (compComputer hf hg).Cfg := @@ -715,9 +534,9 @@ def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} OTape := cfg.OTape } -def liftCompCfg_right{f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) - (hg : ComputableInTime g) +def liftCompCfg_right {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : ComputableInTime f) + (hg : ComputableInTime g) (cfg : hg.tm.Cfg) : (compComputer hf hg).Cfg := { @@ -802,7 +621,7 @@ def liftCompCfg_left_or_right {f : List Bool → List Bool} {g : List Bool → L /-- The lifting function commutes with step, converting halt to transition -/ theorem map_liftCompCfg_left_or_right_step {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : ComputableInTime f) (hg : ComputableInTime g) (x : hf.tm.Cfg) (hx : x.state.isSome) : Option.map (liftCompCfg_left_or_right hf hg) (hf.tm.step x) = @@ -822,7 +641,7 @@ theorem map_liftCompCfg_left_or_right_step /-- General simulation: if the first machine goes from cfg to halt, the composed machine goes from lifted cfg to Sum.inr hg.tm.q₀ -/ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : ComputableInTime f) (hg : ComputableInTime g) (cfg : hf.tm.Cfg) (hcfg : cfg.state.isSome) (haltCfg : hf.tm.Cfg) @@ -873,25 +692,25 @@ This takes the same number of steps because the halt transition becomes a transi second machine. -/ theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : ComputableInTime f) (hg : ComputableInTime g) (a : List Bool) (hf_outputsFun : EvalsToWithinTime hf.tm.step - { state := some hf.tm.q₀, OTape := OTape.mk₁ ( a) } - (some { state := none, OTape := OTape.mk₁ ( (f a)) }) - (hf.time ( a).length)) : + { state := some hf.tm.q₀, OTape := OTape.mk₁ a } + (some { state := none, OTape := OTape.mk₁ (f a) }) + (hf.time a.length)) : EvalsToWithinTime (compComputer hf hg).step - { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ ( a) } - (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ ( (f a)) }) - (hf.time ( a).length) := by + { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ a } + (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) }) + (hf.time a.length) := by obtain ⟨steps, hsteps_le, hsteps_eval⟩ := hf_outputsFun use steps constructor · exact hsteps_le · have := comp_left_simulation_general hf hg - { state := some hf.tm.q₀, OTape := OTape.mk₁ ( a) } + { state := some hf.tm.q₀, OTape := OTape.mk₁ a } (by simp) - { state := none, OTape := OTape.mk₁ ( (f a)) } + { state := none, OTape := OTape.mk₁ (f a) } steps hsteps_eval simp only [liftCompCfg_left_or_right] at this @@ -900,7 +719,7 @@ theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → Li /-- Simulation lemma for the second machine in the composed computer -/ theorem comp_right_simulation {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : ComputableInTime f) (hg : ComputableInTime g) (x : hg.tm.Cfg) (y : Option hg.tm.Cfg) (m : ℕ) (h : EvalsToWithinTime hg.tm.step x y m) : EvalsToWithinTime (compComputer hf hg).step @@ -949,7 +768,7 @@ then from the intermediate state to the final state. -/ def ComputableInTime.comp {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) + (hf : ComputableInTime f) (hg : ComputableInTime g) (h_mono : Monotone hg.time) : (ComputableInTime (g ∘ f)) where @@ -960,23 +779,23 @@ def ComputableInTime.comp have hg_outputsFun := hg.outputsFun (f a) simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, Option.map_some, haltCfg] at hg_outputsFun hf_outputsFun ⊢ - -- The computer evals a to f a in time hf.time ( a) + -- The computer evals a to f a in time hf.time a have h_a_evalsTo_f_a : EvalsToWithinTime (compComputer hf hg).step - { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ ( a) } - (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ ( ((f a))) }) - (hf.time ( a).length) := + { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ a } + (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) }) + (hf.time a.length) := comp_left_simulation hf hg a hf_outputsFun have h_f_a_evalsTo_g_f_a : EvalsToWithinTime (compComputer hf hg).step - { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ ( ((f a))) } - (some { state := none, OTape := OTape.mk₁ ( ((g (f a)))) }) - (hg.time ( ((f a))).length) := by + { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) } + (some { state := none, OTape := OTape.mk₁ (g (f a)) }) + (hg.time (f a).length) := by -- Use the simulation lemma for the second machine have := comp_right_simulation hf hg - { state := some hg.tm.q₀, OTape := OTape.mk₁ ( (f a)) } - (some { state := none, OTape := OTape.mk₁ ( (g (f a))) }) - (hg.time ( (f a)).length) + { state := some hg.tm.q₀, OTape := OTape.mk₁ (f a) } + (some { state := none, OTape := OTape.mk₁ (g (f a)) }) + (hg.time (f a).length) hg_outputsFun simp only [liftCompCfg_right, Option.map_some] at this exact this diff --git a/Cslib/Foundations/Data/OList.lean b/Cslib/Foundations/Data/OList.lean new file mode 100644 index 00000000..c3c724ca --- /dev/null +++ b/Cslib/Foundations/Data/OList.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2025 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey +-/ + +module + +public import Mathlib.Data.List.Basic + +@[expose] public section + +/-! +# OList: Lists of Options that don't end with none + +This file defines `OList`, a list of option values where the list cannot end with `none`. +This is useful for representing tape contents where trailing blanks are not stored. +-/ + +namespace Turing + +/-- +List of option values that don't end with none +-/ +structure OList (α : Type) where + (asList : List (Option α)) + -- The list can be empty (i.e. none), but if it is not empty, the last element is not (some) none + (h : asList.getLast? ≠ some none) + +def OList.empty {α} : OList α := { asList := [], h := by simp } + +def OList.map_some {α} (l : List α) : OList α := { asList := l.map some, h := by simp } + +instance {α : Type} : Inhabited (OList α) where + default := OList.empty + + +def OList.length {α} (l : OList α) : ℕ := l.asList.length + +def OList.cons {α} : Option α -> OList α -> OList α +| none, l => { asList := [], h := by simp } +| some a, l => { + asList := some a :: l.asList, + h := by + cases hl : l.asList with + | nil => simp + | cons hd tl => + simp only [List.getLast?_cons_cons] + rw [← hl] + exact l.h + } + +def OList.tail {α} (l : OList α) : OList α := + match hl : l.asList with + | [] => OList.empty + | hd :: t => { asList := t, h := by + match t with + | [] => simp + | hd' :: t' => + have lh := l.h + rw [hl] at lh + simp only [List.getLast?_cons_cons] at lh + have := l.h + rw [hl, List.getLast?_cons_cons] at this + exact this + } + +def OList.head {α} (l : OList α) : Option α := + match l.asList with + | [] => none + | h :: _ => h + +lemma OList.length_tail_le {α} (l : OList α) : l.tail.length ≤ l.length := by + unfold tail length + split + · simp [empty] + · next heq => simp [heq] + +lemma OList.length_cons_none {α} (l : OList α) : (OList.cons none l).length = 0 := by + simp [cons, length] + +lemma OList.length_cons_some {α} (a : α) (l : OList α) : + (OList.cons (some a) l).length = l.length + 1 := by + simp [cons, length] + +lemma OList.length_cons_le {α} (o : Option α) (l : OList α) : + (OList.cons o l).length ≤ l.length + 1 := by + cases o with + | none => simp [length_cons_none] + | some a => simp [length_cons_some] + +lemma OList.length_map_some {α} (l : List α) : (OList.map_some l).length = l.length := by + simp [map_some, length] + +lemma OList.length_empty {α} : (OList.empty : OList α).length = 0 := by + simp [empty, length] + +end Turing diff --git a/Cslib/Foundations/Data/OTape.lean b/Cslib/Foundations/Data/OTape.lean new file mode 100644 index 00000000..765c875d --- /dev/null +++ b/Cslib/Foundations/Data/OTape.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2025 Bolton Bailey. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey +-/ + +module + +public import Cslib.Foundations.Data.OList +public import Mathlib.Computability.TuringMachine + +@[expose] public section + +/-! +# OTape: Tape representation using OList + +This file defines `OTape`, a tape representation for Turing machines +in the form of an `List` of `Option` values, +with the additional property that the list cannot end with `none`. + +## Design + +Note that Mathlib has a `Tape` type, but it requires the alphabet type to be inhabited, +and considers the ends of the tape to be filled with default values. + +The design that requires the tape elements to be `Option` values ensures that +Lists of the base alphabet, rendered directly onto the tape by mapping over `some`, +will not collide. + +## Main definitions + +* `OTape`: A tape with a head symbol and left/right contents stored as `OList` +* `OTape.move`: Move the tape head left or right +* `OTape.write`: Write a symbol at the current head position +* `OTape.space_used`: The space used by the tape +-/ + +namespace Turing + +/-- +I find this more convenient than mathlib's Tape type, +because that requires the type tobe inhabited, +and it is easy to confuse a list representing one thing with a list representing another, +if the representations are the same except for a sequence of default values at the end. + +The head of the machine is the current symbol under the tape head. +We do not assume here, but could add, that the ends of the tape are never none. +The move function should guarantee this, so that two tapes are equal +even if one has written none to the side +-/ +structure OTape (α : Type) where + (head : Option α) + (left : OList α) + (right : OList α) +deriving Inhabited + +def OTape.mk₁ (l : List Bool) : OTape Bool := + match l with + | [] => { head := none, left := OList.empty, right := OList.empty } + | h :: t => { head := some h, left := OList.empty, right := OList.map_some t } + +def OTape.move {α} : Turing.OTape α → Dir → Turing.OTape α + | t, .left => + match t.left, t.head, t.right with + | l, h, r => { head := l.head, left := l.tail, right := OList.cons h r } + | t, .right => + match t.left, t.head, t.right with + | l, h, r => { head := r.head, left := OList.cons h l, right := r.tail } + + +def OTape.move? {α} : Turing.OTape α → Option Dir → Turing.OTape α + | t, none => t + | t, some d => t.move d + +def OTape.write {α} : Turing.OTape α → Option α → Turing.OTape α + | t, a => { t with head := a } + +open Classical in +noncomputable def ListBlank.space_used {α} [Inhabited α] (l : ListBlank α) : ℕ := + Nat.find (p := fun n => ∀ i > n, l.nth i = default) + (l.inductionOn (fun xs => ⟨xs.length, fun i hi => by + change (ListBlank.mk xs).nth i = default + rw [ListBlank.nth_mk] + exact List.getI_eq_default xs (Nat.le_of_lt hi)⟩)) + +/-- +The space used by a OTape is the number of symbols +between and including the head, and leftmost and rightmost non-blank symbols on the OTape +-/ +noncomputable def OTape.space_used {α} [Inhabited α] (t : Turing.OTape α) : ℕ := + 1 + t.left.length + t.right.length + +lemma OTape.space_used_write {α} [Inhabited α] (t : Turing.OTape α) (a : Option α) : + (t.write a).space_used = t.space_used := by + rfl + +lemma OTape.space_used_mk₁ (l : List Bool) : + (OTape.mk₁ l).space_used = max 1 l.length := by + cases l with + | nil => + simp [mk₁, space_used, OList.length_empty] + | cons h t => + simp [mk₁, space_used, OList.length_empty, OList.length_map_some] + omega + +lemma OTape.space_used_move {α} [Inhabited α] (t : Turing.OTape α) (d : Dir) : + (t.move d).space_used ≤ t.space_used + 1 := by + cases d with + | left => + simp only [move, space_used] + have h1 := OList.length_tail_le t.left + have h2 := OList.length_cons_le t.head t.right + omega + | right => + simp only [move, space_used] + have h1 := OList.length_cons_le t.head t.left + have h2 := OList.length_tail_le t.right + omega + +end Turing From 946f4a385edd04bcf812bf23d0841d2e083b9e52 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Tue, 13 Jan 2026 21:38:36 -0800 Subject: [PATCH 03/13] remove listblank content --- .../Machines/SingleTapeTuring/Basic.lean | 104 ++++-------------- Cslib/Foundations/Data/OTape.lean | 8 -- 2 files changed, 20 insertions(+), 92 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index cf195ff1..ab463813 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -105,41 +105,6 @@ def ReductionSystem (tm : BinTM0) : Cslib.ReductionSystem (tm.Cfg) := noncomputable def Cfg.space_used (tm : BinTM0) (cfg : tm.Cfg) : ℕ := cfg.OTape.space_used -open Classical in -lemma ListBlank.space_used_mk_nil {α} [Inhabited α] : - (ListBlank.mk ([] : List α)).space_used = 0 := by - unfold ListBlank.space_used - rw [Nat.find_eq_zero] - intro i hi - rw [ListBlank.nth_mk] - exact List.getI_nil i - --- Helper lemma for space_used of a ListBlank created from a list -open Classical in -lemma ListBlank.space_used_mk {α} [Inhabited α] (l : List α) : - (ListBlank.mk l).space_used ≤ l.length := by - unfold ListBlank.space_used - apply Nat.find_le - intro i hi - rw [ListBlank.nth_mk] - exact List.getI_eq_default l (Nat.le_of_lt hi) - --- /-- The space_used of a OTape created from a list --- equals the maximum of 1 and the list length -/ --- lemma OTape.space_used_mk₁ {α} [Inhabited α] (l : List α) : --- (OTape.mk₁ l).space_used = max 1 l.length := by --- unfold OTape.mk₁ OTape.mk₂ OTape.mk' OTape.space_used --- simp only [ListBlank.space_used_mk_nil, add_zero, ListBlank.tail_mk] --- cases l with --- | nil => --- simp [ListBlank.space_used_mk_nil] --- | cons h t => --- simp only [List.tail_cons, List.length_cons, le_add_iff_nonneg_left, zero_le, --- sup_of_le_right] --- rw [add_comm] --- simp only [Nat.add_right_cancel_iff] --- sorry - lemma Cfg.space_used_initCfg (tm : BinTM0) (s : List Bool) : (tm.initCfg s).space_used = max 1 s.length := by simp [initCfg, Cfg.space_used, OTape.space_used_mk₁] @@ -149,28 +114,17 @@ lemma Cfg.space_used_haltCfg (tm : BinTM0) (s : List Bool) : simp [haltCfg, Cfg.space_used, OTape.space_used_mk₁] lemma Cfg.space_used_step {tm : BinTM0} (cfg cfg' : tm.Cfg) - (hstep : tm.step cfg = some cfg') : - cfg'.space_used ≤ cfg.space_used + 1 := by - unfold Cfg.space_used - cases cfg with | mk state tape => - cases state with - | none => simp [step] at hstep - | some q => - simp only [step] at hstep + (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by + obtain ⟨_ | q, tape⟩ := cfg + · simp [step] at hstep + · simp only [step] at hstep generalize hM : tm.M q tape.head = result at hstep obtain ⟨⟨wr, dir⟩, q''⟩ := result - simp only at hstep - cases hstep - cases dir with - | none => - simp only [OTape.move?] - rw [OTape.space_used_write] - omega + cases hstep; cases dir with + | none => simp [Cfg.space_used, OTape.move?, OTape.space_used_write] | some d => - simp only [OTape.move?] - have h1 := OTape.space_used_move (tape.write wr) d - rw [OTape.space_used_write] at h1 - exact h1 + have := OTape.space_used_move (tape.write wr) d + simp only [Cfg.space_used, OTape.move?, OTape.space_used_write] at this ⊢; exact this /-- `f` eventually reaches `b` when repeatedly evaluated on `a`, in exactly `steps` steps. -/ def EvalsToInTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (steps : ℕ) : Prop := @@ -183,43 +137,25 @@ lemma EvalsToInTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : EvalsToI /-- Transitivity of `EvalsTo` in the sum of the numbers of steps. -/ @[trans] lemma EvalsToInTime.trans {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (c : Option σ) - (steps₁ steps₂ : ℕ) - (h₁ : EvalsToInTime f a b steps₁) - (h₂ : EvalsToInTime f b c steps₂) : + (steps₁ steps₂ : ℕ) (h₁ : EvalsToInTime f a b steps₁) (h₂ : EvalsToInTime f b c steps₂) : EvalsToInTime f a c (steps₂ + steps₁) := by - simp_all only [EvalsToInTime, Option.bind_eq_bind] - rw [Function.iterate_add_apply, h₁, h₂] + simp only [EvalsToInTime] at *; rw [Function.iterate_add_apply, h₁, h₂] /-- If we evaluate to some state in n+1 steps, there is an intermediate state that we reach in n steps, and then one more step reaches the final state. -/ lemma EvalsToInTime.succ_decompose {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (n : ℕ) (h : EvalsToInTime f a (some b) (n + 1)) : ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := by - set c' := (· >>= f)^[n] (some a) with hc' - simp only [EvalsToInTime, Option.bind_eq_bind] at h hc' ⊢ - rw [Function.iterate_succ_apply'] at h - -- h : (· >>= f) ((· >>= f)^[n] (some a)) = some b - -- This means (· >>= f)^[n] (some a) >>= f = some b - -- So (· >>= f)^[n] (some a) = some c for some c with f c = some b - rw [<-hc'] at h - revert h hc' - cases c' with - | none => - grind - | some c => - intros h hc' - use c - grind - -lemma EvalsToInTime.succ_iff {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) - (n : ℕ) : - EvalsToInTime f a (some b) (n + 1) ↔ - ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := by - constructor - · exact EvalsToInTime.succ_decompose f a b n - · intro ⟨c, hc_eval, hc_step⟩ - simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_succ_apply'] at hc_eval ⊢ - simp only [hc_eval, Option.bind_some, hc_step] + simp only [EvalsToInTime, Function.iterate_succ_apply'] at h + match hc' : (· >>= f)^[n] (some a) with + | none => simp_all + | some c => exact ⟨c, hc', by simp_all⟩ + +lemma EvalsToInTime.succ_iff {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (n : ℕ) : + EvalsToInTime f a (some b) (n + 1) ↔ ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := + ⟨succ_decompose f a b n, fun ⟨_, hc_eval, hc_step⟩ => by + simp only [EvalsToInTime, Function.iterate_succ_apply'] at hc_eval ⊢; + rw [hc_eval]; exact hc_step⟩ theorem Turing.BinTM0.EvalsToInTime.congr.extracted_1_2.{u_2, u_1} {σ : Type u_1} {σ' : Type u_2} (f : σ → Option σ) diff --git a/Cslib/Foundations/Data/OTape.lean b/Cslib/Foundations/Data/OTape.lean index 765c875d..f2c09213 100644 --- a/Cslib/Foundations/Data/OTape.lean +++ b/Cslib/Foundations/Data/OTape.lean @@ -75,14 +75,6 @@ def OTape.move? {α} : Turing.OTape α → Option Dir → Turing.OTape α def OTape.write {α} : Turing.OTape α → Option α → Turing.OTape α | t, a => { t with head := a } -open Classical in -noncomputable def ListBlank.space_used {α} [Inhabited α] (l : ListBlank α) : ℕ := - Nat.find (p := fun n => ∀ i > n, l.nth i = default) - (l.inductionOn (fun xs => ⟨xs.length, fun i hi => by - change (ListBlank.mk xs).nth i = default - rw [ListBlank.nth_mk] - exact List.getI_eq_default xs (Nat.le_of_lt hi)⟩)) - /-- The space used by a OTape is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the OTape From 0c3b4325cc4ba14cad82b4f126b59c589b458f2d Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 10:16:08 -0800 Subject: [PATCH 04/13] clean up --- .gitignore | 1 + .../Machines/SingleTapeTuring/Basic.lean | 374 +++++------------- .../Semantics/ReductionSystem/Basic.lean | 211 +++++++++- 3 files changed, 302 insertions(+), 284 deletions(-) diff --git a/.gitignore b/.gitignore index 94f4582b..85b216ae 100644 --- a/.gitignore +++ b/.gitignore @@ -14,3 +14,4 @@ /docs/Std-manifest.json.hash /docs/Std-manifest.json.trace .DS_Store +.claude diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index ab463813..b95473a1 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -1,23 +1,33 @@ /- Copyright (c) 2025 Bolton Bailey. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Bolton Bailey +Authors: Bolton Bailey TODO add the authors of the mathlib file this is based on -/ module --- TODO golf imports -public import Cslib.Computability.Automata.Acceptors.Acceptor -public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor -public import Cslib.Foundations.Data.OmegaSequence.InfOcc public import Cslib.Foundations.Data.OTape public import Cslib.Foundations.Semantics.ReductionSystem.Basic public import Mathlib.Algebra.Polynomial.Eval.Defs -public import Mathlib.Computability.PostTuringMachine -public import Mathlib.Computability.TuringMachine @[expose] public section +/-! +# Single-Tape Turing Machine + +Defines a single-tape Turing machine over the alphabet of `Option Bool`, +where `none` represents a blank OTape symbol. + +## TODOs + +- Generalize Bool to an arbitrary (finite?) alphabet +- switch transition system to use the `ReductionSystem` framework +- refactor polynomial time to another file +- remove unfold + +-/ + +open Cslib namespace Turing @@ -99,7 +109,7 @@ which maps a configuration to its next configuration if it exists. -/ def ReductionSystem (tm : BinTM0) : Cslib.ReductionSystem (tm.Cfg) := { Red := fun cfg cfg' => tm.step cfg = some cfg' } --- TODO use this, rather than the current setup +-- TODO use this, rather than the current setup, or better yet an LTS? noncomputable def Cfg.space_used (tm : BinTM0) (cfg : tm.Cfg) : ℕ := @@ -126,155 +136,6 @@ lemma Cfg.space_used_step {tm : BinTM0} (cfg cfg' : tm.Cfg) have := OTape.space_used_move (tape.write wr) d simp only [Cfg.space_used, OTape.move?, OTape.space_used_write] at this ⊢; exact this -/-- `f` eventually reaches `b` when repeatedly evaluated on `a`, in exactly `steps` steps. -/ -def EvalsToInTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (steps : ℕ) : Prop := - (· >>= f)^[steps] a = b - -/-- Reflexivity of `EvalsTo` in 0 steps. -/ -lemma EvalsToInTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : EvalsToInTime f a (some a) 0 := - rfl - -/-- Transitivity of `EvalsTo` in the sum of the numbers of steps. -/ -@[trans] -lemma EvalsToInTime.trans {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (c : Option σ) - (steps₁ steps₂ : ℕ) (h₁ : EvalsToInTime f a b steps₁) (h₂ : EvalsToInTime f b c steps₂) : - EvalsToInTime f a c (steps₂ + steps₁) := by - simp only [EvalsToInTime] at *; rw [Function.iterate_add_apply, h₁, h₂] - -/-- If we evaluate to some state in n+1 steps, there is an intermediate state - that we reach in n steps, and then one more step reaches the final state. -/ -lemma EvalsToInTime.succ_decompose {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) - (n : ℕ) (h : EvalsToInTime f a (some b) (n + 1)) : - ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := by - simp only [EvalsToInTime, Function.iterate_succ_apply'] at h - match hc' : (· >>= f)^[n] (some a) with - | none => simp_all - | some c => exact ⟨c, hc', by simp_all⟩ - -lemma EvalsToInTime.succ_iff {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (n : ℕ) : - EvalsToInTime f a (some b) (n + 1) ↔ ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := - ⟨succ_decompose f a b n, fun ⟨_, hc_eval, hc_step⟩ => by - simp only [EvalsToInTime, Function.iterate_succ_apply'] at hc_eval ⊢; - rw [hc_eval]; exact hc_step⟩ - -theorem Turing.BinTM0.EvalsToInTime.congr.extracted_1_2.{u_2, u_1} - {σ : Type u_1} {σ' : Type u_2} (f : σ → Option σ) - (f' : σ' → Option σ') (g : σ → σ') - (hg : ∀ (x : σ), Option.map g (f x) = f' (g x)) (n : ℕ) (a : σ) : - (Option.map g ((flip Option.bind f)^[n] (some a))).bind f' = - ((flip Option.bind f)^[n] (some a)).bind fun a ↦ f' (g a) := by - induction n with - | zero => simp - | succ n ih => - simp only [Function.iterate_succ_apply, flip, Option.bind_some, <- hg] at ih ⊢ - grind - - - - - -/-- -If `f` is homomorphic to `f'` via `g`, then if `f` evals to `b` from `a` in `steps` steps, -then `f'` evals to `g b` from `g a` in `steps` steps. --/ -lemma EvalsToInTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') - (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) - (a : σ) (b : Option σ) - (steps : ℕ) - (h : EvalsToInTime f a b steps) : EvalsToInTime f' (g a) (Option.map g b) steps := by - induction steps generalizing a b with - | zero => - simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq] at h ⊢ - subst h - rfl - | succ n ih => - simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_succ_apply', - forall_eq'] at h ih ⊢ - subst h - rw [ih] - clear ih - simp only [Option.map_bind, Function.comp_apply, hg] - exact Turing.BinTM0.EvalsToInTime.congr.extracted_1_2 f f' g hg n a - -/-- -If `h : σ → ℕ` increases by at most 1 on each step of `f`, -then the value of `h` at the output after `steps` steps is at most `h` at the input plus `steps`. --/ -lemma EvalsToInTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) - (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) - (a : σ) (b : σ) - (steps : ℕ) - (hevals : EvalsToInTime f a b steps) : - h b ≤ h a + steps := by - induction steps generalizing a b with - | zero => - simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq, Option.some.injEq, - add_zero] at hevals ⊢ - subst hevals - exact Nat.le_refl (h a) - | succ n ih => - rw [EvalsToInTime.succ_iff] at hevals - obtain ⟨c, hevals_n, h_step_eq⟩ := hevals - specialize ih a c hevals_n - specialize h_step c b h_step_eq - omega - - --- m -> step_bound -/-- `f` eventually reaches `b` in at most `m` steps when repeatedly -evaluated on `a`. -/ -def EvalsToWithinTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (m : ℕ) : Prop := - ∃ steps ≤ m, EvalsToInTime f a b steps - -/-- Reflexivity of `EvalsToWithinTime` in 0 steps. -/ -def EvalsToWithinTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : - EvalsToWithinTime f a (some a) 0 := by - use 0 - exact if_false_right.mp rfl - -/-- Transitivity of `EvalsToWithinTime` in the sum of the numbers of steps. -/ -@[trans] -def EvalsToWithinTime.trans {σ : Type*} (f : σ → Option σ) (m₁ : ℕ) (m₂ : ℕ) (a : σ) (b : σ) - (c : Option σ) (h₁ : EvalsToWithinTime f a b m₁) (h₂ : EvalsToWithinTime f b c m₂) : - EvalsToWithinTime f a c (m₂ + m₁) := by - obtain ⟨steps₁, hsteps₁, hevals₁⟩ := h₁ - obtain ⟨steps₂, hsteps₂, hevals₂⟩ := h₂ - use steps₂ + steps₁ - constructor - · omega - · exact EvalsToInTime.trans f a b c steps₁ steps₂ hevals₁ hevals₂ - -def EvalsToWithinTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') - (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) - (a : σ) (b : Option σ) - (m : ℕ) - (h : EvalsToWithinTime f a b m) : EvalsToWithinTime f' (g a) (Option.map g b) m := by - obtain ⟨steps, hsteps, hevals⟩ := h - use steps - constructor - · exact hsteps - · exact EvalsToInTime.map f f' g hg a b steps hevals - -/-- -Monotonicity of `EvalsToWithinTime` in the time bound. --/ -def EvalsToWithinTime.mono_time {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) - {m₁ m₂ : ℕ} (h : EvalsToWithinTime f a b m₁) (hm : m₁ ≤ m₂) : EvalsToWithinTime f a b m₂ := by - obtain ⟨steps, hsteps, hevals⟩ := h - use steps - simp_all only - simp - omega - -lemma EvalsToWithinTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) - (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) - (a : σ) (b : σ) - (m : ℕ) - (hevals : EvalsToWithinTime f a (some b) m) : - h b ≤ h a + m := by - obtain ⟨steps, hsteps, hevals_steps⟩ := hevals - have := EvalsToInTime.small_change f h h_step a b steps hevals_steps - omega /-- A proof of tm outputting l' when given l. -/ def OutputsInTime (tm : BinTM0) (l : List (Bool)) (l' : Option (List (Bool))) := @@ -285,18 +146,6 @@ def OutputsWithinTime (tm : BinTM0) (l : List (Bool)) (l' : Option (List (Bool)) (m : ℕ) := EvalsToWithinTime tm.step (initCfg tm l) ((Option.map (haltCfg tm)) l') m --- /-- A (bundled TM0) Turing machine --- with input alphabet equivalent to `Γ₀` and output alphabet equivalent to `Γ₁`. --- TODO this is something of a holdover, might get rid --- -/ --- structure ComputableAux (Γ₀ Γ₁ : Type) where --- /-- the underlying bundled TM0 -/ --- tm : BinTM0 --- /-- the input alphabet is equivalent to `Γ₀` -/ --- inputAlphabet : Bool ≃ Γ₀ --- /-- the output alphabet is equivalent to `Γ₁` -/ --- outputAlphabet : Bool ≃ Γ₁ - /-- A Turing machine + a proof it outputsInTime `f`. -/ structure Computable (f : List Bool → List Bool) where /-- the underlying bundled TM0 -/ @@ -311,7 +160,7 @@ structure Computable (f : List Bool → List Bool) where /-- A Turing machine + a time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ -structure ComputableInTime (f : List Bool → List Bool) where +structure TimeComputable (f : List Bool → List Bool) where /-- the underlying bundled TM0 -/ tm : BinTM0 /-- a time function -/ @@ -324,33 +173,6 @@ structure ComputableInTime (f : List Bool → List Bool) where (Option.some (f a)) (time a.length) -/-- A Turing machine + a polynomial time function + -a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ -structure ComputableInPolyTime (f : List Bool → List Bool) where - /-- the underlying bundled TM0 -/ - tm : BinTM0 - /-- a polynomial time function -/ - time : Polynomial ℕ - /-- proof that this machine outputsInTime `f` in at most `time(input.length)` steps -/ - outputsFun : - ∀ a, - OutputsWithinTime tm a - (Option.some (f a)) - (time.eval a.length) - --- /-- A forgetful map, forgetting the time bound on the number of steps. -/ --- def ComputableInTime.toComputable {α β : Type} {ea : BinEncoding α} {eb : BinEncoding β} --- {f : α → β} (h : ComputableInTime ea eb f) : Computable ea eb f := --- ⟨h.tm, fun a => OutputsWithinTime.toOutputsInTime (h.outputsFun a)⟩ - -/-- A forgetful map, forgetting that the time function is polynomial. -/ -def ComputableInPolyTime.toComputableInTime {f : List Bool → List Bool} - (h : ComputableInPolyTime f) : - ComputableInTime f := - ⟨h.tm, fun n => h.time.eval n, h.outputsFun⟩ - -open Turing.TM0.Stmt - /-- A Turing machine computing the identity. -/ def idComputer : BinTM0 where Λ := PUnit @@ -359,71 +181,19 @@ def idComputer : BinTM0 where noncomputable section -/-- A proof that the identity map on α is computable in polytime. -/ -def ComputableInPolyTime.id : - @ComputableInPolyTime id where - tm := idComputer - time := 1 - outputsFun x := by +/-- A proof that the identity map on α is computable in time. -/ +def TimeComputable.id : + @TimeComputable id := + ⟨idComputer, fun _ => 1, fun x => by use 1 - simp only [Polynomial.eval_one, le_refl, id_eq, Option.map_some, true_and] + simp only [le_refl, id_eq, Option.map_some, true_and] simp only [EvalsToInTime, initCfg, haltCfg, idComputer, Function.iterate_succ, Function.iterate_zero, Function.comp_apply, id_eq] - congr 1 - - - -- { steps := 1 - -- evals_in_steps := rfl - -- steps_le_m := by simp only [Polynomial.eval_one, le_refl] } - --- instance inhabitedComputableInPolyTime : --- Inhabited (ComputableInPolyTime (default : BinEncoding Bool) default id) := --- ⟨idComputableInPolyTime Computability.inhabitedBinEncoding.default⟩ - --- instance inhabitedOutputsWithinTime : --- Inhabited --- (OutputsWithinTime (idComputer finEncodingBoolBool) --- (List.map (Equiv.cast rfl).invFun [false]) --- (some (List.map (Equiv.cast rfl).invFun [false])) (Polynomial.eval 1 1)) := --- ⟨(idComputableInPolyTime finEncodingBoolBool).outputsFun false⟩ - --- instance inhabitedOutputsInTime : --- Inhabited --- (OutputsInTime (idComputer finEncodingBoolBool) (List.map (Equiv.cast rfl).invFun [false]) --- (some (List.map (Equiv.cast rfl).invFun [false]))) := --- ⟨OutputsWithinTime.toOutputsInTime Turing.inhabitedOutputsWithinTime.default⟩ - --- instance inhabitedEvalsToWithinTime : --- Inhabited (EvalsToWithinTime (fun _ : Unit => some ⟨⟩) ⟨⟩ (some ⟨⟩) 0) := --- ⟨EvalsToWithinTime.refl _ _⟩ - --- instance inhabitedTM0EvalsToInTime : --- Inhabited (EvalsToInTime (fun _ : Unit => some ⟨⟩) ⟨⟩ (some ⟨⟩)) := --- ⟨EvalsTo.refl _ _⟩ - -/-- A proof that the identity map on α is computable in time. -/ -def ComputableInTime.id : - @ComputableInTime id := - ComputableInPolyTime.toComputableInTime <| ComputableInPolyTime.id - --- instance inhabitedComputableInTime : --- Inhabited (ComputableInTime finEncodingBoolBool finEncodingBoolBool id) := --- ⟨idComputableInTime Computability.inhabitedBinEncoding.default⟩ - --- /-- A proof that the identity map on α is computable. -/ --- def idComputable {α : Type} (ea : BinEncoding α) : @Computable α α ea ea id := --- ComputableInTime.toComputable <| ComputableInTime.id ea - --- instance inhabitedComputable : --- Inhabited (Computable finEncodingBoolBool finEncodingBoolBool id) := --- ⟨idComputable Computability.inhabitedBinEncoding.default⟩ - --- instance inhabitedComputableAux : Inhabited (ComputableAux Bool Bool) := --- ⟨(default : Computable finEncodingBoolBool finEncodingBoolBool id).toComputableAux⟩ + congr 1⟩ def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) - (hg : ComputableInTime g) : + (hf : TimeComputable f) + (hg : TimeComputable g) : BinTM0 := { Λ := hf.tm.Λ ⊕ hg.tm.Λ @@ -454,15 +224,15 @@ def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} } lemma compComputer_q₀_eq (f : List Bool → List Bool) (g : List Bool → List Bool) - (hf : ComputableInTime f) - (hg : ComputableInTime g) : + (hf : TimeComputable f) + (hg : TimeComputable g) : (compComputer hf hg).q₀ = Sum.inl hf.tm.q₀ := rfl /-- Lift a config over a tm to a config over the comp -/ def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) - (hg : ComputableInTime g) + (hf : TimeComputable f) + (hg : TimeComputable g) (cfg : hf.tm.Cfg) : (compComputer hf hg).Cfg := { @@ -471,8 +241,8 @@ def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} } def liftCompCfg_right {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) - (hg : ComputableInTime g) + (hf : TimeComputable f) + (hg : TimeComputable g) (cfg : hg.tm.Cfg) : (compComputer hf hg).Cfg := { @@ -482,7 +252,7 @@ def liftCompCfg_right {f : List Bool → List Bool} {g : List Bool → List Bool theorem map_liftCompCfg_left_step {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : TimeComputable f) (hg : TimeComputable g) (x : hf.tm.Cfg) (hx : ∀ cfg, hf.tm.step x = some cfg → cfg.state.isSome) : Option.map (liftCompCfg_left hf hg) (hf.tm.step x) = @@ -513,7 +283,7 @@ theorem map_liftCompCfg_left_step /-- Helper lemma: liftCompCfg_right commutes with step for the second machine -/ theorem map_liftCompCfg_right_step {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : TimeComputable f) (hg : TimeComputable g) (x : hg.tm.Cfg) : Option.map (liftCompCfg_right hf hg) (hg.tm.step x) = (compComputer hf hg).step (liftCompCfg_right hf hg x) := by @@ -532,7 +302,7 @@ theorem map_liftCompCfg_right_step /-- When the first machine would halt, the composed machine transitions to the second machine -/ theorem comp_transition_to_right {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : TimeComputable f) (hg : TimeComputable g) (tp : OTape (Bool)) (q : hf.tm.Λ) (hM : (hf.tm.M q tp.head).2 = none) : @@ -546,8 +316,8 @@ theorem comp_transition_to_right {f : List Bool → List Bool} {g : List Bool /-- Helper: lifting to Sum.inl and transitioning to Sum.inr on halt -/ def liftCompCfg_left_or_right {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) - (hg : ComputableInTime g) + (hf : TimeComputable f) + (hg : TimeComputable g) (cfg : hf.tm.Cfg) : (compComputer hf hg).Cfg := match cfg.state with @@ -557,7 +327,7 @@ def liftCompCfg_left_or_right {f : List Bool → List Bool} {g : List Bool → L /-- The lifting function commutes with step, converting halt to transition -/ theorem map_liftCompCfg_left_or_right_step {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : TimeComputable f) (hg : TimeComputable g) (x : hf.tm.Cfg) (hx : x.state.isSome) : Option.map (liftCompCfg_left_or_right hf hg) (hf.tm.step x) = @@ -577,7 +347,7 @@ theorem map_liftCompCfg_left_or_right_step /-- General simulation: if the first machine goes from cfg to halt, the composed machine goes from lifted cfg to Sum.inr hg.tm.q₀ -/ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hf.tm.Cfg) (hcfg : cfg.state.isSome) (haltCfg : hf.tm.Cfg) @@ -628,7 +398,7 @@ This takes the same number of steps because the halt transition becomes a transi second machine. -/ theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : TimeComputable f) (hg : TimeComputable g) (a : List Bool) (hf_outputsFun : EvalsToWithinTime hf.tm.step @@ -655,7 +425,7 @@ theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → Li /-- Simulation lemma for the second machine in the composed computer -/ theorem comp_right_simulation {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) (hg : ComputableInTime g) + (hf : TimeComputable f) (hg : TimeComputable g) (x : hg.tm.Cfg) (y : Option hg.tm.Cfg) (m : ℕ) (h : EvalsToWithinTime hg.tm.step x y m) : EvalsToWithinTime (compComputer hf hg).step @@ -682,7 +452,7 @@ lemma output_length_le_input_length_add_time (tm : BinTM0) (l l' : List Bool) (t omega /-- -A composition for ComputableInTime. +A composition for TimeComputable. If f and g are computed by turing machines M₁ and M₂ then we can construct a turing machine M which computes g ∘ f by first running M₁ @@ -702,12 +472,12 @@ Prove separately that it evals to the intermediate state from the start state and then from the intermediate state to the final state. -/ -def ComputableInTime.comp +def TimeComputable.comp {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : ComputableInTime f) - (hg : ComputableInTime g) + (hf : TimeComputable f) + (hg : TimeComputable g) (h_mono : Monotone hg.time) : - (ComputableInTime (g ∘ f)) where + (TimeComputable (g ∘ f)) where tm := compComputer hf hg time l := (hf.time l) + hg.time (max 1 l + hf.time l) outputsFun a := by @@ -748,6 +518,56 @@ def ComputableInTime.comp end +/-! +## Polynomial Time Computability + +This section defines polynomial time computable functions on Turing machines. +-/ + +section PolyTime + +/-- A Turing machine + a polynomial time function + +a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ +structure PolyTimeComputable (f : List Bool → List Bool) extends TimeComputable f where + /-- a polynomial time bound -/ + poly : Polynomial ℕ + /-- proof that this machine outputsInTime `f` in at most `time(input.length)` steps -/ + bounds : ∀ n, time n ≤ poly.eval n + +/-- A proof that the identity map on α is computable in polytime. -/ +noncomputable def PolyTimeComputable.id : @PolyTimeComputable id where + toTimeComputable := TimeComputable.id + poly := 1 + bounds n := by simp only [TimeComputable.id, Polynomial.eval_one, le_refl] + +/-- +A proof that the composition of two polytime computable functions is polytime computable. +-/ +noncomputable def PolyTimeComputable.comp + {f : List Bool → List Bool} {g : List Bool → List Bool} + (hf : PolyTimeComputable f) + (hg : PolyTimeComputable g) + -- all Nat polynomials are monotone, but the tighter internal bound maybe is not + (h_mono : Monotone hg.time) : + PolyTimeComputable (g ∘ f) where + toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono + + poly := hf.poly + hg.poly.comp (1 + Polynomial.X + hf.poly) + bounds n := by + simp only [TimeComputable.comp, Polynomial.eval_add, Polynomial.eval_comp, Polynomial.eval_X, + Polynomial.eval_one] + apply add_le_add + · exact hf.bounds n + · have : hg.time (max 1 n + hf.time n) ≤ hg.time (1 + n + hf.poly.eval n) := by + apply h_mono + apply add_le_add + · omega + · exact hf.bounds n + apply le_trans this _ + exact hg.bounds (1 + n + hf.poly.eval n) + +end PolyTime + end BinTM0 end Turing diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 1c85c16d..02d65ef2 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -10,6 +10,9 @@ public import Cslib.Init public import Mathlib.Logic.Relation public import Mathlib.Util.Notation3 +-- TODO remove this import +public import Mathlib.Algebra.Polynomial.Eval.Defs + @[expose] public section /-! @@ -29,6 +32,11 @@ structure ReductionSystem (Term : Type u) where /-- The reduction relation. -/ Red : Term → Term → Prop +structure TerminalReductionSystem (Term : Type u) extends ReductionSystem Term where + /-- The terminal terms. -/ + Terminal : Term → Prop + /-- A terminal term cannot be further reduced. -/ + terminal_not_reducible : ∀ t t', Terminal t → ¬ Red t t' section MultiStep @@ -50,17 +58,206 @@ theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b) end MultiStep -section Timed +section Steps + +inductive ReductionSystem.reducesToInSteps + (rs : ReductionSystem Term) : Term → Term → ℕ → Prop + | refl (t : Term) : reducesToInSteps rs t t 0 + | cons (t t' t'' : Term) (n : ℕ) (h₁ : rs.Red t t') (h₂ : reducesToInSteps rs t' t'' n) : + reducesToInSteps rs t t'' (n + 1) + +lemma ReductionSystem.reducesToInSteps.trans {rs : ReductionSystem Term} {a b c : Term} {n m : ℕ} + (h₁ : reducesToInSteps rs a b n) (h₂ : reducesToInSteps rs b c m) : + reducesToInSteps rs a c (n + m) := by + sorry + +lemma ReductionSystem.reducesToInSteps.succ {rs : ReductionSystem Term} {a b : Term} {n : ℕ} + (h : reducesToInSteps rs a b (n + 1)) : + ∃ t', rs.Red a t' ∧ reducesToInSteps rs t' b n := by + sorry + +-- TODO iff + +lemma ReductionSystem.reducesToInSteps.succ' {rs : ReductionSystem Term} {a b : Term} {n : ℕ} + (h : reducesToInSteps rs a b (n + 1)) : + ∃ t', reducesToInSteps rs a t' n ∧ rs.Red t' b := by + sorry + +-- TODO iff + +end Steps + +/-- +Given a map σ → Option σ, we can construct a terminal reduction system on `σ` +where a term is terminal if it maps to `none` under the given function. +and otherwise is reducible to its `some` value under the given function. +-/ +def TerminalReductionSystem.Option {σ : Type*} (f : σ → Option σ) : TerminalReductionSystem σ where + Red := fun a b => f a = some b + Terminal := fun a => f a = none + terminal_not_reducible := by + intros t t' h_terminal h_red + simp [h_terminal] at h_red + + +-- TODO refactor the contents of this section into ReductionSystem +-- then delete them +section EvalsToJunk + + + +/-- `f` eventually reaches `b` when repeatedly evaluated on `a`, in exactly `steps` steps. -/ +def EvalsToInTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (steps : ℕ) : Prop := + (· >>= f)^[steps] a = b + +/-- Reflexivity of `EvalsTo` in 0 steps. -/ +lemma EvalsToInTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : EvalsToInTime f a (some a) 0 := + rfl + +/-- Transitivity of `EvalsTo` in the sum of the numbers of steps. -/ +@[trans] +lemma EvalsToInTime.trans {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (c : Option σ) + (steps₁ steps₂ : ℕ) (h₁ : EvalsToInTime f a b steps₁) (h₂ : EvalsToInTime f b c steps₂) : + EvalsToInTime f a c (steps₂ + steps₁) := by + simp only [EvalsToInTime] at *; rw [Function.iterate_add_apply, h₁, h₂] + +/-- If we evaluate to some state in n+1 steps, there is an intermediate state + that we reach in n steps, and then one more step reaches the final state. -/ +lemma EvalsToInTime.succ_decompose {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) + (n : ℕ) (h : EvalsToInTime f a (some b) (n + 1)) : + ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := by + simp only [EvalsToInTime, Function.iterate_succ_apply'] at h + match hc' : (· >>= f)^[n] (some a) with + | none => simp_all + | some c => exact ⟨c, hc', by simp_all⟩ -/-! ## Timed reductions -/ +lemma EvalsToInTime.succ_iff {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (n : ℕ) : + EvalsToInTime f a (some b) (n + 1) ↔ ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := + ⟨succ_decompose f a b n, fun ⟨_, hc_eval, hc_step⟩ => by + simp only [EvalsToInTime, Function.iterate_succ_apply'] at hc_eval ⊢; + rw [hc_eval]; exact hc_step⟩ + +theorem Turing.BinTM0.EvalsToInTime.congr.extracted_1_2.{u_2, u_1} + {σ : Type u_1} {σ' : Type u_2} (f : σ → Option σ) + (f' : σ' → Option σ') (g : σ → σ') + (hg : ∀ (x : σ), Option.map g (f x) = f' (g x)) (n : ℕ) (a : σ) : + (Option.map g ((flip Option.bind f)^[n] (some a))).bind f' = + ((flip Option.bind f)^[n] (some a)).bind fun a ↦ f' (g a) := by + induction n with + | zero => simp + | succ n ih => + simp only [Function.iterate_succ_apply, flip, Option.bind_some, <- hg] at ih ⊢ + grind + + + + + +/-- +If `f` is homomorphic to `f'` via `g`, then if `f` evals to `b` from `a` in `steps` steps, +then `f'` evals to `g b` from `g a` in `steps` steps. +-/ +lemma EvalsToInTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') + (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) + (a : σ) (b : Option σ) + (steps : ℕ) + (h : EvalsToInTime f a b steps) : EvalsToInTime f' (g a) (Option.map g b) steps := by + induction steps generalizing a b with + | zero => + simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq] at h ⊢ + subst h + rfl + | succ n ih => + simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_succ_apply', + forall_eq'] at h ih ⊢ + subst h + rw [ih] + clear ih + simp only [Option.map_bind, Function.comp_apply, hg] + exact Turing.BinTM0.EvalsToInTime.congr.extracted_1_2 f f' g hg n a + +/-- +If `h : σ → ℕ` increases by at most 1 on each step of `f`, +then the value of `h` at the output after `steps` steps is at most `h` at the input plus `steps`. +-/ +lemma EvalsToInTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) + (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) + (a : σ) (b : σ) + (steps : ℕ) + (hevals : EvalsToInTime f a b steps) : + h b ≤ h a + steps := by + induction steps generalizing a b with + | zero => + simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq, Option.some.injEq, + add_zero] at hevals ⊢ + subst hevals + exact Nat.le_refl (h a) + | succ n ih => + rw [EvalsToInTime.succ_iff] at hevals + obtain ⟨c, hevals_n, h_step_eq⟩ := hevals + specialize ih a c hevals_n + specialize h_step c b h_step_eq + omega + + +-- m -> step_bound +/-- `f` eventually reaches `b` in at most `m` steps when repeatedly +evaluated on `a`. -/ +def EvalsToWithinTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (m : ℕ) : Prop := + ∃ steps ≤ m, EvalsToInTime f a b steps + +/-- Reflexivity of `EvalsToWithinTime` in 0 steps. -/ +def EvalsToWithinTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : + EvalsToWithinTime f a (some a) 0 := by + use 0 + exact if_false_right.mp rfl + +/-- Transitivity of `EvalsToWithinTime` in the sum of the numbers of steps. -/ +@[trans] +def EvalsToWithinTime.trans {σ : Type*} (f : σ → Option σ) (m₁ : ℕ) (m₂ : ℕ) (a : σ) (b : σ) + (c : Option σ) (h₁ : EvalsToWithinTime f a b m₁) (h₂ : EvalsToWithinTime f b c m₂) : + EvalsToWithinTime f a c (m₂ + m₁) := by + obtain ⟨steps₁, hsteps₁, hevals₁⟩ := h₁ + obtain ⟨steps₂, hsteps₂, hevals₂⟩ := h₂ + use steps₂ + steps₁ + constructor + · omega + · exact EvalsToInTime.trans f a b c steps₁ steps₂ hevals₁ hevals₂ + +def EvalsToWithinTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') + (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) + (a : σ) (b : Option σ) + (m : ℕ) + (h : EvalsToWithinTime f a b m) : EvalsToWithinTime f' (g a) (Option.map g b) m := by + obtain ⟨steps, hsteps, hevals⟩ := h + use steps + constructor + · exact hsteps + · exact EvalsToInTime.map f f' g hg a b steps hevals + +/-- +Monotonicity of `EvalsToWithinTime` in the time bound. +-/ +def EvalsToWithinTime.mono_time {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) + {m₁ m₂ : ℕ} (h : EvalsToWithinTime f a b m₁) (hm : m₁ ≤ m₂) : EvalsToWithinTime f a b m₂ := by + obtain ⟨steps, hsteps, hevals⟩ := h + use steps + simp_all only + simp + omega -/-- Given a reduction system `rs` on `Term`, returns a reduction system on `Term × ℕ` -where the second component of the pair represents the number of steps taken. -/ -def Timed (rs : ReductionSystem Term) : ReductionSystem (Term × ℕ) := - { Red := fun ⟨t, n⟩ ⟨t', n'⟩ => rs.Red t t' ∧ n' = n + 1 } +lemma EvalsToWithinTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) + (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) + (a : σ) (b : σ) + (m : ℕ) + (hevals : EvalsToWithinTime f a (some b) m) : + h b ≤ h a + m := by + obtain ⟨steps, hsteps, hevals_steps⟩ := hevals + have := EvalsToInTime.small_change f h h_step a b steps hevals_steps + omega -end Timed +end EvalsToJunk open Lean Elab Meta Command Term From 630ce615d86cdb87d4f5591a6bfadccbe8f99a89 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 11:10:28 -0800 Subject: [PATCH 05/13] claude build/switch to reduces API --- .../Machines/SingleTapeTuring/Basic.lean | 112 ++++++------ .../Semantics/ReductionSystem/Basic.lean | 171 +++++++++++++++++- 2 files changed, 224 insertions(+), 59 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index b95473a1..57a65479 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -104,13 +104,11 @@ def initCfg (tm : BinTM0) (s : List Bool) : tm.Cfg := ⟨some tm.q₀, OTape.mk def haltCfg (tm : BinTM0) (s : List (Bool)) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ /-- -The `ReductionSystem` corresponding to a `BinTM0` is defined by the `step` function, +The `TerminalReductionSystem` corresponding to a `BinTM0` is defined by the `step` function, which maps a configuration to its next configuration if it exists. -/ -def ReductionSystem (tm : BinTM0) : Cslib.ReductionSystem (tm.Cfg) := - { Red := fun cfg cfg' => tm.step cfg = some cfg' } --- TODO use this, rather than the current setup, or better yet an LTS? - +def TerminalReductionSystem (tm : BinTM0) : Cslib.TerminalReductionSystem (tm.Cfg) := + TerminalReductionSystem.Option tm.step noncomputable def Cfg.space_used (tm : BinTM0) (cfg : tm.Cfg) : ℕ := cfg.OTape.space_used @@ -138,25 +136,21 @@ lemma Cfg.space_used_step {tm : BinTM0} (cfg cfg' : tm.Cfg) /-- A proof of tm outputting l' when given l. -/ -def OutputsInTime (tm : BinTM0) (l : List (Bool)) (l' : Option (List (Bool))) := - EvalsToInTime tm.step (initCfg tm l) ((Option.map (haltCfg tm)) l') +def Outputs (tm : BinTM0) (l : List (Bool)) (l' : List (Bool)) : Prop := + tm.TerminalReductionSystem.MRed (initCfg tm l) (haltCfg tm l') /-- A proof of tm outputting l' when given l in at most m steps. -/ -def OutputsWithinTime (tm : BinTM0) (l : List (Bool)) (l' : Option (List (Bool))) +def OutputsWithinTime (tm : BinTM0) (l : List (Bool)) (l' : (List (Bool))) (m : ℕ) := - EvalsToWithinTime tm.step (initCfg tm l) ((Option.map (haltCfg tm)) l') m + tm.TerminalReductionSystem.reducesToWithinSteps (initCfg tm l) (haltCfg tm l') m /-- A Turing machine + a proof it outputsInTime `f`. -/ structure Computable (f : List Bool → List Bool) where /-- the underlying bundled TM0 -/ tm : BinTM0 - steps : ℕ /-- a proof this machine outputsInTime `f` -/ outputsFun : - ∀ a, - OutputsInTime tm a - (Option.some (f a)) - steps + ∀ a, tm.Outputs a (f a) /-- A Turing machine + a time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ @@ -170,7 +164,7 @@ structure TimeComputable (f : List Bool → List Bool) where ∀ a, tm.OutputsWithinTime a - (Option.some (f a)) + ((f a)) (time a.length) /-- A Turing machine computing the identity. -/ @@ -181,14 +175,16 @@ def idComputer : BinTM0 where noncomputable section +-- TODO switch to where syntax /-- A proof that the identity map on α is computable in time. -/ -def TimeComputable.id : - @TimeComputable id := +def TimeComputable.id : TimeComputable id := ⟨idComputer, fun _ => 1, fun x => by - use 1 - simp only [le_refl, id_eq, Option.map_some, true_and] - simp only [EvalsToInTime, initCfg, haltCfg, idComputer, - Function.iterate_succ, Function.iterate_zero, Function.comp_apply, id_eq] + refine ⟨1, le_refl 1, ?_⟩ + -- Need to show reducesToInSteps for 1 step + refine Cslib.ReductionSystem.reducesToInSteps.cons _ _ _ 0 ?_ (Cslib.ReductionSystem.reducesToInSteps.refl _) + -- Show the single step reduction: step (init x) = some (halt x) + simp only [TerminalReductionSystem, Cslib.TerminalReductionSystem.Option, initCfg, haltCfg, + idComputer, step, OTape.move?] congr 1⟩ def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} @@ -353,10 +349,10 @@ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Boo (haltCfg : hf.tm.Cfg) -- (haltCfg_state : haltCfg.state = none) (steps : ℕ) - (h : EvalsToInTime hf.tm.step cfg (some haltCfg) steps) : - EvalsToInTime (compComputer hf hg).step + (h : hf.tm.TerminalReductionSystem.reducesToInSteps cfg ( haltCfg) steps) : + (compComputer hf hg).TerminalReductionSystem.reducesToInSteps (liftCompCfg_left_or_right hf hg cfg) - (some (liftCompCfg_left_or_right hf hg haltCfg)) + ( (liftCompCfg_left_or_right hf hg haltCfg)) steps := by -- Proof by induction on steps. -- Key insight: liftCompCfg_left_or_right maps: @@ -366,14 +362,17 @@ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Boo -- When the first machine halts, the composed machine transitions to Sum.inr hg.tm.q₀. induction steps generalizing cfg haltCfg with | zero => - simp only [EvalsToInTime, Option.bind_eq_bind, step, Function.iterate_zero, id_eq, + -- rw [ReductionSystem.reducesToInSteps.zero_iff] at h + -- rw [ReductionSystem.reducesToInSteps.zero_iff] + -- rw [h] + simp [Option.bind_eq_bind, step, Function.iterate_zero, id_eq, Option.some.injEq] at h ⊢ rw [h] | succ n ih => -- Use the decomposition lemma: cfg evals to some intermediate c in n steps, -- and then c steps to haltCfg -- obtain ⟨c, hc_n, hc_step⟩ := EvalsToInTime.succ_decompose hf.tm.step cfg haltCfg n h - rw [EvalsToInTime.succ_iff] at h ⊢ + rw [ReductionSystem.reducesToInSteps.succ'_iff] at h ⊢ obtain ⟨c, hc_n, hc_step⟩ := h use liftCompCfg_left_or_right hf hg c constructor @@ -384,10 +383,11 @@ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Boo | mk state OTape => cases state with | none => - simp_all + sorry | some q => - rw [← map_liftCompCfg_left_or_right_step hf hg ⟨some q, OTape⟩ (by simp)] - simp only [hc_step, Option.map_some] + sorry + -- rw [← map_liftCompCfg_left_or_right_step hf hg ⟨some q, OTape⟩ (by simp)] + -- simp only [hc_step, Option.map_some] /-- @@ -401,13 +401,13 @@ theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → Li (hf : TimeComputable f) (hg : TimeComputable g) (a : List Bool) (hf_outputsFun : - EvalsToWithinTime hf.tm.step + hf.tm.TerminalReductionSystem.reducesToWithinSteps { state := some hf.tm.q₀, OTape := OTape.mk₁ a } - (some { state := none, OTape := OTape.mk₁ (f a) }) + ({ state := none, OTape := OTape.mk₁ (f a) }) (hf.time a.length)) : - EvalsToWithinTime (compComputer hf hg).step + (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ a } - (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) }) + ({ state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) }) (hf.time a.length) := by obtain ⟨steps, hsteps_le, hsteps_eval⟩ := hf_outputsFun use steps @@ -426,20 +426,25 @@ theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → Li theorem comp_right_simulation {f : List Bool → List Bool} {g : List Bool → List Bool} (hf : TimeComputable f) (hg : TimeComputable g) - (x : hg.tm.Cfg) (y : Option hg.tm.Cfg) (m : ℕ) - (h : EvalsToWithinTime hg.tm.step x y m) : - EvalsToWithinTime (compComputer hf hg).step + (x : hg.tm.Cfg) (y : hg.tm.Cfg) (m : ℕ) + (h : hg.tm.TerminalReductionSystem.reducesToWithinSteps x y m) : + (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps (liftCompCfg_right hf hg x) - (Option.map (liftCompCfg_right hf hg) y) + ((liftCompCfg_right hf hg) y) m := by - exact EvalsToWithinTime.map hg.tm.step (compComputer hf hg).step - (liftCompCfg_right hf hg) (map_liftCompCfg_right_step hf hg) x y m h + refine Cslib.ReductionSystem.reducesToWithinSteps.map (liftCompCfg_right hf hg) ?_ h + intro a b hab + -- hab : hg.tm.step a = some b (this is Red for TerminalReductionSystem.Option) + -- Need: (compComputer hf hg).step (liftCompCfg_right hf hg a) = some (liftCompCfg_right hf hg b) + have h1 := map_liftCompCfg_right_step hf hg a + rw [hab, Option.map_some] at h1 + exact h1.symm lemma output_length_le_input_length_add_time (tm : BinTM0) (l l' : List Bool) (t : ℕ) - (h : tm.OutputsWithinTime l (some l') t) : + (h : tm.OutputsWithinTime l l' t) : l'.length ≤ max 1 l.length + t := by unfold OutputsWithinTime at h obtain ⟨steps, hsteps_le, hevals⟩ := h @@ -485,31 +490,30 @@ def TimeComputable.comp have hg_outputsFun := hg.outputsFun (f a) simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, Option.map_some, haltCfg] at hg_outputsFun hf_outputsFun ⊢ - -- The computer evals a to f a in time hf.time a - have h_a_evalsTo_f_a : - EvalsToWithinTime (compComputer hf hg).step + -- The computer reduces a to f a in time hf.time a + have h_a_reducesTo_f_a : + (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps { state := some (Sum.inl hf.tm.q₀), OTape := OTape.mk₁ a } - (some { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) }) + { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) } (hf.time a.length) := comp_left_simulation hf hg a hf_outputsFun - have h_f_a_evalsTo_g_f_a : - EvalsToWithinTime (compComputer hf hg).step + have h_f_a_reducesTo_g_f_a : + (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps { state := some (Sum.inr hg.tm.q₀), OTape := OTape.mk₁ (f a) } - (some { state := none, OTape := OTape.mk₁ (g (f a)) }) + { state := none, OTape := OTape.mk₁ (g (f a)) } (hg.time (f a).length) := by -- Use the simulation lemma for the second machine have := comp_right_simulation hf hg { state := some hg.tm.q₀, OTape := OTape.mk₁ (f a) } - (some { state := none, OTape := OTape.mk₁ (g (f a)) }) + { state := none, OTape := OTape.mk₁ (g (f a)) } (hg.time (f a).length) hg_outputsFun - simp only [liftCompCfg_right, Option.map_some] at this + simp only [liftCompCfg_right] at this exact this - have h_a_evalsTo_g_f_a := - EvalsToWithinTime.trans - (compComputer hf hg).step _ _ _ _ _ h_a_evalsTo_f_a h_f_a_evalsTo_g_f_a - apply EvalsToWithinTime.mono_time _ _ _ h_a_evalsTo_g_f_a - nth_rw 1 [← add_comm] + have h_a_reducesTo_g_f_a := + Cslib.ReductionSystem.reducesToWithinSteps.trans + h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a + apply Cslib.ReductionSystem.reducesToWithinSteps.mono_steps h_a_reducesTo_g_f_a apply add_le_add · omega · apply h_mono diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 02d65ef2..0e4bb300 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -69,21 +69,182 @@ inductive ReductionSystem.reducesToInSteps lemma ReductionSystem.reducesToInSteps.trans {rs : ReductionSystem Term} {a b c : Term} {n m : ℕ} (h₁ : reducesToInSteps rs a b n) (h₂ : reducesToInSteps rs b c m) : reducesToInSteps rs a c (n + m) := by - sorry + induction h₁ with + | refl _ => simp only [Nat.zero_add]; exact h₂ + | cons t t' t'' k h_red _ ih => + simp only [Nat.add_right_comm] + exact reducesToInSteps.cons t t' c (k + m) h_red (ih h₂) + +lemma ReductionSystem.reducesToInSteps.zero {rs : ReductionSystem Term} {a b : Term} + (h : reducesToInSteps rs a b 0) : + a = b := by + cases h + rfl + +@[simp] +lemma ReductionSystem.reducesToInSteps.zero_iff {rs : ReductionSystem Term} {a b : Term} : + reducesToInSteps rs a b 0 ↔ a = b := by + constructor + · exact reducesToInSteps.zero + · intro h; subst h; exact reducesToInSteps.refl a + lemma ReductionSystem.reducesToInSteps.succ {rs : ReductionSystem Term} {a b : Term} {n : ℕ} (h : reducesToInSteps rs a b (n + 1)) : ∃ t', rs.Red a t' ∧ reducesToInSteps rs t' b n := by - sorry + cases h with + | cons _ t' _ _ h_red h_steps => exact ⟨t', h_red, h_steps⟩ --- TODO iff +lemma ReductionSystem.reducesToInSteps.succ_iff {rs : ReductionSystem Term} {a b : Term} {n : ℕ} : + reducesToInSteps rs a b (n + 1) ↔ ∃ t', rs.Red a t' ∧ reducesToInSteps rs t' b n := by + constructor + · exact ReductionSystem.reducesToInSteps.succ + · rintro ⟨t', h_red, h_steps⟩ + exact ReductionSystem.reducesToInSteps.cons a t' b n h_red h_steps lemma ReductionSystem.reducesToInSteps.succ' {rs : ReductionSystem Term} {a b : Term} {n : ℕ} (h : reducesToInSteps rs a b (n + 1)) : ∃ t', reducesToInSteps rs a t' n ∧ rs.Red t' b := by - sorry + induction n generalizing a b with + | zero => + obtain ⟨t', h_red, h_steps⟩ := succ h + rw [zero_iff] at h_steps + subst h_steps + exact ⟨a, reducesToInSteps.refl a, h_red⟩ + | succ k ih => + obtain ⟨t', h_red, h_steps⟩ := succ h + obtain ⟨t'', h_steps', h_red'⟩ := ih h_steps + exact ⟨t'', reducesToInSteps.cons a t' t'' k h_red h_steps', h_red'⟩ + +lemma ReductionSystem.reducesToInSteps.succ'_iff + {rs : ReductionSystem Term} {a b : Term} {n : ℕ} : + reducesToInSteps rs a b (n + 1) ↔ ∃ t', reducesToInSteps rs a t' n ∧ rs.Red t' b := by + constructor + · exact succ' + · rintro ⟨t', h_steps, h_red⟩ + have h_one : reducesToInSteps rs t' b 1 := cons t' b b 0 h_red (refl b) + have := trans h_steps h_one + simp only [Nat.add_one] at this + exact this + +lemma ReductionSystem.reducesToInSteps.small_change + {rs : ReductionSystem Term} {a b : Term} (h : Term → ℕ) + (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1) + (m : ℕ) + (hevals : rs.reducesToInSteps a b m) : + h b ≤ h a + m := by + induction hevals with + | refl _ => simp + | cons t t' t'' k h_red _ ih => + have h_step' := h_step t t' h_red + omega + +/-- +If `g` is a homomorphism from `rs` to `rs'` (i.e., it preserves the reduction relation), +then `reducesToInSteps` is preserved under `g`. +-/ +lemma ReductionSystem.reducesToInSteps.map {Term Term' : Type*} + {rs : ReductionSystem Term} {rs' : ReductionSystem Term'} + (g : Term → Term') (hg : ∀ a b, rs.Red a b → rs'.Red (g a) (g b)) + {a b : Term} {n : ℕ} + (h : reducesToInSteps rs a b n) : + reducesToInSteps rs' (g a) (g b) n := by + induction h with + | refl t => exact reducesToInSteps.refl (g t) + | cons t t' t'' m h_red h_steps ih => + exact reducesToInSteps.cons (g t) (g t') (g t'') m (hg t t' h_red) ih + +def ReductionSystem.reducesToWithinSteps (rs : ReductionSystem Term) (a b : Term) (n : ℕ) : Prop := + ∃ m ≤ n, reducesToInSteps rs a b m + +/-- Reflexivity of `reducesToWithinSteps` in 0 steps. -/ +lemma ReductionSystem.reducesToWithinSteps.refl {rs : ReductionSystem Term} (a : Term) : + reducesToWithinSteps rs a a 0 := by + use 0 + exact ⟨Nat.le_refl 0, reducesToInSteps.refl a⟩ --- TODO iff +/-- Transitivity of `reducesToWithinSteps` in the sum of the step bounds. -/ +@[trans] +lemma ReductionSystem.reducesToWithinSteps.trans {rs : ReductionSystem Term} + {a b c : Term} {n₁ n₂ : ℕ} + (h₁ : reducesToWithinSteps rs a b n₁) (h₂ : reducesToWithinSteps rs b c n₂) : + reducesToWithinSteps rs a c (n₁ + n₂) := by + obtain ⟨m₁, hm₁, hevals₁⟩ := h₁ + obtain ⟨m₂, hm₂, hevals₂⟩ := h₂ + use m₁ + m₂ + constructor + · omega + · exact reducesToInSteps.trans hevals₁ hevals₂ + +/-- Monotonicity of `reducesToWithinSteps` in the step bound. -/ +lemma ReductionSystem.reducesToWithinSteps.mono_steps {rs : ReductionSystem Term} + {a b : Term} {n₁ n₂ : ℕ} + (h : reducesToWithinSteps rs a b n₁) (hn : n₁ ≤ n₂) : + reducesToWithinSteps rs a b n₂ := by + obtain ⟨m, hm, hevals⟩ := h + use m + constructor + · omega + · exact hevals + +/-- If `h : Term → ℕ` increases by at most 1 on each step of `rs`, +then the value of `h` at the output is at most `h` at the input plus the step bound. -/ +lemma ReductionSystem.reducesToWithinSteps.small_change {rs : ReductionSystem Term} + {a b : Term} (h : Term → ℕ) + (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1) + (n : ℕ) + (hevals : reducesToWithinSteps rs a b n) : + h b ≤ h a + n := by + obtain ⟨m, hm, hevals_m⟩ := hevals + have := reducesToInSteps.small_change h h_step m hevals_m + omega + +/-- +If `g` is a homomorphism from `rs` to `rs'` (i.e., it preserves the reduction relation), +then `reducesToWithinSteps` is preserved under `g`. +-/ +lemma ReductionSystem.reducesToWithinSteps.map {Term Term' : Type*} + {rs : ReductionSystem Term} {rs' : ReductionSystem Term'} + (g : Term → Term') (hg : ∀ a b, rs.Red a b → rs'.Red (g a) (g b)) + {a b : Term} {n : ℕ} + (h : reducesToWithinSteps rs a b n) : + reducesToWithinSteps rs' (g a) (g b) n := by + obtain ⟨m, hm, hevals⟩ := h + exact ⟨m, hm, reducesToInSteps.map g hg hevals⟩ + +/-- A single reduction step gives `reducesToWithinSteps` with bound 1. -/ +lemma ReductionSystem.reducesToWithinSteps.single {rs : ReductionSystem Term} + {a b : Term} (h : rs.Red a b) : + reducesToWithinSteps rs a b 1 := by + use 1 + constructor + · exact Nat.le_refl 1 + · exact reducesToInSteps.cons a b b 0 h (reducesToInSteps.refl b) + +/-- `reducesToInSteps` implies `reducesToWithinSteps` with the same bound. -/ +lemma ReductionSystem.reducesToWithinSteps.of_reducesToInSteps {rs : ReductionSystem Term} + {a b : Term} {n : ℕ} + (h : reducesToInSteps rs a b n) : + reducesToWithinSteps rs a b n := + ⟨n, Nat.le_refl n, h⟩ + +/-- Zero steps means the terms are equal. -/ +lemma ReductionSystem.reducesToWithinSteps.zero {rs : ReductionSystem Term} {a b : Term} + (h : reducesToWithinSteps rs a b 0) : + a = b := by + obtain ⟨m, hm, hevals⟩ := h + have : m = 0 := Nat.le_zero.mp hm + subst this + exact reducesToInSteps.zero hevals + +@[simp] +lemma ReductionSystem.reducesToWithinSteps.zero_iff {rs : ReductionSystem Term} {a b : Term} : + reducesToWithinSteps rs a b 0 ↔ a = b := by + constructor + · exact reducesToWithinSteps.zero + · intro h + subst h + exact reducesToWithinSteps.refl a end Steps From 4587a743f50ce622c9c4ed450e933a9444d272e3 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 11:12:15 -0800 Subject: [PATCH 06/13] claude: remove sorries --- .../Machines/SingleTapeTuring/Basic.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 57a65479..d646cbf2 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -383,11 +383,15 @@ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Boo | mk state OTape => cases state with | none => - sorry + -- c is in halting state, but step of halting state is none, contradiction + simp only [TerminalReductionSystem, Cslib.TerminalReductionSystem.Option, step] at hc_step + cases hc_step | some q => - sorry - -- rw [← map_liftCompCfg_left_or_right_step hf hg ⟨some q, OTape⟩ (by simp)] - -- simp only [hc_step, Option.map_some] + -- Use the lifting lemma + have h1 := map_liftCompCfg_left_or_right_step hf hg ⟨some q, OTape⟩ (by simp) + simp only [TerminalReductionSystem, Cslib.TerminalReductionSystem.Option] at hc_step ⊢ + rw [hc_step, Option.map_some] at h1 + exact h1.symm /-- From 35558b849668ae41e477da427e8e53f3f94ea363 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 11:15:05 -0800 Subject: [PATCH 07/13] delete evals junk --- .../Semantics/ReductionSystem/Basic.lean | 160 ------------------ 1 file changed, 160 deletions(-) diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index 0e4bb300..fc01c18d 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -260,166 +260,6 @@ def TerminalReductionSystem.Option {σ : Type*} (f : σ → Option σ) : Termina intros t t' h_terminal h_red simp [h_terminal] at h_red - --- TODO refactor the contents of this section into ReductionSystem --- then delete them -section EvalsToJunk - - - -/-- `f` eventually reaches `b` when repeatedly evaluated on `a`, in exactly `steps` steps. -/ -def EvalsToInTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (steps : ℕ) : Prop := - (· >>= f)^[steps] a = b - -/-- Reflexivity of `EvalsTo` in 0 steps. -/ -lemma EvalsToInTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : EvalsToInTime f a (some a) 0 := - rfl - -/-- Transitivity of `EvalsTo` in the sum of the numbers of steps. -/ -@[trans] -lemma EvalsToInTime.trans {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (c : Option σ) - (steps₁ steps₂ : ℕ) (h₁ : EvalsToInTime f a b steps₁) (h₂ : EvalsToInTime f b c steps₂) : - EvalsToInTime f a c (steps₂ + steps₁) := by - simp only [EvalsToInTime] at *; rw [Function.iterate_add_apply, h₁, h₂] - -/-- If we evaluate to some state in n+1 steps, there is an intermediate state - that we reach in n steps, and then one more step reaches the final state. -/ -lemma EvalsToInTime.succ_decompose {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) - (n : ℕ) (h : EvalsToInTime f a (some b) (n + 1)) : - ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := by - simp only [EvalsToInTime, Function.iterate_succ_apply'] at h - match hc' : (· >>= f)^[n] (some a) with - | none => simp_all - | some c => exact ⟨c, hc', by simp_all⟩ - -lemma EvalsToInTime.succ_iff {σ : Type*} (f : σ → Option σ) (a : σ) (b : σ) (n : ℕ) : - EvalsToInTime f a (some b) (n + 1) ↔ ∃ c : σ, EvalsToInTime f a (some c) n ∧ f c = some b := - ⟨succ_decompose f a b n, fun ⟨_, hc_eval, hc_step⟩ => by - simp only [EvalsToInTime, Function.iterate_succ_apply'] at hc_eval ⊢; - rw [hc_eval]; exact hc_step⟩ - -theorem Turing.BinTM0.EvalsToInTime.congr.extracted_1_2.{u_2, u_1} - {σ : Type u_1} {σ' : Type u_2} (f : σ → Option σ) - (f' : σ' → Option σ') (g : σ → σ') - (hg : ∀ (x : σ), Option.map g (f x) = f' (g x)) (n : ℕ) (a : σ) : - (Option.map g ((flip Option.bind f)^[n] (some a))).bind f' = - ((flip Option.bind f)^[n] (some a)).bind fun a ↦ f' (g a) := by - induction n with - | zero => simp - | succ n ih => - simp only [Function.iterate_succ_apply, flip, Option.bind_some, <- hg] at ih ⊢ - grind - - - - - -/-- -If `f` is homomorphic to `f'` via `g`, then if `f` evals to `b` from `a` in `steps` steps, -then `f'` evals to `g b` from `g a` in `steps` steps. --/ -lemma EvalsToInTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') - (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) - (a : σ) (b : Option σ) - (steps : ℕ) - (h : EvalsToInTime f a b steps) : EvalsToInTime f' (g a) (Option.map g b) steps := by - induction steps generalizing a b with - | zero => - simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq] at h ⊢ - subst h - rfl - | succ n ih => - simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_succ_apply', - forall_eq'] at h ih ⊢ - subst h - rw [ih] - clear ih - simp only [Option.map_bind, Function.comp_apply, hg] - exact Turing.BinTM0.EvalsToInTime.congr.extracted_1_2 f f' g hg n a - -/-- -If `h : σ → ℕ` increases by at most 1 on each step of `f`, -then the value of `h` at the output after `steps` steps is at most `h` at the input plus `steps`. --/ -lemma EvalsToInTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) - (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) - (a : σ) (b : σ) - (steps : ℕ) - (hevals : EvalsToInTime f a b steps) : - h b ≤ h a + steps := by - induction steps generalizing a b with - | zero => - simp only [EvalsToInTime, Option.bind_eq_bind, Function.iterate_zero, id_eq, Option.some.injEq, - add_zero] at hevals ⊢ - subst hevals - exact Nat.le_refl (h a) - | succ n ih => - rw [EvalsToInTime.succ_iff] at hevals - obtain ⟨c, hevals_n, h_step_eq⟩ := hevals - specialize ih a c hevals_n - specialize h_step c b h_step_eq - omega - - --- m -> step_bound -/-- `f` eventually reaches `b` in at most `m` steps when repeatedly -evaluated on `a`. -/ -def EvalsToWithinTime {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) (m : ℕ) : Prop := - ∃ steps ≤ m, EvalsToInTime f a b steps - -/-- Reflexivity of `EvalsToWithinTime` in 0 steps. -/ -def EvalsToWithinTime.refl {σ : Type*} (f : σ → Option σ) (a : σ) : - EvalsToWithinTime f a (some a) 0 := by - use 0 - exact if_false_right.mp rfl - -/-- Transitivity of `EvalsToWithinTime` in the sum of the numbers of steps. -/ -@[trans] -def EvalsToWithinTime.trans {σ : Type*} (f : σ → Option σ) (m₁ : ℕ) (m₂ : ℕ) (a : σ) (b : σ) - (c : Option σ) (h₁ : EvalsToWithinTime f a b m₁) (h₂ : EvalsToWithinTime f b c m₂) : - EvalsToWithinTime f a c (m₂ + m₁) := by - obtain ⟨steps₁, hsteps₁, hevals₁⟩ := h₁ - obtain ⟨steps₂, hsteps₂, hevals₂⟩ := h₂ - use steps₂ + steps₁ - constructor - · omega - · exact EvalsToInTime.trans f a b c steps₁ steps₂ hevals₁ hevals₂ - -def EvalsToWithinTime.map {σ σ' : Type*} (f : σ → Option σ) (f' : σ' → Option σ') - (g : σ → σ') (hg : ∀ x, Option.map g (f x) = f' (g x)) - (a : σ) (b : Option σ) - (m : ℕ) - (h : EvalsToWithinTime f a b m) : EvalsToWithinTime f' (g a) (Option.map g b) m := by - obtain ⟨steps, hsteps, hevals⟩ := h - use steps - constructor - · exact hsteps - · exact EvalsToInTime.map f f' g hg a b steps hevals - -/-- -Monotonicity of `EvalsToWithinTime` in the time bound. --/ -def EvalsToWithinTime.mono_time {σ : Type*} (f : σ → Option σ) (a : σ) (b : Option σ) - {m₁ m₂ : ℕ} (h : EvalsToWithinTime f a b m₁) (hm : m₁ ≤ m₂) : EvalsToWithinTime f a b m₂ := by - obtain ⟨steps, hsteps, hevals⟩ := h - use steps - simp_all only - simp - omega - -lemma EvalsToWithinTime.small_change {σ : Type*} (f : σ → Option σ) (h : σ → ℕ) - (h_step : ∀ a b, f a = some b → h b ≤ h a + 1) - (a : σ) (b : σ) - (m : ℕ) - (hevals : EvalsToWithinTime f a (some b) m) : - h b ≤ h a + m := by - obtain ⟨steps, hsteps, hevals_steps⟩ := hevals - have := EvalsToInTime.small_change f h h_step a b steps hevals_steps - omega - - -end EvalsToJunk - open Lean Elab Meta Command Term -- thank you to Kyle Miller for this: From 1ef61821f4b24f81e8bc0bd7e76e7f79de35c26d Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 13:17:52 -0800 Subject: [PATCH 08/13] clean whitespace --- .../Machines/SingleTapeTuring/Basic.lean | 57 ++++++++----------- Cslib/Foundations/Data/OTape.lean | 2 +- 2 files changed, 26 insertions(+), 33 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index d646cbf2..9286d79e 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -52,7 +52,6 @@ structure BinTM0 where to a Stmt to invoke, and optionally a new state (none for halt) -/ (M : Λ → (Option Bool) → (Turing.BinTM0.Stmt × Option Λ)) - namespace BinTM0 section @@ -110,7 +109,7 @@ which maps a configuration to its next configuration if it exists. def TerminalReductionSystem (tm : BinTM0) : Cslib.TerminalReductionSystem (tm.Cfg) := TerminalReductionSystem.Option tm.step -noncomputable def Cfg.space_used (tm : BinTM0) (cfg : tm.Cfg) : ℕ := +def Cfg.space_used (tm : BinTM0) (cfg : tm.Cfg) : ℕ := cfg.OTape.space_used lemma Cfg.space_used_initCfg (tm : BinTM0) (s : List Bool) : @@ -149,8 +148,7 @@ structure Computable (f : List Bool → List Bool) where /-- the underlying bundled TM0 -/ tm : BinTM0 /-- a proof this machine outputsInTime `f` -/ - outputsFun : - ∀ a, tm.Outputs a (f a) + outputsFun : ∀ a, tm.Outputs a (f a) /-- A Turing machine + a time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ @@ -160,12 +158,7 @@ structure TimeComputable (f : List Bool → List Bool) where /-- a time function -/ time : ℕ → ℕ /-- proof this machine outputsInTime `f` in at most `time(input.length)` steps -/ - outputsFun : - ∀ a, - tm.OutputsWithinTime - a - ((f a)) - (time a.length) + outputsFun : ∀ a, tm.OutputsWithinTime a (f a) (time a.length) /-- A Turing machine computing the identity. -/ def idComputer : BinTM0 where @@ -173,7 +166,7 @@ def idComputer : BinTM0 where q₀ := PUnit.unit M := fun _ b => ⟨(b, none), none⟩ -noncomputable section +section -- TODO switch to where syntax /-- A proof that the identity map on α is computable in time. -/ @@ -181,7 +174,8 @@ def TimeComputable.id : TimeComputable id := ⟨idComputer, fun _ => 1, fun x => by refine ⟨1, le_refl 1, ?_⟩ -- Need to show reducesToInSteps for 1 step - refine Cslib.ReductionSystem.reducesToInSteps.cons _ _ _ 0 ?_ (Cslib.ReductionSystem.reducesToInSteps.refl _) + refine Cslib.ReductionSystem.reducesToInSteps.cons _ _ _ 0 ?_ + (Cslib.ReductionSystem.reducesToInSteps.refl _) -- Show the single step reduction: step (init x) = some (halt x) simp only [TerminalReductionSystem, Cslib.TerminalReductionSystem.Option, initCfg, haltCfg, idComputer, step, OTape.move?] @@ -220,15 +214,13 @@ def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} } lemma compComputer_q₀_eq (f : List Bool → List Bool) (g : List Bool → List Bool) - (hf : TimeComputable f) - (hg : TimeComputable g) : + (hf : TimeComputable f) (hg : TimeComputable g) : (compComputer hf hg).q₀ = Sum.inl hf.tm.q₀ := rfl /-- Lift a config over a tm to a config over the comp -/ def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : TimeComputable f) - (hg : TimeComputable g) + (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hf.tm.Cfg) : (compComputer hf hg).Cfg := { @@ -237,8 +229,7 @@ def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} } def liftCompCfg_right {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : TimeComputable f) - (hg : TimeComputable g) + (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hg.tm.Cfg) : (compComputer hf hg).Cfg := { @@ -249,8 +240,7 @@ def liftCompCfg_right {f : List Bool → List Bool} {g : List Bool → List Bool theorem map_liftCompCfg_left_step {f : List Bool → List Bool} {g : List Bool → List Bool} (hf : TimeComputable f) (hg : TimeComputable g) - (x : hf.tm.Cfg) - (hx : ∀ cfg, hf.tm.step x = some cfg → cfg.state.isSome) : + (x : hf.tm.Cfg) (hx : ∀ cfg, hf.tm.step x = some cfg → cfg.state.isSome) : Option.map (liftCompCfg_left hf hg) (hf.tm.step x) = (compComputer hf hg).step (liftCompCfg_left hf hg x) := by cases x with @@ -312,8 +302,7 @@ theorem comp_transition_to_right {f : List Bool → List Bool} {g : List Bool /-- Helper: lifting to Sum.inl and transitioning to Sum.inr on halt -/ def liftCompCfg_left_or_right {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : TimeComputable f) - (hg : TimeComputable g) + (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hf.tm.Cfg) : (compComputer hf hg).Cfg := match cfg.state with @@ -347,12 +336,11 @@ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Boo (cfg : hf.tm.Cfg) (hcfg : cfg.state.isSome) (haltCfg : hf.tm.Cfg) - -- (haltCfg_state : haltCfg.state = none) (steps : ℕ) - (h : hf.tm.TerminalReductionSystem.reducesToInSteps cfg ( haltCfg) steps) : + (h : hf.tm.TerminalReductionSystem.reducesToInSteps cfg haltCfg steps) : (compComputer hf hg).TerminalReductionSystem.reducesToInSteps (liftCompCfg_left_or_right hf hg cfg) - ( (liftCompCfg_left_or_right hf hg haltCfg)) + (liftCompCfg_left_or_right hf hg haltCfg) steps := by -- Proof by induction on steps. -- Key insight: liftCompCfg_left_or_right maps: @@ -365,8 +353,7 @@ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Boo -- rw [ReductionSystem.reducesToInSteps.zero_iff] at h -- rw [ReductionSystem.reducesToInSteps.zero_iff] -- rw [h] - simp [Option.bind_eq_bind, step, Function.iterate_zero, id_eq, - Option.some.injEq] at h ⊢ + simp only [ReductionSystem.reducesToInSteps.zero_iff] at h ⊢ rw [h] | succ n ih => -- Use the decomposition lemma: cfg evals to some intermediate c in n steps, @@ -483,8 +470,7 @@ then from the intermediate state to the final state. -/ def TimeComputable.comp {f : List Bool → List Bool} {g : List Bool → List Bool} - (hf : TimeComputable f) - (hg : TimeComputable g) + (hf : TimeComputable f) (hg : TimeComputable g) (h_mono : Monotone hg.time) : (TimeComputable (g ∘ f)) where tm := compComputer hf hg @@ -493,7 +479,7 @@ def TimeComputable.comp have hf_outputsFun := hf.outputsFun a have hg_outputsFun := hg.outputsFun (f a) simp only [OutputsWithinTime, initCfg, compComputer_q₀_eq, Function.comp_apply, - Option.map_some, haltCfg] at hg_outputsFun hf_outputsFun ⊢ + haltCfg] at hg_outputsFun hf_outputsFun ⊢ -- The computer reduces a to f a in time hf.time a have h_a_reducesTo_f_a : (compComputer hf hg).TerminalReductionSystem.reducesToWithinSteps @@ -529,11 +515,18 @@ end /-! ## Polynomial Time Computability -This section defines polynomial time computable functions on Turing machines. +This section defines polynomial time computable functions on Turing machines, +and proves that +* The identity function is polynomial time computable +* The composition of two polynomial time computable functions is polynomial time computable + + -/ section PolyTime +-- TODO noncomputable due to use of Polynomial +-- perhaps could we switch to one of those computable polynomial representations? /-- A Turing machine + a polynomial time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ structure PolyTimeComputable (f : List Bool → List Bool) extends TimeComputable f where @@ -555,7 +548,7 @@ noncomputable def PolyTimeComputable.comp {f : List Bool → List Bool} {g : List Bool → List Bool} (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) - -- all Nat polynomials are monotone, but the tighter internal bound maybe is not + -- all Nat polynomials are monotone, but the tighter internal bound maybe is not, awkwardly (h_mono : Monotone hg.time) : PolyTimeComputable (g ∘ f) where toTimeComputable := TimeComputable.comp hf.toTimeComputable hg.toTimeComputable h_mono diff --git a/Cslib/Foundations/Data/OTape.lean b/Cslib/Foundations/Data/OTape.lean index f2c09213..b2de4065 100644 --- a/Cslib/Foundations/Data/OTape.lean +++ b/Cslib/Foundations/Data/OTape.lean @@ -79,7 +79,7 @@ def OTape.write {α} : Turing.OTape α → Option α → Turing.OTape α The space used by a OTape is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the OTape -/ -noncomputable def OTape.space_used {α} [Inhabited α] (t : Turing.OTape α) : ℕ := +def OTape.space_used {α} [Inhabited α] (t : Turing.OTape α) : ℕ := 1 + t.left.length + t.right.length lemma OTape.space_used_write {α} [Inhabited α] (t : Turing.OTape α) (a : Option α) : From 6a2d234743a6027f615f9108d7164649edc89a6f Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 13:18:39 -0800 Subject: [PATCH 09/13] TM0 -> SingleTapeTM --- .../Machines/SingleTapeTuring/Basic.lean | 51 ++++++++++--------- 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 9286d79e..730755c4 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -31,17 +31,17 @@ open Cslib namespace Turing -namespace BinTM0 +namespace BinSingleTapeTM /-- A Turing machine "statement" is just a command to move left or right, and write a symbol on the OTape. -/ def Stmt := (Option Bool) × Option (Dir) deriving Inhabited -end BinTM0 +end BinSingleTapeTM -/-- A TM0 over the alphabet of Option Bool (none is blank OTape symbol). -/ -structure BinTM0 where +/-- A SingleTapeTM over the alphabet of Option Bool (none is blank OTape symbol). -/ +structure BinSingleTapeTM where /-- type of state labels -/ (Λ : Type) /-- finiteness of the state type -/ @@ -50,13 +50,13 @@ structure BinTM0 where (q₀ : Λ) /-- Transition function, mapping a state and a head symbol to a Stmt to invoke, and optionally a new state (none for halt) -/ - (M : Λ → (Option Bool) → (Turing.BinTM0.Stmt × Option Λ)) + (M : Λ → (Option Bool) → (Turing.BinSingleTapeTM.Stmt × Option Λ)) -namespace BinTM0 +namespace BinSingleTapeTM section -variable (tm : BinTM0) +variable (tm : BinSingleTapeTM) instance : Inhabited tm.Λ := ⟨tm.q₀⟩ @@ -95,32 +95,33 @@ def step : tm.Cfg → Option tm.Cfg := end /-- The initial configuration corresponding to a list in the input alphabet. -/ -def initCfg (tm : BinTM0) (s : List Bool) : tm.Cfg := ⟨some tm.q₀, OTape.mk₁ s⟩ +def initCfg (tm : BinSingleTapeTM) (s : List Bool) : tm.Cfg := ⟨some tm.q₀, OTape.mk₁ s⟩ /-- The final configuration corresponding to a list in the output alphabet. (We demand that the head halts at the leftmost position of the output.) -/ -def haltCfg (tm : BinTM0) (s : List (Bool)) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ +def haltCfg (tm : BinSingleTapeTM) (s : List (Bool)) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ /-- -The `TerminalReductionSystem` corresponding to a `BinTM0` is defined by the `step` function, +The `TerminalReductionSystem` corresponding to a `BinSingleTapeTM` +is defined by the `step` function, which maps a configuration to its next configuration if it exists. -/ -def TerminalReductionSystem (tm : BinTM0) : Cslib.TerminalReductionSystem (tm.Cfg) := +def TerminalReductionSystem (tm : BinSingleTapeTM) : Cslib.TerminalReductionSystem (tm.Cfg) := TerminalReductionSystem.Option tm.step -def Cfg.space_used (tm : BinTM0) (cfg : tm.Cfg) : ℕ := +def Cfg.space_used (tm : BinSingleTapeTM) (cfg : tm.Cfg) : ℕ := cfg.OTape.space_used -lemma Cfg.space_used_initCfg (tm : BinTM0) (s : List Bool) : +lemma Cfg.space_used_initCfg (tm : BinSingleTapeTM) (s : List Bool) : (tm.initCfg s).space_used = max 1 s.length := by simp [initCfg, Cfg.space_used, OTape.space_used_mk₁] -lemma Cfg.space_used_haltCfg (tm : BinTM0) (s : List Bool) : +lemma Cfg.space_used_haltCfg (tm : BinSingleTapeTM) (s : List Bool) : (tm.haltCfg s).space_used = max 1 s.length := by simp [haltCfg, Cfg.space_used, OTape.space_used_mk₁] -lemma Cfg.space_used_step {tm : BinTM0} (cfg cfg' : tm.Cfg) +lemma Cfg.space_used_step {tm : BinSingleTapeTM} (cfg cfg' : tm.Cfg) (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by obtain ⟨_ | q, tape⟩ := cfg · simp [step] at hstep @@ -135,33 +136,33 @@ lemma Cfg.space_used_step {tm : BinTM0} (cfg cfg' : tm.Cfg) /-- A proof of tm outputting l' when given l. -/ -def Outputs (tm : BinTM0) (l : List (Bool)) (l' : List (Bool)) : Prop := +def Outputs (tm : BinSingleTapeTM) (l : List (Bool)) (l' : List (Bool)) : Prop := tm.TerminalReductionSystem.MRed (initCfg tm l) (haltCfg tm l') /-- A proof of tm outputting l' when given l in at most m steps. -/ -def OutputsWithinTime (tm : BinTM0) (l : List (Bool)) (l' : (List (Bool))) +def OutputsWithinTime (tm : BinSingleTapeTM) (l : List (Bool)) (l' : (List (Bool))) (m : ℕ) := tm.TerminalReductionSystem.reducesToWithinSteps (initCfg tm l) (haltCfg tm l') m /-- A Turing machine + a proof it outputsInTime `f`. -/ structure Computable (f : List Bool → List Bool) where - /-- the underlying bundled TM0 -/ - tm : BinTM0 + /-- the underlying bundled SingleTapeTM -/ + tm : BinSingleTapeTM /-- a proof this machine outputsInTime `f` -/ outputsFun : ∀ a, tm.Outputs a (f a) /-- A Turing machine + a time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ structure TimeComputable (f : List Bool → List Bool) where - /-- the underlying bundled TM0 -/ - tm : BinTM0 + /-- the underlying bundled SingleTapeTM -/ + tm : BinSingleTapeTM /-- a time function -/ time : ℕ → ℕ /-- proof this machine outputsInTime `f` in at most `time(input.length)` steps -/ outputsFun : ∀ a, tm.OutputsWithinTime a (f a) (time a.length) /-- A Turing machine computing the identity. -/ -def idComputer : BinTM0 where +def idComputer : BinSingleTapeTM where Λ := PUnit q₀ := PUnit.unit M := fun _ b => ⟨(b, none), none⟩ @@ -184,7 +185,7 @@ def TimeComputable.id : TimeComputable id := def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} (hf : TimeComputable f) (hg : TimeComputable g) : - BinTM0 := + BinSingleTapeTM := { Λ := hf.tm.Λ ⊕ hg.tm.Λ q₀ := Sum.inl hf.tm.q₀ @@ -434,7 +435,7 @@ theorem comp_right_simulation -lemma output_length_le_input_length_add_time (tm : BinTM0) (l l' : List Bool) (t : ℕ) +lemma output_length_le_input_length_add_time (tm : BinSingleTapeTM) (l l' : List Bool) (t : ℕ) (h : tm.OutputsWithinTime l l' t) : l'.length ≤ max 1 l.length + t := by unfold OutputsWithinTime at h @@ -569,6 +570,6 @@ noncomputable def PolyTimeComputable.comp end PolyTime -end BinTM0 +end BinSingleTapeTM end Turing From 68c6ae4112861f84386e09b5fb291808ac719d3c Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 13:51:41 -0800 Subject: [PATCH 10/13] generalize alphabet --- .../Machines/SingleTapeTuring/Basic.lean | 175 ++++++++++-------- Cslib/Foundations/Data/OTape.lean | 10 +- 2 files changed, 103 insertions(+), 82 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 730755c4..1c958ff3 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -15,15 +15,12 @@ public import Mathlib.Algebra.Polynomial.Eval.Defs /-! # Single-Tape Turing Machine -Defines a single-tape Turing machine over the alphabet of `Option Bool`, +Defines a single-tape Turing machine over the alphabet of `Option α`, where `none` represents a blank OTape symbol. ## TODOs -- Generalize Bool to an arbitrary (finite?) alphabet -- switch transition system to use the `ReductionSystem` framework -- refactor polynomial time to another file -- remove unfold +- refactor polynomial time to another file? -/ @@ -31,17 +28,23 @@ open Cslib namespace Turing -namespace BinSingleTapeTM +variable {α : Type} + +namespace SingleTapeTM /-- A Turing machine "statement" is just a command to move left or right, and write a symbol on the OTape. -/ -def Stmt := (Option Bool) × Option (Dir) +def Stmt (α : Type) := (Option α) × Option Dir deriving Inhabited -end BinSingleTapeTM +end SingleTapeTM -/-- A SingleTapeTM over the alphabet of Option Bool (none is blank OTape symbol). -/ -structure BinSingleTapeTM where +/-- A SingleTapeTM over the alphabet of Option α (none is blank OTape symbol). -/ +structure SingleTapeTM (α) where + /-- Inhabited instance for the alphabet -/ + [Inhabitedα : Inhabited α] + /-- Finiteness of the alphabet -/ + [Fintypeα : Fintype α] /-- type of state labels -/ (Λ : Type) /-- finiteness of the state type -/ @@ -50,13 +53,21 @@ structure BinSingleTapeTM where (q₀ : Λ) /-- Transition function, mapping a state and a head symbol to a Stmt to invoke, and optionally a new state (none for halt) -/ - (M : Λ → (Option Bool) → (Turing.BinSingleTapeTM.Stmt × Option Λ)) + (M : Λ → (Option α) → (Turing.SingleTapeTM.Stmt α × Option Λ)) -namespace BinSingleTapeTM +namespace SingleTapeTM -section +section Cfg -variable (tm : BinSingleTapeTM) +/-! +## Configurations of a Turing Machine + +This section defines the configurations of a Turing machine, +the step function that lets the machine transition from one configuration to the next, +and the intended initial and final configurations. +-/ + +variable (tm : SingleTapeTM α) instance : Inhabited tm.Λ := ⟨tm.q₀⟩ @@ -64,14 +75,18 @@ instance : Inhabited tm.Λ := instance : Fintype tm.Λ := tm.FintypeΛ -instance inhabitedStmt : Inhabited (Stmt) := inferInstance +instance inhabitedStmt : Inhabited (Stmt α) := inferInstance -/-- The type of configurations (functions) corresponding to this TM. -/ +/-- +The configurations of a Turing machine consist of an `Option`al state +(or none for the halting state) +and an OTape representing the tape contents. +-/ structure Cfg : Type where /-- the state of the TM (or none for the halting state) -/ state : Option tm.Λ - /-- the OTape contents, which -/ - OTape : OTape (Bool) + /-- the OTape contents -/ + OTape : OTape (α) deriving Inhabited /-- The step function corresponding to this TM. -/ @@ -92,36 +107,27 @@ def step : tm.Cfg → Option tm.Cfg := q'', -- And OTape updated according to the Stmt (t.write wr).move? dir⟩ -end /-- The initial configuration corresponding to a list in the input alphabet. -/ -def initCfg (tm : BinSingleTapeTM) (s : List Bool) : tm.Cfg := ⟨some tm.q₀, OTape.mk₁ s⟩ +def initCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨some tm.q₀, OTape.mk₁ s⟩ /-- The final configuration corresponding to a list in the output alphabet. (We demand that the head halts at the leftmost position of the output.) -/ -def haltCfg (tm : BinSingleTapeTM) (s : List (Bool)) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ +def haltCfg (tm : SingleTapeTM α) (s : List (α)) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ -/-- -The `TerminalReductionSystem` corresponding to a `BinSingleTapeTM` -is defined by the `step` function, -which maps a configuration to its next configuration if it exists. --/ -def TerminalReductionSystem (tm : BinSingleTapeTM) : Cslib.TerminalReductionSystem (tm.Cfg) := - TerminalReductionSystem.Option tm.step - -def Cfg.space_used (tm : BinSingleTapeTM) (cfg : tm.Cfg) : ℕ := +def Cfg.space_used (tm : SingleTapeTM α) (cfg : tm.Cfg) : ℕ := cfg.OTape.space_used -lemma Cfg.space_used_initCfg (tm : BinSingleTapeTM) (s : List Bool) : +lemma Cfg.space_used_initCfg (tm : SingleTapeTM α) (s : List α) : (tm.initCfg s).space_used = max 1 s.length := by - simp [initCfg, Cfg.space_used, OTape.space_used_mk₁] + simp only [space_used, initCfg, OTape.space_used_mk₁] -lemma Cfg.space_used_haltCfg (tm : BinSingleTapeTM) (s : List Bool) : +lemma Cfg.space_used_haltCfg (tm : SingleTapeTM α) (s : List α) : (tm.haltCfg s).space_used = max 1 s.length := by simp [haltCfg, Cfg.space_used, OTape.space_used_mk₁] -lemma Cfg.space_used_step {tm : BinSingleTapeTM} (cfg cfg' : tm.Cfg) +lemma Cfg.space_used_step {tm : SingleTapeTM α} (cfg cfg' : tm.Cfg) (hstep : tm.step cfg = some cfg') : cfg'.space_used ≤ cfg.space_used + 1 := by obtain ⟨_ | q, tape⟩ := cfg · simp [step] at hstep @@ -134,44 +140,55 @@ lemma Cfg.space_used_step {tm : BinSingleTapeTM} (cfg cfg' : tm.Cfg) have := OTape.space_used_move (tape.write wr) d simp only [Cfg.space_used, OTape.move?, OTape.space_used_write] at this ⊢; exact this +end Cfg + +/-- +The `TerminalReductionSystem` corresponding to a `SingleTapeTM α` +is defined by the `step` function, +which maps a configuration to its next configuration if it exists. +-/ +def TerminalReductionSystem (tm : SingleTapeTM α) : Cslib.TerminalReductionSystem (tm.Cfg) := + TerminalReductionSystem.Option tm.step /-- A proof of tm outputting l' when given l. -/ -def Outputs (tm : BinSingleTapeTM) (l : List (Bool)) (l' : List (Bool)) : Prop := +def Outputs (tm : SingleTapeTM α) (l : List (α)) (l' : List (α)) : Prop := tm.TerminalReductionSystem.MRed (initCfg tm l) (haltCfg tm l') /-- A proof of tm outputting l' when given l in at most m steps. -/ -def OutputsWithinTime (tm : BinSingleTapeTM) (l : List (Bool)) (l' : (List (Bool))) +def OutputsWithinTime (tm : SingleTapeTM α) (l : List (α)) (l' : (List (α))) (m : ℕ) := tm.TerminalReductionSystem.reducesToWithinSteps (initCfg tm l) (haltCfg tm l') m /-- A Turing machine + a proof it outputsInTime `f`. -/ -structure Computable (f : List Bool → List Bool) where +structure Computable (f : List α → List α) where /-- the underlying bundled SingleTapeTM -/ - tm : BinSingleTapeTM + tm : SingleTapeTM α /-- a proof this machine outputsInTime `f` -/ outputsFun : ∀ a, tm.Outputs a (f a) /-- A Turing machine + a time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ -structure TimeComputable (f : List Bool → List Bool) where +structure TimeComputable (f : List α → List α) where /-- the underlying bundled SingleTapeTM -/ - tm : BinSingleTapeTM + tm : SingleTapeTM α /-- a time function -/ time : ℕ → ℕ /-- proof this machine outputsInTime `f` in at most `time(input.length)` steps -/ outputsFun : ∀ a, tm.OutputsWithinTime a (f a) (time a.length) +section + +variable [Inhabited α] [Fintype α] + /-- A Turing machine computing the identity. -/ -def idComputer : BinSingleTapeTM where +def idComputer : SingleTapeTM α where Λ := PUnit q₀ := PUnit.unit M := fun _ b => ⟨(b, none), none⟩ -section - -- TODO switch to where syntax /-- A proof that the identity map on α is computable in time. -/ -def TimeComputable.id : TimeComputable id := +def TimeComputable.id : TimeComputable (α := α) id := ⟨idComputer, fun _ => 1, fun x => by refine ⟨1, le_refl 1, ?_⟩ -- Need to show reducesToInSteps for 1 step @@ -182,10 +199,10 @@ def TimeComputable.id : TimeComputable id := idComputer, step, OTape.move?] congr 1⟩ -def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} +def compComputer {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) : - BinSingleTapeTM := + SingleTapeTM α := { Λ := hf.tm.Λ ⊕ hg.tm.Λ q₀ := Sum.inl hf.tm.q₀ @@ -214,13 +231,13 @@ def compComputer {f : List Bool → List Bool} {g : List Bool → List Bool} | _ => Option.map Sum.inr stmt) } -lemma compComputer_q₀_eq (f : List Bool → List Bool) (g : List Bool → List Bool) +lemma compComputer_q₀_eq (f : List α → List α) (g : List α → List α) (hf : TimeComputable f) (hg : TimeComputable g) : (compComputer hf hg).q₀ = Sum.inl hf.tm.q₀ := rfl /-- Lift a config over a tm to a config over the comp -/ -def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} +def liftCompCfg_left {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hf.tm.Cfg) : (compComputer hf hg).Cfg := @@ -229,7 +246,7 @@ def liftCompCfg_left {f : List Bool → List Bool} {g : List Bool → List Bool} OTape := cfg.OTape } -def liftCompCfg_right {f : List Bool → List Bool} {g : List Bool → List Bool} +def liftCompCfg_right {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hg.tm.Cfg) : (compComputer hf hg).Cfg := @@ -239,7 +256,7 @@ def liftCompCfg_right {f : List Bool → List Bool} {g : List Bool → List Bool } theorem map_liftCompCfg_left_step - {f : List Bool → List Bool} {g : List Bool → List Bool} + {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (x : hf.tm.Cfg) (hx : ∀ cfg, hf.tm.step x = some cfg → cfg.state.isSome) : Option.map (liftCompCfg_left hf hg) (hf.tm.step x) = @@ -269,7 +286,7 @@ theorem map_liftCompCfg_left_step /-- Helper lemma: liftCompCfg_right commutes with step for the second machine -/ theorem map_liftCompCfg_right_step - {f : List Bool → List Bool} {g : List Bool → List Bool} + {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (x : hg.tm.Cfg) : Option.map (liftCompCfg_right hf hg) (hg.tm.step x) = @@ -287,10 +304,9 @@ theorem map_liftCompCfg_right_step | none => simp only [hM, Option.map_some, liftCompCfg_right, Option.map_none] | some q' => simp only [hM, Option.map_some, liftCompCfg_right] -/-- When the first machine would halt, the composed machine transitions to the second machine -/ -theorem comp_transition_to_right {f : List Bool → List Bool} {g : List Bool → List Bool} +theorem comp_transition_to_right {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) - (tp : OTape (Bool)) + (tp : OTape (α)) (q : hf.tm.Λ) (hM : (hf.tm.M q tp.head).2 = none) : (compComputer hf hg).step { state := some (Sum.inl q), OTape := tp } = @@ -302,7 +318,7 @@ theorem comp_transition_to_right {f : List Bool → List Bool} {g : List Bool simp only [hfM_eq] /-- Helper: lifting to Sum.inl and transitioning to Sum.inr on halt -/ -def liftCompCfg_left_or_right {f : List Bool → List Bool} {g : List Bool → List Bool} +def liftCompCfg_left_or_right {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hf.tm.Cfg) : (compComputer hf hg).Cfg := @@ -312,7 +328,7 @@ def liftCompCfg_left_or_right {f : List Bool → List Bool} {g : List Bool → L /-- The lifting function commutes with step, converting halt to transition -/ theorem map_liftCompCfg_left_or_right_step - {f : List Bool → List Bool} {g : List Bool → List Bool} + {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (x : hf.tm.Cfg) (hx : x.state.isSome) : @@ -332,7 +348,7 @@ theorem map_liftCompCfg_left_or_right_step /-- General simulation: if the first machine goes from cfg to halt, the composed machine goes from lifted cfg to Sum.inr hg.tm.q₀ -/ -theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Bool → List Bool} +theorem comp_left_simulation_general {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (cfg : hf.tm.Cfg) (hcfg : cfg.state.isSome) @@ -351,9 +367,6 @@ theorem comp_left_simulation_general {f : List Bool → List Bool} {g : List Boo -- When the first machine halts, the composed machine transitions to Sum.inr hg.tm.q₀. induction steps generalizing cfg haltCfg with | zero => - -- rw [ReductionSystem.reducesToInSteps.zero_iff] at h - -- rw [ReductionSystem.reducesToInSteps.zero_iff] - -- rw [h] simp only [ReductionSystem.reducesToInSteps.zero_iff] at h ⊢ rw [h] | succ n ih => @@ -389,9 +402,9 @@ runs from start (with Sum.inl state) to Sum.inr hg.tm.q₀ (the start of the sec This takes the same number of steps because the halt transition becomes a transition to the second machine. -/ -theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → List Bool} +theorem comp_left_simulation {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) - (a : List Bool) + (a : List α) (hf_outputsFun : hf.tm.TerminalReductionSystem.reducesToWithinSteps { state := some hf.tm.q₀, OTape := OTape.mk₁ a } @@ -416,7 +429,7 @@ theorem comp_left_simulation {f : List Bool → List Bool} {g : List Bool → Li /-- Simulation lemma for the second machine in the composed computer -/ theorem comp_right_simulation - {f : List Bool → List Bool} {g : List Bool → List Bool} + {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (x : hg.tm.Cfg) (y : hg.tm.Cfg) (m : ℕ) (h : hg.tm.TerminalReductionSystem.reducesToWithinSteps x y m) : @@ -426,19 +439,23 @@ theorem comp_right_simulation m := by refine Cslib.ReductionSystem.reducesToWithinSteps.map (liftCompCfg_right hf hg) ?_ h intro a b hab - -- hab : hg.tm.step a = some b (this is Red for TerminalReductionSystem.Option) - -- Need: (compComputer hf hg).step (liftCompCfg_right hf hg a) = some (liftCompCfg_right hf hg b) have h1 := map_liftCompCfg_right_step hf hg a rw [hab, Option.map_some] at h1 exact h1.symm - - - -lemma output_length_le_input_length_add_time (tm : BinSingleTapeTM) (l l' : List Bool) (t : ℕ) +/-- +Lemma about the size blow-up of the output of a Turing machine +relative to its input length and time bound. +This lemma states that the length of the output list is bounded by the time the TM runs +(and the input length). +This is important for guaranteeing that composition of polynomial time Turing machines +remains polynomial time, as the input to the second machine +is bounded by the output length of the first machine. +-/ +lemma output_length_le_input_length_add_time (tm : SingleTapeTM α) (l l' : List α) (t : ℕ) (h : tm.OutputsWithinTime l l' t) : l'.length ≤ max 1 l.length + t := by - unfold OutputsWithinTime at h + simp only [OutputsWithinTime] at h obtain ⟨steps, hsteps_le, hevals⟩ := h replace hevals := hevals.small_change specialize hevals (Cfg.space_used tm) @@ -470,7 +487,7 @@ evals to the intermediate state from the start state and then from the intermediate state to the final state. -/ def TimeComputable.comp - {f : List Bool → List Bool} {g : List Bool → List Bool} + {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) (h_mono : Monotone hg.time) : (TimeComputable (g ∘ f)) where @@ -521,23 +538,27 @@ and proves that * The identity function is polynomial time computable * The composition of two polynomial time computable functions is polynomial time computable +### TODO +Use of mathlib's `Polynomial` type leads to noncomputable definitions here. +Perhaps we could switch to a computable polynomial representation? -/ section PolyTime --- TODO noncomputable due to use of Polynomial --- perhaps could we switch to one of those computable polynomial representations? +variable [Inhabited α] [Fintype α] + + /-- A Turing machine + a polynomial time function + a proof it outputsInTime `f` in at most `time(input.length)` steps. -/ -structure PolyTimeComputable (f : List Bool → List Bool) extends TimeComputable f where +structure PolyTimeComputable (f : List α → List α) extends TimeComputable f where /-- a polynomial time bound -/ poly : Polynomial ℕ /-- proof that this machine outputsInTime `f` in at most `time(input.length)` steps -/ bounds : ∀ n, time n ≤ poly.eval n /-- A proof that the identity map on α is computable in polytime. -/ -noncomputable def PolyTimeComputable.id : @PolyTimeComputable id where +noncomputable def PolyTimeComputable.id : @PolyTimeComputable (α := α) id where toTimeComputable := TimeComputable.id poly := 1 bounds n := by simp only [TimeComputable.id, Polynomial.eval_one, le_refl] @@ -546,7 +567,7 @@ noncomputable def PolyTimeComputable.id : @PolyTimeComputable id where A proof that the composition of two polytime computable functions is polytime computable. -/ noncomputable def PolyTimeComputable.comp - {f : List Bool → List Bool} {g : List Bool → List Bool} + {f : List α → List α} {g : List α → List α} (hf : PolyTimeComputable f) (hg : PolyTimeComputable g) -- all Nat polynomials are monotone, but the tighter internal bound maybe is not, awkwardly @@ -570,6 +591,6 @@ noncomputable def PolyTimeComputable.comp end PolyTime -end BinSingleTapeTM +end SingleTapeTM end Turing diff --git a/Cslib/Foundations/Data/OTape.lean b/Cslib/Foundations/Data/OTape.lean index b2de4065..cad574d1 100644 --- a/Cslib/Foundations/Data/OTape.lean +++ b/Cslib/Foundations/Data/OTape.lean @@ -54,7 +54,7 @@ structure OTape (α : Type) where (right : OList α) deriving Inhabited -def OTape.mk₁ (l : List Bool) : OTape Bool := +def OTape.mk₁ {α} (l : List α) : OTape α := match l with | [] => { head := none, left := OList.empty, right := OList.empty } | h :: t => { head := some h, left := OList.empty, right := OList.map_some t } @@ -79,14 +79,14 @@ def OTape.write {α} : Turing.OTape α → Option α → Turing.OTape α The space used by a OTape is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the OTape -/ -def OTape.space_used {α} [Inhabited α] (t : Turing.OTape α) : ℕ := +def OTape.space_used {α} (t : Turing.OTape α) : ℕ := 1 + t.left.length + t.right.length -lemma OTape.space_used_write {α} [Inhabited α] (t : Turing.OTape α) (a : Option α) : +lemma OTape.space_used_write {α} (t : Turing.OTape α) (a : Option α) : (t.write a).space_used = t.space_used := by rfl -lemma OTape.space_used_mk₁ (l : List Bool) : +lemma OTape.space_used_mk₁ (l : List α) : (OTape.mk₁ l).space_used = max 1 l.length := by cases l with | nil => @@ -95,7 +95,7 @@ lemma OTape.space_used_mk₁ (l : List Bool) : simp [mk₁, space_used, OList.length_empty, OList.length_map_some] omega -lemma OTape.space_used_move {α} [Inhabited α] (t : Turing.OTape α) (d : Dir) : +lemma OTape.space_used_move {α} (t : Turing.OTape α) (d : Dir) : (t.move d).space_used ≤ t.space_used + 1 := by cases d with | left => From 6cb8c862fd8b4c16422a7bc4639b5defb8798947 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 13:58:01 -0800 Subject: [PATCH 11/13] move blowuplemma earlier --- .../Machines/SingleTapeTuring/Basic.lean | 46 +++++++++---------- .../Semantics/ReductionSystem/Basic.lean | 6 +-- 2 files changed, 25 insertions(+), 27 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 1c958ff3..5c31b64f 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -16,7 +16,7 @@ public import Mathlib.Algebra.Polynomial.Eval.Defs # Single-Tape Turing Machine Defines a single-tape Turing machine over the alphabet of `Option α`, -where `none` represents a blank OTape symbol. +where `none` represents a blank `OTape` symbol. ## TODOs @@ -33,7 +33,7 @@ variable {α : Type} namespace SingleTapeTM /-- A Turing machine "statement" is just a command to move - left or right, and write a symbol on the OTape. -/ + left or right, and write a symbol on the `OTape`. -/ def Stmt (α : Type) := (Option α) × Option Dir deriving Inhabited @@ -159,6 +159,26 @@ def OutputsWithinTime (tm : SingleTapeTM α) (l : List (α)) (l' : (List (α))) (m : ℕ) := tm.TerminalReductionSystem.reducesToWithinSteps (initCfg tm l) (haltCfg tm l') m +/-- +This lemma bounds the size blow-up of the output of a Turing machine. +It states that the increase in length of the output over the input is bounded by the runtime. +This is important for guaranteeing that composition of polynomial time Turing machines +remains polynomial time, as the input to the second machine +is bounded by the output length of the first machine. +-/ +lemma output_length_le_input_length_add_time (tm : SingleTapeTM α) (l l' : List α) (t : ℕ) + (h : tm.OutputsWithinTime l l' t) : + l'.length ≤ max 1 l.length + t := by + simp only [OutputsWithinTime] at h + obtain ⟨steps, hsteps_le, hevals⟩ := h + replace hevals := hevals.small_change + specialize hevals (Cfg.space_used tm) + simp only [Cfg.space_used_initCfg, Cfg.space_used_haltCfg] at hevals + suffices l'.length ≤ max 1 l.length + steps + by omega + specialize hevals fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep) + omega + /-- A Turing machine + a proof it outputsInTime `f`. -/ structure Computable (f : List α → List α) where /-- the underlying bundled SingleTapeTM -/ @@ -443,28 +463,6 @@ theorem comp_right_simulation rw [hab, Option.map_some] at h1 exact h1.symm -/-- -Lemma about the size blow-up of the output of a Turing machine -relative to its input length and time bound. -This lemma states that the length of the output list is bounded by the time the TM runs -(and the input length). -This is important for guaranteeing that composition of polynomial time Turing machines -remains polynomial time, as the input to the second machine -is bounded by the output length of the first machine. --/ -lemma output_length_le_input_length_add_time (tm : SingleTapeTM α) (l l' : List α) (t : ℕ) - (h : tm.OutputsWithinTime l l' t) : - l'.length ≤ max 1 l.length + t := by - simp only [OutputsWithinTime] at h - obtain ⟨steps, hsteps_le, hevals⟩ := h - replace hevals := hevals.small_change - specialize hevals (Cfg.space_used tm) - simp only [Cfg.space_used_initCfg, Cfg.space_used_haltCfg] at hevals - suffices l'.length ≤ max 1 l.length + steps - by omega - specialize hevals fun a b hstep ↦ Cfg.space_used_step a b (Option.mem_def.mp hstep) - omega - /-- A composition for TimeComputable. diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index fc01c18d..a53a9f8c 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -249,9 +249,9 @@ lemma ReductionSystem.reducesToWithinSteps.zero_iff {rs : ReductionSystem Term} end Steps /-- -Given a map σ → Option σ, we can construct a terminal reduction system on `σ` -where a term is terminal if it maps to `none` under the given function. -and otherwise is reducible to its `some` value under the given function. +Given a map σ → Option σ, we can construct a terminal reduction system on `σ` where: +* a term is terminal if it maps to `none` under the given function, +* and otherwise is reducible to its `some` value under the given function. -/ def TerminalReductionSystem.Option {σ : Type*} (f : σ → Option σ) : TerminalReductionSystem σ where Red := fun a b => f a = some b From 33d74e8c7f4f3e07effaeef4c192acdeed1692a4 Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 14:06:32 -0800 Subject: [PATCH 12/13] Stmt API --- .../Machines/SingleTapeTuring/Basic.lean | 33 ++++++++++++------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 5c31b64f..20bc37ec 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -20,6 +20,7 @@ where `none` represents a blank `OTape` symbol. ## TODOs +- encoding? - refactor polynomial time to another file? -/ @@ -32,15 +33,24 @@ variable {α : Type} namespace SingleTapeTM -/-- A Turing machine "statement" is just a command to move - left or right, and write a symbol on the `OTape`. -/ -def Stmt (α : Type) := (Option α) × Option Dir +-- TODO make into a structure? +/-- +A Turing machine "statement" is just a `Option`al command to move left or right, +and write a symbol on the `OTape`. +-/ +def Stmt (α : Type) := Option α × Option Dir deriving Inhabited +def Stmt.symbol : Stmt α → Option α + | (symbol, _) => symbol + +def Stmt.movement : Stmt α → Option Dir + | (_, movement) => movement + end SingleTapeTM /-- A SingleTapeTM over the alphabet of Option α (none is blank OTape symbol). -/ -structure SingleTapeTM (α) where +structure SingleTapeTM α where /-- Inhabited instance for the alphabet -/ [Inhabitedα : Inhabited α] /-- Finiteness of the alphabet -/ @@ -86,7 +96,7 @@ structure Cfg : Type where /-- the state of the TM (or none for the halting state) -/ state : Option tm.Λ /-- the OTape contents -/ - OTape : OTape (α) + OTape : OTape α deriving Inhabited /-- The step function corresponding to this TM. -/ @@ -114,7 +124,7 @@ def initCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨some tm.q₀, OT /-- The final configuration corresponding to a list in the output alphabet. (We demand that the head halts at the leftmost position of the output.) -/ -def haltCfg (tm : SingleTapeTM α) (s : List (α)) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ +def haltCfg (tm : SingleTapeTM α) (s : List α) : tm.Cfg := ⟨none, OTape.mk₁ s⟩ def Cfg.space_used (tm : SingleTapeTM α) (cfg : tm.Cfg) : ℕ := cfg.OTape.space_used @@ -151,11 +161,11 @@ def TerminalReductionSystem (tm : SingleTapeTM α) : Cslib.TerminalReductionSyst TerminalReductionSystem.Option tm.step /-- A proof of tm outputting l' when given l. -/ -def Outputs (tm : SingleTapeTM α) (l : List (α)) (l' : List (α)) : Prop := +def Outputs (tm : SingleTapeTM α) (l : List α) (l' : List α) : Prop := tm.TerminalReductionSystem.MRed (initCfg tm l) (haltCfg tm l') /-- A proof of tm outputting l' when given l in at most m steps. -/ -def OutputsWithinTime (tm : SingleTapeTM α) (l : List (α)) (l' : (List (α))) +def OutputsWithinTime (tm : SingleTapeTM α) (l : List α) (l' : List α) (m : ℕ) := tm.TerminalReductionSystem.reducesToWithinSteps (initCfg tm l) (haltCfg tm l') m @@ -326,13 +336,14 @@ theorem map_liftCompCfg_right_step theorem comp_transition_to_right {f : List α → List α} {g : List α → List α} (hf : TimeComputable f) (hg : TimeComputable g) - (tp : OTape (α)) + (tp : OTape α) (q : hf.tm.Λ) (hM : (hf.tm.M q tp.head).2 = none) : (compComputer hf hg).step { state := some (Sum.inl q), OTape := tp } = some { state := some (Sum.inr hg.tm.q₀), - OTape := (tp.write (hf.tm.M q tp.head).1.1).move? (hf.tm.M q tp.head).1.2 } := by - simp only [step, compComputer, hM] + OTape := (tp.write (hf.tm.M q tp.head).1.symbol).move? + (hf.tm.M q tp.head).1.movement } := by + simp only [step, compComputer, hM, Stmt.symbol, Stmt.movement] generalize hfM_eq : hf.tm.M q tp.head = result obtain ⟨⟨wr, dir⟩, nextState⟩ := result simp only [hfM_eq] From 24bd6de239a3ced53eb7d56167b9b2350d7e07ae Mon Sep 17 00:00:00 2001 From: Bolton Bailey Date: Sat, 17 Jan 2026 14:11:59 -0800 Subject: [PATCH 13/13] clean up reduction --- .../Machines/SingleTapeTuring/Basic.lean | 2 +- .../Semantics/ReductionSystem/Basic.lean | 16 +++++++++------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean index 20bc37ec..a5756591 100644 --- a/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/SingleTapeTuring/Basic.lean @@ -181,7 +181,7 @@ lemma output_length_le_input_length_add_time (tm : SingleTapeTM α) (l l' : List l'.length ≤ max 1 l.length + t := by simp only [OutputsWithinTime] at h obtain ⟨steps, hsteps_le, hevals⟩ := h - replace hevals := hevals.small_change + replace hevals := hevals.bounded_increase specialize hevals (Cfg.space_used tm) simp only [Cfg.space_used_initCfg, Cfg.space_used_haltCfg] at hevals suffices l'.length ≤ max 1 l.length + steps diff --git a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean index a53a9f8c..b1b8127c 100644 --- a/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean +++ b/Cslib/Foundations/Semantics/ReductionSystem/Basic.lean @@ -10,9 +10,6 @@ public import Cslib.Init public import Mathlib.Logic.Relation public import Mathlib.Util.Notation3 --- TODO remove this import -public import Mathlib.Algebra.Polynomial.Eval.Defs - @[expose] public section /-! @@ -127,7 +124,7 @@ lemma ReductionSystem.reducesToInSteps.succ'_iff simp only [Nat.add_one] at this exact this -lemma ReductionSystem.reducesToInSteps.small_change +lemma ReductionSystem.reducesToInSteps.bounded_increase {rs : ReductionSystem Term} {a b : Term} (h : Term → ℕ) (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1) (m : ℕ) @@ -154,7 +151,12 @@ lemma ReductionSystem.reducesToInSteps.map {Term Term' : Type*} | cons t t' t'' m h_red h_steps ih => exact reducesToInSteps.cons (g t) (g t') (g t'') m (hg t t' h_red) ih -def ReductionSystem.reducesToWithinSteps (rs : ReductionSystem Term) (a b : Term) (n : ℕ) : Prop := +/-- +`reducesToWithinSteps` is a variant of `reducesToInSteps` that allows for a loose bound. +It states that a term `a` reduces to a term `b` in *at most* `n` steps. +-/ +def ReductionSystem.reducesToWithinSteps (rs : ReductionSystem Term) + (a b : Term) (n : ℕ) : Prop := ∃ m ≤ n, reducesToInSteps rs a b m /-- Reflexivity of `reducesToWithinSteps` in 0 steps. -/ @@ -189,14 +191,14 @@ lemma ReductionSystem.reducesToWithinSteps.mono_steps {rs : ReductionSystem Term /-- If `h : Term → ℕ` increases by at most 1 on each step of `rs`, then the value of `h` at the output is at most `h` at the input plus the step bound. -/ -lemma ReductionSystem.reducesToWithinSteps.small_change {rs : ReductionSystem Term} +lemma ReductionSystem.reducesToWithinSteps.bounded_increase {rs : ReductionSystem Term} {a b : Term} (h : Term → ℕ) (h_step : ∀ a b, rs.Red a b → h b ≤ h a + 1) (n : ℕ) (hevals : reducesToWithinSteps rs a b n) : h b ≤ h a + n := by obtain ⟨m, hm, hevals_m⟩ := hevals - have := reducesToInSteps.small_change h h_step m hevals_m + have := reducesToInSteps.bounded_increase h h_step m hevals_m omega /--