From f2cb157fe956c2fcfa6217019409e765d85bf8b7 Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 21 Feb 2026 14:15:06 +0100 Subject: [PATCH 01/20] More pseudo-code for reachability. --- .../MultiTapeTuring/GraphReachability.lean | 58 +++++++++++++------ 1 file changed, 40 insertions(+), 18 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 508491caa..786e4f609 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -6,9 +6,6 @@ Authors: Christian Reitwiessner module -import Cslib.Foundations.Data.BiTape -import Cslib.Foundations.Data.RelatesInSteps - public import Cslib.Computability.Machines.MultiTapeTuring.Basic public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats @@ -41,31 +38,56 @@ uses "goto", and every variable is a stack: def reachable(a, b, t, r): terminate = 0 result = 0 - section = [0] + initial_t = t + section = [:terminate, :fun_start] while !terminate: match section.pop() - | 0 => + | :fun_start => if t = 0: result = r(a, b) - terminate = 1 - section.push(7) + section.push(:fun_return) else: - section.push(1) - | 1 => - c.push(0) - section.push(2) - | 2 => + c.push(0) + section.push(:loop_start) + | :loop_start => if c.top() = num_vertices: - section.push(6) + c.pop() + result = 0 + section.push(:fun_return) else: a.push(a.top()) b.push(c.top()) - section.push(0) t.push(t.top() - 1) - section.push(3) - | 3 => - section.push(4) - + section.push(:after_first_rec) + section.push(:fun_start) + | :after_first_rec => + if result == 1: + a.push(c.top()) + b.push(b.top()) + t.push(t.top() - 1) + section.push(:after_second_rec) + section.push(0) + else: + result = 0 + section.push(:loop_continue) + | :after_second_rec => + if result == 1: + c.pop() + section.push(:fun_return) + else: + section.push(:loop_continue) + | :loop_continue => + c.push(c.top() + 1) + section.push(:loop_start) + | :fun_return => + a.pop() + b.pop() + t.pop() + | :terminate => + terminate = 1 + -- cleanup + terminate.pop() + initial_t.pop() -/ From c55d0ab22824d0059bf639beb7efc758218c7a8c Mon Sep 17 00:00:00 2001 From: crei Date: Sat, 21 Feb 2026 23:38:18 +0100 Subject: [PATCH 02/20] reachability and decrement. --- .../Machines/MultiTapeTuring/CopyRoutine.lean | 25 ++- .../Machines/MultiTapeTuring/DecRoutine.lean | 101 +++++++++++ .../MultiTapeTuring/DuplicateRoutine.lean | 53 ++++++ .../MultiTapeTuring/EqualRoutine.lean | 5 +- .../MultiTapeTuring/GraphReachability.lean | 161 ++++++++++++++---- .../Machines/MultiTapeTuring/SuccRoutine.lean | 8 +- 6 files changed, 305 insertions(+), 48 deletions(-) create mode 100644 Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean create mode 100644 Cslib/Computability/Machines/MultiTapeTuring/DuplicateRoutine.lean diff --git a/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean index 96a715047..aca3d10d9 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/CopyRoutine.lean @@ -31,22 +31,21 @@ lemma copy₁_eval_list {tapes : Fin 2 → List (List α)} : A Turing machine that copies the first word on tape `i` to tape `j`. If Tape `i` is empty, pushes the empty word to tape `j`. -/ -public def copy {k : ℕ} (i j : ℕ) - (h_neq : i ≠ j := by decide) - (h_i_lt : i < k := by decide) - (h_j_lt : j < k := by decide) : - MultiTapeTM k (WithSep α) := - copy₁.with_tapes [⟨i, h_i_lt⟩, ⟨j, h_j_lt⟩].get (by intro x y; grind) +public def copy {k : ℕ} + (i j : Fin (k + 2)) + (h_inj : [i, j].get.Injective := by intro x y; grind) : + MultiTapeTM (k + 2) (WithSep α) := + copy₁.with_tapes [i, j].get (by intro x y; grind) @[simp, grind =] public lemma copy_eval_list - {k : ℕ} {i j : ℕ} {h_neq : i ≠ j} {h_i_lt : i < k} {h_j_lt : j < k} - {tapes : Fin k → List (List α)} : - (copy i j (h_neq := h_neq) (h_i_lt) (h_j_lt)).eval_list tapes = Part.some - (Function.update tapes ⟨j, h_j_lt⟩ - (((tapes ⟨i, h_i_lt⟩).headD []) :: (tapes ⟨j, h_j_lt⟩))) := by - have h_inj : [(⟨i, h_i_lt⟩ : Fin k), ⟨j, h_j_lt⟩].get.Injective := by intro x y; grind - simp_all [copy] + {k : ℕ} + (i j : Fin (k + 2)) + (h_inj : [i, j].get.Injective := by intro x y; grind) + {tapes : Fin (k + 2) → List (List α)} : + (copy i j h_inj).eval_list tapes = Part.some + (Function.update tapes j (((tapes i).headD []) :: (tapes j))) := by + simpa [copy] using apply_updates_function_update h_inj end Routines diff --git a/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean new file mode 100644 index 000000000..c5b2bb237 --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean @@ -0,0 +1,101 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes +public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.SuccRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.LoopCombinator + +namespace Turing + +namespace Routines + +def dec₀ : MultiTapeTM 6 (WithSep OneTwo) := + push 1 [] <;> push 2 [] <;> + loop 0 (h_i := by decide) (pop 2 <;> copy 1 2 <;> succ 1) <;> + pop 0 <;> + copy 2 0 <;> + pop 2 <;> + pop 1 + +@[simp] +lemma inner_eval_list {tapes : Fin 3 → List (List OneTwo)} : + (pop 2 <;> copy 1 2 <;> succ 1).eval_list tapes = .some ( + (if h : tapes 1 = [] then Function.update tapes 2 ((tapes 1).head?.getD [] :: (tapes 2).tail) + else + Function.update (Function.update tapes 2 ((tapes 1).head?.getD [] :: (tapes 2).tail)) 1 + (dya (dya_inv ((tapes 1).headD []) + 1) :: (tapes 1).tail))) := by + simp + grind + +@[simp] +lemma inner_eval_iter {r : ℕ} {tapes : Fin 3 → List (List OneTwo)} : + (Part.bind · (pop 2 <;> copy 1 2 <;> succ 1).eval_list)^[r] (.some tapes) = Part.some ( + if r = 0 then + tapes + else if tapes 1 = [] then + Function.update tapes 2 ([] :: (tapes 2).tail) + else + Function.update (Function.update tapes + 2 ((dya ((dya_inv ((tapes 1).headD [])) + (r - 1))) :: (tapes 2).tail)) + 1 ((dya ((dya_inv ((tapes 1).headD [])) + r)) :: (tapes 1).tail)) := by + induction r with + | zero => simp + | succ r ih => + rw [Function.iterate_succ_apply'] + simp [ih, inner_eval_list, -copy_eval_list, -succ_eval_list, -pop_eval_list, -MultiTapeTM.seq_eval_list] + by_cases h_tape1_empty : tapes 1 = [] + · simp [h_tape1_empty] + by_cases h : r = 0 + · simp [h]; grind + · simp [h]; grind + · simp [h_tape1_empty] + by_cases h : r = 0 + · simp [h, h_tape1_empty] + · simp [h]; grind + +@[simp, grind =] +lemma dec₀_eval_list {tapes : Fin 6 → List (List OneTwo)} : + dec₀.eval_list tapes = .some (Function.update tapes 0 + ((dya ((dya_inv ((tapes 0).headD [])) - 1)) :: (tapes 0).tail)) := by + simp [dec₀] + grind + +/-- +A Turing machine that decrements the dyadic value at the head of tape `i`. +If the value is zero already, keeps it at zero. If the tape is empty, pushes zero. +-/ +public def dec {k : ℕ} (i : Fin (k + 3)) + (aux : Fin (k + 3) := ⟨k, by omega⟩) + (h_inj : [i, aux, aux + 1].get.Injective := by intro x y; grind) : + MultiTapeTM (k + 6) (WithSep OneTwo) := + push ⟨aux, by omega⟩ [] <;> push ⟨aux + 1, by omega⟩ [] <;> + loop i (h_i := by omega) (copy aux (aux + 1) (by sorry) <;> succ aux) <;> + pop ⟨i, by omega⟩ <;> + copy ⟨aux + 1, by omega⟩ ⟨i, by omega⟩ (by sorry) <;> + pop ⟨aux + 1, by omega⟩ <;> + pop ⟨aux, by omega⟩ + +@[simp, grind =] +public theorem duplicate_eval_list {k : ℕ} {i : Fin k.succ} + (aux : Fin k.succ := ⟨k, by omega⟩) + (h_inj : [i, aux].get.Injective) + {tapes : Fin k.succ → List (List OneTwo)} : + (duplicate i aux h_inj).eval_list tapes = Part.some (Function.update tapes i + (((tapes i).headD []) :: (tapes i))) := by + simp [duplicate] + grind + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/DuplicateRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/DuplicateRoutine.lean new file mode 100644 index 000000000..c4ef352bb --- /dev/null +++ b/Cslib/Computability/Machines/MultiTapeTuring/DuplicateRoutine.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module + +public import Cslib.Computability.Machines.MultiTapeTuring.Basic +public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding +public import Cslib.Computability.Machines.MultiTapeTuring.WithTapes +public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator + +namespace Turing + +namespace Routines + +variable [Inhabited α] [Fintype α] + +def duplicate₀ : MultiTapeTM 2 (WithSep α) := copy 0 1 <;> copy 1 0 <;> pop 1 + +@[simp] +lemma duplicate₀_eval_list {tapes : Fin 2 → List (List α)} : + duplicate₀.eval_list tapes = .some (Function.update tapes 0 + (((tapes 0).headD []) :: (tapes 0))) := by + simp [duplicate₀] + grind + +/-- +A Turing machine that duplicates the head of tape `i` (or pushes the empty word +if the tape is empty. +-/ +public def duplicate {k : ℕ} (i : Fin k.succ) + (aux : Fin k.succ := ⟨k, by omega⟩) + (h_inj : [i, aux].get.Injective := by intro x y; grind) : + MultiTapeTM k.succ (WithSep α) := + duplicate₀.with_tapes [i, aux].get h_inj + +@[simp, grind =] +public theorem duplicate_eval_list {k : ℕ} {i : Fin k.succ} + (aux : Fin k.succ := ⟨k, by omega⟩) + (h_inj : [i, aux].get.Injective) + {tapes : Fin k.succ → List (List OneTwo)} : + (duplicate i aux h_inj).eval_list tapes = Part.some (Function.update tapes i + (((tapes i).headD []) :: (tapes i))) := by + simp [duplicate] + grind + +end Routines + +end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean index 7ad2b42c9..271c06ede 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/EqualRoutine.lean @@ -47,10 +47,11 @@ public def eq {k : ℕ} (q s t : Fin k) MultiTapeTM k (WithSep OneTwo) := eq₀.with_tapes [q, s, t].get h_inj +-- TODO why does the linter complain about simp here? @[grind =] -public theorem eq_eval_list {k : ℕ} {q s t : Fin k} +public theorem eq_eval_list {k : ℕ} {q s t : Fin k.succ} (h_inj : [q, s, t].get.Injective) - {tapes : Fin k → List (List OneTwo)} : + {tapes : Fin k.succ → List (List OneTwo)} : (eq q s t).eval_list tapes = Part.some (Function.update tapes t ((if (tapes q).headD [] = (tapes s).headD [] then [.one] diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 786e4f609..1ecd04a84 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -8,13 +8,17 @@ module public import Cslib.Computability.Machines.MultiTapeTuring.Basic public import Cslib.Computability.Machines.MultiTapeTuring.ListEncoding -public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats +public import Cslib.Computability.Machines.MultiTapeTuring.IteCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.SequentialCombinator +public import Cslib.Computability.Machines.MultiTapeTuring.EqualRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.DuplicateRoutine --- TODO create a "common file" -import Cslib.Computability.Machines.SingleTapeTuring.Basic namespace Turing +namespace Routines -- This is an attempt at proving Savitch's theorem. We start by stating a generic -- space-efficient graph reachability algorithm. @@ -35,62 +39,159 @@ def reachable(a, b, t, r): Until we have a generic mechanism for recursion, let's translate this into a program that uses "goto", and every variable is a stack: -def reachable(a, b, t, r): - terminate = 0 +def reachable(a, b, t, edge): result = 0 initial_t = t - section = [:terminate, :fun_start] - while !terminate: - match section.pop() + pc = [:fun_start] + while !pc.is_empty(): + match pc.pop() | :fun_start => if t = 0: - result = r(a, b) - section.push(:fun_return) + result = edge(a, b) else: c.push(0) - section.push(:loop_start) + pc.push(:loop_start) | :loop_start => if c.top() = num_vertices: c.pop() result = 0 - section.push(:fun_return) else: a.push(a.top()) b.push(c.top()) - t.push(t.top() - 1) - section.push(:after_first_rec) - section.push(:fun_start) + t = t - 1 + pc.push(:after_first_rec) + pc.push(:fun_start) | :after_first_rec => + a.pop() + b.pop() + t = t + 1 if result == 1: a.push(c.top()) b.push(b.top()) - t.push(t.top() - 1) - section.push(:after_second_rec) - section.push(0) + t = t - 1 + pc.push(:after_second_rec) + pc.push(:fun_start) else: result = 0 - section.push(:loop_continue) + pc.push(:loop_continue) | :after_second_rec => + a.pop() + b.pop() + t = t + 1 if result == 1: c.pop() - section.push(:fun_return) else: - section.push(:loop_continue) + pc.push(:loop_continue) | :loop_continue => c.push(c.top() + 1) - section.push(:loop_start) - | :fun_return => - a.pop() - b.pop() - t.pop() - | :terminate => - terminate = 1 + pc.push(:loop_start) -- cleanup - terminate.pop() initial_t.pop() + t.pop() + a.pop() + b.pop() +-/ + +def tapeCount := 20 + +lemma tape_count_eq : tapeCount = 20 := rfl + +def a : Fin tapeCount := ⟨3, sorry⟩ +def b : Fin tapeCount := ⟨4, sorry⟩ +def t : Fin tapeCount := ⟨5, sorry⟩ +def result : Fin tapeCount := ⟨6, sorry⟩ +def initialT : Fin tapeCount := ⟨7, sorry⟩ +def pc : Fin tapeCount := ⟨8, sorry⟩ +def c : Fin tapeCount := ⟨9, sorry⟩ +def mainAux : Fin tapeCount := ⟨10, sorry⟩ + +def l_funStart := dya 1 +def l_loopStart := dya 2 + +-- if t = 0: +-- result = edge(a, b) +-- else: +-- c.push(0) +-- pc.push(:loop_start) + +def funStart (edge : MultiTapeTM tapeCount (WithSep OneTwo)) := + ite t (push c [] <;> push pc l_loopStart) edge + +@[simp] +lemma funStart_eval_list + (tapes : Fin tapeCount → List (List OneTwo)) + (edge : MultiTapeTM tapeCount (WithSep OneTwo)) : + (funStart edge).eval_list tapes = + if (tapes t).headD [] = [] then + (edge.eval_list tapes) + else + .some (Function.update (Function.update tapes c ([] :: (tapes c))) + pc (l_loopStart :: (tapes pc))) := by + have : pc ≠ c := by decide + simp [funStart] + grind + +def infiniteLoop {α : Type} {k : ℕ} : MultiTapeTM k (WithSep α) := sorry + +public def eqLit {k : ℕ} + (q : Fin (k + 3)) + (w : List OneTwo) + (s : Fin (k + 3)) + (aux : Fin (k + 3) := ⟨k + 2, by omega⟩) + (h_inj : [q, aux, s].get.Injective := by intro x y; grind) : + MultiTapeTM (k + 3) (WithSep OneTwo) := + push aux w <;> eq q aux s h_inj <;> pop aux + +public theorem eqLit_eval_list {k : ℕ} {q s aux : Fin (k + 3)} {w : List OneTwo} + {h_inj : [q, aux, s].get.Injective} + {tapes : Fin (k + 3) → List (List OneTwo)} : + (eqLit q w s aux h_inj).eval_list tapes = + .some (Function.update tapes s ( + (if (tapes q).headD [] = w then + [.one] + else + []) :: (tapes s))) := by + simp [eqLit, eq_eval_list h_inj] + have h_neq : aux ≠ s := Function.Injective.ne h_inj (a₁ := 1) (a₂ := 2) (by grind) + have h_neq : q ≠ aux := Function.Injective.ne h_inj (a₁ := 0) (a₂ := 1) (by grind) + grind + +-- | :loop_start => +-- if c.top() = num_vertices: +-- c.pop() +-- result = 0 +-- else: +-- a.push(a.top()) +-- b.push(c.top()) +-- t = t - 1 +-- pc.push(:after_first_rec) +-- pc.push(:fun_start) + +def loopStart (maxConfig : List OneTwo) := + eqLit c maxConfig mainAux <;> + ite mainAux + (pop mainAux <;> pop c <;> push result []) + (duplicate a <;> copy c b <;> dec t <;> push pc l_funStart <;> push pc l_loopStart) + +public def matchCombine {k : ℕ} + (i : Fin (k + 3)) (aux : Fin (k + 3)) (h_inj : [i, aux, aux + 1].get.Injective) + (branches : List ((List OneTwo) × (MultiTapeTM (k + 3) (WithSep OneTwo)))) : + MultiTapeTM (k + 3) (WithSep OneTwo) := + match branches with + | [] => infiniteLoop + | (w, tm) :: branches => + eqLit i w aux (aux + 1) (h_inj := by sorry /- use swap on h_inj? -/) <;> + ite aux (pop aux <;> tm) (pop aux <;> matchCombine i aux (by intro x y; grind) branches) + +def innerLoop (edge : MultiTapeTM tapeCount (WithSep OneTwo)) : + MultiTapeTM tapeCount (WithSep OneTwo) := + matchCombine pc mainAux (by decide) + [ (l_funStart, funStart edge), + (l_loopStart, loop 1, infiniteLoop) ] --/ +theorem reachable +end Routines end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean index 9c5c61e89..e82acdea4 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean @@ -70,9 +70,11 @@ public theorem succ_computes {k : ℕ} {i : Fin k} : @[simp] public theorem succ_eval_list {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} : - (succ i).eval_list tapes = .some (succ_f i tapes) := by - -- TOOD why does simp not find it? - simp [MultiTapeTM.eval_of_computes succ_computes] + (succ i).eval_list tapes = .some (if h_ne : tapes i ≠ [] then + Function.update tapes i ((dya ((dya_inv ((tapes i).head h_ne)).succ)) :: (tapes i).tail) + else + tapes) := by + sorry lemma succ₀_evalWithStats_list {n : ℕ} {ls : List (List OneTwo)} : succ₀.evalWithStats_list [(dya n) :: ls].get = From b2085f7905cad8474195e24ae8315bf645c16d41 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 22 Feb 2026 19:13:11 +0100 Subject: [PATCH 03/20] Simplify semantics of succ. --- .../Machines/MultiTapeTuring/AddRoutine.lean | 15 +++--- .../Machines/MultiTapeTuring/SuccRoutine.lean | 46 +++---------------- 2 files changed, 14 insertions(+), 47 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean index 8afe7cb22..3cc0737f8 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean @@ -25,19 +25,16 @@ namespace Routines @[simp] lemma succ_iter {k r : ℕ} {i : Fin k.succ} {tapes : Fin k.succ → List (List OneTwo)} : (Part.bind · (succ i).eval_list)^[r] (.some tapes) = Part.some (Function.update tapes i ( - if h : tapes i ≠ [] then - (dya ((dya_inv ((tapes i).head h)) + r)) :: (tapes i).tail + if r ≠ 0 then + (dya ((dya_inv ((tapes i).headD [])) + r)) :: (tapes i).tail else tapes i)) := by induction r with | zero => simp | succ r ih => rw [Function.iterate_succ_apply'] - simp [ih, succ_eval_list] - by_cases h_empty : tapes i = [] - · simp [h_empty] - · simp [h_empty] - grind + simp [ih] + grind --- Add 0 and 1 and store the result in 2. --- Assumes zero for an empty tape. @@ -50,7 +47,9 @@ theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} : (Function.update tapes 2 ((dya (dya_inv ((tapes 0).headD []) + dya_inv ((tapes 1).headD [])) :: (tapes 2)))) := by simp [add₀] - grind + by_cases h : dya_inv ((tapes 0).head?.getD []) = 0 + · simp [h]; grind + · grind /-- A Turing machine that adds the heads of tapes i and j (in dyadic encoding) and pushes the result diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean index 9c5c61e89..8c4f6bb93 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean @@ -25,54 +25,22 @@ def succ₀ : MultiTapeTM 1 (WithSep OneTwo) where M _ syms := sorry @[simp] -lemma succ₀_eval_list {n : ℕ} {ls : List (List OneTwo)} : - succ₀.eval_list [(dya n) :: ls].get = .some [(dya n.succ) :: ls].get := by +lemma succ₀_eval_list {tapes : Fin 1 → List (List OneTwo)} : + succ₀.eval_list tapes = .some (Function.update tapes 0 + ((dya (dya_inv ((tapes 0).headD [])).succ) :: (tapes 0).tail)) := by sorry /-- A Turing machine that increments the head of tape `i` by one (in dyadic encoding). Pushes zero if the tape is empty. -/ public def succ {k : ℕ} (i : Fin k) : MultiTapeTM k (WithSep OneTwo) := - succ₀.with_tapes (fun _ => i) (by intro x y; grind) - -/-- -The function computed by `succ`. --/ -public def succ_f {k : ℕ} - (i : Fin k) - (tapes : Fin k → List (List OneTwo)) : Fin k → List (List OneTwo) := - if h_ne : tapes i ≠ [] then - Function.update tapes i ((dya ((dya_inv ((tapes i).head h_ne)).succ)) :: (tapes i).tail) - else - tapes - -@[simp] -public lemma succ_f_neq {k : ℕ} - (i : Fin k) - (tapes : Fin k → List (List OneTwo)) - (h_ne : tapes i ≠ []) : - succ_f i tapes = Function.update tapes i - ((dya ((dya_inv ((tapes i).head h_ne)).succ)) :: (tapes i).tail) := by - simp [succ_f, h_ne] - -@[simp] -public lemma succ_f_empty {k : ℕ} - (i : Fin k) - (tapes : Fin k → List (List OneTwo)) - (h_empty : tapes i = []) : - succ_f i tapes = tapes := by - simp [succ_f, h_empty] - -@[simp] -public theorem succ_computes {k : ℕ} {i : Fin k} : - (succ i).computes (succ_f i) := by - sorry + succ₀.with_tapes [i].get (by intro x y; grind) @[simp] public theorem succ_eval_list {k : ℕ} {i : Fin k} {tapes : Fin k → List (List OneTwo)} : - (succ i).eval_list tapes = .some (succ_f i tapes) := by - -- TOOD why does simp not find it? - simp [MultiTapeTM.eval_of_computes succ_computes] + (succ i).eval_list tapes = .some (Function.update tapes i + ((dya (dya_inv ((tapes i).headD [])).succ) :: (tapes i).tail)) := by + simpa [succ] using apply_updates_function_update (by intro x y; grind) lemma succ₀_evalWithStats_list {n : ℕ} {ls : List (List OneTwo)} : succ₀.evalWithStats_list [(dya n) :: ls].get = From 228dbb56ff955bddd773b7578478fa2a59b62ce0 Mon Sep 17 00:00:00 2001 From: crei Date: Sun, 22 Feb 2026 19:44:23 +0100 Subject: [PATCH 04/20] Decrement routine. --- .../Machines/MultiTapeTuring/DecRoutine.lean | 72 ++++++++----------- .../MultiTapeTuring/TapeExtension.lean | 10 +++ 2 files changed, 41 insertions(+), 41 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean index c5b2bb237..bad8973f2 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean @@ -28,23 +28,11 @@ def dec₀ : MultiTapeTM 6 (WithSep OneTwo) := pop 2 <;> pop 1 -@[simp] -lemma inner_eval_list {tapes : Fin 3 → List (List OneTwo)} : - (pop 2 <;> copy 1 2 <;> succ 1).eval_list tapes = .some ( - (if h : tapes 1 = [] then Function.update tapes 2 ((tapes 1).head?.getD [] :: (tapes 2).tail) - else - Function.update (Function.update tapes 2 ((tapes 1).head?.getD [] :: (tapes 2).tail)) 1 - (dya (dya_inv ((tapes 1).headD []) + 1) :: (tapes 1).tail))) := by - simp - grind - @[simp] lemma inner_eval_iter {r : ℕ} {tapes : Fin 3 → List (List OneTwo)} : (Part.bind · (pop 2 <;> copy 1 2 <;> succ 1).eval_list)^[r] (.some tapes) = Part.some ( if r = 0 then tapes - else if tapes 1 = [] then - Function.update tapes 2 ([] :: (tapes 2).tail) else Function.update (Function.update tapes 2 ((dya ((dya_inv ((tapes 1).headD [])) + (r - 1))) :: (tapes 2).tail)) @@ -53,48 +41,50 @@ lemma inner_eval_iter {r : ℕ} {tapes : Fin 3 → List (List OneTwo)} : | zero => simp | succ r ih => rw [Function.iterate_succ_apply'] - simp [ih, inner_eval_list, -copy_eval_list, -succ_eval_list, -pop_eval_list, -MultiTapeTM.seq_eval_list] - by_cases h_tape1_empty : tapes 1 = [] - · simp [h_tape1_empty] - by_cases h : r = 0 - · simp [h]; grind - · simp [h]; grind - · simp [h_tape1_empty] - by_cases h : r = 0 - · simp [h, h_tape1_empty] - · simp [h]; grind + simp [ih] + grind + +@[simp] +lemma loop_eval_iter {tapes : Fin 6 → List (List OneTwo)} : + (loop 0 (h_i := by decide) (pop 2 <;> copy 1 2 <;> succ 1)).eval_list tapes = .some ( + if dya_inv ((tapes 0).head?.getD []) = 0 then + tapes + else + Function.update (Function.update tapes + 2 (dya (dya_inv ((tapes 1).head?.getD []) + + (dya_inv ((tapes 0).head?.getD []) - 1)) :: (tapes 2).tail)) + 1 (dya (dya_inv ((tapes 1).head?.getD []) + + dya_inv ((tapes 0).head?.getD [])) :: (tapes 1).tail)) := by + by_cases h : dya_inv ((tapes 0).head?.getD []) = 0 + · simp [h] + · simp [h]; grind @[simp, grind =] lemma dec₀_eval_list {tapes : Fin 6 → List (List OneTwo)} : dec₀.eval_list tapes = .some (Function.update tapes 0 ((dya ((dya_inv ((tapes 0).headD [])) - 1)) :: (tapes 0).tail)) := by - simp [dec₀] - grind + by_cases h : dya_inv ((tapes 0).head?.getD []) = 0 + · simp [dec₀, h]; grind + · simp [dec₀, h]; grind /-- A Turing machine that decrements the dyadic value at the head of tape `i`. If the value is zero already, keeps it at zero. If the tape is empty, pushes zero. -/ -public def dec {k : ℕ} (i : Fin (k + 3)) - (aux : Fin (k + 3) := ⟨k, by omega⟩) - (h_inj : [i, aux, aux + 1].get.Injective := by intro x y; grind) : +public def dec {k : ℕ} (i : Fin (k + 6)) + (aux : Fin (k + 6) := ⟨k, by omega⟩) + (h_inj : [i, aux, aux + 1, aux + 2, aux + 3, aux + 4].get.Injective := + by intro x y; grind) : MultiTapeTM (k + 6) (WithSep OneTwo) := - push ⟨aux, by omega⟩ [] <;> push ⟨aux + 1, by omega⟩ [] <;> - loop i (h_i := by omega) (copy aux (aux + 1) (by sorry) <;> succ aux) <;> - pop ⟨i, by omega⟩ <;> - copy ⟨aux + 1, by omega⟩ ⟨i, by omega⟩ (by sorry) <;> - pop ⟨aux + 1, by omega⟩ <;> - pop ⟨aux, by omega⟩ + dec₀.with_tapes [i, aux, aux + 1, aux + 2, aux + 3, aux + 4].get h_inj @[simp, grind =] -public theorem duplicate_eval_list {k : ℕ} {i : Fin k.succ} - (aux : Fin k.succ := ⟨k, by omega⟩) - (h_inj : [i, aux].get.Injective) - {tapes : Fin k.succ → List (List OneTwo)} : - (duplicate i aux h_inj).eval_list tapes = Part.some (Function.update tapes i - (((tapes i).headD []) :: (tapes i))) := by - simp [duplicate] - grind +public theorem dec_eval_list {k : ℕ} (i aux : Fin (k + 6)) + (h_inj : [i, aux, aux + 1, aux + 2, aux + 3, aux + 4].get.Injective) + (tapes : Fin (k + 6) → List (List OneTwo)) : + (dec i aux h_inj).eval_list tapes = .some (Function.update tapes i + ((dya ((dya_inv ((tapes i).headD [])) - 1)) :: (tapes i).tail)) := by + simpa [dec] using apply_updates_function_update h_inj end Routines diff --git a/Cslib/Computability/Machines/MultiTapeTuring/TapeExtension.lean b/Cslib/Computability/Machines/MultiTapeTuring/TapeExtension.lean index 43c6e9cac..260d5d8cc 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/TapeExtension.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/TapeExtension.lean @@ -63,6 +63,16 @@ public abbrev tapes_extend_by (i : Fin k₂) : γ := if h : i < k₁ then tapes ⟨i, h⟩ else extend_by i +@[simp] +public lemma tapes_extend_by_tapes_take + {γ : Type} + {k₁ k₂ : ℕ} + {h_le : k₁ ≤ k₂} + (tapes : Fin k₂ → γ) : + tapes_extend_by (tapes_take tapes k₁ h_le) tapes = tapes := by + unfold tapes_extend_by tapes_take + simp + @[simp, grind =] public lemma MultiTapeTM.extend_eval {k₁ k₂ : ℕ} (h_le : k₁ ≤ k₂) (tm : MultiTapeTM k₁ α) From e68a1272a81b526116850ede1d0098b44b83e008 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 23 Feb 2026 10:25:45 +0100 Subject: [PATCH 05/20] finish inner algorithm --- .../Machines/MultiTapeTuring/AddRoutine.lean | 2 +- .../Machines/MultiTapeTuring/DecRoutine.lean | 2 +- .../MultiTapeTuring/GraphReachability.lean | 125 +++++++++++++++--- 3 files changed, 106 insertions(+), 23 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean index 3cc0737f8..53f66b37e 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/AddRoutine.lean @@ -48,7 +48,7 @@ theorem add₀_eval_list {tapes : Fin 6 → List (List OneTwo)} : dya_inv ((tapes 1).headD [])) :: (tapes 2)))) := by simp [add₀] by_cases h : dya_inv ((tapes 0).head?.getD []) = 0 - · simp [h]; grind + · simp [h] · grind /-- diff --git a/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean index bad8973f2..9d8cae754 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/DecRoutine.lean @@ -72,7 +72,7 @@ A Turing machine that decrements the dyadic value at the head of tape `i`. If the value is zero already, keeps it at zero. If the tape is empty, pushes zero. -/ public def dec {k : ℕ} (i : Fin (k + 6)) - (aux : Fin (k + 6) := ⟨k, by omega⟩) + (aux : Fin (k + 6) := ⟨k + 1, by omega⟩) (h_inj : [i, aux, aux + 1, aux + 2, aux + 3, aux + 4].get.Injective := by intro x y; grind) : MultiTapeTM (k + 6) (WithSep OneTwo) := diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 1ecd04a84..114a36cb2 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -14,6 +14,7 @@ public import Cslib.Computability.Machines.MultiTapeTuring.EqualRoutine public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine public import Cslib.Computability.Machines.MultiTapeTuring.DuplicateRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.DecRoutine namespace Turing @@ -83,7 +84,7 @@ def reachable(a, b, t, edge): else: pc.push(:loop_continue) | :loop_continue => - c.push(c.top() + 1) + c.top() += 1 pc.push(:loop_start) -- cleanup initial_t.pop() @@ -92,21 +93,25 @@ def reachable(a, b, t, edge): b.pop() -/ -def tapeCount := 20 +abbrev tapeCount := 20 +@[simp, grind =] lemma tape_count_eq : tapeCount = 20 := rfl -def a : Fin tapeCount := ⟨3, sorry⟩ -def b : Fin tapeCount := ⟨4, sorry⟩ -def t : Fin tapeCount := ⟨5, sorry⟩ -def result : Fin tapeCount := ⟨6, sorry⟩ -def initialT : Fin tapeCount := ⟨7, sorry⟩ -def pc : Fin tapeCount := ⟨8, sorry⟩ -def c : Fin tapeCount := ⟨9, sorry⟩ -def mainAux : Fin tapeCount := ⟨10, sorry⟩ +abbrev a : Fin tapeCount := ⟨3, sorry⟩ +abbrev b : Fin tapeCount := ⟨4, sorry⟩ +abbrev t : Fin tapeCount := ⟨5, sorry⟩ +abbrev result : Fin tapeCount := ⟨6, sorry⟩ +abbrev initialT : Fin tapeCount := ⟨7, sorry⟩ +abbrev pc : Fin tapeCount := ⟨8, sorry⟩ +abbrev c : Fin tapeCount := ⟨9, sorry⟩ +abbrev mainAux : Fin tapeCount := ⟨10, sorry⟩ -def l_funStart := dya 1 -def l_loopStart := dya 2 +abbrev l_funStart := dya 1 +abbrev l_loopStart := dya 2 +abbrev l_afterFirstRec := dya 3 +abbrev l_afterSecondRec := dya 4 +abbrev l_loopContinue := dya 5 -- if t = 0: -- result = edge(a, b) @@ -127,9 +132,7 @@ lemma funStart_eval_list else .some (Function.update (Function.update tapes c ([] :: (tapes c))) pc (l_loopStart :: (tapes pc))) := by - have : pc ≠ c := by decide simp [funStart] - grind def infiniteLoop {α : Type} {k : ℕ} : MultiTapeTM k (WithSep α) := sorry @@ -142,6 +145,7 @@ public def eqLit {k : ℕ} MultiTapeTM (k + 3) (WithSep OneTwo) := push aux w <;> eq q aux s h_inj <;> pop aux +@[simp] public theorem eqLit_eval_list {k : ℕ} {q s aux : Fin (k + 3)} {w : List OneTwo} {h_inj : [q, aux, s].get.Injective} {tapes : Fin (k + 3) → List (List OneTwo)} : @@ -171,7 +175,79 @@ def loopStart (maxConfig : List OneTwo) := eqLit c maxConfig mainAux <;> ite mainAux (pop mainAux <;> pop c <;> push result []) - (duplicate a <;> copy c b <;> dec t <;> push pc l_funStart <;> push pc l_loopStart) + (pop mainAux <;> duplicate a <;> copy c b <;> + dec t mainAux (by decide) <;> push pc l_afterFirstRec <;> push pc l_funStart) + +-- TODO this simp lemma is probably not really needed, because the proof is just `simp [loopStart]` + +-- @[simp] +-- lemma loopStart_eval_list +-- (maxConfig : List OneTwo) +-- (loopStart maxConfig).eval_list tapes = .some sorry := by +-- simp [loopStart] +-- sorry + +-- | :after_first_rec => +-- a.pop() +-- b.pop() +-- t = t + 1 +-- if result == 1: +-- a.push(c.top()) +-- b.push(b.top()) +-- t = t - 1 +-- pc.push(:after_second_rec) +-- pc.push(:fun_start) +-- else: +-- result = 0 +-- pc.push(:loop_continue) + +def afterFirstRec := + pop a <;> pop b <;> succ t <;> ite result + (duplicate c <;> duplicate b <;> dec t mainAux (by decide) <;> + push pc l_afterSecondRec <;> push pc l_funStart) + (pop result <;> push result [] <;> push pc l_loopContinue) + +-- | :after_second_rec => +-- a.pop() +-- b.pop() +-- t = t + 1 +-- if result == 1: +-- c.pop() +-- else: +-- pc.push(:loop_continue) + +def afterSecondRec := + pop a <;> pop b <;> succ t <;> ite result (pop c) (push pc l_loopContinue) + +-- | :loop_continue => +-- c.top() += 1 +-- pc.push(:loop_start) + +def loopContinue := succ c <;> push pc l_loopStart + +public def iteLit {k : ℕ} + (i : Fin (k + 3)) + (w : List OneTwo) + (aux : Fin (k + 3) := ⟨k + 1, by omega⟩) + (tm₁ tm₂ : MultiTapeTM (k + 3) (WithSep OneTwo)) + (h_inj : [i, aux, aux + 1].get.Injective := by decide) : + MultiTapeTM (k + 3) (WithSep OneTwo) := + eqLit i w (aux + 1) aux (h_inj := by intro x y; grind) <;> + ite (aux + 1) (pop (aux + 1) <;> tm₁) (pop (aux + 1) <;> tm₂) + +-- TODO not sure if this simp lemma is needed. We can also put @[simp] at iteLit instead. + +@[simp] +lemma itLit_eval_list {k : ℕ} + (i : Fin (k + 3)) + (w : List OneTwo) + (aux : Fin (k + 3)) + (tm₁ tm₂ : MultiTapeTM (k + 3) (WithSep OneTwo)) + (h_inj : [i, aux, aux + 1].get.Injective) + (tapes : Fin (k + 3) → List (List OneTwo)) : + (iteLit i w aux tm₁ tm₂ h_inj).eval_list tapes = + if (tapes i).headD [] = w then tm₁.eval_list tapes else tm₂.eval_list tapes := by + simp [iteLit] public def matchCombine {k : ℕ} (i : Fin (k + 3)) (aux : Fin (k + 3)) (h_inj : [i, aux, aux + 1].get.Injective) @@ -183,15 +259,22 @@ public def matchCombine {k : ℕ} eqLit i w aux (aux + 1) (h_inj := by sorry /- use swap on h_inj? -/) <;> ite aux (pop aux <;> tm) (pop aux <;> matchCombine i aux (by intro x y; grind) branches) -def innerLoop (edge : MultiTapeTM tapeCount (WithSep OneTwo)) : +def innerLoop (edge : MultiTapeTM tapeCount (WithSep OneTwo)) (maxConfig : List OneTwo) : MultiTapeTM tapeCount (WithSep OneTwo) := - matchCombine pc mainAux (by decide) - [ (l_funStart, funStart edge), - (l_loopStart, loop 1, infiniteLoop) ] - + iteLit pc l_funStart mainAux (pop pc <;> funStart edge) + (iteLit pc l_loopStart mainAux (pop pc <;> loopStart maxConfig) + (iteLit pc l_afterFirstRec mainAux (pop pc <;> afterFirstRec) + (iteLit pc l_afterSecondRec mainAux (pop pc <;> afterSecondRec) + (pop pc <;> loopContinue)))) +lemma innerLoop_eval_list + (edge : MultiTapeTM tapeCount (WithSep OneTwo)) + (maxConfig : List OneTwo) + (tapes : Fin tapeCount → List (List OneTwo)) : + (innerLoop edge maxConfig).eval_list tapes = sorry := by + simp [innerLoop, loopStart, afterFirstRec, afterSecondRec, loopContinue] + sorry -theorem reachable end Routines end Turing From cdc5eb193469dd29d73f18023974a3cbb57475f3 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 23 Feb 2026 17:53:28 +0100 Subject: [PATCH 06/20] Finish complete algorithm. --- .../MultiTapeTuring/GraphReachability.lean | 109 ++++++++++++++++-- .../MultiTapeTuring/WhileCombinator.lean | 12 +- 2 files changed, 108 insertions(+), 13 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 114a36cb2..850995a82 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -15,7 +15,7 @@ public import Cslib.Computability.Machines.MultiTapeTuring.PushRoutine public import Cslib.Computability.Machines.MultiTapeTuring.PopRoutine public import Cslib.Computability.Machines.MultiTapeTuring.DuplicateRoutine public import Cslib.Computability.Machines.MultiTapeTuring.DecRoutine - +public import Cslib.Computability.Machines.MultiTapeTuring.WhileCombinator namespace Turing @@ -42,7 +42,6 @@ uses "goto", and every variable is a stack: def reachable(a, b, t, edge): result = 0 - initial_t = t pc = [:fun_start] while !pc.is_empty(): match pc.pop() @@ -87,7 +86,6 @@ def reachable(a, b, t, edge): c.top() += 1 pc.push(:loop_start) -- cleanup - initial_t.pop() t.pop() a.pop() b.pop() @@ -98,10 +96,10 @@ abbrev tapeCount := 20 @[simp, grind =] lemma tape_count_eq : tapeCount = 20 := rfl -abbrev a : Fin tapeCount := ⟨3, sorry⟩ -abbrev b : Fin tapeCount := ⟨4, sorry⟩ -abbrev t : Fin tapeCount := ⟨5, sorry⟩ -abbrev result : Fin tapeCount := ⟨6, sorry⟩ +abbrev a : Fin tapeCount := ⟨0, sorry⟩ +abbrev b : Fin tapeCount := ⟨1, sorry⟩ +abbrev t : Fin tapeCount := ⟨3, sorry⟩ +abbrev result : Fin tapeCount := ⟨2, sorry⟩ abbrev initialT : Fin tapeCount := ⟨7, sorry⟩ abbrev pc : Fin tapeCount := ⟨8, sorry⟩ abbrev c : Fin tapeCount := ⟨9, sorry⟩ @@ -275,6 +273,103 @@ lemma innerLoop_eval_list simp [innerLoop, loopStart, afterFirstRec, afterSecondRec, loopContinue] sorry +lemma relatesInStepsExp {α : Type} + (r : α → α → Prop) + (a b : α) + (t : ℕ) : + (Relation.RelatesInSteps r a b (Nat.pow 2 t.succ)) ↔ + ∃ c, Relation.RelatesInSteps r a c (Nat.pow 2 t) ∧ + Relation.RelatesInSteps r c b (Nat.pow 2 t) := by + sorry + +def finiteRel (r : (List OneTwo) → (List OneTwo) → Prop) (max : ℕ) : Prop := + ∀ a b, r a b → (dya_inv a < max ∧ dya_inv b < max) + +def edge_semantics + (r : (List OneTwo) → (List OneTwo) → Prop) + (h_r_dec : ∀ x y, Decidable (r x y)) + (edge : MultiTapeTM tapeCount (WithSep OneTwo)) : Prop := + ∀ tapes, + edge.eval_list tapes = .some (if r ((tapes a).headD []) ((tapes b).headD []) then + Function.update tapes result ([.one] :: (tapes result)) + else + Function.update tapes result ([] :: (tapes result))) + +lemma inner_loop_induction_basis + (r : (List OneTwo) → (List OneTwo) → Prop) + (h_r_dec : ∀ x y, Decidable (r x y)) + (max : ℕ) + (edge : MultiTapeTM tapeCount (WithSep OneTwo)) + (h_edge_semantics : edge_semantics r h_r_dec edge) + (tapes : Fin tapeCount → List (List OneTwo)) + (h_pc : (tapes pc).head?.getD [] = l_funStart) + (h_t : (tapes t).head?.getD [] = []) : + (innerLoop edge (dya max)).eval_list tapes = .some + (Function.update (Function.update tapes + pc (tapes pc).tail) + result (if r ((tapes a).headD []) ((tapes b).headD []) then + [.one] :: (tapes result) + else + [] :: (tapes result))) := by + unfold edge_semantics at h_edge_semantics + simp [innerLoop, h_pc, h_t, h_edge_semantics] + grind + +def reachability (edge : MultiTapeTM tapeCount (WithSep OneTwo)) (maxConfig : List OneTwo) : + MultiTapeTM tapeCount (WithSep OneTwo) := + doWhile pc (innerLoop edge maxConfig) + +theorem reachability_eval_list + (r : (List OneTwo) → (List OneTwo) → Prop) + (h_r_dec : ∀ x y, Decidable (r x y)) + (h_rs_dec : ∀ x y t, Decidable (Relation.RelatesInSteps r x y t)) + (max : ℕ) + (h_finite : finiteRel r max) + (edge : MultiTapeTM tapeCount (WithSep OneTwo)) + (h_edge_semantics : edge_semantics r h_r_dec edge) + (t_val : ℕ) + (a_val b_val : List OneTwo) + (tapes : Fin tapeCount → List (List OneTwo)) : + (push a a_val <;> push b b_val <;> push t (dya t_val) <;> + reachability edge (dya max)).eval_list tapes = .some (Function.update tapes result ( + if Relation.RelatesInSteps r a_val b_val t_val then + [.one] :: (tapes result) + else + [] :: (tapes result))) := by + sorry + +lemma induction_step + (r : (List OneTwo) → (List OneTwo) → Prop) + (h_r_dec : ∀ x y, Decidable (r x y)) + (max : ℕ) + (edge : MultiTapeTM tapeCount (WithSep OneTwo)) + (h_edge_semantics : edge_semantics r h_r_dec edge) + (tapes : Fin tapeCount → List (List OneTwo)) + (h_pc : (tapes pc).head?.getD [] = l_funStart) + (t_val : ℕ) + (h_t : (tapes t).head?.getD [] = dya t_val.succ) + (h_ih : ∀ tapes', + (tapes' pc).head?.getD [] = l_funStart → + (tapes' t).head?.getD [] = dya t_val → + (innerLoop edge (dya max)).eval_list tapes' = .some + (Function.update (Function.update tapes' + pc (tapes' pc).tail) + result (if r ((tapes' a).headD []) ((tapes' b).headD []) then + [.one] :: (tapes' result) + else + [] :: (tapes' result))) → + : + (innerLoop edge (dya max)).eval_list tapes = .some + (Function.update (Function.update tapes + pc (tapes pc).tail) + result (if r ((tapes a).headD []) ((tapes b).headD []) then + [.one] :: (tapes result) + else + [] :: (tapes result))) := by + unfold edge_semantics at h_edge_semantics + simp [innerLoop, h_pc, h_t, h_edge_semantics] + grind + end Routines end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean index 2538c73f4..eafbea2a8 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean @@ -50,14 +50,14 @@ public def doWhile (i : Fin k) (tm : MultiTapeTM k (WithSep α)) : M _ syms := sorry @[simp] -public theorem doWhile_eval +public theorem doWhile_eval_list (i : Fin k) (tm : MultiTapeTM k (WithSep α)) - (tapes_seq : ℕ → Fin k → List (List α)) - (h_transform : ∀ j, tm.eval_list (tapes_seq j) = .some (tapes_seq j.succ)) - (h_nonempty : ∀ j, tapes_seq j i ≠ []) - (h_stops : ∃ m, (tapes_seq m i).head (h_nonempty m) = []) : - (doWhile i tm).eval_list (tapes_seq 0) = .some (tapes_seq (Nat.find h_stops)) := by + {tapes : Fin k → List (List α)} + (f : (Fin k → List (List α)) → Fin k → List (List α)) + (h_computes : ∀ tapes, tm.eval_list tapes = .some (f tapes)) + (h_halts : ∃ t, (f^[t] tapes) i = []) : + (doWhile i tm).eval_list tapes = .some (f^[Nat.find h_halts] tapes) := by sorry end Routines From ab69c63bc480ec0e1515f9ca153b7ab2e2bd7f79 Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 24 Feb 2026 14:39:07 +0100 Subject: [PATCH 07/20] Halting Turing machines. --- Cslib/Computability/Machines/MultiTapeTuring/Basic.lean | 8 ++++++++ .../Machines/MultiTapeTuring/ListEncoding.lean | 6 ++++++ 2 files changed, 14 insertions(+) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean index 67c89864c..5336cc2e2 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean @@ -238,6 +238,10 @@ def TransformsTapes (tapes tapes' : Fin k → BiTape α) : Prop := ∃ t, tm.TransformsTapesInTime tapes tapes' t +/-- The Turing machine `tm` eventually halts starting from any initial tape configuration. -/ +def haltsOn (tm : MultiTapeTM k α) (tapes : Fin k → BiTape α) : Prop := + ∃ tapes', tm.TransformsTapes tapes tapes' + @[scoped grind =] lemma relatesInSteps_iff_step_iter_eq_some (tm : MultiTapeTM k α) @@ -294,6 +298,10 @@ public noncomputable def eval (tm : MultiTapeTM k α) (tapes : Fin k → BiTape Part (Fin k → BiTape α) := ⟨∃ tapes', tm.TransformsTapes tapes tapes', fun h => h.choose⟩ +public noncomputable def eval_tot (tm : MultiTapeTM k α) {h : ∀ tapes, tm.haltsOn tapes} + (tapes : Fin k → BiTape α) : Fin k → BiTape α := + (tm.eval tapes).get (h tapes) + -- TODO use MultiTapeTM.configurations? -- TODO this is a simple consequence of relatesInSteps_iff_configurations_eq_some, maybe not needed. lemma configurations_of_transformsTapesInTime diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean index 255883715..feba4872a 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean @@ -53,6 +53,12 @@ public def MultiTapeTM.TransformsLists (tapes tapes' : Fin k → List (List α)) : Prop := tm.TransformsTapes (listToTape ∘ tapes) (listToTape ∘ tapes') +/-- The Turing machine `tm` halts starting with list-encoded tapes `tapes`. -/ +public def MultiTapeTM.HaltsOnLists + (tm : MultiTapeTM k (WithSep α)) + (tapes : Fin k → List (List α)) : Prop := + ∃ tapes', tm.TransformsTapes (listToTape ∘ tapes) (listToTape ∘ tapes') + /-- Execute the Turing machine `tm` on the list-encoded tapes `tapes`. -/ public noncomputable def MultiTapeTM.eval_list (tm : MultiTapeTM k (WithSep α)) From 0b98846479011ae270462ff536d7aca5c3500761 Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 24 Feb 2026 14:49:14 +0100 Subject: [PATCH 08/20] While loop using always-halting TMs. --- .../Machines/MultiTapeTuring/ListEncoding.lean | 9 +++++++++ .../MultiTapeTuring/WhileCombinator.lean | 16 ++++++++-------- 2 files changed, 17 insertions(+), 8 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean index feba4872a..f099d2988 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean @@ -66,6 +66,15 @@ public noncomputable def MultiTapeTM.eval_list Part (Fin k → List (List α)) := ⟨∃ tapes', tm.TransformsLists tapes tapes', fun h => h.choose⟩ +/-- Execute the Turing machine `tm` knowing that it always halts, thus yielding a total function +on the tapes. -/ +public noncomputable def MultiTapeTM.eval_list_tot + (tm : MultiTapeTM k (WithSep α)) + (h_alwaysHalts : ∀ tapes, tm.HaltsOnLists tapes) + (tapes : Fin k → List (List α)) : + Fin k → List (List α) := + (tm.eval_list tapes).get (h_alwaysHalts tapes) + @[simp, grind =] public theorem MultiTapeTM.extend_eval_list {α : Type} [Fintype α] diff --git a/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean index 2538c73f4..19e24e9f9 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean @@ -50,14 +50,14 @@ public def doWhile (i : Fin k) (tm : MultiTapeTM k (WithSep α)) : M _ syms := sorry @[simp] -public theorem doWhile_eval - (i : Fin k) - (tm : MultiTapeTM k (WithSep α)) - (tapes_seq : ℕ → Fin k → List (List α)) - (h_transform : ∀ j, tm.eval_list (tapes_seq j) = .some (tapes_seq j.succ)) - (h_nonempty : ∀ j, tapes_seq j i ≠ []) - (h_stops : ∃ m, (tapes_seq m i).head (h_nonempty m) = []) : - (doWhile i tm).eval_list (tapes_seq 0) = .some (tapes_seq (Nat.find h_stops)) := by +public theorem doWhile_eval_list + {i : Fin k} + {tm : MultiTapeTM k (WithSep α)} + {tapes : Fin k → List (List α)} + (h_halts : ∀ tapes', tm.HaltsOnLists tapes') + (h_loopEnds : ∃ t, ((tm.eval_list_tot h_halts)^[n] tapes i).headD [] = []) : + (doWhile i tm).eval_list tapes = .some + ((tm.eval_list_tot h_halts)^[Nat.find h_loopEnds] tapes) := by sorry end Routines From 55b1e3da049119056c3cc44399a587b9f3a1c39a Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 24 Feb 2026 15:21:15 +0100 Subject: [PATCH 09/20] Fix lint warnings. --- Cslib/Computability/Machines/MultiTapeTuring/Basic.lean | 3 +++ .../Machines/MultiTapeTuring/WhileCombinator.lean | 8 ++++---- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean index 5336cc2e2..5d1f04646 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/Basic.lean @@ -298,6 +298,9 @@ public noncomputable def eval (tm : MultiTapeTM k α) (tapes : Fin k → BiTape Part (Fin k → BiTape α) := ⟨∃ tapes', tm.TransformsTapes tapes tapes', fun h => h.choose⟩ +/-- +Execute the Turing machine `tm` on initial tapes `tapes` given a proof that it always halts +and thus this yields a total function. -/ public noncomputable def eval_tot (tm : MultiTapeTM k α) {h : ∀ tapes, tm.haltsOn tapes} (tapes : Fin k → BiTape α) : Fin k → BiTape α := (tm.eval tapes).get (h tapes) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean index 19e24e9f9..dbc787219 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/WhileCombinator.lean @@ -54,10 +54,10 @@ public theorem doWhile_eval_list {i : Fin k} {tm : MultiTapeTM k (WithSep α)} {tapes : Fin k → List (List α)} - (h_halts : ∀ tapes', tm.HaltsOnLists tapes') - (h_loopEnds : ∃ t, ((tm.eval_list_tot h_halts)^[n] tapes i).headD [] = []) : - (doWhile i tm).eval_list tapes = .some - ((tm.eval_list_tot h_halts)^[Nat.find h_loopEnds] tapes) := by + (h_halts : ∀ tapes', tm.HaltsOnLists tapes') : + (doWhile i tm).eval_list tapes = + ⟨∃ n, ((tm.eval_list_tot h_halts)^[n] tapes i).head?.getD [] = [], + fun h_loopEnds => (tm.eval_list_tot h_halts)^[Nat.find h_loopEnds] tapes⟩ := by sorry end Routines From f6818cfed17e5552252a5f9b3c14846768e058bb Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 24 Feb 2026 20:44:24 +0100 Subject: [PATCH 10/20] correction for halting. --- .../Machines/MultiTapeTuring/ListEncoding.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean index f099d2988..7e44e4d3b 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean @@ -57,14 +57,21 @@ public def MultiTapeTM.TransformsLists public def MultiTapeTM.HaltsOnLists (tm : MultiTapeTM k (WithSep α)) (tapes : Fin k → List (List α)) : Prop := - ∃ tapes', tm.TransformsTapes (listToTape ∘ tapes) (listToTape ∘ tapes') + ∃ tapes', tm.TransformsLists tapes tapes' /-- Execute the Turing machine `tm` on the list-encoded tapes `tapes`. -/ public noncomputable def MultiTapeTM.eval_list (tm : MultiTapeTM k (WithSep α)) (tapes : Fin k → List (List α)) : Part (Fin k → List (List α)) := - ⟨∃ tapes', tm.TransformsLists tapes tapes', fun h => h.choose⟩ + ⟨tm.HaltsOnLists tapes, fun h => h.choose⟩ + +public theorem MultiTapeTM.HaltsOnLists_of_eval_list + {tm : MultiTapeTM k (WithSep α)} + {tapes : Fin k → List (List α)} + (h_dom : (tm.eval_list tapes).Dom) : + tm.HaltsOnLists tapes := by + simpa using h_dom /-- Execute the Turing machine `tm` knowing that it always halts, thus yielding a total function on the tapes. -/ From e4cedbc5f86eddb790cf0d60093125d2a9b6cab3 Mon Sep 17 00:00:00 2001 From: crei Date: Tue, 24 Feb 2026 20:44:38 +0100 Subject: [PATCH 11/20] partial inner loop loop semantics. --- .../MultiTapeTuring/GraphReachability.lean | 26 +++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 850995a82..ccdc32be1 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -315,6 +315,29 @@ lemma inner_loop_induction_basis simp [innerLoop, h_pc, h_t, h_edge_semantics] grind +lemma inner_loop_halts_on_lists + {r : (List OneTwo) → (List OneTwo) → Prop} + {h_r_dec : ∀ x y, Decidable (r x y)} + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} + (h_edge_semantics : edge_semantics r h_r_dec edge) + {maxConfig : List OneTwo} : + ∀ tapes, (innerLoop edge maxConfig).HaltsOnLists tapes := by + intro tapes + apply MultiTapeTM.HaltsOnLists_of_eval_list + unfold edge_semantics at h_edge_semantics + simp [innerLoop, loopStart, afterFirstRec, afterSecondRec, loopContinue, h_edge_semantics] + split_ifs -- todo use <;> + · simp + · simp + · simp + · simp + · simp + · simp + · simp + · simp + · simp + · simp + def reachability (edge : MultiTapeTM tapeCount (WithSep OneTwo)) (maxConfig : List OneTwo) : MultiTapeTM tapeCount (WithSep OneTwo) := doWhile pc (innerLoop edge maxConfig) @@ -336,6 +359,9 @@ theorem reachability_eval_list [.one] :: (tapes result) else [] :: (tapes result))) := by + simp [reachability] + rw [doWhile_eval_list (inner_loop_halts_on_lists h_edge_semantics)] + simp sorry lemma induction_step From fcebfa358fa438c8ae2cfacee7dceb46339b2e39 Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 25 Feb 2026 17:14:52 +0100 Subject: [PATCH 12/20] Re-write algorithm without shortcuts. --- .../MultiTapeTuring/GraphReachability.lean | 357 ++++++++---------- .../MultiTapeTuring/ListEncoding.lean | 11 + Cslib/Foundations/Data/RelatesInSteps.lean | 3 + 3 files changed, 171 insertions(+), 200 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index ccdc32be1..4d93fde92 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -32,29 +32,28 @@ def reachable(a, b, t, r): if t = 0: return r(a, b) else: + result = False for c in vertices: - if reachable(a, c, t - 1, r) and reachable(c, b, t - 1, r): - return True - return False + result |= reachable(a, c, t - 1, r) and reachable(c, b, t - 1, r) + return result Until we have a generic mechanism for recursion, let's translate this into a program that uses "goto", and every variable is a stack: def reachable(a, b, t, edge): - result = 0 pc = [:fun_start] while !pc.is_empty(): match pc.pop() | :fun_start => if t = 0: - result = edge(a, b) + result.push(edge(a, b)) else: c.push(0) + result.push(0) pc.push(:loop_start) | :loop_start => if c.top() = num_vertices: c.pop() - result = 0 else: a.push(a.top()) b.push(c.top()) @@ -64,25 +63,16 @@ def reachable(a, b, t, edge): | :after_first_rec => a.pop() b.pop() - t = t + 1 - if result == 1: - a.push(c.top()) - b.push(b.top()) - t = t - 1 - pc.push(:after_second_rec) - pc.push(:fun_start) - else: - result = 0 - pc.push(:loop_continue) + -- we keep the result of the first recursive call. + a.push(c.top()) + b.push(b.top()) + pc.push(:after_second_rec) + pc.push(:fun_start) | :after_second_rec => a.pop() b.pop() t = t + 1 - if result == 1: - c.pop() - else: - pc.push(:loop_continue) - | :loop_continue => + result.push(result.pop() ∨ result.pop() ∨ result.pop()) c.top() += 1 pc.push(:loop_start) -- cleanup @@ -111,29 +101,6 @@ abbrev l_afterFirstRec := dya 3 abbrev l_afterSecondRec := dya 4 abbrev l_loopContinue := dya 5 --- if t = 0: --- result = edge(a, b) --- else: --- c.push(0) --- pc.push(:loop_start) - -def funStart (edge : MultiTapeTM tapeCount (WithSep OneTwo)) := - ite t (push c [] <;> push pc l_loopStart) edge - -@[simp] -lemma funStart_eval_list - (tapes : Fin tapeCount → List (List OneTwo)) - (edge : MultiTapeTM tapeCount (WithSep OneTwo)) : - (funStart edge).eval_list tapes = - if (tapes t).headD [] = [] then - (edge.eval_list tapes) - else - .some (Function.update (Function.update tapes c ([] :: (tapes c))) - pc (l_loopStart :: (tapes pc))) := by - simp [funStart] - -def infiniteLoop {α : Type} {k : ℕ} : MultiTapeTM k (WithSep α) := sorry - public def eqLit {k : ℕ} (q : Fin (k + 3)) (w : List OneTwo) @@ -158,10 +125,43 @@ public theorem eqLit_eval_list {k : ℕ} {q s aux : Fin (k + 3)} {w : List OneTw have h_neq : q ≠ aux := Function.Injective.ne h_inj (a₁ := 0) (a₂ := 1) (by grind) grind +@[simp] +public def iteLit {k : ℕ} + (i : Fin (k + 3)) + (w : List OneTwo) + (aux : Fin (k + 3) := ⟨k + 1, by omega⟩) + (tm₁ tm₂ : MultiTapeTM (k + 3) (WithSep OneTwo)) + (h_inj : [i, aux, aux + 1].get.Injective := by decide) : + MultiTapeTM (k + 3) (WithSep OneTwo) := + eqLit i w (aux + 1) aux (h_inj := by intro x y; grind) <;> + ite (aux + 1) (pop (aux + 1) <;> tm₁) (pop (aux + 1) <;> tm₂) + +@[simp] +public def combineOr {k : ℕ} (i : Fin k) : + MultiTapeTM k (WithSep OneTwo) := + ite i + (pop i <;> pop i <;> push i [OneTwo.one]) + (pop i <;> + ite i + (pop i <;> push i [OneTwo.one]) + (pop i <;> push i [])) + + +-- | :fun_start => +-- if t = 0: +-- result.push(edge(a, b)) +-- else: +-- c.push(0) +-- result.push(0) +-- pc.push(:loop_start) + +@[simp] +def funStart (edge : MultiTapeTM tapeCount (WithSep OneTwo)) := + ite t (push c [] <;> push result [] <;> push pc l_loopStart) edge + -- | :loop_start => -- if c.top() = num_vertices: -- c.pop() --- result = 0 -- else: -- a.push(a.top()) -- b.push(c.top()) @@ -169,109 +169,48 @@ public theorem eqLit_eval_list {k : ℕ} {q s aux : Fin (k + 3)} {w : List OneTw -- pc.push(:after_first_rec) -- pc.push(:fun_start) +@[simp] def loopStart (maxConfig : List OneTwo) := - eqLit c maxConfig mainAux <;> - ite mainAux - (pop mainAux <;> pop c <;> push result []) - (pop mainAux <;> duplicate a <;> copy c b <;> - dec t mainAux (by decide) <;> push pc l_afterFirstRec <;> push pc l_funStart) - --- TODO this simp lemma is probably not really needed, because the proof is just `simp [loopStart]` - --- @[simp] --- lemma loopStart_eval_list --- (maxConfig : List OneTwo) --- (loopStart maxConfig).eval_list tapes = .some sorry := by --- simp [loopStart] --- sorry + iteLit c maxConfig mainAux + (pop c) + (duplicate a <;> copy c b <;> + dec t mainAux (by decide) <;> push pc l_afterFirstRec <;> push pc l_funStart) -- | :after_first_rec => --- a.pop() --- b.pop() --- t = t + 1 --- if result == 1: --- a.push(c.top()) --- b.push(b.top()) --- t = t - 1 --- pc.push(:after_second_rec) --- pc.push(:fun_start) --- else: --- result = 0 --- pc.push(:loop_continue) +-- a.pop() +-- b.pop() +-- -- we keep the result of the first recursive call. +-- a.push(c.top()) +-- b.push(b.top()) +-- pc.push(:after_second_rec) +-- pc.push(:fun_start) +@[simp] def afterFirstRec := - pop a <;> pop b <;> succ t <;> ite result - (duplicate c <;> duplicate b <;> dec t mainAux (by decide) <;> - push pc l_afterSecondRec <;> push pc l_funStart) - (pop result <;> push result [] <;> push pc l_loopContinue) + pop a <;> pop b <;> copy c a <;> duplicate b <;> + push pc l_afterSecondRec <;> push pc l_funStart -- | :after_second_rec => --- a.pop() --- b.pop() --- t = t + 1 --- if result == 1: --- c.pop() --- else: --- pc.push(:loop_continue) +-- a.pop() +-- b.pop() +-- t = t + 1 +-- result.push(result.pop() ∨ result.pop() ∨ result.pop()) +-- c.top() += 1 +-- pc.push(:loop_start) +@[simp] def afterSecondRec := - pop a <;> pop b <;> succ t <;> ite result (pop c) (push pc l_loopContinue) - --- | :loop_continue => --- c.top() += 1 --- pc.push(:loop_start) - -def loopContinue := succ c <;> push pc l_loopStart - -public def iteLit {k : ℕ} - (i : Fin (k + 3)) - (w : List OneTwo) - (aux : Fin (k + 3) := ⟨k + 1, by omega⟩) - (tm₁ tm₂ : MultiTapeTM (k + 3) (WithSep OneTwo)) - (h_inj : [i, aux, aux + 1].get.Injective := by decide) : - MultiTapeTM (k + 3) (WithSep OneTwo) := - eqLit i w (aux + 1) aux (h_inj := by intro x y; grind) <;> - ite (aux + 1) (pop (aux + 1) <;> tm₁) (pop (aux + 1) <;> tm₂) + pop a <;> pop b <;> succ t <;> + combineOr result <;> combineOr result <;> succ c <;> push pc l_loopStart --- TODO not sure if this simp lemma is needed. We can also put @[simp] at iteLit instead. @[simp] -lemma itLit_eval_list {k : ℕ} - (i : Fin (k + 3)) - (w : List OneTwo) - (aux : Fin (k + 3)) - (tm₁ tm₂ : MultiTapeTM (k + 3) (WithSep OneTwo)) - (h_inj : [i, aux, aux + 1].get.Injective) - (tapes : Fin (k + 3) → List (List OneTwo)) : - (iteLit i w aux tm₁ tm₂ h_inj).eval_list tapes = - if (tapes i).headD [] = w then tm₁.eval_list tapes else tm₂.eval_list tapes := by - simp [iteLit] - -public def matchCombine {k : ℕ} - (i : Fin (k + 3)) (aux : Fin (k + 3)) (h_inj : [i, aux, aux + 1].get.Injective) - (branches : List ((List OneTwo) × (MultiTapeTM (k + 3) (WithSep OneTwo)))) : - MultiTapeTM (k + 3) (WithSep OneTwo) := - match branches with - | [] => infiniteLoop - | (w, tm) :: branches => - eqLit i w aux (aux + 1) (h_inj := by sorry /- use swap on h_inj? -/) <;> - ite aux (pop aux <;> tm) (pop aux <;> matchCombine i aux (by intro x y; grind) branches) - def innerLoop (edge : MultiTapeTM tapeCount (WithSep OneTwo)) (maxConfig : List OneTwo) : MultiTapeTM tapeCount (WithSep OneTwo) := iteLit pc l_funStart mainAux (pop pc <;> funStart edge) (iteLit pc l_loopStart mainAux (pop pc <;> loopStart maxConfig) (iteLit pc l_afterFirstRec mainAux (pop pc <;> afterFirstRec) - (iteLit pc l_afterSecondRec mainAux (pop pc <;> afterSecondRec) - (pop pc <;> loopContinue)))) - -lemma innerLoop_eval_list - (edge : MultiTapeTM tapeCount (WithSep OneTwo)) - (maxConfig : List OneTwo) - (tapes : Fin tapeCount → List (List OneTwo)) : - (innerLoop edge maxConfig).eval_list tapes = sorry := by - simp [innerLoop, loopStart, afterFirstRec, afterSecondRec, loopContinue] - sorry + (pop pc <;> afterSecondRec))) lemma relatesInStepsExp {α : Type} (r : α → α → Prop) @@ -285,6 +224,14 @@ lemma relatesInStepsExp {α : Type} def finiteRel (r : (List OneTwo) → (List OneTwo) → Prop) (max : ℕ) : Prop := ∀ a b, r a b → (dya_inv a < max ∧ dya_inv b < max) +lemma finiteRel_apply₁ {r : (List OneTwo) → (List OneTwo) → Prop} {max : ℕ} + (h_finite : finiteRel r max) {a b : List OneTwo} (h_r : r a b) : + dya_inv a < max := (h_finite a b h_r).1 + +lemma finiteRel_apply₂ {r : (List OneTwo) → (List OneTwo) → Prop} {max : ℕ} + (h_finite : finiteRel r max) {a b : List OneTwo} (h_r : r a b) : + dya_inv b < max := (h_finite a b h_r).2 + def edge_semantics (r : (List OneTwo) → (List OneTwo) → Prop) (h_r_dec : ∀ x y, Decidable (r x y)) @@ -295,26 +242,6 @@ def edge_semantics else Function.update tapes result ([] :: (tapes result))) -lemma inner_loop_induction_basis - (r : (List OneTwo) → (List OneTwo) → Prop) - (h_r_dec : ∀ x y, Decidable (r x y)) - (max : ℕ) - (edge : MultiTapeTM tapeCount (WithSep OneTwo)) - (h_edge_semantics : edge_semantics r h_r_dec edge) - (tapes : Fin tapeCount → List (List OneTwo)) - (h_pc : (tapes pc).head?.getD [] = l_funStart) - (h_t : (tapes t).head?.getD [] = []) : - (innerLoop edge (dya max)).eval_list tapes = .some - (Function.update (Function.update tapes - pc (tapes pc).tail) - result (if r ((tapes a).headD []) ((tapes b).headD []) then - [.one] :: (tapes result) - else - [] :: (tapes result))) := by - unfold edge_semantics at h_edge_semantics - simp [innerLoop, h_pc, h_t, h_edge_semantics] - grind - lemma inner_loop_halts_on_lists {r : (List OneTwo) → (List OneTwo) → Prop} {h_r_dec : ∀ x y, Decidable (r x y)} @@ -325,9 +252,8 @@ lemma inner_loop_halts_on_lists intro tapes apply MultiTapeTM.HaltsOnLists_of_eval_list unfold edge_semantics at h_edge_semantics - simp [innerLoop, loopStart, afterFirstRec, afterSecondRec, loopContinue, h_edge_semantics] - split_ifs -- todo use <;> - · simp + simp [h_edge_semantics] + split_ifs · simp · simp · simp @@ -335,67 +261,98 @@ lemma inner_loop_halts_on_lists · simp · simp · simp + split_ifs + · simp + · simp · simp · simp -def reachability (edge : MultiTapeTM tapeCount (WithSep OneTwo)) (maxConfig : List OneTwo) : - MultiTapeTM tapeCount (WithSep OneTwo) := - doWhile pc (innerLoop edge maxConfig) +def reachability + (edge : MultiTapeTM tapeCount (WithSep OneTwo)) + (maxConfig : List OneTwo) + (x y : List OneTwo) + (t_val : ℕ) := + push a x <;> push b y <;> push t (dya t_val) <;> push pc [] <;> push pc l_funStart <;> + doWhile pc (innerLoop edge maxConfig) <;> + pop t <;> pop a <;> pop b + +@[simp] +def iter_count_bound (max : ℕ) (t : ℕ) : ℕ := match t with + | .zero => 1 + | .succ t' => 2 + max * (3 + 2 * iter_count_bound max t') + +@[simp] +noncomputable def innerLoopFun + {r : (List OneTwo) → (List OneTwo) → Prop} + {h_r_dec : ∀ x y, Decidable (r x y)} + (max : ℕ) + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} + (h_edge_semantics : edge_semantics r h_r_dec edge) := + (innerLoop edge (dya max)).eval_list_tot (inner_loop_halts_on_lists h_edge_semantics) + +-- TODO continue here: prove this theorem by induction. +lemma loop_semantics + {r : (List OneTwo) → (List OneTwo) → Prop} + {h_r_dec : ∀ x y, Decidable (r x y)} + (h_rs_dec : ∀ x y t, Decidable (Relation.RelatesInSteps r x y t)) + {max : ℕ} + (h_finite : finiteRel r max) + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} + (h_edge_semantics : edge_semantics r h_r_dec edge) + (tapes : Fin tapeCount → List (List OneTwo)) + (h_pc_funStart : (tapes pc).head?.getD [] = l_funStart) : + (innerLoopFun max h_edge_semantics)^[iter_count_bound max (dya_inv ((tapes t).headD []))] + tapes = Function.update (Function.update tapes + pc (tapes pc).tail) + result ( + if Relation.RelatesInSteps r ((tapes a).headD []) ((tapes b).headD []) + (Nat.pow 2 (dya_inv ((tapes t).headD []))) then + [.one] :: (tapes result) + else + [] :: (tapes result)) ∧ + ∀ n' < iter_count_bound max (dya_inv ((tapes t).headD [])), + (((innerLoopFun max h_edge_semantics)^[n'] tapes) pc).length ≥ (tapes pc).length := by + induction h_t : (dya_inv ((tapes t).headD [])) generalizing tapes with + | zero => + have h_t_dya : (tapes t).head?.getD [] = dya 0 := by rw [← h_t]; simp + unfold edge_semantics at h_edge_semantics + simp [h_edge_semantics, h_pc_funStart, h_t_dya, Relation.RelatesInSteps.single_iff] + split + · simp + · simp + | succ t_val ih => + by_cases h_rel : Relation.RelatesInSteps r + ((tapes a).headD []) ((tapes b).headD []) (Nat.pow 2 (t_val + 1)) + · simp only [h_rel] + simp + obtain ⟨c, h_c_rel⟩ := + (relatesInStepsExp r ((tapes a).headD []) ((tapes b).headD []) t_val).mp h_rel + have h_c_le : dya_inv c < max := by sorry + + sorry + · sorry + theorem reachability_eval_list - (r : (List OneTwo) → (List OneTwo) → Prop) - (h_r_dec : ∀ x y, Decidable (r x y)) + {r : (List OneTwo) → (List OneTwo) → Prop} + {h_r_dec : ∀ x y, Decidable (r x y)} (h_rs_dec : ∀ x y t, Decidable (Relation.RelatesInSteps r x y t)) - (max : ℕ) + {max : ℕ} (h_finite : finiteRel r max) - (edge : MultiTapeTM tapeCount (WithSep OneTwo)) + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} (h_edge_semantics : edge_semantics r h_r_dec edge) - (t_val : ℕ) - (a_val b_val : List OneTwo) - (tapes : Fin tapeCount → List (List OneTwo)) : - (push a a_val <;> push b b_val <;> push t (dya t_val) <;> - reachability edge (dya max)).eval_list tapes = .some (Function.update tapes result ( + {t_val : ℕ} + {a_val b_val : List OneTwo} + {tapes : Fin tapeCount → List (List OneTwo)} : + (reachability edge (dya max) a_val b_val t_val).eval_list tapes = .some (Function.update tapes + result ( if Relation.RelatesInSteps r a_val b_val t_val then [.one] :: (tapes result) else [] :: (tapes result))) := by simp [reachability] - rw [doWhile_eval_list (inner_loop_halts_on_lists h_edge_semantics)] - simp sorry -lemma induction_step - (r : (List OneTwo) → (List OneTwo) → Prop) - (h_r_dec : ∀ x y, Decidable (r x y)) - (max : ℕ) - (edge : MultiTapeTM tapeCount (WithSep OneTwo)) - (h_edge_semantics : edge_semantics r h_r_dec edge) - (tapes : Fin tapeCount → List (List OneTwo)) - (h_pc : (tapes pc).head?.getD [] = l_funStart) - (t_val : ℕ) - (h_t : (tapes t).head?.getD [] = dya t_val.succ) - (h_ih : ∀ tapes', - (tapes' pc).head?.getD [] = l_funStart → - (tapes' t).head?.getD [] = dya t_val → - (innerLoop edge (dya max)).eval_list tapes' = .some - (Function.update (Function.update tapes' - pc (tapes' pc).tail) - result (if r ((tapes' a).headD []) ((tapes' b).headD []) then - [.one] :: (tapes' result) - else - [] :: (tapes' result))) → - : - (innerLoop edge (dya max)).eval_list tapes = .some - (Function.update (Function.update tapes - pc (tapes pc).tail) - result (if r ((tapes a).headD []) ((tapes b).headD []) then - [.one] :: (tapes result) - else - [] :: (tapes result))) := by - unfold edge_semantics at h_edge_semantics - simp [innerLoop, h_pc, h_t, h_edge_semantics] - grind - end Routines end Turing diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean index 7e44e4d3b..33ca731a8 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean @@ -82,6 +82,14 @@ public noncomputable def MultiTapeTM.eval_list_tot Fin k → List (List α) := (tm.eval_list tapes).get (h_alwaysHalts tapes) +@[simp] +public theorem MultiTapeTM.eval_list_tot_eq_eval_list_get + (tm : MultiTapeTM k (WithSep α)) + (h_alwaysHalts : ∀ tapes, tm.HaltsOnLists tapes) + (tapes : Fin k → List (List α)) : + tm.eval_list_tot h_alwaysHalts tapes = + (tm.eval_list tapes).get (sorry /- this should be h_alwaysHalts tapes --/) := by rfl + @[simp, grind =] public theorem MultiTapeTM.extend_eval_list {α : Type} [Fintype α] @@ -166,6 +174,9 @@ public def dya (n : ℕ) : List OneTwo := /-- Dyadic decoding of natural numbers. -/ public def dya_inv : List OneTwo → ℕ := sorry +@[simp, grind =] +public lemma dya_zero : dya 0 = [] := by simp [dya] + @[simp, grind =] public lemma dya_inv_zero : dya_inv [] = 0 := by sorry diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean index 04106f013..a5fa9da7e 100644 --- a/Cslib/Foundations/Data/RelatesInSteps.lean +++ b/Cslib/Foundations/Data/RelatesInSteps.lean @@ -47,6 +47,9 @@ theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInS lemma RelatesInSteps.single {a b : α} (h : r a b) : RelatesInSteps r a b 1 := tail a a b 0 (refl a) h +lemma RelatesInSteps.single_iff {a b : α} : RelatesInSteps r a b 1 ↔ r a b := by + sorry + theorem RelatesInSteps.head (t t' t'' : α) (n : ℕ) (h₁ : r t t') (h₂ : RelatesInSteps r t' t'' n) : RelatesInSteps r t t'' (n+1) := by induction h₂ with From 608dd1c7199f86b80ae70e8f744c3ab5dfb44274 Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 25 Feb 2026 21:27:02 +0100 Subject: [PATCH 13/20] Attempt at proving semantics of inner loop. --- .../MultiTapeTuring/GraphReachability.lean | 45 ++++++++++++++----- .../Machines/MultiTapeTuring/SuccRoutine.lean | 3 ++ 2 files changed, 38 insertions(+), 10 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 4d93fde92..26bc12771 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -203,8 +203,6 @@ def afterSecondRec := pop a <;> pop b <;> succ t <;> combineOr result <;> combineOr result <;> succ c <;> push pc l_loopStart - -@[simp] def innerLoop (edge : MultiTapeTM tapeCount (WithSep OneTwo)) (maxConfig : List OneTwo) : MultiTapeTM tapeCount (WithSep OneTwo) := iteLit pc l_funStart mainAux (pop pc <;> funStart edge) @@ -252,7 +250,7 @@ lemma inner_loop_halts_on_lists intro tapes apply MultiTapeTM.HaltsOnLists_of_eval_list unfold edge_semantics at h_edge_semantics - simp [h_edge_semantics] + simp [h_edge_semantics, innerLoop] split_ifs · simp · simp @@ -281,7 +279,6 @@ def iter_count_bound (max : ℕ) (t : ℕ) : ℕ := match t with | .zero => 1 | .succ t' => 2 + max * (3 + 2 * iter_count_bound max t') -@[simp] noncomputable def innerLoopFun {r : (List OneTwo) → (List OneTwo) → Prop} {h_r_dec : ∀ x y, Decidable (r x y)} @@ -312,23 +309,51 @@ lemma loop_semantics [] :: (tapes result)) ∧ ∀ n' < iter_count_bound max (dya_inv ((tapes t).headD [])), (((innerLoopFun max h_edge_semantics)^[n'] tapes) pc).length ≥ (tapes pc).length := by - induction h_t : (dya_inv ((tapes t).headD [])) generalizing tapes with + induction h_t : (dya_inv ((tapes t).head?.getD [])) generalizing tapes with | zero => have h_t_dya : (tapes t).head?.getD [] = dya 0 := by rw [← h_t]; simp unfold edge_semantics at h_edge_semantics - simp [h_edge_semantics, h_pc_funStart, h_t_dya, Relation.RelatesInSteps.single_iff] + simp [h_edge_semantics, h_pc_funStart, h_t_dya, Relation.RelatesInSteps.single_iff, + innerLoop, innerLoopFun] split · simp · simp | succ t_val ih => + have h_inner (tapes : Fin tapeCount → List (List OneTwo)) + (h_pc : (tapes pc).head?.getD [] = l_loopStart) + (h_c : (tapes c).head?.getD [] ≠ dya max) + (h_t : dya_inv ((tapes t).head?.getD []) = t_val.succ) : + (innerLoopFun max h_edge_semantics)^[3 + 2 * (iter_count_bound max t_val)] tapes = + Function.update (Function.update tapes + c ((dya_succ ((tapes c).headD [])) :: (tapes pc).tail)) + result (if + ((tapes result).headD [] != []) ∨ + (Relation.RelatesInSteps r ((tapes a).headD []) ((tapes c).headD []) (2 ^ t_val) ∧ + Relation.RelatesInSteps r ((tapes c).headD []) ((tapes b).headD []) (2 ^ t_val)) + then + [.one] :: (tapes result).tail + else + [] :: (tapes result).tail) := by + have {α : Type} {x : α} {n : ℕ} (f : α → α): f^[3 + 2 * n] x = + f (f^[n] (f (f^[n] (f x)))) := by + rw [← Function.iterate_succ_apply, ← Function.iterate_succ_apply] + rw [← Function.iterate_add_apply, ← Function.iterate_succ_apply' (f := f)] + grind + rw [this] + simp [innerLoopFun] + -- TODO continue here, see if we can apply the IH two times. + rw [(ih tapes (by sorry) (by sorry)).1] + simpa using h_fun_start + exact h_fun_start + sorry + by_cases h_rel : Relation.RelatesInSteps r ((tapes a).headD []) ((tapes b).headD []) (Nat.pow 2 (t_val + 1)) - · simp only [h_rel] + · -- simp only [h_rel] simp - obtain ⟨c, h_c_rel⟩ := + obtain ⟨c_val, h_c_rel⟩ := (relatesInStepsExp r ((tapes a).headD []) ((tapes b).headD []) t_val).mp h_rel - have h_c_le : dya_inv c < max := by sorry - + have h_c_le : dya_inv c_val < max := by sorry sorry · sorry diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean index 8c4f6bb93..f057fcf0c 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean @@ -42,6 +42,9 @@ public theorem succ_eval_list {k : ℕ} {i : Fin k} {tapes : Fin k → List (Lis ((dya (dya_inv ((tapes i).headD [])).succ) :: (tapes i).tail)) := by simpa [succ] using apply_updates_function_update (by intro x y; grind) +@[simp] +public def dya_succ (w : List OneTwo) := dya ((dya_inv w).succ) + lemma succ₀_evalWithStats_list {n : ℕ} {ls : List (List OneTwo)} : succ₀.evalWithStats_list [(dya n) :: ls].get = .some ( From f81fde1fdec3924a129e42fbb3236776d1ea53db Mon Sep 17 00:00:00 2001 From: crei Date: Thu, 26 Feb 2026 12:37:30 +0100 Subject: [PATCH 14/20] Prove first iteration. --- .../MultiTapeTuring/GraphReachability.lean | 36 +++++++++++++++---- 1 file changed, 29 insertions(+), 7 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 26bc12771..f2fc5191e 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -95,11 +95,11 @@ abbrev pc : Fin tapeCount := ⟨8, sorry⟩ abbrev c : Fin tapeCount := ⟨9, sorry⟩ abbrev mainAux : Fin tapeCount := ⟨10, sorry⟩ -abbrev l_funStart := dya 1 -abbrev l_loopStart := dya 2 -abbrev l_afterFirstRec := dya 3 -abbrev l_afterSecondRec := dya 4 -abbrev l_loopContinue := dya 5 +abbrev l_funStart := [OneTwo.one] +abbrev l_loopStart := [OneTwo.two] +abbrev l_afterFirstRec := [OneTwo.one, OneTwo.one] +abbrev l_afterSecondRec := [OneTwo.one, OneTwo.two] +abbrev l_loopContinue := [OneTwo.two, OneTwo.one] public def eqLit {k : ℕ} (q : Fin (k + 3)) @@ -287,6 +287,24 @@ noncomputable def innerLoopFun (h_edge_semantics : edge_semantics r h_r_dec edge) := (innerLoop edge (dya max)).eval_list_tot (inner_loop_halts_on_lists h_edge_semantics) +lemma inner_loop_start + {max : ℕ} + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} + {tapes : Fin tapeCount → List (List OneTwo)} + (h_pc_loopStart : (tapes pc).head?.getD [] = l_loopStart) : + (innerLoop edge (dya max)).eval_list tapes = Part.some (if (tapes c).head?.getD [] = dya max then + Function.update (Function.update tapes pc (tapes pc).tail) c (tapes c).tail + else + Function.update (Function.update (Function.update (Function.update tapes + a ((tapes a).head?.getD [] :: tapes a)) + b ((tapes c).head?.getD [] :: tapes b)) + t (dya (dya_inv ((tapes t).head?.getD []) - 1) :: (tapes t).tail)) + pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail)) := by + simp [innerLoop, h_pc_loopStart] + split_ifs + · simp + · simp; grind + -- TODO continue here: prove this theorem by induction. lemma loop_semantics {r : (List OneTwo) → (List OneTwo) → Prop} @@ -341,8 +359,12 @@ lemma loop_semantics grind rw [this] simp [innerLoopFun] - -- TODO continue here, see if we can apply the IH two times. - rw [(ih tapes (by sorry) (by sorry)).1] + rw [inner_loop_start h_pc] + simp [h_c] + simp [innerLoopFun] at ih + -- TODO continue here. We need to make the iteration count and the head on tape t + -- equal + rw [(ih _ (by sorry) (by sorry)).1] simpa using h_fun_start exact h_fun_start sorry From b6d6e7ee0360e7c416689011d2117bff48bfca14 Mon Sep 17 00:00:00 2001 From: crei Date: Thu, 26 Feb 2026 18:30:33 +0100 Subject: [PATCH 15/20] proof of inner loop almost finished. --- .../MultiTapeTuring/GraphReachability.lean | 142 +++++++++++++++--- .../Machines/MultiTapeTuring/SuccRoutine.lean | 2 +- 2 files changed, 125 insertions(+), 19 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index f2fc5191e..1df55f2be 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -136,6 +136,16 @@ public def iteLit {k : ℕ} eqLit i w (aux + 1) aux (h_inj := by intro x y; grind) <;> ite (aux + 1) (pop (aux + 1) <;> tm₁) (pop (aux + 1) <;> tm₂) +@[simp] +public def combineAnd {k : ℕ} (i : Fin k) : + MultiTapeTM k (WithSep OneTwo) := + ite i + (pop i <;> + ite i + (pop i <;> push i [OneTwo.one]) + (pop i <;> push i [])) + (pop i <;> pop i <;> push i []) + @[simp] public def combineOr {k : ℕ} (i : Fin k) : MultiTapeTM k (WithSep OneTwo) := @@ -201,7 +211,7 @@ def afterFirstRec := @[simp] def afterSecondRec := pop a <;> pop b <;> succ t <;> - combineOr result <;> combineOr result <;> succ c <;> push pc l_loopStart + combineAnd result <;> combineOr result <;> succ c <;> push pc l_loopStart def innerLoop (edge : MultiTapeTM tapeCount (WithSep OneTwo)) (maxConfig : List OneTwo) : MultiTapeTM tapeCount (WithSep OneTwo) := @@ -263,6 +273,9 @@ lemma inner_loop_halts_on_lists · simp · simp · simp + split_ifs + · simp + · simp · simp def reachability @@ -305,6 +318,80 @@ lemma inner_loop_start · simp · simp; grind +-- TODO the result of eval_list makes heavy use of +-- Function.update tapes x (f(tapes) :: (tapes x).tail) +-- create an abstraction for that? Sometimes we need .tail.tail + +lemma inner_loop_after_first_rec + {max : ℕ} + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} + {tapes : Fin tapeCount → List (List OneTwo)} + (h_pc_afterFirstRec : (tapes pc).head?.getD [] = l_afterFirstRec) : + (innerLoop edge (dya max)).eval_list tapes = Part.some ( + Function.update (Function.update (Function.update tapes + a ((tapes c).head?.getD [] :: (tapes a).tail)) + b ((tapes b)[1]?.getD [] :: (tapes b).tail)) + pc (l_funStart :: l_afterSecondRec :: (tapes pc).tail)) := by + simp [innerLoop, h_pc_afterFirstRec] + grind + +lemma function_update_sort + {α : Type} {k : ℕ} {x y : Fin k} {h_lt : x.val < y.val} + {a b : α} {f : Fin k → α} : + Function.update (Function.update f y b) x a = + Function.update (Function.update f x a) y b := by grind + +lemma inner_loop_after_second_rec + {max : ℕ} + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} + {tapes : Fin tapeCount → List (List OneTwo)} + (h_pc_afterSecondRec : (tapes pc).head?.getD [] = l_afterSecondRec) : + (innerLoop edge (dya max)).eval_list tapes = Part.some ( + Function.update (Function.update (Function.update (Function.update + (Function.update (Function.update tapes + a (tapes a).tail) + b (tapes b).tail) + t (dya (dya_inv ((tapes t).head?.getD []) + 1) :: (tapes t).tail)) + result ( + (if (((tapes result).head?.getD [] != []) ∧ + (tapes result)[1]?.getD [] != []) ∨ + (tapes result)[2]?.getD [] != [] then + [.one] + else + []) :: (tapes result).tail.tail.tail)) + c (dya (dya_inv ((tapes c).head?.getD []) + 1) :: (tapes c).tail)) + pc (l_loopStart :: (tapes pc).tail)) := by + simp [innerLoop, h_pc_afterSecondRec] + split_ifs + · simp + split_ifs + · simp + grind + · simp + grind + · simp + split_ifs + · simp + grind + · simp + grind + · simp + split_ifs + · simp + grind + · simp + grind + · simp + split_ifs + · simp + grind + · simp + grind + · simp + grind + · simp + grind + -- TODO continue here: prove this theorem by induction. lemma loop_semantics {r : (List OneTwo) → (List OneTwo) → Prop} @@ -342,8 +429,10 @@ lemma loop_semantics (h_c : (tapes c).head?.getD [] ≠ dya max) (h_t : dya_inv ((tapes t).head?.getD []) = t_val.succ) : (innerLoopFun max h_edge_semantics)^[3 + 2 * (iter_count_bound max t_val)] tapes = - Function.update (Function.update tapes - c ((dya_succ ((tapes c).headD [])) :: (tapes pc).tail)) + Function.update (Function.update (Function.update (Function.update tapes + c ((dya_succ ((tapes c).headD [])) :: (tapes c).tail)) + t (dya (t_val.succ) :: (tapes t).tail)) -- TODO But we already have that + pc (l_loopStart :: (tapes pc).tail)) result (if ((tapes result).headD [] != []) ∨ (Relation.RelatesInSteps r ((tapes a).headD []) ((tapes c).headD []) (2 ^ t_val) ∧ @@ -362,22 +451,39 @@ lemma loop_semantics rw [inner_loop_start h_pc] simp [h_c] simp [innerLoopFun] at ih - -- TODO continue here. We need to make the iteration count and the head on tape t - -- equal - rw [(ih _ (by sorry) (by sorry)).1] - simpa using h_fun_start - exact h_fun_start - sorry - - by_cases h_rel : Relation.RelatesInSteps r - ((tapes a).headD []) ((tapes b).headD []) (Nat.pow 2 (t_val + 1)) - · -- simp only [h_rel] - simp - obtain ⟨c_val, h_c_rel⟩ := - (relatesInStepsExp r ((tapes a).headD []) ((tapes b).headD []) t_val).mp h_rel - have h_c_le : dya_inv c_val < max := by sorry + simp [h_t] + let ih' := ih (Function.update (Function.update (Function.update (Function.update tapes + a ((tapes a).head?.getD [] :: tapes a)) + b ((tapes c).head?.getD [] :: tapes b)) + t ((dya t_val) :: (tapes t).tail)) + pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail)) + simp at ih' + let ih' := ih'.1 + simp [ih'] + simp [inner_loop_after_first_rec] + let ih' := ih (Function.update + (Function.update + (Function.update + (Function.update + (Function.update + (Function.update + (Function.update (Function.update tapes 0 ((tapes 0).head?.getD [] :: tapes 0)) 1 + ((tapes c).head?.getD [] :: tapes 1)) + t (dya t_val :: (tapes t).tail)) + pc (l_afterFirstRec :: (tapes pc).tail)) + result + (if Relation.RelatesInSteps r ((tapes 0).head?.getD []) ((tapes c).head?.getD []) (2 ^ t_val) then + [OneTwo.one] :: tapes result + else [] :: tapes result)) + 0 ((tapes c).head?.getD [] :: tapes 0)) + 1 ((tapes 1)[0]?.getD [] :: tapes 1)) + pc (l_funStart :: l_afterSecondRec :: (tapes pc).tail)) + simp at ih' + let ih' := ih'.1 + simp [ih'] + simp [inner_loop_after_second_rec] sorry - · sorry + sorry theorem reachability_eval_list diff --git a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean index f057fcf0c..30274df7d 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/SuccRoutine.lean @@ -43,7 +43,7 @@ public theorem succ_eval_list {k : ℕ} {i : Fin k} {tapes : Fin k → List (Lis simpa [succ] using apply_updates_function_update (by intro x y; grind) @[simp] -public def dya_succ (w : List OneTwo) := dya ((dya_inv w).succ) +public abbrev dya_succ (w : List OneTwo) := dya ((dya_inv w).succ) lemma succ₀_evalWithStats_list {n : ℕ} {ls : List (List OneTwo)} : succ₀.evalWithStats_list [(dya n) :: ls].get = From 8372e3995e7855cfae940e9659e3606ea912f49e Mon Sep 17 00:00:00 2001 From: crei Date: Fri, 27 Feb 2026 18:02:09 +0100 Subject: [PATCH 16/20] prove inner loop semantics. --- .../MultiTapeTuring/GraphReachability.lean | 41 ++++++++++++++++--- 1 file changed, 36 insertions(+), 5 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 1df55f2be..8763b4834 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -336,10 +336,16 @@ lemma inner_loop_after_first_rec grind lemma function_update_sort - {α : Type} {k : ℕ} {x y : Fin k} {h_lt : x.val < y.val} + {α : Type} {k : ℕ} {x y : Fin k} {h_lt : x < y} {a b : α} {f : Fin k → α} : - Function.update (Function.update f y b) x a = - Function.update (Function.update f x a) y b := by grind + Function.update (Function.update f x a) y b = + Function.update (Function.update f y b) x a := by grind + +lemma function_update_pull + {α : Type} {k : ℕ} (x : Fin k) {y : Fin k} {h_lt : x ≠ y} + {a b : α} {f : Fin k → α} : + Function.update (Function.update f x a) y b = + Function.update (Function.update f y b) x a := by grind lemma inner_loop_after_second_rec {max : ℕ} @@ -392,6 +398,13 @@ lemma inner_loop_after_second_rec · simp grind +@[simp] +lemma list_getElem?_zero_eq_head? {α : Type} (l : List α) : + l[0]? = l.head? := by + cases l with + | nil => simp + | cons a l => simp + -- TODO continue here: prove this theorem by induction. lemma loop_semantics {r : (List OneTwo) → (List OneTwo) → Prop} @@ -476,13 +489,31 @@ lemma loop_semantics [OneTwo.one] :: tapes result else [] :: tapes result)) 0 ((tapes c).head?.getD [] :: tapes 0)) - 1 ((tapes 1)[0]?.getD [] :: tapes 1)) + 1 ((tapes 1).head?.getD [] :: tapes 1)) pc (l_funStart :: l_afterSecondRec :: (tapes pc).tail)) simp at ih' let ih' := ih'.1 simp [ih'] simp [inner_loop_after_second_rec] - sorry + simp [function_update_pull 0] + simp [function_update_pull 1] + simp [function_update_pull result] + simp [function_update_pull pc] + simp [function_update_pull c] + simp [function_update_pull t] + by_cases h_r₁ : Relation.RelatesInSteps r + ((tapes 0).head?.getD []) ((tapes c).head?.getD []) (2 ^ t_val) + · by_cases h_r₂ : Relation.RelatesInSteps r + ((tapes c).head?.getD []) ((tapes 1).head?.getD []) (2 ^ t_val) + · simp [h_r₁, h_r₂] + · simp [h_r₁, h_r₂] + grind + · by_cases h_r₂ : Relation.RelatesInSteps r + ((tapes c).head?.getD []) ((tapes 1).head?.getD []) (2 ^ t_val) + · simp [h_r₁, h_r₂] + grind + · simp [h_r₁, h_r₂] + grind sorry From be8a3dc15d2c16b21bc5197cb9bcf5679a6dbb91 Mon Sep 17 00:00:00 2001 From: crei Date: Fri, 27 Feb 2026 18:56:19 +0100 Subject: [PATCH 17/20] some simplifications. --- .../MultiTapeTuring/GraphReachability.lean | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 8763b4834..204ed1276 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -460,18 +460,22 @@ lemma loop_semantics rw [← Function.iterate_add_apply, ← Function.iterate_succ_apply' (f := f)] grind rw [this] - simp [innerLoopFun] + simp only [innerLoopFun, MultiTapeTM.eval_list_tot_eq_eval_list_get] rw [inner_loop_start h_pc] - simp [h_c] - simp [innerLoopFun] at ih - simp [h_t] - let ih' := ih (Function.update (Function.update (Function.update (Function.update tapes + simp only [Part.get_some] + simp only [h_c, h_t] + simp only [↓reduceIte] + simp only [Nat.succ_eq_add_one, add_tsub_cancel_right] + simp only [innerLoopFun] at ih + let tapes₁ := (Function.update (Function.update (Function.update (Function.update tapes a ((tapes a).head?.getD [] :: tapes a)) b ((tapes c).head?.getD [] :: tapes b)) t ((dya t_val) :: (tapes t).tail)) pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail)) - simp at ih' - let ih' := ih'.1 + let ih' := (ih tapes₁ (by simp [tapes₁]) (by simp [tapes₁])).1 + have : (dya_inv ((tapes₁ t).headD [])) = t_val := by simp [tapes₁] + rw [this] at ih' + simp [tapes₁] at ih' simp [ih'] simp [inner_loop_after_first_rec] let ih' := ih (Function.update @@ -514,6 +518,7 @@ lemma loop_semantics grind · simp [h_r₁, h_r₂] grind + sorry From b0fe0c53035276049401954216336a3207e863b4 Mon Sep 17 00:00:00 2001 From: crei Date: Mon, 2 Mar 2026 14:41:08 +0100 Subject: [PATCH 18/20] fix build --- Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean b/Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean index 1eee25958..33161aee2 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/MulRoutine.lean @@ -52,7 +52,6 @@ theorem mul₀_eval_list {tapes : Fin 9 → List (List OneTwo)} : (dya (dya_inv ((tapes 0).headD []) * dya_inv ((tapes 1).headD [])) :: (tapes 2)))) := by by_cases h_zero: dya_inv ((tapes 0).head?.getD []) = 0 · simp [mul₀, h_zero] - grind · simp [mul₀, h_zero] grind From 957a878d054a174d3642551c37a3cdf20bdda926 Mon Sep 17 00:00:00 2001 From: crei Date: Thu, 5 Mar 2026 10:14:54 +0100 Subject: [PATCH 19/20] remove noncomputable. --- .../Machines/MultiTapeTuring/GraphReachability.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 7b6a5abc3..4005311e5 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -277,7 +277,7 @@ def iter_count_bound (max : ℕ) (t : ℕ) : ℕ := match t with | .zero => 1 | .succ t' => 2 + max * (3 + 2 * iter_count_bound max t') -noncomputable def innerLoopFun +def innerLoopFun {r : (List OneTwo) → (List OneTwo) → Prop} {h_r_dec : ∀ x y, Decidable (r x y)} (max : ℕ) From aca6541716c69f025c210597ccd08b6e06b14366 Mon Sep 17 00:00:00 2001 From: crei Date: Wed, 11 Mar 2026 11:57:09 +0100 Subject: [PATCH 20/20] claude tries to finish the proof. --- Cslib.lean | 2 + .../MultiTapeTuring/GraphReachability.lean | 683 ++++++++++++++++-- .../MultiTapeTuring/ListEncoding.lean | 9 + 3 files changed, 616 insertions(+), 78 deletions(-) diff --git a/Cslib.lean b/Cslib.lean index 3c8097aec..ce2e5e367 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -32,6 +32,8 @@ public import Cslib.Computability.Languages.RegularLanguage public import Cslib.Computability.Machines.MultiTapeTuring.AddRoutine public import Cslib.Computability.Machines.MultiTapeTuring.Basic public import Cslib.Computability.Machines.MultiTapeTuring.CopyRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.DecRoutine +public import Cslib.Computability.Machines.MultiTapeTuring.DuplicateRoutine public import Cslib.Computability.Machines.MultiTapeTuring.EqualRoutine public import Cslib.Computability.Machines.MultiTapeTuring.GraphReachability public import Cslib.Computability.Machines.MultiTapeTuring.HeadStats diff --git a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean index 4005311e5..df87472a5 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/GraphReachability.lean @@ -372,7 +372,18 @@ lemma list_getElem?_zero_eq_head? {α : Type} (l : List α) : | nil => simp | cons a l => simp --- TODO continue here: prove this theorem by induction. +private lemma innerLoopFun_eq_of_eval_list + {r : (List OneTwo) → (List OneTwo) → Prop} + {h_r_dec : ∀ x y, Decidable (r x y)} + {max : ℕ} + {edge : MultiTapeTM tapeCount (WithSep OneTwo)} + {h_edge_semantics : edge_semantics r h_r_dec edge} + {tapes result' : Fin tapeCount → List (List OneTwo)} + (h : (innerLoop edge (dya max)).eval_list tapes = Part.some result') : + innerLoopFun max h_edge_semantics tapes = result' := + MultiTapeTM.eval_list_tot_eq_of_eval_list _ _ _ _ h + +set_option maxHeartbeats 4000000 in lemma loop_semantics {r : (List OneTwo) → (List OneTwo) → Prop} {h_r_dec : ∀ x y, Decidable (r x y)} @@ -397,13 +408,29 @@ lemma loop_semantics induction h_t : (dya_inv ((tapes t).head?.getD [])) generalizing tapes with | zero => have h_t_dya : (tapes t).head?.getD [] = dya 0 := by rw [← h_t]; simp + have h_t_empty : (tapes t).head?.getD [] = [] := by rw [h_t_dya]; simp unfold edge_semantics at h_edge_semantics - sorry - -- simp [h_edge_semantics, h_pc_funStart, h_t_dya, Relation.RelatesInSteps.single_iff, - -- innerLoop, innerLoopFun] - -- split - -- · simp - -- · simp + have h_headD : dya_inv ((tapes t).headD []) = 0 := by + rw [List.headD_eq_head?]; exact h_t + rw [h_headD]; simp only [iter_count_bound, Function.iterate_one, Nat.pow] + constructor + · -- Main equality: innerLoopFun tapes = expected (with 2^0 = 1) + show innerLoopFun max h_edge_semantics tapes = _ + have h_eval : (innerLoop edge (dya max)).eval_list tapes = + Part.some (if r ((tapes a).headD []) ((tapes b).headD []) then + Function.update (Function.update tapes pc (tapes pc).tail) + result ([OneTwo.one] :: tapes result) + else + Function.update (Function.update tapes pc (tapes pc).tail) + result ([] :: tapes result)) := by + simp [innerLoop, h_pc_funStart, h_t_empty, h_edge_semantics] + rw [innerLoopFun_eq_of_eval_list h_eval] + simp only [Relation.RelatesInSteps.single_iff] + split_ifs <;> rfl + · -- PC length property: trivially true for n' < 1 (n' = 0) + intro n' h_n' + have : n' = 0 := by omega + subst this; simp | succ t_val ih => have h_inner (tapes : Fin tapeCount → List (List OneTwo)) (h_pc : (tapes pc).head?.getD [] = l_loopStart) @@ -412,7 +439,7 @@ lemma loop_semantics (innerLoopFun max h_edge_semantics)^[3 + 2 * (iter_count_bound max t_val)] tapes = Function.update (Function.update (Function.update (Function.update tapes c ((dya_succ ((tapes c).headD [])) :: (tapes c).tail)) - t (dya (t_val.succ) :: (tapes t).tail)) -- TODO But we already have that + t (dya (t_val.succ) :: (tapes t).tail)) pc (l_loopStart :: (tapes pc).tail)) result (if ((tapes result).headD [] != []) ∨ @@ -422,77 +449,577 @@ lemma loop_semantics [.one] :: (tapes result).tail else [] :: (tapes result).tail) := by - have {α : Type} {x : α} {n : ℕ} (f : α → α): f^[3 + 2 * n] x = - f (f^[n] (f (f^[n] (f x)))) := by - rw [← Function.iterate_succ_apply, ← Function.iterate_succ_apply] - rw [← Function.iterate_add_apply, ← Function.iterate_succ_apply' (f := f)] - grind - rw [this] + -- Decompose f^[3+2n] into f ∘ f^[n] ∘ f ∘ f^[n] ∘ f + conv_lhs => rw [show 3 + 2 * iter_count_bound max t_val = + 1 + (iter_count_bound max t_val + + (1 + (iter_count_bound max t_val + 1))) from by omega] + simp only [Function.iterate_add_apply, Function.iterate_one] + -- Goal: f (f^[n] (f (f^[n] (f tapes)))) = target + -- Step 1: inner_loop_start (loopStart, c ≠ max) + have h_step1_eval := @inner_loop_start max edge tapes h_pc + simp only [if_neg h_c] at h_step1_eval + have h_step1 := @innerLoopFun_eq_of_eval_list r h_r_dec max edge + h_edge_semantics _ _ h_step1_eval + rw [h_step1] + -- After step 1: a pushed, b gets c.headD, t decremented, pc = funStart::afterFirstRec::tail + -- Step 2: First recursive call (ih with t_val) + have h_t_sub : dya_inv ((tapes t).head?.getD []) - 1 = t_val := by omega + have h_pc₁ : (Function.update (Function.update (Function.update (Function.update tapes + a ((tapes a).head?.getD [] :: tapes a)) + b ((tapes c).head?.getD [] :: tapes b)) + t (dya (dya_inv ((tapes t).head?.getD []) - 1) :: (tapes t).tail)) + pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail) pc).head?.getD [] + = l_funStart := by + simp [Function.update_self] + have h_t₁ : dya_inv ((Function.update (Function.update (Function.update (Function.update + tapes + a ((tapes a).head?.getD [] :: tapes a)) + b ((tapes c).head?.getD [] :: tapes b)) + t (dya (dya_inv ((tapes t).head?.getD []) - 1) :: (tapes t).tail)) + pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail) t).head?.getD []) + = t_val := by + have h_ne : pc ≠ t := by decide + simp [Function.update_of_ne h_ne, Function.update_self, h_t_sub, dya_inv_dya] + obtain ⟨h_ih₁, h_ih₁_pc⟩ := ih _ h_pc₁ h_t₁ + -- h_ih₁ uses dya_inv(headD) which we need to show equals t_val + -- Convert headD to head?.getD for matching + have h_headD₁ : dya_inv ((Function.update (Function.update (Function.update + (Function.update tapes + a ((tapes a).head?.getD [] :: tapes a)) + b ((tapes c).head?.getD [] :: tapes b)) + t (dya (dya_inv ((tapes t).head?.getD []) - 1) :: (tapes t).tail)) + pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail) t).headD []) + = t_val := by + rw [List.headD_eq_head?]; exact h_t₁ + rw [h_headD₁] at h_ih₁ + rw [h_ih₁] + -- After step 2: goal is f (f^[n] (f )) = target + -- where post-IH1 = Function.update (Function.update tapes₁ pc tail) result (...) + -- Step 3: inner_loop_after_first_rec + -- Need pc of post-IH1 = l_afterFirstRec + -- post-IH1 pc = (Function.update tapes₁ pc (tapes₁ pc).tail) pc = (tapes₁ pc).tail + -- = (l_funStart :: l_afterFirstRec :: (tapes pc).tail).tail + -- = l_afterFirstRec :: (tapes pc).tail + -- So head?.getD [] = l_afterFirstRec ✓ + -- Define tapes₁ for reference in step 3 proofs + set tapes₁ := Function.update (Function.update (Function.update (Function.update tapes + a ((tapes a).head?.getD [] :: tapes a)) + b ((tapes c).head?.getD [] :: tapes b)) + t (dya (dya_inv ((tapes t).head?.getD []) - 1) :: (tapes t).tail)) + pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail) with htapes₁_def + set tapes₂ := Function.update (Function.update tapes₁ + pc (tapes₁ pc).tail) + result (if Relation.RelatesInSteps r ((tapes₁ a).headD []) ((tapes₁ b).headD []) + (Nat.pow 2 t_val) then [OneTwo.one] :: tapes₁ result + else [] :: tapes₁ result) with htapes₂_def + have h_pc₂ : (tapes₂ pc).head?.getD [] = l_afterFirstRec := by + simp only [htapes₂_def] + have : result ≠ pc := by decide + simp [Function.update_of_ne this, Function.update_self] + simp [htapes₁_def, Function.update_self] + have h_step3_eval := @inner_loop_after_first_rec max edge tapes₂ h_pc₂ + have h_step3 := @innerLoopFun_eq_of_eval_list r h_r_dec max edge + h_edge_semantics _ _ h_step3_eval + rw [h_step3] + -- After step 3: a/b swapped, pc = funStart::afterSecondRec::tail + -- Step 4: Second recursive call (ih with t_val) + set tapes₃ := Function.update (Function.update (Function.update tapes₂ + a ((tapes₂ c).head?.getD [] :: (tapes₂ a).tail)) + b ((tapes₂ b)[1]?.getD [] :: (tapes₂ b).tail)) + pc (l_funStart :: l_afterSecondRec :: (tapes₂ pc).tail) with htapes₃_def + have h_pc₃ : (tapes₃ pc).head?.getD [] = l_funStart := by + simp [htapes₃_def, Function.update_self] + have h_t₃ : dya_inv ((tapes₃ t).head?.getD []) = t_val := by + have h1 : pc ≠ t := by decide + have h2 : b ≠ t := by decide + have h3 : a ≠ t := by decide + have h4 : result ≠ t := by decide + simp [htapes₃_def, htapes₂_def, htapes₁_def, + Function.update_of_ne h1, Function.update_of_ne h2, + Function.update_of_ne h3, Function.update_of_ne h4, + Function.update_self, h_t_sub, dya_inv_dya] + obtain ⟨h_ih₂, h_ih₂_pc⟩ := ih _ h_pc₃ h_t₃ + have h_headD₃ : dya_inv ((tapes₃ t).headD []) = t_val := by + rw [List.headD_eq_head?]; exact h_t₃ + rw [h_headD₃] at h_ih₂ + rw [h_ih₂] + -- After step 4: result has second recursive check + -- Step 5: inner_loop_after_second_rec + set tapes₄ := Function.update (Function.update tapes₃ + pc (tapes₃ pc).tail) + result (if Relation.RelatesInSteps r ((tapes₃ a).headD []) ((tapes₃ b).headD []) + (Nat.pow 2 t_val) then [OneTwo.one] :: tapes₃ result + else [] :: tapes₃ result) with htapes₄_def + have h_pc₄ : (tapes₄ pc).head?.getD [] = l_afterSecondRec := by + simp only [htapes₄_def] + have : result ≠ pc := by decide + simp [Function.update_of_ne this, Function.update_self] + simp [htapes₃_def, Function.update_self] + have h_step5_eval := @inner_loop_after_second_rec max edge tapes₄ h_pc₄ + have h_step5 := @innerLoopFun_eq_of_eval_list r h_r_dec max edge + h_edge_semantics _ _ h_step5_eval + rw [h_step5] + -- Now goal is: the 6-nested Function.update chain on tapes₄ = the 4-nested target + -- We need to show that after unfolding tapes₄, tapes₃, tapes₂, tapes₁, the result + -- matches the target. This requires extensive Function.update simplification for + -- each tape index (a, b, c, t, pc, result, and all others). + -- The key equalities needed: + -- * a: (... a).tail restores original tapes a + -- * b: (... b).tail restores original tapes b + -- * c: dya(dya_inv(c.head) + 1) = dya_succ(c.headD) by definition + -- * t: dya(dya_inv(dya(t_val)) + 1) = dya(t_val.succ) since dya_inv_dya + -- * pc: l_loopStart :: tail chain = l_loopStart :: (tapes pc).tail + -- * result: combines the two recursive checks via inner_loop_after_second_rec logic + ext i + by_cases h_i_result : i = result + · -- result tape: most complex case + subst h_i_result + -- Don't unfold set definitions - instead compute through layers + -- The outer Function.update chain (from inner_loop_after_second_rec) at result: + -- Since pc ≠ result and c ≠ result, the result value is the 4th update. + simp only [ + Function.update_of_ne (show pc ≠ result by decide), + Function.update_of_ne (show c ≠ result by decide), + Function.update_self] + -- Now goal: (if cond_on_tapes₄ then [.one] else []) :: (tapes₄ result).tail.tail.tail + -- = (if target_cond then [.one] :: tail else [] :: tail) + -- Extract what tapes₄ result is + have h_t4_result : tapes₄ result = + (if Relation.RelatesInSteps r ((tapes₃ a).headD []) ((tapes₃ b).headD []) + (Nat.pow 2 t_val) then [OneTwo.one] :: tapes₃ result + else [] :: tapes₃ result) := by + simp [htapes₄_def, Function.update_self] + have h_t3_result : tapes₃ result = tapes₂ result := by + simp [htapes₃_def, Function.update_of_ne (show pc ≠ result by decide), + Function.update_of_ne (show b ≠ result by decide), + Function.update_of_ne (show a ≠ result by decide)] + have h_t2_result : tapes₂ result = + (if Relation.RelatesInSteps r ((tapes₁ a).headD []) ((tapes₁ b).headD []) + (Nat.pow 2 t_val) then [OneTwo.one] :: tapes₁ result + else [] :: tapes₁ result) := by + simp [htapes₂_def, Function.update_self] + have h_t1_result : tapes₁ result = tapes result := by + simp [htapes₁_def, Function.update_of_ne (show pc ≠ result by decide), + Function.update_of_ne (show t ≠ result by decide), + Function.update_of_ne (show b ≠ result by decide), + Function.update_of_ne (show a ≠ result by decide)] + -- Extract IH tape values + have h_t1_a : (tapes₁ a).headD [] = (tapes a).head?.getD [] := by + simp [htapes₁_def, Function.update_of_ne (show pc ≠ a by decide), + Function.update_of_ne (show t ≠ a by decide), + Function.update_of_ne (show b ≠ a by decide), + Function.update_self] + have h_t1_b : (tapes₁ b).headD [] = (tapes c).head?.getD [] := by + simp [htapes₁_def, Function.update_of_ne (show pc ≠ b by decide), + Function.update_of_ne (show t ≠ b by decide), + Function.update_self] + have h_t3_a : (tapes₃ a).headD [] = (tapes c).head?.getD [] := by + simp [htapes₃_def, Function.update_of_ne (show pc ≠ a by decide), + Function.update_of_ne (show b ≠ a by decide), + Function.update_self, htapes₂_def, + Function.update_of_ne (show result ≠ a by decide), + htapes₁_def, Function.update_of_ne (show t ≠ a by decide), + Function.update_of_ne (show c ≠ a by decide), List.headD_eq_head?] + have h_t3_b : (tapes₃ b).headD [] = (tapes b).head?.getD [] := by + simp [htapes₃_def, Function.update_of_ne (show pc ≠ b by decide), + Function.update_of_ne (show a ≠ b by decide), + htapes₂_def, Function.update_of_ne (show result ≠ b by decide), + htapes₁_def, Function.update_of_ne (show t ≠ b by decide), + Function.update_self, List.headD_eq_head?] + -- Rewrite tapes₄ result through the chain + rw [h_t4_result, h_t3_result, h_t2_result, h_t1_result] + rw [h_t1_a, h_t1_b, h_t3_a, h_t3_b] + simp only [List.headD_eq_head?] + -- Now the goal has small terms with explicit ifs + -- Case split on path2 (the outer if of tapes₄ result) + split_ifs with h_path2 h_path1 h_path1 h_path2 h_path1 h_path1 + all_goals simp_all [bne_iff_ne] + · by_cases h_i_c : i = c + · subst h_i_c + -- c: dya(dya_inv(c.head) + 1) :: c.tail = dya_succ(c.headD) :: c.tail + simp_all only [htapes₄_def, htapes₃_def, htapes₂_def, htapes₁_def] + simp [Function.update_self, + Function.update_of_ne (show pc ≠ c by decide), + Function.update_of_ne (show result ≠ c by decide), + Function.update_of_ne (show t ≠ c by decide), + Function.update_of_ne (show b ≠ c by decide), + Function.update_of_ne (show a ≠ c by decide), + dya_succ, List.headD_eq_head?] + · by_cases h_i_t : i = t + · subst h_i_t + -- t: dya(dya_inv(tapes₄ t head) + 1) :: tail → dya(t_val.succ) :: tail + simp_all only [htapes₄_def, htapes₃_def, htapes₂_def, htapes₁_def] + simp [Function.update_self, + Function.update_of_ne (show pc ≠ t by decide), + Function.update_of_ne (show c ≠ t by decide), + Function.update_of_ne (show result ≠ t by decide), + Function.update_of_ne (show b ≠ t by decide), + Function.update_of_ne (show a ≠ t by decide), + h_t_sub, dya_inv_dya] + · by_cases h_i_pc : i = pc + · subst h_i_pc + -- pc: l_loopStart :: (tapes₄ pc).tail → l_loopStart :: (tapes pc).tail + simp only [Function.update_self, + Function.update_of_ne (show c ≠ pc by decide), + Function.update_of_ne (show result ≠ pc by decide), + Function.update_of_ne (show t ≠ pc by decide), + Function.update_of_ne (show b ≠ pc by decide), + Function.update_of_ne (show a ≠ pc by decide)] + simp only [htapes₄_def, Function.update_of_ne (show result ≠ pc by decide), + Function.update_self] + simp only [htapes₃_def, Function.update_self] + simp only [htapes₂_def, Function.update_of_ne (show result ≠ pc by decide), + Function.update_self] + simp [htapes₁_def, Function.update_self] + · -- Other tapes: a, b need special handling (push/pop) + by_cases h_i_a : i = a + · -- a tape: pushed in step 1, popped in step 5 → restored + subst h_i_a + simp [htapes₄_def, htapes₃_def, htapes₂_def, htapes₁_def, + Function.update_self, Function.update_of_ne (show a ≠ pc by decide), + Function.update_of_ne (show a ≠ result by decide), + Function.update_of_ne (show a ≠ b by decide), + Function.update_of_ne (show a ≠ t by decide), + Function.update_of_ne (show a ≠ c by decide)] + · by_cases h_i_b : i = b + · -- b tape: pushed in step 1, popped in step 5 → restored + subst h_i_b + simp [htapes₄_def, htapes₃_def, htapes₂_def, htapes₁_def, + Function.update_self, Function.update_of_ne (show b ≠ pc by decide), + Function.update_of_ne (show b ≠ result by decide), + Function.update_of_ne (show b ≠ a by decide), + Function.update_of_ne (show b ≠ t by decide), + Function.update_of_ne (show b ≠ c by decide)] + · -- All remaining tapes: not a,b,c,t,pc,result → truly unchanged + -- Step through each layer of Function.update + simp only [Function.update_of_ne h_i_pc, Function.update_of_ne h_i_c, + Function.update_of_ne h_i_result, Function.update_of_ne h_i_t, + Function.update_of_ne h_i_b, Function.update_of_ne h_i_a] + -- Now both sides should reduce to tapes i through tapes₄, ₃, ₂, ₁ + simp only [htapes₄_def, Function.update_of_ne h_i_result, + Function.update_of_ne h_i_pc] + simp only [htapes₃_def, Function.update_of_ne h_i_pc, + Function.update_of_ne h_i_b, Function.update_of_ne h_i_a] + simp only [htapes₂_def, Function.update_of_ne h_i_result, + Function.update_of_ne h_i_pc] + simp only [htapes₁_def, Function.update_of_ne h_i_pc, + Function.update_of_ne h_i_t, Function.update_of_ne h_i_b, + Function.update_of_ne h_i_a] + -- Main inductive step for succ case + -- iter_count_bound max (t_val+1) = 2 + max*(3 + 2*iter_count_bound max t_val) + -- Structure: 1 step (funStart, t>0) + max*(3+2n) steps (loop) + 1 step (loopStart, c=max) + have h_headD : dya_inv ((tapes t).headD []) = t_val.succ := by + rw [List.headD_eq_head?]; exact h_t + rw [h_headD] + simp only [iter_count_bound] + -- Step 1: funStart with t > 0 (t_val.succ ≠ 0) + -- Since t ≠ 0, funStart pushes c=[], result=[], pc=l_loopStart + have h_t_nonzero : (tapes t).head?.getD [] ≠ [] := by + intro h_eq + have : dya_inv ((tapes t).head?.getD []) = 0 := by rw [h_eq]; simp + omega + unfold edge_semantics at h_edge_semantics + have h_funstart_eval : (innerLoop edge (dya max)).eval_list tapes = + Part.some (Function.update (Function.update (Function.update tapes + c ([] :: tapes c)) + result ([] :: tapes result)) + pc (l_loopStart :: (tapes pc).tail)) := by + simp [innerLoop, h_pc_funStart, h_t_nonzero, h_edge_semantics]; grind + have h_funstart := @innerLoopFun_eq_of_eval_list r h_r_dec max edge + h_edge_semantics _ _ h_funstart_eval + -- After funStart: c=[]::tapes c, result=[]::tapes result, pc=l_loopStart::tail + -- Decompose: f^[2 + max*(3+2n)] x = f (f^[max*(3+2n)] (f x)) + conv_lhs => rw [show 2 + max * (3 + 2 * iter_count_bound max t_val) = + Nat.succ (max * (3 + 2 * iter_count_bound max t_val) + 1) from by omega] + rw [Function.iterate_succ_apply'] + conv_lhs => arg 1; rw [Function.iterate_add_apply, Function.iterate_one] + rw [h_funstart] + -- Post-funStart state + set tapes_post := Function.update (Function.update (Function.update tapes + c ([] :: tapes c)) + result ([] :: tapes result)) + pc (l_loopStart :: (tapes pc).tail) with h_tapes_post + -- Goal: innerLoopFun (innerLoopFun^[max*(3+2n)] tapes_post) = expected + -- Loop invariant: after k iterations of h_inner, the tape state is predictable + -- Each h_inner iteration takes (3 + 2*iter_count_bound max t_val) steps + -- We need max such iterations, followed by one final step + -- + -- Key steps: + -- 1. max iterations of h_inner: c increments from dya(0) to dya(max-1), + -- result accumulates path checks, t and pc preserved + -- 2. Final innerLoopFun: inner_loop_start with c = dya(max) → pops c and result + -- 3. The accumulated result matches RelatesInSteps r a b (2^(t_val+1)) + -- via relatesInStepsExp and h_finite (finiteness bounds the search space) + -- + -- The loop invariant proof requires induction on max, tracking Function.update + -- chains through each iteration. Each iteration uses h_inner to advance the state. + -- The final step uses inner_loop_start with the c = max branch. + -- The accumulated result equivalence uses relatesInStepsExp (sorry) and + -- h_finite (finiteness) to connect the iterated check to RelatesInSteps. + constructor + · -- Main equality: the accumulated result of max h_inner iterations + final step + -- Proof sketch: + -- 1. By induction on k ≤ max, show that after k*(3+2n) steps from tapes_post: + -- c = dya(k) :: tapes c, result = (accumulated_check k) :: tapes result, + -- t = dya(t_val.succ) :: (tapes t).tail, pc = l_loopStart :: (tapes pc).tail + -- where accumulated_check k = (∃ c_val with dya_inv < k, + -- RelatesInSteps r a_val c_val (2^t_val) ∧ RelatesInSteps r c_val b_val (2^t_val)) + -- ∨ (tapes result).headD [] ≠ [] + -- 2. After max iterations (k=max), the final innerLoopFun uses inner_loop_start + -- with c = dya(max), hitting the "c = max" branch that pops c and result. + -- 3. The accumulated check for k=max is equivalent to + -- RelatesInSteps r a_val b_val (2^(t_val+1)) via relatesInStepsExp and h_finite + -- (finiteness bounds search to dya_inv values < max). + -- 4. Combined with (tapes result).headD [] = [] (since result was pushed with []), + -- the final result matches the target. sorry - -- simp only [innerLoopFun, MultiTapeTM.eval_list_tot_eq_eval_list_get] - -- rw [inner_loop_start h_pc] - -- simp only [Part.get_some] - -- simp only [h_c, h_t] - -- simp only [↓reduceIte] - -- simp only [Nat.succ_eq_add_one, add_tsub_cancel_right] - -- simp only [innerLoopFun] at ih - -- let tapes₁ := (Function.update (Function.update (Function.update (Function.update tapes - -- a ((tapes a).head?.getD [] :: tapes a)) - -- b ((tapes c).head?.getD [] :: tapes b)) - -- t ((dya t_val) :: (tapes t).tail)) - -- pc (l_funStart :: l_afterFirstRec :: (tapes pc).tail)) - -- let ih' := (ih tapes₁ (by simp [tapes₁]) (by simp [tapes₁])).1 - -- have : (dya_inv ((tapes₁ t).headD [])) = t_val := by simp [tapes₁] - -- rw [this] at ih' - -- simp [tapes₁] at ih' - -- simp [ih'] - -- simp [inner_loop_after_first_rec] - -- let ih' := ih (Function.update - -- (Function.update - -- (Function.update - -- (Function.update - -- (Function.update - -- (Function.update - -- (Function.update (Function.update tapes - -- 0 ((tapes 0).head?.getD [] :: tapes 0)) - -- 1 ((tapes c).head?.getD [] :: tapes 1)) - -- t (dya t_val :: (tapes t).tail)) - -- pc (l_afterFirstRec :: (tapes pc).tail)) - -- result - -- (if Relation.RelatesInSteps r - -- ((tapes 0).head?.getD []) - -- ((tapes c).head?.getD []) - -- (2 ^ t_val) then - -- [OneTwo.one] :: tapes result - -- else [] :: tapes result)) - -- 0 ((tapes c).head?.getD [] :: tapes 0)) - -- 1 ((tapes 1).head?.getD [] :: tapes 1)) - -- pc (l_funStart :: l_afterSecondRec :: (tapes pc).tail)) - -- simp at ih' - -- let ih' := ih'.1 - -- simp [ih'] - -- simp [inner_loop_after_second_rec] - -- simp [function_update_pull 0] - -- simp [function_update_pull 1] - -- simp [function_update_pull result] - -- simp [function_update_pull pc] - -- simp [function_update_pull c] - -- simp [function_update_pull t] - -- by_cases h_r₁ : Relation.RelatesInSteps r - -- ((tapes 0).head?.getD []) ((tapes c).head?.getD []) (2 ^ t_val) - -- · by_cases h_r₂ : Relation.RelatesInSteps r - -- ((tapes c).head?.getD []) ((tapes 1).head?.getD []) (2 ^ t_val) - -- · simp [h_r₁, h_r₂] - -- · simp [h_r₁, h_r₂] - -- grind - -- · by_cases h_r₂ : Relation.RelatesInSteps r - -- ((tapes c).head?.getD []) ((tapes 1).head?.getD []) (2 ^ t_val) - -- · simp [h_r₁, h_r₂] - -- grind - -- · simp [h_r₁, h_r₂] - -- grind - - sorry + · -- PC length preservation during all iterations + intro n' h_n' + -- tapes pc is non-empty since head = l_funStart ≠ [] + have h_pc_ne : tapes pc ≠ [] := by intro h; simp [h] at h_pc_funStart + -- n' = 0: trivial (identity) + by_cases h0 : n' = 0 + · subst h0; simp + · -- n' ≥ 1: factor out funStart step + rw [show n' = (n' - 1) + 1 from by omega, + Function.iterate_add_apply, Function.iterate_one, h_funstart] + -- tapes_post pc = l_loopStart :: (tapes pc).tail, same length as tapes pc + have h_post_pc : tapes_post pc = l_loopStart :: (tapes pc).tail := by + simp [h_tapes_post, Function.update_self] + have h_post_len : (tapes_post pc).length = (tapes pc).length := by + rw [h_post_pc] + rcases h_list : tapes pc with _ | ⟨_, tl⟩ + · exact absurd h_list h_pc_ne + · simp + -- Suffices to show preservation from tapes_post + suffices h_suff : ((innerLoopFun max h_edge_semantics)^[n' - 1] + tapes_post pc).length ≥ (tapes_post pc).length by omega + -- Decompose n'-1 into k complete h_inner iterations + j remaining steps + set step_size := 3 + 2 * iter_count_bound max t_val with h_step_size_def + have h_step_pos : step_size > 0 := by omega + have h_n1_bound : n' - 1 ≤ max * step_size := by omega + -- Loop invariant: after k complete iterations, pc/c/t are preserved + have h_loop_inv : ∀ ki ≤ max, + ((innerLoopFun max h_edge_semantics)^[ki * step_size] tapes_post pc) = + l_loopStart :: (tapes pc).tail ∧ + ((innerLoopFun max h_edge_semantics)^[ki * step_size] + tapes_post c).head?.getD [] = dya ki ∧ + dya_inv (((innerLoopFun max h_edge_semantics)^[ki * step_size] + tapes_post t).head?.getD []) = t_val.succ := by + intro ki + induction ki with + | zero => + intro _ + simp only [Nat.zero_mul, Function.iterate_zero_apply] + refine ⟨h_post_pc, ?_, ?_⟩ + · -- (tapes_post c).head?.getD [] = dya 0 = [] + have h_c_val : tapes_post c = [] :: tapes c := by + simp [h_tapes_post, Function.update_of_ne (show pc ≠ c from by decide), + Function.update_of_ne (show result ≠ c from by decide), + Function.update_self] + simp [h_c_val] + · -- dya_inv((tapes_post t).head?.getD []) = t_val.succ + have h_t_val : tapes_post t = tapes t := by + simp [h_tapes_post, Function.update_of_ne (show pc ≠ t from by decide), + Function.update_of_ne (show result ≠ t from by decide), + Function.update_of_ne (show c ≠ t from by decide)] + rw [h_t_val]; exact h_t + | succ ki' ih_ki => + intro h_ki + obtain ⟨h_pc_ki, h_c_ki, h_t_ki⟩ := ih_ki (by omega) + rw [show (ki' + 1) * step_size = step_size + ki' * step_size from + by simp [Nat.add_mul]; omega, + Function.iterate_add_apply] + -- Preconditions for h_inner on the intermediate state + have h_s_pc : ((innerLoopFun max h_edge_semantics)^[ki' * step_size] + tapes_post pc).head?.getD [] = l_loopStart := by + rw [h_pc_ki]; simp + have h_s_c : ((innerLoopFun max h_edge_semantics)^[ki' * step_size] + tapes_post c).head?.getD [] ≠ dya max := by + rw [h_c_ki]; intro h_eq + have := congr_arg dya_inv h_eq + simp [dya_inv_dya] at this; omega + -- Apply h_inner + have h_step := h_inner ((innerLoopFun max h_edge_semantics)^[ki' * step_size] + tapes_post) h_s_pc h_s_c h_t_ki + -- Prove each component using congr_fun + Function.update unfolding + refine ⟨?_, ?_, ?_⟩ + · -- pc = l_loopStart :: (tapes pc).tail + have := congr_fun h_step pc + simp [Function.update, show result ≠ pc from by decide, + show pc = pc from rfl] at this + rw [this, h_pc_ki]; simp + · -- c head = dya (ki' + 1) + have := congr_fun h_step c + simp [Function.update, show result ≠ c from by decide, + show pc ≠ c from by decide, show t ≠ c from by decide, + show c = c from rfl] at this + rw [this]; simp only [List.head?_cons, Option.getD_some] + simp only [dya_succ, List.headD_eq_head?, h_c_ki, dya_inv_dya] + · -- t: dya_inv(head) = t_val.succ + have := congr_fun h_step t + simp [Function.update, show result ≠ t from by decide, + show pc ≠ t from by decide, show t = t from rfl] at this + rw [this]; simp [List.head?_cons, Option.getD_some, dya_inv_dya] + -- Within one h_inner iteration, PC length ≥ input at all intermediate steps + have h_inner_pc : ∀ (s : Fin tapeCount → List (List OneTwo)), + (s pc).head?.getD [] = l_loopStart → + (s c).head?.getD [] ≠ dya max → + dya_inv ((s t).head?.getD []) = t_val.succ → + ∀ ji ≤ step_size, + ((innerLoopFun max h_edge_semantics)^[ji] s pc).length ≥ (s pc).length := by + intro s h_s_pc h_s_c h_s_t ji h_ji + set n := iter_count_bound max t_val with hn_def + have h_s_pc_ne : s pc ≠ [] := by intro h; simp [h] at h_s_pc + have h_s_pc_tail_len : (s pc).tail.length + 1 = (s pc).length := by + rcases s pc with _ | ⟨_, _⟩ <;> simp_all + -- Step 1: inner_loop_start (c ≠ max) + have h_step1_eval := @inner_loop_start max edge s h_s_pc + simp only [if_neg h_s_c] at h_step1_eval + have h_step1 := @innerLoopFun_eq_of_eval_list r h_r_dec max edge + h_edge_semantics _ _ h_step1_eval + by_cases h0 : ji = 0 + · subst h0; simp + · -- ji ≥ 1: factor out Step 1 + rw [show ji = (ji - 1) + 1 from by omega, + Function.iterate_add_apply, Function.iterate_one, h_step1] + set s₁ := Function.update (Function.update (Function.update + (Function.update s + a ((s a).head?.getD [] :: s a)) + b ((s c).head?.getD [] :: s b)) + t (dya (dya_inv ((s t).head?.getD []) - 1) :: (s t).tail)) + pc (l_funStart :: l_afterFirstRec :: (s pc).tail) with hs₁ + have h_s1_pc_val : s₁ pc = l_funStart :: l_afterFirstRec :: (s pc).tail := by + simp [hs₁, Function.update_self] + have h_s1_pc_head : (s₁ pc).head?.getD [] = l_funStart := by + rw [h_s1_pc_val]; simp + have h_s1_pc_len : (s₁ pc).length = (s pc).length + 1 := by + rw [h_s1_pc_val]; simp; omega + have h_s1_t_val : dya_inv ((s₁ t).head?.getD []) = t_val := by + simp [hs₁, Function.update_self, dya_inv_dya]; omega + obtain ⟨h_ih₁_main, h_ih₁_pc⟩ := ih s₁ h_s1_pc_head h_s1_t_val + have h_n_eq₁ : iter_count_bound max (dya_inv ((s₁ t).headD [])) = n := by + rw [List.headD_eq_head?, h_s1_t_val] + rw [h_n_eq₁] at h_ih₁_main h_ih₁_pc + -- During IH₁: ji-1 < n + by_cases hlt₁ : ji - 1 < n + · have := h_ih₁_pc (ji - 1) hlt₁; omega + · -- After IH₁ + rw [show ji - 1 = (ji - 1 - n) + n from by omega, + Function.iterate_add_apply] + set s₂ := (innerLoopFun max h_edge_semantics)^[n] s₁ with hs₂_def + have hs₂_eq := hs₂_def.trans h_ih₁_main + have h_s2_pc_val : s₂ pc = l_afterFirstRec :: (s pc).tail := by + rw [hs₂_eq] + simp [Function.update_self, h_s1_pc_val] + have h_s2_pc_len : (s₂ pc).length = (s pc).length := by + rw [h_s2_pc_val]; simp; omega + -- ji-1-n = 0: IH₁ just completed + by_cases h2 : ji - 1 - n = 0 + · rw [h2]; simp; omega + · -- Step 3: after_first_rec + have h_s2_pc_head : (s₂ pc).head?.getD [] = l_afterFirstRec := by + rw [h_s2_pc_val]; simp + have h_step3_eval := + @inner_loop_after_first_rec max edge s₂ h_s2_pc_head + have h_step3 := @innerLoopFun_eq_of_eval_list r h_r_dec max edge + h_edge_semantics _ _ h_step3_eval + rw [show ji - 1 - n = (ji - 1 - n - 1) + 1 from by omega, + Function.iterate_add_apply, Function.iterate_one] + set s₃ := innerLoopFun max h_edge_semantics s₂ with hs₃_def + have hs₃_eq := hs₃_def.trans h_step3 + have h_s3_pc_val : + s₃ pc = l_funStart :: l_afterSecondRec :: (s pc).tail := by + rw [hs₃_eq]; simp [Function.update_self, h_s2_pc_val] + have h_s3_pc_head : (s₃ pc).head?.getD [] = l_funStart := by + rw [h_s3_pc_val]; simp + have h_s3_pc_len : (s₃ pc).length = (s pc).length + 1 := by + rw [h_s3_pc_val]; simp; omega + have h_s3_t_val : + dya_inv ((s₃ t).head?.getD []) = t_val := by + have h_s3_t_eq : s₃ t = s₁ t := by + rw [hs₃_eq]; simp + rw [hs₂_eq]; simp + rw [h_s3_t_eq]; exact h_s1_t_val + obtain ⟨h_ih₂_main, h_ih₂_pc⟩ := ih s₃ h_s3_pc_head h_s3_t_val + have h_n_eq₂ : + iter_count_bound max (dya_inv ((s₃ t).headD [])) = n := by + rw [List.headD_eq_head?, h_s3_t_val] + rw [h_n_eq₂] at h_ih₂_main h_ih₂_pc + -- During IH₂: ji-1-n-1 < n + by_cases hlt₂ : ji - 1 - n - 1 < n + · have := h_ih₂_pc (ji - 1 - n - 1) hlt₂; omega + · -- After IH₂ + rw [show ji - 1 - n - 1 = (ji - 1 - n - 1 - n) + n from by omega, + Function.iterate_add_apply] + set s₄ := (innerLoopFun max h_edge_semantics)^[n] s₃ with hs₄_def + have hs₄_eq := hs₄_def.trans h_ih₂_main + have h_s4_pc_val : s₄ pc = l_afterSecondRec :: (s pc).tail := by + rw [hs₄_eq] + simp [Function.update_self, h_s3_pc_val] + have h_s4_pc_len : (s₄ pc).length = (s pc).length := by + rw [h_s4_pc_val]; simp; omega + -- ji-1-n-1-n = 0: IH₂ just completed + by_cases h4 : ji - 1 - n - 1 - n = 0 + · rw [h4]; simp; omega + · -- Step 5: after_second_rec (ji-1-n-1-n = 1) + have h5 : ji - 1 - n - 1 - n = 1 := by omega + rw [h5, Function.iterate_one] + have h_s4_pc_head : + (s₄ pc).head?.getD [] = l_afterSecondRec := by + rw [h_s4_pc_val]; simp + have h_step5_eval := + @inner_loop_after_second_rec max edge s₄ h_s4_pc_head + have h_step5 := @innerLoopFun_eq_of_eval_list r h_r_dec max edge + h_edge_semantics _ _ h_step5_eval + rw [h_step5]; simp [h_s4_pc_val]; omega + -- Combine h_loop_inv and h_inner_pc to prove overall preservation + -- Decompose (n'-1) = ji + ki * step_size using Euclidean division + have h_div_mod := Nat.div_add_mod (n' - 1) step_size + have h_ji_lt : (n' - 1) % step_size < step_size := Nat.mod_lt _ h_step_pos + have h_ki_mul_le : (n' - 1) / step_size * step_size ≤ n' - 1 := + Nat.div_mul_le_self _ _ + have h_sum : n' - 1 = (n' - 1) % step_size + (n' - 1) / step_size * step_size := by + have h := Nat.div_add_mod (n' - 1) step_size + -- h : step_size * ((n' - 1) / step_size) + (n' - 1) % step_size = n' - 1 + have h2 : step_size * ((n' - 1) / step_size) = (n' - 1) / step_size * step_size := + Nat.mul_comm _ _ + omega + have h_ki_bound : (n' - 1) / step_size ≤ max := by + have h1 : (n' - 1) / step_size ≤ (max * step_size) / step_size := + Nat.div_le_div_right h_n1_bound + have h2 : max * step_size / step_size = max := + Nat.mul_div_cancel max h_step_pos + omega + rw [h_sum, Function.iterate_add_apply] + obtain ⟨h_sk_pc, h_sk_c, h_sk_t⟩ := h_loop_inv _ h_ki_bound + have h_sk_len : ((innerLoopFun max h_edge_semantics)^[ + (n' - 1) / step_size * step_size] tapes_post pc).length = + (tapes_post pc).length := by + rw [h_sk_pc, h_post_pc] + by_cases hk_max : (n' - 1) / step_size = max + · -- ki = max: ji must be 0 since n'-1 ≤ max*step_size + have hj0 : (n' - 1) % step_size = 0 := by + have h1 : max * step_size ≤ n' - 1 := by + rw [← hk_max]; exact h_ki_mul_le + have h3 : n' - 1 = max * step_size := Nat.le_antisymm h_n1_bound h1 + rw [h3, show max * step_size = step_size * max from Nat.mul_comm _ _, + Nat.mul_mod_right] + rw [hj0]; simp; omega + · -- ki < max: apply h_inner_pc to the state after ki iterations + have hk_lt : (n' - 1) / step_size < max := by omega + have h_pc_cond : ((innerLoopFun max h_edge_semantics)^[ + (n' - 1) / step_size * step_size] tapes_post pc).head?.getD [] = + l_loopStart := by + rw [h_sk_pc]; simp + have h_c_cond : ((innerLoopFun max h_edge_semantics)^[ + (n' - 1) / step_size * step_size] tapes_post c).head?.getD [] ≠ dya max := by + rw [h_sk_c]; intro h_eq + have := congr_arg dya_inv h_eq + simp [dya_inv_dya] at this; omega + have h_res := h_inner_pc _ h_pc_cond h_c_cond h_sk_t + ((n' - 1) % step_size) h_ji_lt.le + omega theorem reachability_eval_list diff --git a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean index caab7aaf5..e713b3d08 100644 --- a/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean +++ b/Cslib/Computability/Machines/MultiTapeTuring/ListEncoding.lean @@ -121,6 +121,15 @@ public def MultiTapeTM.eval_list_tot Fin k → List (List Symbol) := (tm.eval_list tapes).get (tm.eval_list_dom_of_halts_on_lists (h_alwaysHalts tapes)) +/-- If `eval_list` returns `Part.some result'`, then `eval_list_tot` returns `result'`. -/ +public theorem MultiTapeTM.eval_list_tot_eq_of_eval_list + (tm : MultiTapeTM k (WithSep Symbol)) + (h_alwaysHalts : ∀ tapes, tm.HaltsOnLists tapes) + (tapes result' : Fin k → List (List Symbol)) + (h : tm.eval_list tapes = Part.some result') : + tm.eval_list_tot h_alwaysHalts tapes = result' := by + simp [eval_list_tot, Part.get_eq_iff_eq_some, h] + @[simp, grind =] public theorem MultiTapeTM.extend_eval_list {k₁ k₂ : ℕ} {h_le : k₁ ≤ k₂}