From e1a386e1b884d332992034b0fcd74f2a46e134c7 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 25 Jan 2026 16:07:52 +0100 Subject: [PATCH 1/5] formalization_of_while --- Complexity/Basic.lean | 1 + Complexity/Pop.lean | 36 ++++++++++++++++++++++++++++++++++++ Complexity/While.lean | 41 +++++++++++++++++++++++++---------------- 3 files changed, 62 insertions(+), 16 deletions(-) create mode 100644 Complexity/Pop.lean diff --git a/Complexity/Basic.lean b/Complexity/Basic.lean index b5a64a4..6f7c333 100644 --- a/Complexity/Basic.lean +++ b/Complexity/Basic.lean @@ -2,6 +2,7 @@ import Complexity.Bounds import Complexity.Classes import Complexity.Dyadic import Complexity.MoveUntil +import Complexity.Pop import Complexity.SpaceInTime import Complexity.Successor import Complexity.TapeExtension diff --git a/Complexity/Pop.lean b/Complexity/Pop.lean new file mode 100644 index 0000000..ba4ef53 --- /dev/null +++ b/Complexity/Pop.lean @@ -0,0 +1,36 @@ +import Complexity.AbstractTape +import Complexity.TuringMachine +import Complexity.TapeLemmas +import Complexity.Routines +import Complexity.MoveUntil +import Complexity.TMComposition +import Complexity.WithTapes + +import Mathlib + +def pop_char : TM 1 (Fin 2) SChar := + let σ := fun _ _ => (1, (fun _ => (.blank, .some .right))) + TM.mk σ 0 1 + +--- This is a 1-tape Turing machine that removes the left-most word +--- from the tape. +def pop := (Routines.while (· ≠ .sep) pop_char).seq pop_char + +@[simp] +theorem pop.eval {w : List Char} {ws₁ ws₂ : List (List Char)} : + pop.eval (list_to_tape ∘ [w :: ws₁].get) = + .some (list_to_tape ∘ [ws₁].get) := by + let semantics := fun tapes => (tapes 0). + let tapes : ℕ → Fin 1 → Turing.Tape SChar := + (fun i j => Turing.Tape.mk₁ ((list_to_string (w :: ws₁)).drop i)) + have h_tapes₀ : tapes 0 = (list_to_tape ∘ [w :: ws₁].get) := by + sorry + have h_inner : ∀ i, pop_char.eval (tapes i) = tapes i.succ := by + sorry + let x := Routines.while.eval (condition := (· ≠ .sep)) (tm := pop_char) tapes h_inner + simp at x + rw [← h_tapes₀] + simp [pop, x] + + + sorry diff --git a/Complexity/While.lean b/Complexity/While.lean index 67dd28d..75b272b 100644 --- a/Complexity/While.lean +++ b/Complexity/While.lean @@ -139,21 +139,30 @@ theorem Routines.while.semantics {k : ℕ} {Q Γ : Type*} convert congr_arg (tm_while.transition.step) ht using 1 exact Function.iterate_succ_apply' _ _ _ -def TM.iterate {k : ℕ} {Q Γ} +-- Semantics of Routines.while in terms of `eval.`. +-- Note that this only works for Turing machines that always halt +-- and whose semantics is explicitly given by `semantics`. +@[simp] +theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] - (tm : TM k Q Γ) (tapes : Part (Fin k → Turing.Tape Γ)) : Part (Fin k → Turing.Tape Γ) := - tapes.bind tm.eval + {condition : Γ → Bool} {tm : TM k.succ Q Γ} + (semantics : (Fin k.succ → (Turing.Tape Γ)) → (Fin k.succ → (Turing.Tape Γ))) + (h_inner : ∀ tapes, tm.eval tapes = .some (semantics tapes)) + (tapes : Fin k.succ → Turing.Tape Γ) : + (Routines.while condition tm).eval tapes = + (PartENat.find + fun i => condition (((semantics^[i] tapes) 0).head) + ).map (semantics^[·] tapes) := by + sorry --- @[simp] --- theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} --- [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] --- {condition : Γ → Bool} {tm : TM k.succ Q Γ} --- {tapes₀ : Fin k.succ → Turing.Tape Γ} : --- (Routines.while condition tm).eval tapes₀ = --- (PartENat.find (fun i => --- ((tm.iterate^[i] (.some tapes₀)).map --- (fun tapes' : Fin k.succ → (Turing.Tape Γ) => --- condition (tapes' 0).head)) = Part.some true --- )).map --- fun i => (tm.iterate^[i] (.some tapes₀)) := by --- sorry +@[simp] +theorem Routines.while.eval' {k : ℕ} {Q Γ : Type*} + [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] + {condition : Γ → Bool} {tm : TM k.succ Q Γ} + (tapes_seq : ℕ → (Fin k.succ → (Turing.Tape Γ))) + (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) : + (Routines.while condition tm).eval (tapes_seq 0) = + (PartENat.find + fun i => condition (((tapes_seq i) 0).head) + ).map tapes_seq := by + sorry From 66b2bb9a57f88827dbf1aac52fef7b106114cd85 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 25 Jan 2026 23:15:55 +0100 Subject: [PATCH 2/5] prog --- Complexity/Pop.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Complexity/Pop.lean b/Complexity/Pop.lean index ba4ef53..9bb70f2 100644 --- a/Complexity/Pop.lean +++ b/Complexity/Pop.lean @@ -20,12 +20,13 @@ def pop := (Routines.while (· ≠ .sep) pop_char).seq pop_char theorem pop.eval {w : List Char} {ws₁ ws₂ : List (List Char)} : pop.eval (list_to_tape ∘ [w :: ws₁].get) = .some (list_to_tape ∘ [ws₁].get) := by - let semantics := fun tapes => (tapes 0). let tapes : ℕ → Fin 1 → Turing.Tape SChar := (fun i j => Turing.Tape.mk₁ ((list_to_string (w :: ws₁)).drop i)) have h_tapes₀ : tapes 0 = (list_to_tape ∘ [w :: ws₁].get) := by - sorry + funext i; simp [tapes, list_to_tape] have h_inner : ∀ i, pop_char.eval (tapes i) = tapes i.succ := by + induction with + | zero => sorry let x := Routines.while.eval (condition := (· ≠ .sep)) (tm := pop_char) tapes h_inner simp at x From c46aa3041b259be5ff68998c4f08a89897a19200 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 25 Jan 2026 23:43:06 +0100 Subject: [PATCH 3/5] prog --- Complexity/Pop.lean | 22 ++++++++++++-- Complexity/While.lean | 71 ++++++++++++++++++++++++++++++++++++++++++- 2 files changed, 89 insertions(+), 4 deletions(-) diff --git a/Complexity/Pop.lean b/Complexity/Pop.lean index 9bb70f2..23cabfd 100644 --- a/Complexity/Pop.lean +++ b/Complexity/Pop.lean @@ -9,9 +9,22 @@ import Complexity.WithTapes import Mathlib def pop_char : TM 1 (Fin 2) SChar := - let σ := fun _ _ => (1, (fun _ => (.blank, .some .right))) + let σ := fun state symbols => match state with + | 0 => (1, (fun _ => (.blank, .some .right))) + | 1 => (1, (symbols ·, .none)) TM.mk σ 0 1 +lemma pop_char.inert_after_stop : + pop_char.inert_after_stop := by + intro conf h_is_stopped + ext <;> simp_all [Transition.step, performTapeOps, pop_char] + +@[simp] +lemma pop_char.eval (tape : Turing.Tape SChar) : + pop_char.eval (fun _ => tape) = .some (fun _ => (tape.write .blank).move .right) := by + apply TM.eval_of_transforms + exact TM.transforms_of_inert pop_char _ _ pop_char.inert_after_stop ⟨1, rfl⟩ + --- This is a 1-tape Turing machine that removes the left-most word --- from the tape. def pop := (Routines.while (· ≠ .sep) pop_char).seq pop_char @@ -25,8 +38,11 @@ theorem pop.eval {w : List Char} {ws₁ ws₂ : List (List Char)} : have h_tapes₀ : tapes 0 = (list_to_tape ∘ [w :: ws₁].get) := by funext i; simp [tapes, list_to_tape] have h_inner : ∀ i, pop_char.eval (tapes i) = tapes i.succ := by - induction with - | zero => + intro i + simp [tapes] + + + simp [pop_char, TM.eval, TM.configurations, Transition.step, tapes] sorry let x := Routines.while.eval (condition := (· ≠ .sep)) (tm := pop_char) tapes h_inner simp at x diff --git a/Complexity/While.lean b/Complexity/While.lean index 75b272b..f0c7160 100644 --- a/Complexity/While.lean +++ b/Complexity/While.lean @@ -142,6 +142,24 @@ theorem Routines.while.semantics {k : ℕ} {Q Γ : Type*} -- Semantics of Routines.while in terms of `eval.`. -- Note that this only works for Turing machines that always halt -- and whose semantics is explicitly given by `semantics`. +-- Helper lemma: if tm always halts and semantics describes its behavior, +-- and condition is always true, then the while machine never halts +lemma Routines.while.no_halt_if_condition_always_true {k : ℕ} {Q Γ : Type*} + [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] + (condition : Γ → Bool) + (tm : TM k.succ Q Γ) + (semantics : (Fin k.succ → (Turing.Tape Γ)) → (Fin k.succ → (Turing.Tape Γ))) + (h_inner : ∀ tapes, tm.eval tapes = .some (semantics tapes)) + (tapes : Fin k.succ → Turing.Tape Γ) + (h_always_true : ∀ i, condition ((semantics^[i] tapes) 0).head) : + ∀ t, ((Routines.while condition tm).configurations tapes t).state ≠ + (Routines.while condition tm).stopState := by + -- TODO: Prove by showing the machine is never in state .main 1 + -- Key idea: machine alternates between .main 0 and subroutine states, + -- never reaching .main 1 because condition is always true. + -- This requires an induction argument tracking the state at each step. + sorry + @[simp] theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] @@ -153,6 +171,41 @@ theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} (PartENat.find fun i => condition (((semantics^[i] tapes) 0).head) ).map (semantics^[·] tapes) := by + have h_transforms : ∀ i, tm.transforms (semantics^[i] tapes) (semantics^[i.succ] tapes) := by + intro i + have : semantics (semantics^[i] tapes) = semantics^[i.succ] tapes := by + simp [Function.iterate_succ_apply'] + rw [← this] + exact TM.transforms_of_eval (h_inner (semantics^[i] tapes)) + by_cases h_stops : ∃ m, ¬condition ((semantics^[m] tapes) 0).head + · -- Case: the while loop terminates + let m := Nat.find h_stops + have h_while_transforms : (Routines.while condition tm).transforms tapes (semantics^[m] tapes) := + Routines.while.semantics condition tm (semantics^[·] tapes) h_transforms h_stops + rw [TM.eval_of_transforms h_while_transforms] + simp [Part.map_some, PartENat.find] + -- TODO: Show that Nat.find finds the same value m for both predicates: + -- 1. ((Routines.while condition tm).configurations tapes t).state = (Routines.while condition tm).stopState + -- 2. condition (((semantics^[·] tapes) 0).head) = false (negated in PartENat.find) + -- This requires relating the while machine's execution to the semantics iteration. + sorry + · -- Case: the while loop does not terminate + push_neg at h_stops + have h_no_halt := Routines.while.no_halt_if_condition_always_true condition tm semantics h_inner tapes h_stops + -- TODO: Show both sides are None/undefined using h_no_halt and h_stops + sorry + +-- Helper lemma for eval' version +lemma Routines.while.no_halt_if_condition_always_true' {k : ℕ} {Q Γ : Type*} + [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] + (condition : Γ → Bool) + (tm : TM k.succ Q Γ) + (tapes_seq : ℕ → (Fin k.succ → (Turing.Tape Γ))) + (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) + (h_always_true : ∀ i, condition ((tapes_seq i) 0).head) : + ∀ t, ((Routines.while condition tm).configurations (tapes_seq 0) t).state ≠ + (Routines.while condition tm).stopState := by + -- TODO: Similar proof as no_halt_if_condition_always_true but with explicit tape sequence sorry @[simp] @@ -165,4 +218,20 @@ theorem Routines.while.eval' {k : ℕ} {Q Γ : Type*} (PartENat.find fun i => condition (((tapes_seq i) 0).head) ).map tapes_seq := by - sorry + have h_transforms : ∀ i, tm.transforms (tapes_seq i) (tapes_seq i.succ) := by + intro i + exact TM.transforms_of_eval (h_inner i) + by_cases h_stops : ∃ m, ¬condition ((tapes_seq m) 0).head + · -- Case: the while loop terminates + let m := Nat.find h_stops + have h_while_transforms : (Routines.while condition tm).transforms (tapes_seq 0) (tapes_seq m) := + Routines.while.semantics condition tm tapes_seq h_transforms h_stops + rw [TM.eval_of_transforms h_while_transforms] + simp [Part.map_some, PartENat.find] + -- TODO: Similar to the eval case, show Nat.find equivalence + sorry + · -- Case: the while loop does not terminate + push_neg at h_stops + have h_no_halt := Routines.while.no_halt_if_condition_always_true' condition tm tapes_seq h_inner h_stops + -- TODO: Show both sides are None/undefined using h_no_halt and h_stops + sorry From e49b392c2cb8ffd7592a028b3470efacd7a43bb0 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 26 Jan 2026 16:01:38 +0100 Subject: [PATCH 4/5] pop.eval --- Complexity/Pop.lean | 43 +++++++++++++++---------- Complexity/Routines.lean | 4 +++ Complexity/TapeLemmas.lean | 5 +++ Complexity/While.lean | 66 +++++++++++++++++++++++++------------- 4 files changed, 78 insertions(+), 40 deletions(-) diff --git a/Complexity/Pop.lean b/Complexity/Pop.lean index 23cabfd..ffa64a9 100644 --- a/Complexity/Pop.lean +++ b/Complexity/Pop.lean @@ -20,34 +20,43 @@ lemma pop_char.inert_after_stop : ext <;> simp_all [Transition.step, performTapeOps, pop_char] @[simp] -lemma pop_char.eval (tape : Turing.Tape SChar) : - pop_char.eval (fun _ => tape) = .some (fun _ => (tape.write .blank).move .right) := by +lemma pop_char.eval (tapes : Fin 1 → Turing.Tape SChar) : + pop_char.eval tapes = .some (fun _ => ((tapes 0).write .blank).move .right) := by apply TM.eval_of_transforms - exact TM.transforms_of_inert pop_char _ _ pop_char.inert_after_stop ⟨1, rfl⟩ + exact TM.transforms_of_inert pop_char _ _ pop_char.inert_after_stop ⟨1, sorry⟩ --- This is a 1-tape Turing machine that removes the left-most word --- from the tape. def pop := (Routines.while (· ≠ .sep) pop_char).seq pop_char @[simp] -theorem pop.eval {w : List Char} {ws₁ ws₂ : List (List Char)} : +theorem pop.eval {w : List Char} {ws₁ : List (List Char)} : pop.eval (list_to_tape ∘ [w :: ws₁].get) = .some (list_to_tape ∘ [ws₁].get) := by + have h_blank : SChar.blank = default := by rfl let tapes : ℕ → Fin 1 → Turing.Tape SChar := (fun i j => Turing.Tape.mk₁ ((list_to_string (w :: ws₁)).drop i)) have h_tapes₀ : tapes 0 = (list_to_tape ∘ [w :: ws₁].get) := by funext i; simp [tapes, list_to_tape] - have h_inner : ∀ i, pop_char.eval (tapes i) = tapes i.succ := by - intro i - simp [tapes] - - - simp [pop_char, TM.eval, TM.configurations, Transition.step, tapes] - sorry - let x := Routines.while.eval (condition := (· ≠ .sep)) (tm := pop_char) tapes h_inner - simp at x + have h_inner : ∀ i, ((TM.eval pop_char (tapes i)) = Part.some (tapes i.succ)) := by + simp [tapes, pop_char.eval, h_blank] + have h_terminate : PartENat.find (fun i => (tapes i 0).head = SChar.sep) = + Part.some w.length := by + rw [Part.eq_some_iff] + use ⟨w.length, by simp [tapes]⟩ + simp only [Fin.isValue, PartENat.find_get] + rw [Nat.find_eq_iff] + constructor + · simp [tapes] + · intro n h_n_lt + simp only [Turing.Tape.mk₁, Turing.Tape.mk₂, list_to_string_cons, Fin.isValue, + Turing.Tape.mk'_head, Turing.ListBlank.head_mk, tapes] + rw [List.drop_eq_getElem_cons (by simp; omega)] + simp [h_n_lt, List.coe_schar_getElem_neq_sep] + have h_move_blank : (fun x ↦ Turing.Tape.move .right (.write .blank (tapes w.length 0))) = + list_to_tape ∘ [ws₁].get := by + funext i; simp [h_blank, tapes, list_to_tape] rw [← h_tapes₀] - simp [pop, x] - - - sorry + let h_eval := Routines.while.eval' (condition := (· ≠ .sep)) (tm := pop_char) tapes h_inner + simp at h_eval + simpa [pop, h_eval, h_terminate, pop_char.eval] using h_move_blank diff --git a/Complexity/Routines.lean b/Complexity/Routines.lean index ac40134..b49eaeb 100644 --- a/Complexity/Routines.lean +++ b/Complexity/Routines.lean @@ -45,6 +45,10 @@ lemma List.coe_schar_get_neq_sep (x : List Char) (n : Fin x.coe_schar.length) : x.coe_schar.get n ≠ .sep := by simp [List.coe_schar] +lemma List.coe_schar_getElem_neq_sep (x : List Char) (n : ℕ) (h_n_lt : n < x.coe_schar.length) : + x.coe_schar[n] ≠ .sep := by + simp [List.coe_schar] + lemma List.coe_schar_get_neq_blank (x : List Char) (n : Fin x.coe_schar.length) : x.coe_schar.get n ≠ .blank := by simp [List.coe_schar] diff --git a/Complexity/TapeLemmas.lean b/Complexity/TapeLemmas.lean index 52246f6..7f12fb0 100644 --- a/Complexity/TapeLemmas.lean +++ b/Complexity/TapeLemmas.lean @@ -135,6 +135,11 @@ theorem Tape.left₀_nth {Γ} [Inhabited Γ] (tape : Turing.Tape Γ) (n : ℕ) : Turing.ListBlank.tail_cons] rfl +@[simp] +lemma Tape.write_eq_drop {Γ} [Inhabited Γ] (c : Γ) (l : List Γ) : + Turing.Tape.write c (Turing.Tape.mk₁ l) = Turing.Tape.mk₁ (c :: (l.drop 1)) := by + simp [Turing.Tape.mk₁, Turing.Tape.mk₂] + @[simp] lemma Tape.move_right_blank {Γ} [Inhabited Γ] (l : List Γ) : Turing.Tape.move .right (Turing.Tape.mk₁ (default :: l)) = Turing.Tape.mk₁ l := by diff --git a/Complexity/While.lean b/Complexity/While.lean index f0c7160..a772b8d 100644 --- a/Complexity/While.lean +++ b/Complexity/While.lean @@ -152,12 +152,21 @@ lemma Routines.while.no_halt_if_condition_always_true {k : ℕ} {Q Γ : Type*} (h_inner : ∀ tapes, tm.eval tapes = .some (semantics tapes)) (tapes : Fin k.succ → Turing.Tape Γ) (h_always_true : ∀ i, condition ((semantics^[i] tapes) 0).head) : - ∀ t, ((Routines.while condition tm).configurations tapes t).state ≠ + ∀ t, ((Routines.while condition tm).configurations tapes t).state ≠ (Routines.while condition tm).stopState := by - -- TODO: Prove by showing the machine is never in state .main 1 - -- Key idea: machine alternates between .main 0 and subroutine states, - -- never reaching .main 1 because condition is always true. - -- This requires an induction argument tracking the state at each step. + intro t + -- The stop state is .main 1 + show ((Routines.while condition tm).configurations tapes t).state ≠ .main 1 + -- We need to show that at each time step, we're either in .main 0 or .sub_routine state + -- and never reach .main 1 because condition is always true + have h_transforms : ∀ i, tm.transforms (semantics^[i] tapes) (semantics^[i.succ] tapes) := by + intro i + have : semantics (semantics^[i] tapes) = semantics^[i.succ] tapes := by + simp [Function.iterate_succ_apply'] + rw [← this] + exact TM.transforms_of_eval (h_inner (semantics^[i] tapes)) + -- The key is that the machine behavior follows a pattern based on semantics iterations + -- But this is complex to formalize without more infrastructure sorry @[simp] @@ -169,7 +178,7 @@ theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} (tapes : Fin k.succ → Turing.Tape Γ) : (Routines.while condition tm).eval tapes = (PartENat.find - fun i => condition (((semantics^[i] tapes) 0).head) + fun i => ¬condition (((semantics^[i] tapes) 0).head) ).map (semantics^[·] tapes) := by have h_transforms : ∀ i, tm.transforms (semantics^[i] tapes) (semantics^[i.succ] tapes) := by intro i @@ -179,21 +188,25 @@ theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} exact TM.transforms_of_eval (h_inner (semantics^[i] tapes)) by_cases h_stops : ∃ m, ¬condition ((semantics^[m] tapes) 0).head · -- Case: the while loop terminates - let m := Nat.find h_stops - have h_while_transforms : (Routines.while condition tm).transforms tapes (semantics^[m] tapes) := + have h_while_transforms : (Routines.while condition tm).transforms tapes (semantics^[Nat.find h_stops] tapes) := Routines.while.semantics condition tm (semantics^[·] tapes) h_transforms h_stops rw [TM.eval_of_transforms h_while_transforms] - simp [Part.map_some, PartENat.find] - -- TODO: Show that Nat.find finds the same value m for both predicates: - -- 1. ((Routines.while condition tm).configurations tapes t).state = (Routines.while condition tm).stopState - -- 2. condition (((semantics^[·] tapes) 0).head) = false (negated in PartENat.find) - -- This requires relating the while machine's execution to the semantics iteration. + simp [PartENat.find, Part.map_some] sorry · -- Case: the while loop does not terminate push_neg at h_stops have h_no_halt := Routines.while.no_halt_if_condition_always_true condition tm semantics h_inner tapes h_stops - -- TODO: Show both sides are None/undefined using h_no_halt and h_stops - sorry + -- LHS: TM.eval is None because machine never halts + -- RHS: PartENat.find.map is None because condition is always true (never false) + ext result + simp [TM.eval, PartENat.find, Part.mem_map_iff] + constructor + · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; exact h_no_halt t h_t + · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; + have h_true := h_stops t + -- h_t : condition ... = false, h_true : condition ... = true + rw [h_t] at h_true + sorry -- Helper lemma for eval' version lemma Routines.while.no_halt_if_condition_always_true' {k : ℕ} {Q Γ : Type*} @@ -203,7 +216,7 @@ lemma Routines.while.no_halt_if_condition_always_true' {k : ℕ} {Q Γ : Type*} (tapes_seq : ℕ → (Fin k.succ → (Turing.Tape Γ))) (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) (h_always_true : ∀ i, condition ((tapes_seq i) 0).head) : - ∀ t, ((Routines.while condition tm).configurations (tapes_seq 0) t).state ≠ + ∀ t, ((Routines.while condition tm).configurations (tapes_seq 0) t).state ≠ (Routines.while condition tm).stopState := by -- TODO: Similar proof as no_halt_if_condition_always_true but with explicit tape sequence sorry @@ -216,22 +229,29 @@ theorem Routines.while.eval' {k : ℕ} {Q Γ : Type*} (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) : (Routines.while condition tm).eval (tapes_seq 0) = (PartENat.find - fun i => condition (((tapes_seq i) 0).head) + fun i => ¬condition (((tapes_seq i) 0).head) ).map tapes_seq := by have h_transforms : ∀ i, tm.transforms (tapes_seq i) (tapes_seq i.succ) := by intro i exact TM.transforms_of_eval (h_inner i) by_cases h_stops : ∃ m, ¬condition ((tapes_seq m) 0).head · -- Case: the while loop terminates - let m := Nat.find h_stops - have h_while_transforms : (Routines.while condition tm).transforms (tapes_seq 0) (tapes_seq m) := + have h_while_transforms : (Routines.while condition tm).transforms (tapes_seq 0) (tapes_seq (Nat.find h_stops)) := Routines.while.semantics condition tm tapes_seq h_transforms h_stops rw [TM.eval_of_transforms h_while_transforms] - simp [Part.map_some, PartENat.find] - -- TODO: Similar to the eval case, show Nat.find equivalence + simp [PartENat.find, Part.map_some] sorry · -- Case: the while loop does not terminate push_neg at h_stops have h_no_halt := Routines.while.no_halt_if_condition_always_true' condition tm tapes_seq h_inner h_stops - -- TODO: Show both sides are None/undefined using h_no_halt and h_stops - sorry + -- LHS: TM.eval is None because machine never halts + -- RHS: PartENat.find.map is None because condition is always true (never false) + ext result + simp [TM.eval, PartENat.find, Part.mem_map_iff] + constructor + · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; exact h_no_halt t h_t + · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; + have h_true := h_stops t + -- h_t : condition ... = false, h_true : condition ... = true + rw [h_t] at h_true + sorry From 08c94c29eec4500f30bd209a4169cebd4a9a1f0e Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 26 Jan 2026 21:06:23 +0100 Subject: [PATCH 5/5] some cleanup --- Complexity/While.lean | 131 ++++++++++-------------------------------- 1 file changed, 30 insertions(+), 101 deletions(-) diff --git a/Complexity/While.lean b/Complexity/While.lean index a772b8d..a056866 100644 --- a/Complexity/While.lean +++ b/Complexity/While.lean @@ -141,35 +141,38 @@ theorem Routines.while.semantics {k : ℕ} {Q Γ : Type*} -- Semantics of Routines.while in terms of `eval.`. -- Note that this only works for Turing machines that always halt --- and whose semantics is explicitly given by `semantics`. --- Helper lemma: if tm always halts and semantics describes its behavior, --- and condition is always true, then the while machine never halts -lemma Routines.while.no_halt_if_condition_always_true {k : ℕ} {Q Γ : Type*} +-- on the sequence of iterated inputs. +@[simp] +theorem Routines.while.eval' {k : ℕ} {Q Γ : Type*} [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] - (condition : Γ → Bool) - (tm : TM k.succ Q Γ) - (semantics : (Fin k.succ → (Turing.Tape Γ)) → (Fin k.succ → (Turing.Tape Γ))) - (h_inner : ∀ tapes, tm.eval tapes = .some (semantics tapes)) - (tapes : Fin k.succ → Turing.Tape Γ) - (h_always_true : ∀ i, condition ((semantics^[i] tapes) 0).head) : - ∀ t, ((Routines.while condition tm).configurations tapes t).state ≠ - (Routines.while condition tm).stopState := by - intro t - -- The stop state is .main 1 - show ((Routines.while condition tm).configurations tapes t).state ≠ .main 1 - -- We need to show that at each time step, we're either in .main 0 or .sub_routine state - -- and never reach .main 1 because condition is always true - have h_transforms : ∀ i, tm.transforms (semantics^[i] tapes) (semantics^[i.succ] tapes) := by - intro i - have : semantics (semantics^[i] tapes) = semantics^[i.succ] tapes := by - simp [Function.iterate_succ_apply'] - rw [← this] - exact TM.transforms_of_eval (h_inner (semantics^[i] tapes)) - -- The key is that the machine behavior follows a pattern based on semantics iterations - -- But this is complex to formalize without more infrastructure - sorry + {condition : Γ → Bool} {tm : TM k.succ Q Γ} + (tapes_seq : ℕ → (Fin k.succ → (Turing.Tape Γ))) + (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) : + (Routines.while condition tm).eval (tapes_seq 0) = + (PartENat.find + fun i => ¬condition (((tapes_seq i) 0).head) + ).map tapes_seq := by + by_cases h_halts: ∃ i, ¬condition ((tapes_seq i) 0).head + · convert TM.eval_of_transforms (Routines.while.semantics condition tm tapes_seq + (by intro i; exact TM.transforms_of_eval (h_inner i)) + (by convert h_halts)) + rw [Part.eq_some_iff] + obtain ⟨i, h_halts⟩ := h_halts + use ⟨i, by simp [h_halts]⟩ + simp + · have h_no_halts : (PartENat.find fun i => ¬condition (tapes_seq i 0).head) = Part.none := by + sorry + sorry + -- rw [h_no_halts] + -- simp + -- rw [Part.eq_none_iff'] + -- simp [TM.eval, PartENat.find] + -- by_contra h_does_halt + -- simp at h_does_halt + -- obtain ⟨t, h_does_halt⟩ := h_does_halt + -- simp at h_halts + -- sorry -@[simp] theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] {condition : Γ → Bool} {tm : TM k.succ Q Γ} @@ -180,78 +183,4 @@ theorem Routines.while.eval {k : ℕ} {Q Γ : Type*} (PartENat.find fun i => ¬condition (((semantics^[i] tapes) 0).head) ).map (semantics^[·] tapes) := by - have h_transforms : ∀ i, tm.transforms (semantics^[i] tapes) (semantics^[i.succ] tapes) := by - intro i - have : semantics (semantics^[i] tapes) = semantics^[i.succ] tapes := by - simp [Function.iterate_succ_apply'] - rw [← this] - exact TM.transforms_of_eval (h_inner (semantics^[i] tapes)) - by_cases h_stops : ∃ m, ¬condition ((semantics^[m] tapes) 0).head - · -- Case: the while loop terminates - have h_while_transforms : (Routines.while condition tm).transforms tapes (semantics^[Nat.find h_stops] tapes) := - Routines.while.semantics condition tm (semantics^[·] tapes) h_transforms h_stops - rw [TM.eval_of_transforms h_while_transforms] - simp [PartENat.find, Part.map_some] - sorry - · -- Case: the while loop does not terminate - push_neg at h_stops - have h_no_halt := Routines.while.no_halt_if_condition_always_true condition tm semantics h_inner tapes h_stops - -- LHS: TM.eval is None because machine never halts - -- RHS: PartENat.find.map is None because condition is always true (never false) - ext result - simp [TM.eval, PartENat.find, Part.mem_map_iff] - constructor - · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; exact h_no_halt t h_t - · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; - have h_true := h_stops t - -- h_t : condition ... = false, h_true : condition ... = true - rw [h_t] at h_true - sorry - --- Helper lemma for eval' version -lemma Routines.while.no_halt_if_condition_always_true' {k : ℕ} {Q Γ : Type*} - [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] - (condition : Γ → Bool) - (tm : TM k.succ Q Γ) - (tapes_seq : ℕ → (Fin k.succ → (Turing.Tape Γ))) - (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) - (h_always_true : ∀ i, condition ((tapes_seq i) 0).head) : - ∀ t, ((Routines.while condition tm).configurations (tapes_seq 0) t).state ≠ - (Routines.while condition tm).stopState := by - -- TODO: Similar proof as no_halt_if_condition_always_true but with explicit tape sequence sorry - -@[simp] -theorem Routines.while.eval' {k : ℕ} {Q Γ : Type*} - [Inhabited Γ] [DecidableEq Γ] [DecidableEq Q] - {condition : Γ → Bool} {tm : TM k.succ Q Γ} - (tapes_seq : ℕ → (Fin k.succ → (Turing.Tape Γ))) - (h_inner : ∀ i, tm.eval (tapes_seq i) = .some (tapes_seq i.succ)) : - (Routines.while condition tm).eval (tapes_seq 0) = - (PartENat.find - fun i => ¬condition (((tapes_seq i) 0).head) - ).map tapes_seq := by - have h_transforms : ∀ i, tm.transforms (tapes_seq i) (tapes_seq i.succ) := by - intro i - exact TM.transforms_of_eval (h_inner i) - by_cases h_stops : ∃ m, ¬condition ((tapes_seq m) 0).head - · -- Case: the while loop terminates - have h_while_transforms : (Routines.while condition tm).transforms (tapes_seq 0) (tapes_seq (Nat.find h_stops)) := - Routines.while.semantics condition tm tapes_seq h_transforms h_stops - rw [TM.eval_of_transforms h_while_transforms] - simp [PartENat.find, Part.map_some] - sorry - · -- Case: the while loop does not terminate - push_neg at h_stops - have h_no_halt := Routines.while.no_halt_if_condition_always_true' condition tm tapes_seq h_inner h_stops - -- LHS: TM.eval is None because machine never halts - -- RHS: PartENat.find.map is None because condition is always true (never false) - ext result - simp [TM.eval, PartENat.find, Part.mem_map_iff] - constructor - · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; exact h_no_halt t h_t - · intro h; obtain ⟨⟨t, h_t⟩, _⟩ := h; exfalso; - have h_true := h_stops t - -- h_t : condition ... = false, h_true : condition ... = true - rw [h_t] at h_true - sorry