From 16321e33ff1e8369df71df3684c86fcdcce89010 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 22:17:11 +0000 Subject: [PATCH] chore(Machines): remove unreferenced tidy declarations (#862) Delete 17 public tidy declarations with no reference in the library, tests, abstracts, guide, docs or scripts: the unused tidy closure rules of ComputableTidilyInPolySpace (the plain ComputableInPolySpace rules cover them), three ComputableTidilyInSpace rules, two ComputableTidilyInDegree list operations, the tidy polynomial-time foldl and encoding transfer, the tidy-space iff bridge and ComputableTidilyInO.isComputable. Lower the tidy surface baseline from 704 to 687 statements. Co-Authored-By: Claude Opus 5.5 --- .../Turing/MultiTape/Complexity/InSpace.lean | 18 ---- .../MultiTape/Complexity/InSpace/Plain.lean | 7 -- .../Turing/MultiTape/Complexity/Lists.lean | 42 +------- .../MultiTape/Complexity/PolySpace.lean | 96 +------------------ .../Turing/MultiTape/Complexity/PolyTime.lean | 61 +----------- .../Turing/MultiTape/Halting/Computable.lean | 8 +- .../Turing/MultiTape/ResourceBounds.lean | 2 +- scripts/tidy_surface_baseline.json | 12 +-- 8 files changed, 16 insertions(+), 230 deletions(-) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean index 2f886f4a8..38e72b2d0 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean @@ -54,10 +54,6 @@ theorem weaken {f : α → β} (h : ComputableTidilyInSpace f encIn encB S) (hS let ⟨T, hT⟩ := h ⟨T, hT.weaken (.refl _) hS⟩ -theorem mono_le {f : α → β} (h : ComputableTidilyInSpace f encIn encB S) - (hS : ∀ a, S a ≤ S₁ a) : ComputableTidilyInSpace f encIn encB S₁ := - h.weaken (.of_le hS) - theorem length_le {f : α → β} (h : ComputableTidilyInSpace f encIn encB S) : (fun a => (encB (f a)).length) ≼ S := let ⟨_, hT⟩ := h @@ -68,12 +64,6 @@ theorem of_enc_eq {f : α → β} {g : α → γ} (h : ComputableTidilyInSpace f let ⟨T, hT⟩ := h ⟨T, hT.of_enc_eq he⟩ -theorem of_encIn_eq {α' : Type} {encIn' : α' ↪ List Bool} {f : α → β} (e : α' → α) - (h : ComputableTidilyInSpace f encIn encB S) (he : ∀ a, encIn' a = encIn (e a)) : - ComputableTidilyInSpace (fun a => f (e a)) encIn' encB fun a => S (e a) := - let ⟨_, hT⟩ := h - ⟨_, hT.of_encIn_eq e he⟩ - theorem comp {f : α → β} {g : β → γ} {S₂ : β → ℕ} (hg : ComputableTidilyInSpace g encB encC S₂) (hf : ComputableTidilyInSpace f encIn encB S₁) : ComputableTidilyInSpace (fun a => g (f a)) encIn encC fun a => S₁ a + S₂ (f a) := @@ -89,14 +79,6 @@ theorem prod {f : α → β} {g : α → γ} (hf : ComputableTidilyInSpace f enc let ⟨_, hg⟩ := hg ⟨_, hf.prod hg⟩ -theorem append {f₁ : α → β} {f₂ : α → γ} {g : α → δ} {encD : δ ↪ List Bool} - (h₁ : ComputableTidilyInSpace f₁ encIn encB S₁) (h₂ : ComputableTidilyInSpace f₂ encIn encC S₂) - (hg : ∀ x, encD (g x) = encB (f₁ x) ++ encC (f₂ x)) : - ComputableTidilyInSpace g encIn encD fun x => S₁ x + S₂ x := - let ⟨_, h₁⟩ := h₁ - let ⟨_, h₂⟩ := h₂ - ⟨_, h₁.append h₂ hg⟩ - theorem ite {c : α → Bool} {f g : α → β} {Sc : α → ℕ} (hc : ComputableTidilyInSpace c encIn encBool Sc) (hf : ComputableTidilyInSpace f encIn encB S₁) (hg : ComputableTidilyInSpace g encIn encB S₂) : diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean index f29fc656f..106d4961b 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean @@ -34,8 +34,6 @@ It also records the equivalence with `Turing.MultiTapeTM.ComputableTidilyInSpace * `Turing.MultiTapeTM.ComputableInSpace.comp`, `.prod`, `.append`, `.ite`: plain closure rules. * `Turing.MultiTapeTM.ComputableInSpace.iterate`, `.foldl`, `.foldlWith`: plain space-bounded loops. -* `Turing.MultiTapeTM.computableInSpace_iff_computableTidilyInSpace`: equivalence with the tidy - counterpart. -/ @[expose] public section @@ -68,11 +66,6 @@ theorem ComputableTidilyInSpace.computableInSpace (h : ComputableTidilyInSpace f ComputableInSpace f encIn encOut S := .of_tidy h -/-- **Plain and tidy computability within a space bound agree.** -/ -theorem computableInSpace_iff_computableTidilyInSpace : - ComputableInSpace f encIn encOut S ↔ ComputableTidilyInSpace f encIn encOut S := - ⟨ComputableInSpace.tidy, ComputableInSpace.of_tidy⟩ - end Bridge namespace ComputableInSpace diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean index dbdc651a3..8957c0af0 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean @@ -17,16 +17,13 @@ import Mathlib.Tactic.Linarith Operations on lists encoded by `Turing.MultiTapeTM.encList`, with explicit degrees (`Turing.MultiTapeTM.ComputableTidilyInDegree`): adding an element at either end and concatenation in linear time; finding the first element that passes a test and keeping the elements that pass a -test, one degree above the test; and dropping a number of elements in quadratic time. The tests may -depend on a parameter. +test, one degree above the test. The tests may depend on a parameter. ## Main results * `Turing.MultiTapeTM.ComputableTidilyInDegree.cons`, `.snoc`, `.listAppend`. * `Turing.MultiTapeTM.ComputableTidilyInDegree.findWith`: the first element passing a test. * `Turing.MultiTapeTM.ComputableTidilyInDegree.filterWith`: the elements passing a test. -* `Turing.MultiTapeTM.ComputableTidilyInDegree.dropUnary`: dropping a number of elements, given - in unary. -/ namespace Turing.MultiTapeTM @@ -182,29 +179,6 @@ public theorem filterWith {t : π × α → Bool} {par : γ → π} {list : γ funext x rw [foldl_filterStep, List.nil_append] -/-- Dropping the first `n` elements, with `n` in unary. -/ -public theorem dropUnary (enc : α ↪ List Bool) : - ComputableTidilyInDegree (fun p : List α × ℕ => p.1.drop p.2) - (encPair (encList enc) encUnary) (encList enc) 2 1 := by - have hrep (l : List α) (n : ℕ) : (List.replicate n true).foldl (fun acc _ => acc.tail) l = - l.drop n := by - simp [List.foldl_const, List.tail_iterate] - have hfold := foldl' (encA := encBool) (encL := encBits) (encB := encList enc) - (list := fun p : List α × ℕ => List.replicate p.2 true) (step := fun acc _ => acc.tail) - ((of_eq (f := fun n => List.replicate n true) (encIn := encUnary) (encMid := encBits) - fun _ => rfl).comp (snd (encList enc) encUnary)) - (fst (encList enc) encUnary) - ((tail (enc₁ := enc)).comp (fst (encList enc) encBool)) - (B := fun p => (encPair (encList enc) encUnary p).length) .self (fun p i hi => by - rw [List.take_replicate, hrep] - have := SizedListEncoding.length_drop_le (encA := enc) (encL := encList enc) p.1 - (min i p.2) - simp only [length_encPair] - omega) - convert hfold.mono (d' := 2) (e' := 1) using 1 - funext p - rw [hrep] - /-- One step of mapping with the parameter `p`. -/ @[expose] public def mapStep {β : Type} (f : π × α → β) (p : π) (acc : List β) (a : α) : List β := @@ -327,20 +301,6 @@ public theorem isSome (enc : α ↪ List Bool) : funext o cases o <;> rfl -/-- The length of a list, in unary. -/ -public theorem length (enc : α ↪ List Bool) : - ComputableTidilyInDegree (fun l : List α => l.length) (encList enc) encUnary 2 1 := by - have hfold := foldl' (encL := encList enc) (encB := encUnary) (list := id) - (init := fun _ => 0) (step := fun n _ => n + 1) (of_eq fun _ => rfl) (const 0) - (unary_succ.comp (fst encUnary enc)) (B := fun l => (encList enc l).length) .self - (fun l i hi => by - have := length_le_length_encList enc l - simp [List.foldl_const] - omega) - convert hfold.mono (d' := 2) (e' := 1) using 1 - funext l - simp [List.foldl_const] - /-- A list of `n` copies of an element. -/ public theorem replicate (enc : α ↪ List Bool) : ComputableTidilyInDegree (fun p : ℕ × α => List.replicate p.1 p.2) (encPair encUnary enc) diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean index 5831e83a4..18557f55f 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean @@ -21,12 +21,9 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Ba `Turing.MultiTapeTM.ComputableTidilyInPolySpace f encIn encOut`: `f` is tidily computable (`Turing.MultiTapeTM.ComputableTidilyInO`) within some time and within space polynomially bounded in the length of the encoded input. Unlike `Turing.MultiTapeTM.ComputableTidilyInPolyTime`, no bound on -the time is imposed, so the notion is closed under iterating a step an exponential number of times, -counted in binary, as long as the states stay of polynomial size -(`Turing.MultiTapeTM.ComputableTidilyInPolySpace.iterate`). It is also closed under composition, -pairing and case distinction, and contains polynomial time; these closure properties are registered -with `fun_prop`. A Boolean function computable within polynomial space decides a problem in `PSPACE` -(`Cslib.Complexity.mem_PSPACE_iff_computableInPolySpace`). +the time is imposed. It contains polynomial time. The closure rules (composition, pairing, case +distinction and binary-counted iteration) are stated for the plain predicate +`Turing.MultiTapeTM.ComputableInPolySpace`. Exhaustive searches within polynomial space enumerate their candidates with the binary counter `Cslib.BitString.increment`, which is computable in linear time @@ -40,8 +37,6 @@ Exhaustive searches within polynomial space enumerate their candidates with the * `Turing.MultiTapeTM.ComputableTidilyInPolySpace.of_polyTime`: polynomial time is within polynomial space. -* `Turing.MultiTapeTM.ComputableTidilyInPolySpace.comp`, `.prod`, `.ite`: closure properties. -* `Turing.MultiTapeTM.ComputableTidilyInPolySpace.iterate`: iteration within polynomial space. * `Turing.MultiTapeTM.ComputableTidilyInDegree.increment`: the binary counter in linear time. -/ @@ -57,8 +52,7 @@ def ComputableTidilyInPolySpace {α β : Type} (f : α → β) (encIn : α ↪ L namespace ComputableTidilyInPolySpace -variable {α β γ δ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} - {encOut : γ ↪ List Bool} {encD : δ ↪ List Bool} +variable {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} /-- **Polynomial time is within polynomial space.** -/ theorem of_polyTime {f : α → β} (h : ComputableTidilyInPolyTime f encIn encMid) : @@ -67,89 +61,9 @@ theorem of_polyTime {f : α → β} (h : ComputableTidilyInPolyTime f encIn encM exact ⟨_, _, PolyBounded.of_forall_le (u := fun a => ((encIn a).length + 1) ^ d) 1 d fun a => by simp, h.inO⟩ -/-- The encoded values have polynomial length. -/ -theorem polyBounded_length {f : α → β} (h : ComputableTidilyInPolySpace f encIn encMid) : - PolyBounded (fun a => (encIn a).length) fun a => (encMid (f a)).length := by - obtain ⟨T, S, hS, h⟩ := h - obtain ⟨c, hc⟩ := h.length_le - exact ((PolyBounded.const c).mul (hS.add (.const 1))).mono hc - -/-- Composition. -/ -theorem comp {f : β → γ} {g : α → β} (hf : ComputableTidilyInPolySpace f encMid encOut) - (hg : ComputableTidilyInPolySpace g encIn encMid) : - ComputableTidilyInPolySpace (fun a => f (g a)) encIn encOut := by - have hlen := hg.polyBounded_length - obtain ⟨Tf, Sf, hSf, hf'⟩ := hf - obtain ⟨Tg, Sg, hSg, hg'⟩ := hg - exact ⟨_, _, hSg.add (hSf.comp hlen), hf'.comp hg'⟩ - -/-- The identity. -/ -theorem id' : ComputableTidilyInPolySpace (fun a : α => a) encIn encIn := - of_polyTime ComputableTidilyInPolyTime.id' - -/-- Pairing. -/ -theorem prod {f : α → β} {g : α → δ} (hf : ComputableTidilyInPolySpace f encIn encMid) - (hg : ComputableTidilyInPolySpace g encIn encD) : - ComputableTidilyInPolySpace (fun a => (f a, g a)) encIn (encPair encMid encD) := by - obtain ⟨Tf, Sf, hSf, hf⟩ := hf - obtain ⟨Tg, Sg, hSg, hg⟩ := hg - exact ⟨_, _, hSf.add hSg, hf.prod hg⟩ - -/-- Case distinction. -/ -theorem ite {c : α → Bool} {f g : α → β} (hc : ComputableTidilyInPolySpace c encIn encBool) - (hf : ComputableTidilyInPolySpace f encIn encMid) - (hg : ComputableTidilyInPolySpace g encIn encMid) : - ComputableTidilyInPolySpace (fun a => if c a then f a else g a) encIn encMid := by - obtain ⟨Tc, Sc, hSc, hc⟩ := hc - obtain ⟨Tf, Sf, hSf, hf⟩ := hf - obtain ⟨Tg, Sg, hSg, hg⟩ := hg - refine ⟨_, _, (hSc.add (hSf.add hSg)).mono fun a => ?_, hc.ite hf hg⟩ - split_ifs <;> lia - -/-- Agreement with a function computable within polynomial space. -/ -theorem congr {f g : α → β} (h : ComputableTidilyInPolySpace f encIn encMid) - (hfg : ∀ a, f a = g a) : ComputableTidilyInPolySpace g encIn encMid := by - rwa [show g = f from funext fun a => (hfg a).symm] - -/-- **Iteration within polynomial space**: iterating a step computable within polynomial space a -number of times computed in polynomial time in binary, from a start computable within polynomial -space, is within polynomial space when all the states along the way have polynomial length. -/ -theorem iterate [Inhabited β] {n : α → ℕ} {init : α → β} {step : β → β} - (hn : ComputableTidilyInPolyTime n encIn encNat) - (hinit : ComputableTidilyInPolySpace init encIn encMid) - (hstep : ComputableTidilyInPolySpace step encMid encMid) {B : α → ℕ} - (hB : PolyBounded (fun a => (encIn a).length) B) - (hstate : ∀ a, ∀ k ≤ n a, (encMid (step^[k] (init a))).length ≤ B a) : - ComputableTidilyInPolySpace (fun a => step^[n a] (init a)) encIn encMid := by - obtain ⟨dn, _, hn'⟩ := hn.exists_degree - obtain ⟨Ti, Si, hSi, hinit⟩ := hinit - obtain ⟨Ts, Ss, hSs, hstep⟩ := hstep - obtain ⟨cs, ds, hSs⟩ := hSs.exists_le - have hit := (ComputableInO.iterate hn'.inO.computableInO hinit.computableInO hstep.computableInO - (R := fun a => (Finset.range (n a + 1)).sup fun k => Ts (step^[k] (init a))) - (Q := fun a => cs * (B a + 1) ^ ds) (B := B) - (fun a k hk => Finset.le_sup (f := fun k => Ts (step^[k] (init a))) - (Finset.mem_range.mpr (Nat.lt_succ_of_le hk))) - (fun a k hk => (hSs _).trans (Nat.mul_le_mul_left cs - (Nat.pow_le_pow_left (Nat.add_le_add_right (hstate a k hk) 1) ds))) - hstate).tidy - refine ⟨_, _, ?_, hit⟩ - have hQ : PolyBounded (fun a => (encIn a).length) fun a => cs * (B a + 1) ^ ds := - PolyBounded.comp (size' := id) (v := fun m => cs * (m + 1) ^ ds) - (PolyBounded.of_forall_le cs ds fun _ => le_rfl) hB - exact ((((PolyBounded.of_forall_le (u := fun a => ((encIn a).length + 1) ^ dn) 1 dn - fun a => by simp).add hSi).add hQ).add hB).add hn.polyBounded_length - /-! ### Automation -/ -attribute [fun_prop] ComputableTidilyInPolySpace of_polyTime id' prod ite - -/-- Composition, in the form used by `fun_prop`. -/ -@[fun_prop] -theorem comp' {f : β → γ} {g : α → β} (hf : ComputableTidilyInPolySpace f encMid encOut) - (hg : ComputableTidilyInPolySpace g encIn encMid) : - ComputableTidilyInPolySpace (fun a => f (g a)) encIn encOut := - hf.comp hg +attribute [fun_prop] ComputableTidilyInPolySpace of_polyTime end ComputableTidilyInPolySpace diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean index c4a458a8f..e86629cae 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean @@ -19,9 +19,8 @@ import Complexity.Computability.Machines.Turing.MultiTape.Combinators.TidyNormal `ComputableTidilyInPolyTime f encIn encOut`: `f` is tidily computable within time and space bounded by a polynomial in the length of the encoded input. The class is closed under composition, -case distinctions and pairing, contains every function tidily computable in linear time and space, -and does not depend on the encodings up to polynomial-time conversions -(`Turing.MultiTapeTM.EncodingEquiv`). +case distinctions and pairing, and contains every function tidily computable in linear time and +space. ## Main definitions @@ -34,10 +33,6 @@ and does not depend on the encodings up to polynomial-time conversions * `Turing.MultiTapeTM.PolyBounded.exists_le`, `.of_forall_le`: recover and supply explicit polynomial bounds for the size adapter over `Cslib.PolynomiallyBounded`. * `Turing.MultiTapeTM.ComputableTidilyInPolyTime.comp`, `.ite`, `.pair`: closure properties. -* `Turing.MultiTapeTM.ComputableTidilyInPolyTime.foldl`: left folds with polynomially bounded - intermediate states. -* `Turing.MultiTapeTM.EncodingEquiv.computableTidilyInPolyTime_iff`: polynomial-time computability - transfers along equivalent encodings. * `Turing.MultiTapeTM.computableTidilyInPolyTime_succ`: the successor in binary. The closure properties are registered with `fun_prop`, so polynomial-time computability of a @@ -228,60 +223,8 @@ public theorem trans (h₁₂ : EncodingEquiv enc₁ enc₂) (h₂₃ : Encoding EncodingEquiv enc₁ enc₃ := ⟨h₂₃.1.comp h₁₂.1, h₁₂.2.comp h₂₃.2⟩ -/-- Polynomial-time computability does not depend on the encodings, up to equivalence. -/ -public theorem computableTidilyInPolyTime_iff {encIn encIn' : α ↪ List Bool} - {encOut encOut' : β ↪ List Bool} (hIn : EncodingEquiv encIn encIn') - (hOut : EncodingEquiv encOut encOut') {f : α → β} : - ComputableTidilyInPolyTime f encIn encOut ↔ ComputableTidilyInPolyTime f encIn' encOut' := - ⟨fun h => (hOut.1.comp h).comp hIn.2, fun h => (hOut.2.comp h).comp hIn.1⟩ - end EncodingEquiv -/-! ### Left folds -/ - -/-- Left folds are tidily computable in polynomial time if the list, the initial value and `step` -are, and the length of the list, the intermediate states and the arguments of `step` are bounded by -a polynomial in the length of the encoded input. -/ -public theorem ComputableTidilyInPolyTime.foldl {γ α β : Type u} {encIn : γ ↪ List Bool} - {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} - {encBA : β × α ↪ List Bool} {encS : List α × β ↪ List Bool} - {encO : Option (List α × β) ↪ List Bool} - [ListEncoding encA encL] [PairEncoding encB encA encBA] [PairEncoding encL encB encS] - [OptionEncoding encS encO] {list : γ → List α} {init : γ → β} {step : β → α → β} - (hlist : ComputableTidilyInPolyTime list encIn encL) - (hinit : ComputableTidilyInPolyTime init encIn encB) - (hstep : ComputableTidilyInPolyTime (fun p : β × α => step p.1 p.2) encBA encB) - {lMax aMax : γ → ℕ} (hlMax' : PolyBounded (fun x => (encIn x).length) lMax) - (haMax' : PolyBounded (fun x => (encIn x).length) aMax) - (hlen : PolyBounded (fun x => (encIn x).length) fun x => (list x).length) - (haMax : ∀ x i (hi : i < (list x).length), - (encBA (((list x).take i).foldl step (init x), (list x)[i])).length ≤ aMax x) - (hlMax : ∀ x, ∀ i ≤ (list x).length, - (encS ((list x).drop i, ((list x).take i).foldl step (init x))).length ≤ lMax x) : - ComputableTidilyInPolyTime (fun x => (list x).foldl step (init x)) encIn encB := by - obtain ⟨t₁, s₁, ht₁, hs₁, h₁⟩ := hlist - obtain ⟨t₂, s₂, ht₂, hs₂, h₂⟩ := hinit - obtain ⟨tS, sS, htS, hsS, hS⟩ := hstep - obtain ⟨ct, dt, htS⟩ := htS.exists_le - obtain ⟨cs, ds, hsS⟩ := hsS.exists_le - have hmax {c d : ℕ} : PolyBounded (fun x => (encIn x).length) fun x => c * (aMax x + 1) ^ d := - PolyBounded.comp (size' := id) (v := fun n => c * (n + 1) ^ d) - (.of_forall_le c d (fun _ => le_rfl)) haMax' - obtain ⟨c, h⟩ := ComputableTidilyInTimeAndSpace.foldl (encA := encA) (encL := encL) - (encBA := encBA) (encS := encS) (encO := encO) - (h₁.mono (t' := fun x => t₁ x + t₂ x) (s' := fun x => s₁ x + s₂ x) - (fun _ => Nat.le_add_right _ _) (fun _ => Nat.le_add_right _ _)) - (h₂.mono (fun _ => Nat.le_add_left _ _) (fun _ => Nat.le_add_left _ _)) hS - (tMax := fun x => ct * (aMax x + 1) ^ dt) (sMax := fun x => cs * (aMax x + 1) ^ ds) - (fun x i hi => (htS _).trans (Nat.mul_le_mul_left ct (Nat.pow_le_pow_left - (Nat.add_le_add_right (haMax x i hi) 1) dt))) - (fun x i hi => (hsS _).trans (Nat.mul_le_mul_left cs (Nat.pow_le_pow_left - (Nat.add_le_add_right (haMax x i hi) 1) ds))) - hlMax - exact ⟨_, _, (PolyBounded.const c).mul ((ht₁.add ht₂).add - ((hlen.add (.const 1)).mul ((hmax.add hlMax').add (.const 1)))), - (PolyBounded.const c).mul ((((hs₁.add hs₂).add hmax).add hlMax').add (.const 1)), h⟩ - /-- The successor is tidily computable in polynomial time, in the binary encoding `encNat`, from the transducer certificate `computableInTimeAndSpace_succ`. -/ @[fun_prop] diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean b/Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean index 79c1f73e7..b27f0850d 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean @@ -29,7 +29,7 @@ into the tidy normal form (`Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_computableTidilyInTimeAndSpace`), whose machines compose. Functions computable within bounds in the senses of `Turing.MultiTapeTM.ComputableInTimeAndSpace`, `Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace`, -`Turing.MultiTapeTM.ComputableTidilyInO`, `Turing.MultiTapeTM.ComputableTidilyInDegree` and +`Turing.MultiTapeTM.ComputableTidilyInDegree` and `Turing.MultiTapeTM.ComputableTidilyInPolyTime` are computable (their `.isComputable` lemmas), and decidable sets are closed under complement. @@ -74,12 +74,6 @@ theorem ComputableTidilyInTimeAndSpace.isComputable {f : α → β} {t s : α (h : ComputableTidilyInTimeAndSpace f encIn encMid t s) : IsComputable f encIn encMid := h.computableInTimeAndSpace.isComputable -/-- Functions tidily computable up to constants are computable. -/ -theorem ComputableTidilyInO.isComputable {f : α → β} {T S : α → ℕ} - (h : ComputableTidilyInO f encIn encMid T S) : IsComputable f encIn encMid := - let ⟨_, h, _⟩ := h - h.isComputable - /-- Functions tidily computable within bounds of given degrees are computable. -/ theorem ComputableTidilyInDegree.isComputable {f : α → β} {d e : ℕ} (h : ComputableTidilyInDegree f encIn encMid d e) : IsComputable f encIn encMid := diff --git a/Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds.lean b/Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds.lean index 3fe3e364b..404834852 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/ResourceBounds.lean @@ -57,7 +57,7 @@ which ask for a machine that also clears its work tapes and rewinds its heads be The plain notions are the ones for definitions and public statements; the tidy notions are proof devices. Each plain notion agrees with its tidy counterpart with the same bounds (`Turing.MultiTapeTM.computableInO_iff_computableTidilyInO`, -`Turing.MultiTapeTM.computableInSpace_iff_computableTidilyInSpace`, +`Turing.MultiTapeTM.ComputableInSpace.tidy` and `Turing.MultiTapeTM.ComputableInSpace.of_tidy`, `Turing.MultiTapeTM.computableInPolySpace_iff_computableTidilyInPolySpace`). ## Main definitions diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index 06f1c636d..3327db327 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -6,11 +6,11 @@ "Complexity/Computability/Machines/Turing/MultiTape/Complexity/BigO/Plain.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Degree.lean": 24, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Fold.lean": 2, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean": 19, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace.lean": 16, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Bit.lean": 1, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 4, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpace/Plain.lean": 3, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/InSpaceLib.lean": 45, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 14, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/Lists.lean": 12, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Radix.lean": 3, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/ConfigurationGraph/Routines.lean": 6, @@ -22,9 +22,9 @@ "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/NondeterministicQueryMachine/Routines.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/QueryMachine.lean": 9, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Reachability.lean": 3, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 12, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolySpace/Plain.lean": 4, - "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean": 19, + "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime.lean": 17, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Basic.lean": 27, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/BitString.lean": 31, "Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Configuration.lean": 18, @@ -52,7 +52,7 @@ "Complexity/Computability/Machines/Turing/MultiTape/Encodings/MultiPass.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Encodings/NatPower.lean": 1, "Complexity/Computability/Machines/Turing/MultiTape/Encodings/StreamFold.lean": 4, - "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 5, + "Complexity/Computability/Machines/Turing/MultiTape/Halting/Computable.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Halting/Rice.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/QueryTake.lean": 2, "Complexity/Computability/Machines/Turing/MultiTape/Universal/Complexity.lean": 6,