From 6b22ba14b0ae64e4a91615993d202002eed59869 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:20:09 -0400 Subject: [PATCH] refactor(machines): move raw machine lemmas out of the classes (part 1) Move machine-layer content out of `Classes` into `Machines/Turing/MultiTape` (#610 item 9, part 1): - `Classes/Constructible.lean` -> new `Complexity/BigO/Constructible.lean`: `two_pow_length_encNat_le`, `exists_pow_length_encNat_le`, `ComputableTidilyInO.lengthNat`, `ComputableTidilyInO.unaryLe` and `ComputableTidilyInO.natToUnary`. `TimeConstructible`, `SpaceConstructible` and their theorems stay in `Classes/Constructible.lean`, which imports the new module. - `Classes/Hierarchy/SpaceUniversal.lean` -> `Universal/SpaceBudget.lean` (the universal machine within a space budget); it now imports the new Machines module instead of `Classes.Constructible`. - The `Frames` section of `Classes/Alternation/GuessVerify.lean` -> `Encodings/Frame.lean`: `frame_append_cons`, `getElem?_frame_append_length`, `getElem?_frame_append_cons`, `lt_length_frame_append_cons`, `set_frame_append_cons`, `two_mul_length_le_length_frame_append` and their private helper. Declaration names and statements are unchanged; proofs are unchanged except that `ring` became `omega` in a private length lemma, and two moved lemmas gained docstrings. Clients (`Hierarchy/ShortDesc`, `Hierarchy/Time`, `Hierarchy/Space`, `Alternation/GuessVerify`) import what they use; module docs are updated. No Machines module imports a Classes module. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 3 +- .../Classes/Alternation/GuessVerify.lean | 55 +----- .../Complexity/Classes/Constructible.lean | 147 +------------- .../Classes/Hierarchy/ShortDesc.lean | 6 +- .../Complexity/Classes/Hierarchy/Space.lean | 3 +- .../Complexity/Classes/Hierarchy/Time.lean | 1 + .../Complexity/BigO/Constructible.lean | 180 ++++++++++++++++++ .../Turing/MultiTape/Encodings/Frame.lean | 61 ++++++ .../MultiTape/Universal/SpaceBudget.lean} | 3 +- 9 files changed, 260 insertions(+), 199 deletions(-) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Constructible.lean rename Complexity/Computability/{Complexity/Classes/Hierarchy/SpaceUniversal.lean => Machines/Turing/MultiTape/Universal/SpaceBudget.lean} (99%) diff --git a/Complexity.lean b/Complexity.lean index 9f02a54dd4..570a120bf3 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -560,7 +560,6 @@ public import Complexity.Computability.Complexity.Classes.FewP.Machine public import Complexity.Computability.Complexity.Classes.Hierarchy public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc public import Complexity.Computability.Complexity.Classes.Hierarchy.Space -public import Complexity.Computability.Complexity.Classes.Hierarchy.SpaceUniversal public import Complexity.Computability.Complexity.Classes.Hierarchy.Time public import Complexity.Computability.Complexity.Classes.IP public import Complexity.Computability.Complexity.Classes.IP.CoinFixing @@ -852,6 +851,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Tid public import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Transducer public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arith public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Option public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Pi public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Plain @@ -1080,6 +1080,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Machi public import Complexity.Computability.Machines.Turing.MultiTape.Universal.PolyTime public import Complexity.Computability.Machines.Turing.MultiTape.Universal.ResourceBound public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Space +public import Complexity.Computability.Machines.Turing.MultiTape.Universal.SpaceBudget public import Complexity.Computability.Machines.Turing.SingleTape.Partrec public import Complexity.Computability.Machines.Turing.SingleTape.PostTuringMachine public import Complexity.Computability.Machines.Turing.TM2.ConfigBound diff --git a/Complexity/Computability/Complexity/Classes/Alternation/GuessVerify.lean b/Complexity/Computability/Complexity/Classes/Alternation/GuessVerify.lean index c15cd07c80..677828823e 100644 --- a/Complexity/Computability/Complexity/Classes/Alternation/GuessVerify.lean +++ b/Complexity/Computability/Complexity/Classes/Alternation/GuessVerify.lean @@ -15,6 +15,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Ba import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame /-! # Games of polynomially many moves are in `AP` @@ -93,60 +94,6 @@ theorem tapeOfList_set {Symbol : Type*} (w : List Symbol) {i : ℕ} (hi : i < w. simp [hi] · simp [h, Ne.symm h] -namespace MultiTapeTM - -/-! ### Frames followed by a word -/ - -section Frames - -private theorem length_flatMap_pair (w : List Bool) : - (w.flatMap fun b => [true, b]).length = 2 * w.length := by - induction w with - | nil => rfl - | cons b w ih => - simp only [List.flatMap_cons, List.length_append, ih, List.length_cons, List.length_nil] - ring - -/-- A frame split at a symbol. -/ -theorem frame_append_cons (w v : List Bool) (c : Bool) : - frame (w ++ c :: v) = (w.flatMap fun b => [true, b]) ++ true :: c :: frame v := by - simp [frame] - -/-- After the pairs of a frame comes its terminator `false`. -/ -theorem getElem?_frame_append_length (w x : List Bool) : - (frame w ++ x)[2 * w.length]? = some false := by - rw [frame, List.append_assoc, List.getElem?_append_right (by rw [length_flatMap_pair]), - length_flatMap_pair] - simp - -/-- Each pair of a frame starts with the tag `true`. -/ -theorem getElem?_frame_append_cons (w v x : List Bool) (c : Bool) : - (frame (w ++ c :: v) ++ x)[2 * w.length]? = some true := by - rw [frame_append_cons, List.append_assoc, - List.getElem?_append_right (by rw [length_flatMap_pair]), length_flatMap_pair] - simp - -theorem lt_length_frame_append_cons (w v x : List Bool) (c : Bool) : - 2 * w.length + 1 < (frame (w ++ c :: v) ++ x).length := by - simp only [List.length_append, length_frame, List.length_cons] - omega - -/-- Setting the second cell of a pair of a frame replaces the framed symbol. -/ -theorem set_frame_append_cons (w v x : List Bool) (c b : Bool) : - (frame (w ++ c :: v) ++ x).set (2 * w.length + 1) b = frame (w ++ b :: v) ++ x := by - rw [frame_append_cons, frame_append_cons, List.append_assoc, List.append_assoc, - List.set_append_right _ _ (by rw [length_flatMap_pair]; omega), length_flatMap_pair] - simp - -theorem two_mul_length_le_length_frame_append (w x : List Bool) : - 2 * w.length ≤ (frame w ++ x).length := by - simp only [List.length_append, length_frame] - omega - -end Frames - -end MultiTapeTM - namespace MultiTapeATM open MultiTapeMachine diff --git a/Complexity/Computability/Complexity/Classes/Constructible.lean b/Complexity/Computability/Complexity/Classes/Constructible.lean index 4ec9b40510..f44c4b9e90 100644 --- a/Complexity/Computability/Complexity/Classes/Constructible.lean +++ b/Complexity/Computability/Complexity/Classes/Constructible.lean @@ -11,10 +11,10 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Spac public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormalForm import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Arith +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower import Complexity.Computability.Machines.Turing.MultiTape.Universal.Compose -import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential import Cslib.Computability.Machines.Turing.MultiTape.Combinators.AlmostConstant /-! @@ -26,8 +26,11 @@ The input tape is read-only and the output tape write-only. Neither definition i bound on the resource function; hierarchy theorems state the lower bounds they need separately. The shared length and arithmetic routines give concrete constructible bounds, without importing -any hierarchy theorem. Unary word length is supplied by the quantitative API -(`Turing.MultiTapeTM.ComputableTidilyInO.lengthUnary`). +any hierarchy theorem. The length of a word in binary +(`Turing.MultiTapeTM.ComputableTidilyInO.lengthNat`) and the bounds on binary digits +(`Turing.MultiTapeTM.exists_pow_length_encNat_le`) are in +`Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible`; unary word +length is supplied by the quantitative API (`Turing.MultiTapeTM.ComputableTidilyInO.lengthUnary`). ## Main definitions @@ -52,144 +55,6 @@ any hierarchy theorem. Unary word length is supplied by the quantitative API @[expose] public section -namespace Turing.MultiTapeTM - -/-- The binary digits of `m` are logarithmic: `2 ^ (encNat m).length ≤ 2 * (m + 1)`. -/ -theorem two_pow_length_encNat_le (m : ℕ) : 2 ^ (encNat m).length ≤ 2 * (m + 1) := by - rw [encNat_apply, Nat.size_eq_bits_len] - rcases Nat.eq_zero_or_pos m with rfl | hm - · simp - · have h₁ : 2 ^ (m.size - 1) ≤ m := Nat.lt_size.mp (by - have := Nat.size_pos.mpr hm - omega) - have h₂ : 1 ≤ m.size := Nat.size_pos.mpr hm - rw [show m.size = (m.size - 1) + 1 by omega, pow_succ] - omega - -/-- Every power of the number of binary digits of `m` is `O(m + 1)`. -/ -theorem exists_pow_length_encNat_le (d : ℕ) : - ∃ C, ∀ m, ((encNat m).length + 1) ^ d ≤ C * (m + 1) := by - obtain ⟨C, hC⟩ := Cslib.PolynomiallyBounded.exists_le_mul_two_pow (p := fun L => (L + 1) ^ d) - (by fun_prop) - refine ⟨2 * C, fun m => (hC _).trans ?_⟩ - calc C * 2 ^ (encNat m).length ≤ C * (2 * (m + 1)) := - Nat.mul_le_mul_left _ (two_pow_length_encNat_le m) - _ = 2 * C * (m + 1) := by ring - -/-! ### Lengths and comparisons, computed -/ - -namespace ComputableTidilyInO - -/-- The length of a bit word in binary, by a binary counter, within quadratic time and linear -space. -/ -theorem lengthNat : ComputableTidilyInO (fun l : List Bool => l.length) encBits encNat - (fun l => (l.length + 1) ^ 2) fun l => l.length + 1 := by - obtain ⟨C, hC⟩ := exists_pow_length_encNat_le 2 - have hstep := natSucc.comp (fst encNat encBool) - have hlen (x : List Bool) (i : ℕ) : - (List.take i x).foldl (fun n _ => n + 1) 0 = min i x.length := by - simp [List.foldl_const] - have h := foldl (encA := encBool) (encL := encBits) (encB := encNat) (list := id) - (init := fun _ => 0) (step := fun n _ => n + 1) (of_linear (.of_eq fun _ => rfl)) (const 0) - hstep (R := fun x => (C + 3) * (x.length + 1)) (Q := fun x => 3 * (x.length + 1)) - (B := fun x => x.length) - (fun x i hi => by - simp only [id] at hi ⊢ - rw [hlen] - have h₁ := hC (min i x.length) - have h₂ := Universal.length_encNat_le (min i x.length) - have h₃ : C * (min i x.length + 1) ≤ C * (x.length + 1) := - Nat.mul_le_mul_left _ (by omega) - have e : (C + 3) * (x.length + 1) = C * (x.length + 1) + 3 * (x.length + 1) := by ring - simp only [length_encPair, encBool_apply, List.length_singleton] - omega) - (fun x i hi => by - simp only [id] at hi ⊢ - rw [hlen] - have h₂ := Universal.length_encNat_le (min i x.length) - simp only [length_encPair, encBool_apply, List.length_singleton] - omega) - (fun x i hi => by - simp only [id] at hi ⊢ - rw [hlen] - exact (Universal.length_encNat_le _).trans (Nat.min_le_right _ _)) - refine (h.mono (C + 16) (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ - · simp only [id, encBits_apply] - nlinarith - · simp only [id, encBits_apply] - nlinarith - · simp [List.foldl_const] - -/-- The comparison of unary numbers, by counting down, within quadratic time and linear space. -/ -theorem unaryLe : ComputableTidilyInO (fun p : ℕ × ℕ => decide (p.1 ≤ p.2)) - (encPair encUnary encUnary) encBool (fun p => ((encPair encUnary encUnary p).length + 1) ^ 2) - fun p => (encPair encUnary encUnary p).length + 1 := by - have hstep := (ComputableTidilyInDegree.unary_pred.inO_one).comp (fst encUnary encBool) - have hrep (a b : ℕ) : (List.replicate b true).foldl (fun n _ => n - 1) a = a - b := by - induction b generalizing a with - | zero => rfl - | succ b ih => rw [List.replicate_succ, List.foldl_cons, ih]; omega - have h := foldl (encA := encBool) (encL := encBits) (encB := encUnary) - (list := fun p : ℕ × ℕ => List.replicate p.2 true) (init := fun p => p.1) - (step := fun n _ => n - 1) - ((of_linear (.of_eq (f := fun n => List.replicate n true) (encIn := encUnary) - (encMid := encBits) fun _ => rfl)).comp (snd encUnary encUnary)) - (fst encUnary encUnary) hstep - (R := fun p => 3 * ((encPair encUnary encUnary p).length + 1)) - (Q := fun p => 3 * ((encPair encUnary encUnary p).length + 1)) - (B := fun p => (encPair encUnary encUnary p).length) - (fun p i hi => by - rw [List.take_replicate, hrep] - simp only [length_encPair, encUnary_apply, List.length_replicate, - encBool_apply, List.length_singleton] - omega) - (fun p i hi => by - rw [List.take_replicate, hrep] - simp only [length_encPair, encUnary_apply, List.length_replicate, - encBool_apply, List.length_singleton] - omega) - (fun p i hi => by - rw [List.take_replicate, hrep] - simp only [length_encPair, encUnary_apply, List.length_replicate] - omega) - have hz := (ComputableTidilyInDegree.unary_isZero.inO_one).comp_linear h - refine (hz.mono 16 (fun p => ?_) fun p => ?_).of_enc_eq fun p => ?_ - · simp only [length_encPair, encUnary_apply, List.length_replicate, - encBits_apply] - nlinarith - · simp only [length_encPair, encUnary_apply, List.length_replicate, - encBits_apply] - omega - · simp only [Function.comp_apply, hrep, Nat.sub_eq_zero_iff_le] - -end ComputableTidilyInO - -/-- **From binary to unary**, by counting down: within time `O((n + 1) ^ 3)` and space `O(n)`. -/ -theorem ComputableTidilyInO.natToUnary : ComputableTidilyInO (fun n : ℕ => n) encNat encUnary - (fun n => (n + 1) ^ 3) fun n => n := by - have hiter (n : ℕ) : (· + 1)^[n] 0 = n := by - induction n with - | zero => rfl - | succ n ih => rw [Function.iterate_succ_apply', ih] - have h := ComputableTidilyInO.iterate (n := fun n : ℕ => n) (init := fun _ => 0) - (step := (· + 1)) (encIn := encNat) (encB := encUnary) - (ComputableTidilyInO.of_linear (.of_eq fun _ => rfl)) (ComputableTidilyInO.const 0) - ComputableTidilyInDegree.unary_succ.inO_one (R := fun n => n) (Q := fun n => n) - (B := fun n => n) - (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk) - (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk) - (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk) - refine (h.of_enc_eq fun n => by rw [hiter]).mono 8 (fun n => ?_) fun n => ?_ - all_goals - have := Universal.length_encNat_le n - have h₁ : (n + 1) ^ 2 ≤ (n + 1) ^ 3 := Nat.pow_le_pow_right (by omega) (by omega) - have h₂ : n + 1 ≤ (n + 1) ^ 2 := Nat.le_self_pow (by norm_num) _ - have h₃ := Nat.pow_le_pow_left (show (encNat n).length + 1 ≤ n + 1 by omega) 2 - · nlinarith - · omega - -end Turing.MultiTapeTM - namespace Cslib.Complexity open Turing Turing.MultiTapeTM Turing.MultiTapeTM.Universal diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean index 06fcee565a..07d8364596 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/ShortDesc.lean @@ -7,8 +7,12 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Computability.Complexity.Classes.Constructible +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative +import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Frame import Complexity.Computability.Machines.Turing.MultiTape.Universal.Bound +import Mathlib.Data.Nat.Size /-! # Short descriptions diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean index cef2153f5a..9c82c73cd1 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/Space.lean @@ -10,10 +10,11 @@ module public import Complexity.Computability.Complexity.Classes.Constructible public import Complexity.Computability.Complexity.Classes.Hierarchy public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc -public import Complexity.Computability.Complexity.Classes.Hierarchy.SpaceUniversal public import Complexity.Computability.Complexity.Classes.LogSpace public import Complexity.Computability.Complexity.Classes.Space.Time public import Complexity.Computability.Machines.Turing.MultiTape.Run +public import Complexity.Computability.Machines.Turing.MultiTape.Universal.SpaceBudget +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean index 5f31d36e49..a253e6a0e8 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean +++ b/Complexity/Computability/Complexity/Classes/Hierarchy/Time.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Complexity.Classes.Hierarchy public import Complexity.Computability.Complexity.Classes.Hierarchy.ShortDesc public import Complexity.Computability.Complexity.Classes.Time public import Complexity.Computability.Machines.Turing.MultiTape.Run +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Constructible.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Constructible.lean new file mode 100644 index 0000000000..9dbbfa86fa --- /dev/null +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Constructible.lean @@ -0,0 +1,180 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Binary +import Complexity.Computability.Machines.Turing.MultiTape.Universal.Bound +import Complexity.Foundations.Data.Nat.PolynomialBound.Exponential +import Mathlib.Data.Nat.Size +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# Lengths, comparisons and unary conversion within given bounds + +Routines that compute resource bounds from an input, with tidy computability up to constants +(`Turing.MultiTapeTM.ComputableTidilyInO`): the length of a bit word in binary, by a binary +counter; the comparison of two unary numbers, by counting down; and the conversion of a number from +binary to unary, by counting up. They are the building blocks of constructible resource bounds and +of the diagonal machines of the hierarchy theorems. The number of binary digits of `m` is +logarithmic in `m`, so every power of it is `O(m + 1)`; this absorbs the binary counters into +bounds linear in the counted value. + +## Main results + +* `Turing.MultiTapeTM.two_pow_length_encNat_le`: the binary digits of `m` are logarithmic. +* `Turing.MultiTapeTM.exists_pow_length_encNat_le`: every power of the number of binary digits of + `m` is `O(m + 1)`. +* `Turing.MultiTapeTM.ComputableTidilyInO.lengthNat`: the length of a bit word in binary, within + quadratic time and linear space. +* `Turing.MultiTapeTM.ComputableTidilyInO.unaryLe`: the comparison of unary numbers, within + quadratic time and linear space. +* `Turing.MultiTapeTM.ComputableTidilyInO.natToUnary`: from binary to unary, within cubic time and + linear space. +-/ + +@[expose] public section + +namespace Turing.MultiTapeTM + +/-- The binary digits of `m` are logarithmic: `2 ^ (encNat m).length ≤ 2 * (m + 1)`. -/ +theorem two_pow_length_encNat_le (m : ℕ) : 2 ^ (encNat m).length ≤ 2 * (m + 1) := by + rw [encNat_apply, Nat.size_eq_bits_len] + rcases Nat.eq_zero_or_pos m with rfl | hm + · simp + · have h₁ : 2 ^ (m.size - 1) ≤ m := Nat.lt_size.mp (by + have := Nat.size_pos.mpr hm + omega) + have h₂ : 1 ≤ m.size := Nat.size_pos.mpr hm + rw [show m.size = (m.size - 1) + 1 by omega, pow_succ] + omega + +/-- Every power of the number of binary digits of `m` is `O(m + 1)`. -/ +theorem exists_pow_length_encNat_le (d : ℕ) : + ∃ C, ∀ m, ((encNat m).length + 1) ^ d ≤ C * (m + 1) := by + obtain ⟨C, hC⟩ := Cslib.PolynomiallyBounded.exists_le_mul_two_pow (p := fun L => (L + 1) ^ d) + (by fun_prop) + refine ⟨2 * C, fun m => (hC _).trans ?_⟩ + calc C * 2 ^ (encNat m).length ≤ C * (2 * (m + 1)) := + Nat.mul_le_mul_left _ (two_pow_length_encNat_le m) + _ = 2 * C * (m + 1) := by ring + +/-! ### Lengths and comparisons, computed -/ + +namespace ComputableTidilyInO + +/-- The length of a bit word in binary, by a binary counter, within quadratic time and linear +space. -/ +theorem lengthNat : ComputableTidilyInO (fun l : List Bool => l.length) encBits encNat + (fun l => (l.length + 1) ^ 2) fun l => l.length + 1 := by + obtain ⟨C, hC⟩ := exists_pow_length_encNat_le 2 + have hstep := natSucc.comp (fst encNat encBool) + have hlen (x : List Bool) (i : ℕ) : + (List.take i x).foldl (fun n _ => n + 1) 0 = min i x.length := by + simp [List.foldl_const] + have h := foldl (encA := encBool) (encL := encBits) (encB := encNat) (list := id) + (init := fun _ => 0) (step := fun n _ => n + 1) (of_linear (.of_eq fun _ => rfl)) (const 0) + hstep (R := fun x => (C + 3) * (x.length + 1)) (Q := fun x => 3 * (x.length + 1)) + (B := fun x => x.length) + (fun x i hi => by + simp only [id] at hi ⊢ + rw [hlen] + have h₁ := hC (min i x.length) + have h₂ := Universal.length_encNat_le (min i x.length) + have h₃ : C * (min i x.length + 1) ≤ C * (x.length + 1) := + Nat.mul_le_mul_left _ (by omega) + have e : (C + 3) * (x.length + 1) = C * (x.length + 1) + 3 * (x.length + 1) := by ring + simp only [length_encPair, encBool_apply, List.length_singleton] + omega) + (fun x i hi => by + simp only [id] at hi ⊢ + rw [hlen] + have h₂ := Universal.length_encNat_le (min i x.length) + simp only [length_encPair, encBool_apply, List.length_singleton] + omega) + (fun x i hi => by + simp only [id] at hi ⊢ + rw [hlen] + exact (Universal.length_encNat_le _).trans (Nat.min_le_right _ _)) + refine (h.mono (C + 16) (fun x => ?_) fun x => ?_).of_enc_eq fun x => ?_ + · simp only [id, encBits_apply] + nlinarith + · simp only [id, encBits_apply] + nlinarith + · simp [List.foldl_const] + +/-- The comparison of unary numbers, by counting down, within quadratic time and linear space. -/ +theorem unaryLe : ComputableTidilyInO (fun p : ℕ × ℕ => decide (p.1 ≤ p.2)) + (encPair encUnary encUnary) encBool (fun p => ((encPair encUnary encUnary p).length + 1) ^ 2) + fun p => (encPair encUnary encUnary p).length + 1 := by + have hstep := (ComputableTidilyInDegree.unary_pred.inO_one).comp (fst encUnary encBool) + have hrep (a b : ℕ) : (List.replicate b true).foldl (fun n _ => n - 1) a = a - b := by + induction b generalizing a with + | zero => rfl + | succ b ih => rw [List.replicate_succ, List.foldl_cons, ih]; omega + have h := foldl (encA := encBool) (encL := encBits) (encB := encUnary) + (list := fun p : ℕ × ℕ => List.replicate p.2 true) (init := fun p => p.1) + (step := fun n _ => n - 1) + ((of_linear (.of_eq (f := fun n => List.replicate n true) (encIn := encUnary) + (encMid := encBits) fun _ => rfl)).comp (snd encUnary encUnary)) + (fst encUnary encUnary) hstep + (R := fun p => 3 * ((encPair encUnary encUnary p).length + 1)) + (Q := fun p => 3 * ((encPair encUnary encUnary p).length + 1)) + (B := fun p => (encPair encUnary encUnary p).length) + (fun p i hi => by + rw [List.take_replicate, hrep] + simp only [length_encPair, encUnary_apply, List.length_replicate, + encBool_apply, List.length_singleton] + omega) + (fun p i hi => by + rw [List.take_replicate, hrep] + simp only [length_encPair, encUnary_apply, List.length_replicate, + encBool_apply, List.length_singleton] + omega) + (fun p i hi => by + rw [List.take_replicate, hrep] + simp only [length_encPair, encUnary_apply, List.length_replicate] + omega) + have hz := (ComputableTidilyInDegree.unary_isZero.inO_one).comp_linear h + refine (hz.mono 16 (fun p => ?_) fun p => ?_).of_enc_eq fun p => ?_ + · simp only [length_encPair, encUnary_apply, List.length_replicate, + encBits_apply] + nlinarith + · simp only [length_encPair, encUnary_apply, List.length_replicate, + encBits_apply] + omega + · simp only [Function.comp_apply, hrep, Nat.sub_eq_zero_iff_le] + +end ComputableTidilyInO + +/-- **From binary to unary**, by counting down: within time `O((n + 1) ^ 3)` and space `O(n)`. -/ +theorem ComputableTidilyInO.natToUnary : ComputableTidilyInO (fun n : ℕ => n) encNat encUnary + (fun n => (n + 1) ^ 3) fun n => n := by + have hiter (n : ℕ) : (· + 1)^[n] 0 = n := by + induction n with + | zero => rfl + | succ n ih => rw [Function.iterate_succ_apply', ih] + have h := ComputableTidilyInO.iterate (n := fun n : ℕ => n) (init := fun _ => 0) + (step := (· + 1)) (encIn := encNat) (encB := encUnary) + (ComputableTidilyInO.of_linear (.of_eq fun _ => rfl)) (ComputableTidilyInO.const 0) + ComputableTidilyInDegree.unary_succ.inO_one (R := fun n => n) (Q := fun n => n) + (B := fun n => n) + (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk) + (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk) + (fun n k hk => by simp only [hiter, encUnary_apply, List.length_replicate]; exact hk) + refine (h.of_enc_eq fun n => by rw [hiter]).mono 8 (fun n => ?_) fun n => ?_ + all_goals + have := Universal.length_encNat_le n + have h₁ : (n + 1) ^ 2 ≤ (n + 1) ^ 3 := Nat.pow_le_pow_right (by omega) (by omega) + have h₂ : n + 1 ≤ (n + 1) ^ 2 := Nat.le_self_pow (by norm_num) _ + have h₃ := Nat.pow_le_pow_left (show (encNat n).length + 1 ≤ n + 1 by omega) 2 + · nlinarith + · omega + +end Turing.MultiTapeTM diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Frame.lean b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Frame.lean index 3c18afd224..62250e7d6e 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Frame.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Encodings/Frame.lean @@ -17,6 +17,11 @@ import Mathlib.Data.List.GetD (`Turing.MultiTapeTM.frame`). Its bits are therefore constants or bits of `w` (`Turing.MultiTapeTM.getElem_frame`), which is what makes framed inputs easy to feed to circuits. +A frame followed by a word, as written on a work tape, splits at each framed bit into the pairs +before it, the pair `true, c` of the bit `c`, and the frame of the rest +(`Turing.MultiTapeTM.frame_append_cons`), so a machine can locate the tag and the bit of each pair +and overwrite the bit in place (`Turing.MultiTapeTM.set_frame_append_cons`). + ## Main results * `Turing.MultiTapeTM.getElem_frame`: the bit at each position of `frame w`. @@ -32,6 +37,14 @@ import Mathlib.Data.List.GetD * `Turing.MultiTapeTM.length_flatMap_frame`: the length of a list of framed words. * `Turing.MultiTapeTM.length_unframe_le`: the word framed at the start of a word is no longer than the word. +* `Turing.MultiTapeTM.frame_append_cons`: a frame split at a framed bit. +* `Turing.MultiTapeTM.getElem?_frame_append_length`, + `Turing.MultiTapeTM.getElem?_frame_append_cons`: the terminator and the tags of a frame followed + by a word. +* `Turing.MultiTapeTM.lt_length_frame_append_cons`, + `Turing.MultiTapeTM.two_mul_length_le_length_frame_append`: positions within a frame followed by + a word. +* `Turing.MultiTapeTM.set_frame_append_cons`: overwriting a framed bit in place. -/ @[expose] public section @@ -203,4 +216,52 @@ theorem length_unframe_le : ∀ w : List Bool, (unframe w).length ≤ w.length omega | [] | [true] | false :: _ => by simp [unframe] +/-! ### Frames followed by a word -/ + +private theorem length_flatMap_pair (w : List Bool) : + (w.flatMap fun b => [true, b]).length = 2 * w.length := by + induction w with + | nil => rfl + | cons b w ih => + simp only [List.flatMap_cons, List.length_append, ih, List.length_cons, List.length_nil] + omega + +/-- A frame split at a symbol. -/ +theorem frame_append_cons (w v : List Bool) (c : Bool) : + frame (w ++ c :: v) = (w.flatMap fun b => [true, b]) ++ true :: c :: frame v := by + simp [frame] + +/-- After the pairs of a frame comes its terminator `false`. -/ +theorem getElem?_frame_append_length (w x : List Bool) : + (frame w ++ x)[2 * w.length]? = some false := by + rw [frame, List.append_assoc, List.getElem?_append_right (by rw [length_flatMap_pair]), + length_flatMap_pair] + simp + +/-- Each pair of a frame starts with the tag `true`. -/ +theorem getElem?_frame_append_cons (w v x : List Bool) (c : Bool) : + (frame (w ++ c :: v) ++ x)[2 * w.length]? = some true := by + rw [frame_append_cons, List.append_assoc, + List.getElem?_append_right (by rw [length_flatMap_pair]), length_flatMap_pair] + simp + +/-- The second cell of a pair of a frame lies within the word. -/ +theorem lt_length_frame_append_cons (w v x : List Bool) (c : Bool) : + 2 * w.length + 1 < (frame (w ++ c :: v) ++ x).length := by + simp only [List.length_append, length_frame, List.length_cons] + omega + +/-- Setting the second cell of a pair of a frame replaces the framed symbol. -/ +theorem set_frame_append_cons (w v x : List Bool) (c b : Bool) : + (frame (w ++ c :: v) ++ x).set (2 * w.length + 1) b = frame (w ++ b :: v) ++ x := by + rw [frame_append_cons, frame_append_cons, List.append_assoc, List.append_assoc, + List.set_append_right _ _ (by rw [length_flatMap_pair]; omega), length_flatMap_pair] + simp + +/-- The pairs of a frame fit in the word. -/ +theorem two_mul_length_le_length_frame_append (w x : List Bool) : + 2 * w.length ≤ (frame w ++ x).length := by + simp only [List.length_append, length_frame] + omega + end Turing.MultiTapeTM diff --git a/Complexity/Computability/Complexity/Classes/Hierarchy/SpaceUniversal.lean b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean similarity index 99% rename from Complexity/Computability/Complexity/Classes/Hierarchy/SpaceUniversal.lean rename to Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean index e13d57c63f..c1d4798aec 100644 --- a/Complexity/Computability/Complexity/Classes/Hierarchy/SpaceUniversal.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean @@ -8,7 +8,8 @@ module -- upstream: candidate public import Complexity.Computability.Machines.Turing.MultiTape.Universal.InPlace -import Complexity.Computability.Complexity.Classes.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO.Constructible +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Quantitative import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Finite /-!