feat: complexity theory

Cslib.lean

@@ -30,6 +30,8 @@ public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
 public import Cslib.Computability.Machines.SingleTapeTuring.Basic
+public import Cslib.Computability.Complexity.Classes
+public import Cslib.Computability.Complexity.Reductions
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs

Cslib/Computability/Complexity/Classes.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Complexity.Classes.Core
+public import Cslib.Computability.Complexity.Classes.Time
+public import Cslib.Computability.Complexity.Classes.Space

Cslib/Computability/Complexity/Classes/Core.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Machines.SingleTapeTuring.Basic
+
+@[expose] public section
+
+/-!
+# Complexity Class Core Definitions
+
+This file contains shared language-level definitions used by both
+time and space complexity classes.
+
+## Main Definitions
+
+* `Decides f L` — `f` decides language `L` (non-empty output means accept)
+* `Verifies verify L p` — `verify` verifies language `L` with polynomial witness bound `p`
+-/
+
+variable {Symbol : Type}
+
+namespace Cslib.Complexity
+
+/--
+A function `f : List Symbol → List Symbol` **decides** a language `L` when
+membership in `L` corresponds to `f` producing non-empty output.
+-/
+def Decides (f : List Symbol → List Symbol) (L : Set (List Symbol)) : Prop :=
+  ∀ x, x ∈ L ↔ f x ≠ []
+
+/--
+A verifier `verify` **verifies** a language `L` with polynomial witness bound `p` when
+membership in `L` is equivalent to the existence of a short witness `w` such that
+`verify (x ++ w)` produces non-empty output.
+-/
+-- TODO: The verifier receives `x ++ w` as a bare concatenation, so it cannot
+-- distinguish the input/witness boundary. A more robust formulation would use
+-- a two-tape machine with a separate read-only witness tape.
+def Verifies (verify : List Symbol → List Symbol) (L : Set (List Symbol))
+    (p : Polynomial ℕ) : Prop :=
+  ∀ x, x ∈ L ↔ ∃ w : List Symbol, w.length ≤ p.eval x.length ∧ verify (x ++ w) ≠ []
+
+end Cslib.Complexity
+
+end

Cslib/Computability/Complexity/Classes/Space.lean

@@ -0,0 +1,133 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Complexity.Classes.Time
+
+@[expose] public section
+
+/-!
+# Space Complexity Classes
+
+This file defines space-bounded computation and the complexity class **PSPACE**.
+
+## Main Definitions
+
+* `OutputsWithinSpace` — TM outputs on input using at most `s` additional work cells
+* `SpaceBoundedComputable f s` — `f` is computable within space `s`
+* `PSPACE` — languages decidable in polynomial space
+
+## Main Results
+
+* `P_subset_PSPACE` — P ⊆ PSPACE
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraB2009]
+-/
+
+open Turing SingleTapeTM Polynomial Relation
+
+variable {Symbol : Type}
+
+namespace Cslib.Complexity
+
+/-- The work space used by a configuration on input `l`: total tape space
+minus the initial input footprint `max 1 l.length`. -/
+def Cfg.work_space_used (tm : SingleTapeTM Symbol) (l : List Symbol) (cfg : tm.Cfg) : ℕ :=
+  SingleTapeTM.Cfg.space_used tm cfg - max 1 l.length
+
+/-- A TM `tm` **outputs** `l'` on input `l` using at most `s` additional work cells
+throughout the computation. This combines the time-based reachability
+with a space bound: every configuration along the computation path
+uses at most `s` work space beyond the initial input footprint. -/
+def OutputsWithinSpace (tm : SingleTapeTM Symbol)
+    (l l' : List Symbol) (s : ℕ) : Prop :=
+  ∃ t : ℕ, tm.OutputsWithinTime l l' t ∧
+    ∀ cfg : tm.Cfg,
+      ReflTransGen tm.TransitionRelation (tm.initCfg l) cfg →
+      Cfg.work_space_used tm l cfg ≤ s
+
+/-- A function `f` is **space-bounded computable** with space bound `s`
+if there exists a TM computing `f` that uses at most `s(|x|)` additional
+work cells on input `x`. -/
+structure SpaceBoundedComputable
+    (f : List Symbol → List Symbol) (s : ℕ → ℕ) where
+  /-- The underlying Turing machine -/
+  tm : SingleTapeTM Symbol
+  /-- Proof that the machine computes `f` within space `s` -/
+  outputsInSpace : ∀ a,
+    OutputsWithinSpace tm a (f a) (s a.length)
+
+/-- **PSPACE** is the class of languages decidable by a Turing machine
+using polynomial work space. -/
+def PSPACE : Set (Set (List Symbol)) :=
+  { L | ∃ f : List Symbol → List Symbol,
+    ∃ p : Polynomial ℕ,
+    Nonempty (SpaceBoundedComputable f (fun n => p.eval n)) ∧
+    Decides f L }
+
+-- TODO: Define L (LOGSPACE) using multi-tape Turing machines with a
+-- read-only input tape. The single-tape model allows overwriting input
+-- cells, giving O(n) writable space instead of O(log n).
+
+/-- Any configuration reachable during a halting computation has its space
+bounded by the initial space plus the halting time. -/
+private lemma space_bounded_of_time_bounded (tm : SingleTapeTM Symbol)
+    (l l' : List Symbol) (t : ℕ)
+    (htime : tm.OutputsWithinTime l l' t)
+    (cfg : tm.Cfg)
+    (hreach : ReflTransGen tm.TransitionRelation (tm.initCfg l) cfg) :
+    Cfg.space_used tm cfg ≤ max 1 l.length + t := by
+  -- Convert ReflTransGen to RelatesInSteps.
+  obtain ⟨m, hm⟩ := ReflTransGen.relatesInSteps hreach
+  -- Extract the halting computation.
+  obtain ⟨t', ht'_le, ht'⟩ := htime
+  -- `haltCfg` has no successors.
+  have hhalt : ∀ cfg', ¬tm.TransitionRelation (tm.haltCfg l') cfg' :=
+    fun cfg' => no_step_from_halt tm _ cfg' rfl
+  -- By determinism, m ≤ t' ≤ t.
+  have hm_le := reachable_steps_le_halting_steps tm ht' hhalt hm
+  -- Space grows by at most 1 per step.
+  have hspace := RelatesInSteps.apply_le_apply_add hm (Cfg.space_used tm)
+    fun a b hstep => Cfg.space_used_step a b (Option.mem_def.mp hstep)
+  rw [Cfg.space_used_initCfg] at hspace
+  omega
+
+/-- Any configuration reachable during a halting computation uses at most `t`
+work cells beyond the initial input footprint. -/
+private lemma work_space_bounded_of_time_bounded (tm : SingleTapeTM Symbol)
+    (l l' : List Symbol) (t : ℕ)
+    (htime : tm.OutputsWithinTime l l' t)
+    (cfg : tm.Cfg)
+    (hreach : ReflTransGen tm.TransitionRelation (tm.initCfg l) cfg) :
+    Cfg.work_space_used tm l cfg ≤ t := by
+  have htotal := space_bounded_of_time_bounded tm l l' t htime cfg hreach
+  apply (Nat.sub_le_iff_le_add).2
+  simpa [Cfg.work_space_used, Nat.add_comm, Nat.add_left_comm,
+    Nat.add_assoc] using htotal
+
+/-- **P ⊆ PSPACE**: every language decidable in polynomial time is also
+decidable in polynomial space.
+
+A TM running in time `t` can use at most `t` additional work cells
+beyond the initial input footprint (at most one new cell per step).
+So a polynomial time bound gives a polynomial work-space bound. -/
+public theorem P_subset_PSPACE :
+    P (Symbol := Symbol) ⊆ PSPACE := by
+  intro L ⟨f, ⟨hf⟩, hDecides⟩
+  refine ⟨f, hf.poly, ⟨{
+    tm := hf.tm
+    outputsInSpace := fun a =>
+      ⟨hf.time_bound a.length, hf.outputsFunInTime a, fun cfg hreach =>
+        le_trans
+          (work_space_bounded_of_time_bounded hf.tm a (f a) (hf.time_bound a.length)
+            (hf.outputsFunInTime a) cfg hreach)
+          (hf.bounds a.length)⟩
+  }⟩, hDecides⟩
+
+end Cslib.Complexity

Cslib/Computability/Complexity/Classes/Time.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Computability.Complexity.Classes.Core
+
+@[expose] public section
+
+/-!
+# Time Complexity Classes
+
+This file defines the fundamental time complexity classes **P**, **NP**, and **coNP**
+using single-tape Turing machines, and states the **P ≠ NP** conjecture.
+
+## Main Definitions
+
+* `P` — the class **P** of languages decidable in polynomial time
+* `NP` — the class **NP** of languages verifiable in polynomial time
+* `CoNP` — the class **coNP**, complements of **NP** languages
+* `PNeNP` — the proposition **P ≠ NP**
+
+## Main Results
+
+* `P_subset_NP` — **P ⊆ NP**
+-/
+
+open Turing SingleTapeTM
+
+variable {Symbol : Type}
+
+namespace Cslib.Complexity
+
+/--
+**P** is the class of languages decidable by a polynomial-time Turing machine.
+
+We use `Nonempty (PolyTimeComputable f)` because `PolyTimeComputable` is a structure
+(carrying computational data), while set membership requires a `Prop`.
+-/
+def P : Set (Set (List Symbol)) :=
+  { L | ∃ f, Nonempty (PolyTimeComputable f) ∧ Decides f L }
+
+/--
+**NP** is the class of languages for which membership can be verified
+in polynomial time given a polynomial-length witness (certificate).
+-/
+def NP : Set (Set (List Symbol)) :=
+  { L | ∃ verify p, Nonempty (PolyTimeComputable verify) ∧ Verifies verify L p }
+
+/--
+**coNP** is the class of languages whose complements are in **NP**.
+-/
+def CoNP : Set (Set (List Symbol)) :=
+  { L | Lᶜ ∈ NP }
+
+/--
+The **P ≠ NP** conjecture states that the complexity classes P and NP are distinct.
+This is stated as a `Prop` definition rather than an axiom.
+-/
+def PNeNP : Prop := P (Symbol := Symbol) ≠ NP
+
+end Cslib.Complexity
+
+end
+
+open Cslib.Complexity
+
+namespace Cslib.Complexity
+
+/--
+**P ⊆ NP**: Every language decidable in polynomial time is also verifiable
+in polynomial time.
+
+*Proof sketch*: Given a polytime decider `f` for `L`, use `f` as a verifier
+that ignores the witness. The witness is taken to be empty (`[]`),
+and the polynomial witness bound is `0`.
+-/
+public theorem P_subset_NP
+    {Symbol : Type} :
+    P (Symbol := Symbol) ⊆ NP := by
+  intro L ⟨f, hf, hDecides⟩
+  refine ⟨f, 0, hf, fun x => ?_⟩
+  simp only [Polynomial.eval_zero]
+  constructor
+  · intro hx
+    exact ⟨[], Nat.le_refl 0, by rwa [List.append_nil, ← hDecides]⟩
+  · rintro ⟨w, hw, hverify⟩
+    rw [hDecides]
+    have : w = [] := List.eq_nil_of_length_eq_zero (Nat.le_zero.mp hw)
+    rwa [this, List.append_nil] at hverify
+
+/-- **NP ⊆ coNP ↔ ∀ L ∈ NP, Lᶜ ∈ NP**. This is just the unfolding of
+the definitions: coNP is defined as `{L | Lᶜ ∈ NP}`, so `NP ⊆ coNP`
+means every NP language has its complement in NP. -/
+public theorem NP_subset_CoNP_iff
+    {Symbol : Type} :
+    NP (Symbol := Symbol) ⊆ CoNP ↔
+    ∀ L ∈ NP (Symbol := Symbol), Lᶜ ∈ NP := by rfl
+
+end Cslib.Complexity