doc(guide): add the NP-completeness chapter

guide/ComplexityGuide.lean

@@ -5,6 +5,7 @@ Authors: Samuel Schlesinger
 -/
 import VersoManual
 import ComplexityGuide.FirstSteps
+import ComplexityGuide.NPCompleteness
 
 open Verso.Genre Manual
 
@@ -30,8 +31,9 @@ docstring and source. Other entry points:
 * [ROADMAP.md][roadmap] records outstanding work, and [CONTRIBUTING.md][contributing] explains how
   to propose and review changes.
 
-The guide is new. Its chapters are being written area by area, starting with NP-completeness, and
-each chapter's friction points are fixed in the library rather than documented around.
+The guide is new: after first steps, it has a chapter on NP-completeness. Further areas follow
+one at a time, and each chapter's friction points are fixed in the library rather than documented
+around.
 
 [cslib]: https://github.com/leanprover/cslib
 [api]: https://www.cslib.io/complexitylib/
@@ -42,3 +44,5 @@ each chapter's friction points are fixed in the library rather than documented a
 [contributing]: https://github.com/cslib-community/complexitylib/blob/main/CONTRIBUTING.md
 
 {include 1 ComplexityGuide.FirstSteps}
+
+{include 1 ComplexityGuide.NPCompleteness}

guide/ComplexityGuide/FirstSteps.lean

@@ -4,43 +4,37 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Samuel Schlesinger
 -/
 import VersoManual
-import Complexity.Computability.Complexity.CookLevin.Completeness
+import Complexity.Computability.Complexity.Classes.NP
 
 open Verso.Genre Manual
 open Verso.Genre.Manual.InlineLean
 
 set_option pp.rawOnError true
+set_option verso.code.warnLineLength 80
 
 #doc (Manual) "First Steps" =>
 %%%
 tag := "first-steps"
 %%%
 
-The package is named `complexitylib` and its modules begin with `Complexity.`; `import Complexity`
-imports the whole library. Declarations use CSLib's namespaces: most begin with `Cslib`, and
-Turing-machine declarations begin with `Turing`. This chapter imports one module,
-`Complexity.Computability.Complexity.CookLevin.Completeness`, which proves the Cook–Levin theorem.
+The package is named `complexitylib`, and its modules begin with `Complexity.` and mirror CSLib's
+layout. `import Complexity` imports the whole library, which is convenient for exploring but slow
+to load; a development imports the modules it uses. Each module's documentation lists its main
+definitions and results, with references.
 
-A decision problem is a set of instances, together with an encoding of instances as bit strings.
-{name}`Cslib.Complexity.NPComplete` takes both:
+Declarations use CSLib's namespaces. Turing machines, encodings and polynomial-time computability
+live under `Turing`, and complexity classes, problems and reductions under `Cslib.Complexity`.
+For example, this chapter imports `Complexity.Computability.Complexity.Classes.NP`, which defines
+the class {name}`Cslib.Complexity.NP` in terms of
+{name}`Turing.MultiTapeTM.ComputableInPolyTime`:
 
-```lean (name := npComplete)
-#check Cslib.Complexity.NPComplete
+```lean (name := npType)
+#check @Cslib.Complexity.NP
 ```
-```leanOutput npComplete
-Cslib.Complexity.NPComplete {β : Type} (encB : β ↪ List Bool) (B : Set β) : Prop
+```leanOutput npType
+@Cslib.Complexity.NP : {α : Type} → (α ↪ List Bool) → Set (Set α)
 ```
 
-The Cook–Levin theorem states that satisfiability of CNF formulas, under the library's encoding of
-formulas, is NP-complete:
-
-```lean (name := cookLevin)
-open Cslib.Complexity CookLevin in
-#check (SAT_npComplete : NPComplete encCNF SAT)
-```
-```leanOutput cookLevin
-SAT_npComplete : NPComplete encCNF SAT
-```
-
-Hovering over a name shows its type and docstring, and clicking it opens its entry in the API
-documentation.
+To find a declaration, search the
+[API documentation](https://www.cslib.io/complexitylib/search.html). In this guide,
+hovering over a name shows its type and docstring, and clicking it opens its entry there.