From 7eddd8049af2014986cdb2763e877fb6d63243bc Mon Sep 17 00:00:00 2001 From: copositive Date: Thu, 12 Nov 2026 20:53:44 +0000 Subject: [PATCH] refactor(Complexity/Space): state PSPACE through ComputableInPolySpace, like P and L MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PSPACE enc is now {A | ∃ f, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true}, with mem_PSPACE as Iff.rfl. mem_PSPACE_iff_computableInPolySpace and mem_PSPACE_of_computableInPolySpace duplicated that unfolding and are removed; their callers use anonymous constructors, as P's do. mem_PSPACE_of_computableInTimeAndSpace packages the time/space-bound constructor that Savitch, TQBF membership and mem_PSPACE_iff share. Part of #4737 --- .../Complexity/Classes/Counting/Space.lean | 6 +- .../Complexity/Classes/IP/PSPACE.lean | 2 +- .../Complexity/Classes/LogSpace.lean | 5 +- .../Complexity/Classes/Space.lean | 55 +++++++++++------- .../Complexity/Classes/Space/Closure.lean | 56 ++++++------------- .../Complexity/Classes/Space/Savitch.lean | 4 +- .../Complexity/Classes/Space/TM2.lean | 3 +- .../Classes/Space/TQBF/Membership.lean | 3 +- .../Complexity/Problems/SAT/Space.lean | 9 ++- .../Machines/Turing/TM2/Reverse/Transfer.lean | 1 - CslibFrontierTests/InteractiveProofs.lean | 3 +- CslibFrontierTests/MathlibTM2Reverse.lean | 3 +- CslibFrontierTests/ResourceBoundsPlain.lean | 6 +- 13 files changed, 71 insertions(+), 85 deletions(-) diff --git a/CslibFrontier/Computability/Complexity/Classes/Counting/Space.lean b/CslibFrontier/Computability/Complexity/Classes/Counting/Space.lean index 600d6ef25c..603dbb05e8 100644 --- a/CslibFrontier/Computability/Complexity/Classes/Counting/Space.lean +++ b/CslibFrontier/Computability/Complexity/Classes/Counting/Space.lean @@ -62,7 +62,7 @@ theorem PP_subset_PSPACE : PP enc ⊆ PSPACE enc := by ((ComputableInPolySpace.of_polyTime hpow).prod ((ComputableInPolySpace.of_polyTime hdouble).comp (SharpP.computableInPolySpace hf))) - exact mem_PSPACE_of_computableInPolySpace htest fun a => by simpa using hA a + exact ⟨_, htest, fun a => by simpa using hA a⟩ /-- Testing whether a fixed modulus divides a #P count is in polynomial space. A quotient has at most one more bit than the verifier's certificate length, even for moduli zero and one. -/ @@ -87,9 +87,9 @@ theorem coModP_subset_PSPACE (k : ℕ) : coModP k enc ⊆ PSPACE enc := by (hle.comp ((ComputableInPolySpace.of_polyTime hright).prod hleft))) have hB : {x : α × List Bool | f x.1 = k * ofBits x.2} ∈ PSPACE (encPair enc encBits) := - mem_PSPACE_of_computableInPolySpace htest fun x => by + ⟨_, htest, fun x => by simp only [Set.mem_ofPred_eq, Bool.and_eq_true, decide_eq_true_eq] - exact le_antisymm_iff + exact le_antisymm_iff⟩ have hbound : ComputableInPolyTime (fun a => p.eval (enc a).length + 1) enc encUnary := by fun_prop have h := setOf_exists_mem_PSPACE hB hbound diff --git a/CslibFrontier/Computability/Complexity/Classes/IP/PSPACE.lean b/CslibFrontier/Computability/Complexity/Classes/IP/PSPACE.lean index df8b805b94..3ed537cc8a 100644 --- a/CslibFrontier/Computability/Complexity/Classes/IP/PSPACE.lean +++ b/CslibFrontier/Computability/Complexity/Classes/IP/PSPACE.lean @@ -620,7 +620,7 @@ theorem IP_subset_PSPACE (enc : α ↪ List Bool) : IP enc ⊆ PSPACE enc := by exact (ComputableInPolySpace.of_polyTime hpost).comp ((ComputableInPolySpace.of_polyTime hcap).prod (computableInPolySpace_evaluate M hfuel)) - refine mem_PSPACE_of_computableInPolySpace hdec fun a => ?_ + refine ⟨_, hdec, fun a => ?_⟩ rw [mem_iff_two_pow_lt_value (fun a S oracle s => hreal a S oracle s) hA a, evaluate_eq, decide_eq_true_iff] diff --git a/CslibFrontier/Computability/Complexity/Classes/LogSpace.lean b/CslibFrontier/Computability/Complexity/Classes/LogSpace.lean index ab5a5d1f60..84136483db 100644 --- a/CslibFrontier/Computability/Complexity/Classes/LogSpace.lean +++ b/CslibFrontier/Computability/Complexity/Classes/LogSpace.lean @@ -164,9 +164,8 @@ theorem L_subset_P : L enc ⊆ P enc := by exact ⟨f, hf.computableInPolyTime, hA⟩ /-- **Deterministic logarithmic space is within polynomial space.** -/ -theorem L_subset_PSPACE : L enc ⊆ PSPACE enc := by - rintro A ⟨f, ⟨t, c, hf⟩, hA⟩ - exact ⟨f, ⟨t, _, polyBounded_log (fun a => (enc a).length) c, hf⟩, hA⟩ +theorem L_subset_PSPACE : L enc ⊆ PSPACE enc := + L_subset_P.trans P_subset_PSPACE /-- **Nondeterministic logarithmic space is within nondeterministic polynomial space.** -/ theorem NL_subset_NPSPACE : NL enc ⊆ NPSPACE enc := by diff --git a/CslibFrontier/Computability/Complexity/Classes/Space.lean b/CslibFrontier/Computability/Complexity/Classes/Space.lean index 955a92ea6a..9ae8ebdfbf 100644 --- a/CslibFrontier/Computability/Complexity/Classes/Space.lean +++ b/CslibFrontier/Computability/Complexity/Classes/Space.lean @@ -11,18 +11,23 @@ public import CslibFrontier.Computability.Complexity.Classes.P public import CslibFrontier.Computability.Complexity.Classes.Space.Basic public import CslibFrontier.Computability.Complexity.Reduction public import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.Nondeterministic +public import CslibFrontier.Computability.Machines.Turing.MultiTape.ResourceBounds +import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain import CslibFrontier.Foundations.Data.Nat.PolynomialBound.Exponential /-! # Polynomial space -`Cslib.Complexity.PSPACE enc` consists of the problems decided by one deterministic machine with a -binary alphabet and finitely many states that halts on every encoded instance `enc a` with output -`[true]` or `[false]`, visiting at most `s a` work-tape cells for an `s` polynomially bounded in -the length of `enc a` (upstream `Turing.MultiTapeTM.ComputableInTimeAndSpace`, with no tidiness +`Cslib.Complexity.PSPACE enc` consists of the problems decided by a Boolean function computable +within polynomial space (`Turing.MultiTapeTM.ComputableInPolySpace`), as `Cslib.Complexity.P` and +`Cslib.Complexity.L` use polynomial time and logarithmic space: one deterministic machine with a +binary alphabet and finitely many states halts on every encoded instance `enc a` with output +`[true]` or `[false]`, visiting at most `s (enc a).length` work-tape cells for a polynomially +bounded `s` (upstream `Turing.MultiTapeTM.ComputableInTimeAndSpace`, with no tidiness requirement). No bound on the time is imposed beyond halting. Equivalently -(`Cslib.Complexity.mem_PSPACE_iff`), the problem is decidable within some time bound and such a -space bound in the sense of upstream `Turing.MultiTapeTM.DecidableInTimeAndSpace`. The proposed +(`Cslib.Complexity.mem_PSPACE_iff`), the problem is decidable within some time bound and a space +bound polynomially bounded in the length of `enc a`, in the sense of upstream +`Turing.MultiTapeTM.DecidableInTimeAndSpace`. The proposed upstream complexity classes (cslib pull request #767, open) build `DSPACE` on the same notion of decidability and define `PSPACE` as the union of the classes of space `O(n ^ k)`; their bounds are functions of the input length. For the local encoded-instance classes, @@ -61,6 +66,9 @@ tape write-only [Sipser, Section 8.4 and Definition 8.21][Sipser2013]. ## Main results +* `Cslib.Complexity.mem_PSPACE`: a Boolean decider computable within polynomial space. +* `Cslib.Complexity.mem_PSPACE_of_computableInTimeAndSpace`: a decider within a polynomially + bounded space bound. * `Cslib.Complexity.mem_PSPACE_iff`: `PSPACE` in terms of upstream `DecidableInTimeAndSpace`. * `Cslib.Complexity.mem_PSPACE_iff_exists_mem_DSPACE`: the union of `DSPACE (n ^ k)`. * `Cslib.Complexity.DSPACE_subset_PSPACE`: polynomially bounded space is within `PSPACE`. @@ -84,19 +92,30 @@ open Turing Turing.MultiTapeTM variable {α : Type} {enc : α ↪ List Bool} {A : Set α} /-- The problems decided by one deterministic machine within polynomial space, with respect to -the encoding `enc`: a Boolean function deciding membership is computable (upstream -`Turing.MultiTapeTM.ComputableInTimeAndSpace`) within some time and within space polynomially -bounded in the length of the encoded instance [Sipser, Section 8.2][Sipser2013]. -/ +the encoding `enc`: a Boolean function deciding membership is computable within some time and +within space polynomial in the length of the encoded instance +(`Turing.MultiTapeTM.ComputableInPolySpace`) [Sipser, Section 8.2][Sipser2013]. -/ def PSPACE (enc : α ↪ List Bool) : Set (Set α) := - {A | ∃ f : α → Bool, (∃ t s, PolyBounded (fun a => (enc a).length) s ∧ - ComputableInTimeAndSpace f enc encBool t s) ∧ ∀ a, a ∈ A ↔ f a = true} + {A | ∃ f : α → Bool, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true} + +theorem mem_PSPACE : A ∈ PSPACE enc ↔ + ∃ f : α → Bool, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true := + Iff.rfl + +/-- A Boolean decider computable within some time and within a space bound polynomially bounded +in the length of the encoded instance decides a problem in `PSPACE`. -/ +theorem mem_PSPACE_of_computableInTimeAndSpace {f : α → Bool} {t s : α → ℕ} + (hs : PolyBounded (fun a => (enc a).length) s) + (hf : ComputableInTimeAndSpace f enc encBool t s) (hA : ∀ a, a ∈ A ↔ f a = true) : + A ∈ PSPACE enc := + ⟨f, .of_inSpace hs ⟨t, 1, hf.mono (fun _ => le_rfl) fun _ => by omega, fun _ => by simp⟩, hA⟩ /-- Membership in `PSPACE` is upstream decidability within some time and polynomial space. -/ theorem mem_PSPACE_iff : A ∈ PSPACE enc ↔ ∃ t s, PolyBounded (fun a => (enc a).length) s ∧ DecidableInTimeAndSpace A enc t s := by simp only [decidableInTimeAndSpace_iff] - exact ⟨fun ⟨f, ⟨t, s, hs, hf⟩, hA⟩ => ⟨t, s, hs, f, hf, hA⟩, - fun ⟨t, s, hs, f, hf, hA⟩ => ⟨f, ⟨t, s, hs, hf⟩, hA⟩⟩ + exact ⟨fun ⟨f, ⟨t, _, hs, hf, _⟩, hA⟩ => ⟨t, _, .of_polynomiallyBounded _ hs, f, hf, hA⟩, + fun ⟨_, _, hs, _, hf, hA⟩ => mem_PSPACE_of_computableInTimeAndSpace hs hf hA⟩ /-- A space class of a polynomially bounded bound is within `PSPACE`. -/ theorem DSPACE_subset_PSPACE {α : Type} {enc : α ↪ List Bool} {s : ℕ → ℕ} @@ -125,17 +144,15 @@ def NPSPACE (enc : α ↪ List Bool) : Set (Set α) := (s : α → ℕ), PolyBounded (fun a => (enc a).length) s ∧ ntm.DecidesInSpace enc A s} /-- **Polynomial time is within polynomial space.** -/ -theorem P_subset_PSPACE : P enc ⊆ PSPACE enc := fun A hA => by - obtain ⟨f, hf, hA⟩ := mem_P.mp hA - obtain ⟨t, s, -, hs, hf⟩ := hf - exact ⟨f, ⟨_, _, .of_polynomiallyBounded _ hs, hf⟩, hA⟩ +theorem P_subset_PSPACE : P enc ⊆ PSPACE enc := fun _ ⟨f, hf, hA⟩ => + ⟨f, .of_polyTime hf, hA⟩ /-- **A deterministic polynomial-space machine is a nondeterministic one**, with one computation path (`Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_decidesInSpace`). -/ theorem PSPACE_subset_NPSPACE : PSPACE enc ⊆ NPSPACE enc := by - rintro A ⟨f, ⟨t, s, hs, hf⟩, hA⟩ + rintro A ⟨f, ⟨t, s, hs, hf, -⟩, hA⟩ obtain ⟨k, State, hfinite, ntm, h⟩ := hf.exists_decidesInSpace hA - exact ⟨k, State, hfinite, ntm, s, hs, h⟩ + exact ⟨k, State, hfinite, ntm, _, .of_polynomiallyBounded _ hs, h⟩ /-! ### Hardness and completeness -/ diff --git a/CslibFrontier/Computability/Complexity/Classes/Space/Closure.lean b/CslibFrontier/Computability/Complexity/Classes/Space/Closure.lean index fe1380fb1f..83bca74f25 100644 --- a/CslibFrontier/Computability/Complexity/Classes/Space/Closure.lean +++ b/CslibFrontier/Computability/Complexity/Classes/Space/Closure.lean @@ -24,9 +24,9 @@ import CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.PolySpac # Characterizations and closure properties of `PSPACE` A problem is in `PSPACE` exactly when a Boolean function deciding it is computable within -some time and space polynomial in the length of the encoded instance -(`Cslib.Complexity.mem_PSPACE_iff_computableInO`, -`Cslib.Complexity.mem_PSPACE_iff_computableInPolySpace`). `PSPACE` is closed under +some time and space polynomial in the length of the encoded instance, in the quantitative calculus +of `Turing.MultiTapeTM.ComputableInO` (`Cslib.Complexity.mem_PSPACE_iff_computableInO`). `PSPACE` +is closed under complement, under polynomial-time reductions, and under polynomially bounded existential quantification [Arora and Barak, Chapter 4][AroraBarak09]. The existential quantifier over words `w` of length `ℓ` streams one candidate at a time and @@ -35,8 +35,6 @@ reuses the space of the decider for each (`Turing.MultiTapeTM.ComputableInO.exis ## Main results * `Cslib.Complexity.mem_PSPACE_iff_computableInO`: `PSPACE` in the quantitative calculus. -* `Cslib.Complexity.mem_PSPACE_iff_computableInPolySpace`, - `Cslib.Complexity.mem_PSPACE_of_computableInPolySpace`: `PSPACE` within polynomial space. * `Cslib.Complexity.compl_mem_PSPACE`, `Cslib.Complexity.PSPACE_eq_preimage_compl_PSPACE`, `Cslib.Complexity.inter_mem_PSPACE`, `Cslib.Complexity.union_mem_PSPACE`, `Cslib.Complexity.diff_mem_PSPACE`, @@ -66,37 +64,17 @@ theorem mem_PSPACE_iff_computableInO : A ∈ PSPACE enc ↔ ∃ (f : α → Bool ComputableInO f enc encBool T S ∧ PolyBounded (fun a => (enc a).length) S ∧ ∀ a, a ∈ A ↔ f a = true := by constructor - · rintro ⟨f, ⟨t, s, hs, hf⟩, hA⟩ - exact ⟨f, t, s, ⟨1, hf.mono (fun _ => by omega) fun _ => by omega, fun _ => by simp⟩, hs, hA⟩ - · rintro ⟨f, T, S, ⟨c, hc, -⟩, hS, hA⟩ - exact ⟨f, ⟨_, _, (PolyBounded.const c).mul (hS.add (.const 1)), hc⟩, hA⟩ - -/-- **`PSPACE` within polynomial space**: a problem is in `PSPACE` exactly when a Boolean function -deciding it is computable within space polynomial in the length of the encoded instance -(`Turing.MultiTapeTM.ComputableInPolySpace`). -/ -theorem mem_PSPACE_iff_computableInPolySpace : A ∈ PSPACE enc ↔ - ∃ f : α → Bool, ComputableInPolySpace f enc encBool ∧ ∀ a, a ∈ A ↔ f a = true := by - constructor - · rintro ⟨f, ⟨t, s, hs, hf⟩, hA⟩ - obtain ⟨c, d, hcd⟩ := hs.exists_le - refine ⟨f, ⟨t, fun n => c * (n + 1) ^ d + 1, by fun_prop, - hf.mono (fun _ => le_rfl) fun a => (hcd a).trans (Nat.le_succ _), - fun _ => by simp⟩, hA⟩ · rintro ⟨f, ⟨t, s, hs, hf, -⟩, hA⟩ - exact ⟨f, ⟨t, _, .of_polynomiallyBounded _ hs, hf⟩, hA⟩ - -/-- A Boolean function computable within polynomial space decides a problem in `PSPACE`. -/ -theorem mem_PSPACE_of_computableInPolySpace {f : α → Bool} - (hf : ComputableInPolySpace f enc encBool) (hA : ∀ a, a ∈ A ↔ f a = true) : - A ∈ PSPACE enc := - mem_PSPACE_iff_computableInPolySpace.mpr ⟨f, hf, hA⟩ + exact ⟨f, t, _, ⟨1, hf.mono (fun _ => by omega) fun _ => by omega, fun _ => by simp⟩, + .of_polynomiallyBounded _ hs, hA⟩ + · rintro ⟨f, T, S, ⟨c, hc, hl⟩, hS, hA⟩ + exact ⟨f, .of_inSpace hS ⟨_, c, hc, hl⟩, hA⟩ /-- **`PSPACE` is closed under complement**: negate the answer. -/ theorem compl_mem_PSPACE (hA : A ∈ PSPACE enc) : Aᶜ ∈ PSPACE enc := by - obtain ⟨f, hf, hA⟩ := mem_PSPACE_iff_computableInPolySpace.mp hA - exact mem_PSPACE_of_computableInPolySpace - ((ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_not).comp hf) - fun a => by simp [hA a] + obtain ⟨f, hf, hA⟩ := hA + exact ⟨_, (ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_not).comp hf, + fun a => by simp [hA a]⟩ /-- `PSPACE` equals its preimage under complement. -/ theorem PSPACE_eq_preimage_compl_PSPACE (enc : α ↪ List Bool) : @@ -108,11 +86,10 @@ open scoped symmDiff /-- **`PSPACE` is closed under intersection.** -/ theorem inter_mem_PSPACE {B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSPACE enc) : A ∩ B ∈ PSPACE enc := by - obtain ⟨f, hf, hA⟩ := mem_PSPACE_iff_computableInPolySpace.mp hA - obtain ⟨g, hg, hB⟩ := mem_PSPACE_iff_computableInPolySpace.mp hB - exact mem_PSPACE_of_computableInPolySpace - ((ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_and).comp (hf.prod hg)) - fun a => by simp [hA a, hB a] + obtain ⟨f, hf, hA⟩ := hA + obtain ⟨g, hg, hB⟩ := hB + exact ⟨_, (ComputableInPolySpace.of_polyTime ComputableInPolyTime.bool_and).comp (hf.prod hg), + fun a => by simp [hA a, hB a]⟩ /-- `PSPACE` as a Boolean subalgebra of `Set α`. -/ def PSPACE.booleanSubalgebra (enc : α ↪ List Bool) : BooleanSubalgebra (Set α) := @@ -146,9 +123,8 @@ theorem symmDiff_mem_PSPACE {B : Set α} (hA : A ∈ PSPACE enc) (hB : B ∈ PSP theorem PolyTimeReducible.mem_PSPACE {β : Type} {encB : β ↪ List Bool} {B : Set β} (h : PolyTimeReducible enc encB A B) (hB : B ∈ PSPACE encB) : A ∈ PSPACE enc := by obtain ⟨g, hg, hAB⟩ := h - obtain ⟨f, hf, hB⟩ := mem_PSPACE_iff_computableInPolySpace.mp hB - exact mem_PSPACE_of_computableInPolySpace (hf.comp (.of_polyTime hg)) - fun a => (hAB a).trans (hB (g a)) + obtain ⟨f, hf, hB⟩ := hB + exact ⟨_, hf.comp (.of_polyTime hg), fun a => (hAB a).trans (hB (g a))⟩ /-- **`PSPACE` is closed under polynomially bounded existential quantification.** The candidates are streamed in place by `ComputableInO.exists_bits`, reusing the decider's workspace without a diff --git a/CslibFrontier/Computability/Complexity/Classes/Space/Savitch.lean b/CslibFrontier/Computability/Complexity/Classes/Space/Savitch.lean index c70e49bf9c..3274d0a5c6 100644 --- a/CslibFrontier/Computability/Complexity/Classes/Space/Savitch.lean +++ b/CslibFrontier/Computability/Complexity/Classes/Space/Savitch.lean @@ -54,8 +54,8 @@ theorem mem_PSPACE_of_recognizesInSpace {k : ℕ} {State : Type} [Finite State] A ∈ PSPACE enc := by obtain ⟨c, d, hcd⟩ := hs.exists_le obtain ⟨t, s', hs', hdecide⟩ := ntm.exists_polyBounded_space_savitchDecide enc c d - exact ⟨fun a => ntm.savitchDecide c d (enc a), ⟨t, s', hs', hdecide⟩, - fun a => (hA a).2.trans (MultiTapeNTM.savitchDecide_eq_true_iff (hA a).1 (hcd a)).symm⟩ + exact mem_PSPACE_of_computableInTimeAndSpace hs' hdecide + fun a => (hA a).2.trans (MultiTapeNTM.savitchDecide_eq_true_iff (hA a).1 (hcd a)).symm /-- **Savitch's theorem for polynomial space**: every problem decided by a nondeterministic machine within polynomial space is decided by a deterministic machine within polynomial space, diff --git a/CslibFrontier/Computability/Complexity/Classes/Space/TM2.lean b/CslibFrontier/Computability/Complexity/Classes/Space/TM2.lean index 8bf691ef89..ad17be1590 100644 --- a/CslibFrontier/Computability/Complexity/Classes/Space/TM2.lean +++ b/CslibFrontier/Computability/Complexity/Classes/Space/TM2.lean @@ -55,7 +55,6 @@ theorem mem_PSPACE_of_tm2 {α αΓ βΓ : Type} [Finite αΓ] [Finite βΓ] ha hb hspace hstacks have hbool := ComputableInPolyTime.of_finite (id : Bool → Bool) (encIn := (⟨eb, hb⟩ : Bool ↪ List βΓ).trans (encList (encFinite βΓ))) (encOut := encBool) - exact mem_PSPACE_of_computableInPolySpace ((ComputableInPolySpace.of_polyTime hbool).comp hf) - hA + exact ⟨_, (ComputableInPolySpace.of_polyTime hbool).comp hf, hA⟩ end Cslib.Complexity diff --git a/CslibFrontier/Computability/Complexity/Classes/Space/TQBF/Membership.lean b/CslibFrontier/Computability/Complexity/Classes/Space/TQBF/Membership.lean index 9c63dd0de6..160c24d056 100644 --- a/CslibFrontier/Computability/Complexity/Classes/Space/TQBF/Membership.lean +++ b/CslibFrontier/Computability/Complexity/Classes/Space/TQBF/Membership.lean @@ -412,8 +412,7 @@ open Turing.MultiTapeTM space polynomial in the length of the encoded formula. -/ theorem TQBF_mem_PSPACE : TQBF ∈ PSPACE encQBF := by obtain ⟨e, c, h, -⟩ := TQBF.exists_computableInO_evaluate - refine ⟨TQBF.evaluate, ⟨_, _, ?_, h⟩, - fun φ => TQBF.evaluate_eq_true_iff.symm⟩ + refine mem_PSPACE_of_computableInTimeAndSpace ?_ h fun φ => TQBF.evaluate_eq_true_iff.symm refine PolyBounded.of_forall_le (2 * c) e fun φ => ?_ have := Nat.one_le_pow e ((encQBF φ).length + 1) (by omega) nlinarith diff --git a/CslibFrontier/Computability/Complexity/Problems/SAT/Space.lean b/CslibFrontier/Computability/Complexity/Problems/SAT/Space.lean index ec60352548..72b08fd00d 100644 --- a/CslibFrontier/Computability/Complexity/Problems/SAT/Space.lean +++ b/CslibFrontier/Computability/Complexity/Problems/SAT/Space.lean @@ -142,8 +142,8 @@ end SharpSAT /-- `SAT` lies in `PSPACE encCNF` by deterministic polynomial-space enumeration of all `2 ^ φ.numVars` assignments. -/ theorem SAT.mem_PSPACE_of_enumeration : SAT ∈ PSPACE encCNF := by - refine mem_PSPACE_of_computableInPolySpace (f := fun φ : CNF ℕ => decide (0 < SharpSAT φ)) - ?_ fun φ => by rw [SharpSAT.mem_SAT_iff, decide_eq_true_eq] + refine ⟨fun φ => decide (0 < SharpSAT φ), ?_, fun φ => by + rw [SharpSAT.mem_SAT_iff, decide_eq_true_eq]⟩ have hpos : ComputableInPolyTime (fun n : ℕ => decide (0 < n)) encNat encBool := by fun_prop exact (ComputableInPolySpace.of_polyTime hpos).comp SharpSAT.computableInPolySpace_numVars @@ -154,10 +154,9 @@ theorem UNSAT.mem_PSPACE_of_enumeration : UNSAT ∈ PSPACE encCNF := /-- `USAT` lies in `PSPACE encCNF` by deterministic polynomial-space enumeration and checking `#SAT = 1`. -/ theorem USAT.mem_PSPACE_of_enumeration : USAT ∈ PSPACE encCNF := by - refine mem_PSPACE_of_computableInPolySpace - (f := fun φ : CNF ℕ => decide (0 < SharpSAT φ) && decide (SharpSAT φ < 2)) ?_ fun φ => by + refine ⟨fun φ => decide (0 < SharpSAT φ) && decide (SharpSAT φ < 2), ?_, fun φ => by rw [SharpSAT.mem_USAT_iff, Bool.and_eq_true, decide_eq_true_eq, decide_eq_true_eq] - omega + omega⟩ have heq1 : ComputableInPolyTime (fun n : ℕ => decide (0 < n) && decide (n < 2)) encNat encBool := by fun_prop exact (ComputableInPolySpace.of_polyTime heq1).comp SharpSAT.computableInPolySpace_numVars diff --git a/CslibFrontier/Computability/Machines/Turing/TM2/Reverse/Transfer.lean b/CslibFrontier/Computability/Machines/Turing/TM2/Reverse/Transfer.lean index f9cde3933a..fc33cb27ac 100644 --- a/CslibFrontier/Computability/Machines/Turing/TM2/Reverse/Transfer.lean +++ b/CslibFrontier/Computability/Machines/Turing/TM2/Reverse/Transfer.lean @@ -172,7 +172,6 @@ theorem mem_PSPACE_iff_tm2 {α : Type} {encIn : α ↪ List Bool} {A : Set α} : (∀ stack, Finite (h.tm.Γ stack)) ∧ (∃ space : α → ℕ, PolyBounded (fun a => (encIn a).length) space ∧ h.StacksBounded space) ∧ (∀ a, a ∈ A ↔ f a = true) := by - rw [mem_PSPACE_iff_computableInPolySpace] constructor · rintro ⟨f, hf, hA⟩ obtain ⟨h, hfinite, hspace⟩ := hf.exists_tm2Computable diff --git a/CslibFrontierTests/InteractiveProofs.lean b/CslibFrontierTests/InteractiveProofs.lean index 3a5032041b..8bd50da772 100644 --- a/CslibFrontierTests/InteractiveProofs.lean +++ b/CslibFrontierTests/InteractiveProofs.lean @@ -192,8 +192,7 @@ example : ComputableInPolySpace (fun w => BitString.increment (BitString.increme -- A Boolean function computable within polynomial space decides a problem in `PSPACE`. example : {w : List Bool | w.headD false = true} ∈ PSPACE encBits := - mem_PSPACE_of_computableInPolySpace (f := fun w => w.headD false) - (.of_polyTime (ComputableInPolyTime.headD false)) fun _ => Iff.rfl + ⟨fun w => w.headD false, .of_polyTime (ComputableInPolyTime.headD false), fun _ => Iff.rfl⟩ -- The seven codes of length `3` decode to the seven words of length at most `2`, each once. example : (List.range (Interaction.codeCount 2)).map (fun i => diff --git a/CslibFrontierTests/MathlibTM2Reverse.lean b/CslibFrontierTests/MathlibTM2Reverse.lean index c1d66cb691..bf489f9cf6 100644 --- a/CslibFrontierTests/MathlibTM2Reverse.lean +++ b/CslibFrontierTests/MathlibTM2Reverse.lean @@ -130,7 +130,6 @@ example : ∃ (f : List Bool → Bool) (h : TM2Computable (encList (encFinEnum B h.StacksBounded space) ∧ (∀ xs, xs ∈ {xs : List Bool | xs.isEmpty = true} ↔ f xs = true) := Cslib.Complexity.mem_PSPACE_iff_tm2.mp - (Cslib.Complexity.mem_PSPACE_of_computableInPolySpace - (.of_polyTime (.of_tidy (.listIsEmpty' (encFinEnum Bool)))) (fun _ => Iff.rfl)) + ⟨_, .of_polyTime (.of_tidy (.listIsEmpty' (encFinEnum Bool))), fun _ => Iff.rfl⟩ end CslibFrontierTests.MathlibTM2Reverse diff --git a/CslibFrontierTests/ResourceBoundsPlain.lean b/CslibFrontierTests/ResourceBoundsPlain.lean index 2227166ca7..f3bccb9331 100644 --- a/CslibFrontierTests/ResourceBoundsPlain.lean +++ b/CslibFrontierTests/ResourceBoundsPlain.lean @@ -229,7 +229,7 @@ example (κ : List Bool → ℕ) : single ∈ PSPACE encBits ∧ single ∈ FPT fun _ => by simp⟩ have hfpt : ComputableInFPTTime (fun w : List Bool => decide (w = [true])) encBits encBool κ := ⟨fun _ => c, 0, h.mono (fun _ => by simp) fun _ => Nat.zero_le _⟩ - exact ⟨mem_PSPACE_iff_computableInPolySpace.mpr ⟨_, hf, fun w => by simp [single]⟩, + exact ⟨⟨_, hf, fun w => by simp [single]⟩, mem_FPT_iff_computableInFPTTime.mpr ⟨_, hfpt, fun w => by simp [single]⟩⟩ /-! ### From library certificates to plain ones -/ @@ -250,14 +250,14 @@ example {α : Type} {enc : α ↪ List Bool} {f : α → Logic.PL.QBF ℕ} {a | f a ∈ TQBF} ∈ PSPACE enc ∧ (∃ g, ComputableInFPTTime g encCNF encBool Logic.PL.CNF.numVars ∧ ∀ φ, φ ∈ SAT ↔ g φ = true) := by - obtain ⟨dec, hdec, hA⟩ := mem_PSPACE_iff_computableInPolySpace.mp TQBF_mem_PSPACE + obtain ⟨dec, hdec, hA⟩ := TQBF_mem_PSPACE have hcomp : ComputableInPolySpace (fun a => dec (f a)) enc encBool := by fun_prop obtain ⟨g, hg, hSAT⟩ := mem_FPT_iff_computableInFPTTime.mp SAT_mem_FPT exact ⟨.of_tidy (ComputableTidilyInO.fst encBits encBits), (ComputableTidilyInSpace.fst encBits encBits).computableInSpace, ComputableInPolySpace.of_polyTime (by polytime), ⟨dec, hdec, hA⟩, - mem_PSPACE_iff_computableInPolySpace.mpr ⟨_, hcomp, fun a => hA (f a)⟩, + ⟨_, hcomp, fun a => hA (f a)⟩, ⟨g, hg, hSAT⟩⟩ end CslibFrontierTests.ResourceBoundsPlain