refactor(problems): give the graph toolkit its own module

Complexity/Computability/Complexity/Problems/Graph.lean

@@ -7,33 +7,56 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Computability.Complexity.Problems.IndependentSet
+public import Complexity.Computability.Complexity.Classes.NP.Witness
+public import Mathlib.Combinatorics.SimpleGraph.Basic
 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
 
 /-!
-# Declared vertices of encoded graphs
+# Graphs given by vertex and edge lists
 
-Shared tools for the graph problems, whose graphs (`Cslib.Complexity.Graph`) are a list of
-declared vertices, possibly with repetitions, and a list of edges.
+The graph problems (`IndependentSet`, `Clique`, `VertexCover`, `KColoring`, the Hamiltonian
+problems, `GraphIsomorphism`, …) take a graph (`Cslib.Complexity.Graph`) as a list of declared
+vertices, possibly with repetitions, and a list of edges, encoded in binary
+(`Cslib.Complexity.encGraph`). Its mathematical reading is a Mathlib simple graph on `ℕ`
+(`Cslib.Complexity.Graph.toSimpleGraph`): two distinct vertices are adjacent when an edge joins
+them in either direction.
 
-* The distinct declared vertices (`Cslib.Complexity.Graph.distinctVertices`) are listed in
-  polynomial time by selecting every first occurrence (`Cslib.Complexity.selectDistinct`).
-* Explicit verifiers with fixed certificate lengths write numbers in unary blocks of a certificate
+This module holds the tools these problems share:
+
+* adjacency is tested in polynomial time (`Cslib.Complexity.Graph.adjBool`);
+* a vertex subset problem with a pairwise condition, such as independent set or clique, is
+  verified by selecting distinct declared vertices with a certificate mask
+  (`Cslib.Complexity.Graph.verifySubset`, an instance of `Cslib.Complexity.subsetVerifier`);
+* the distinct declared vertices (`Cslib.Complexity.Graph.distinctVertices`) are listed in
+  polynomial time by selecting every first occurrence (`Cslib.Complexity.selectDistinct`);
+* explicit verifiers with fixed certificate lengths write numbers in unary blocks of a certificate
   (`Cslib.Complexity.unaryBlocks`): each number, at most `m`, gets its own block of `m` bits, and
   it is read back by counting the set bits of its block (`Cslib.Complexity.countP_unaryBlocks`).
 
 ## Main definitions
 
+* `Cslib.Complexity.Graph`, `Cslib.Complexity.encGraph`, `Cslib.Complexity.Graph.toSimpleGraph`.
+* `Cslib.Complexity.Graph.adjBool`: executable adjacency.
+* `Cslib.Complexity.Graph.verifySubset`: the verifier of a vertex subset problem.
 * `Cslib.Complexity.Graph.distinctVertices`: the declared vertices without repetitions.
 * `Cslib.Complexity.unaryBlocks`: numbers written in unary blocks of a certificate.
 
 ## Main results
 
+* `Cslib.Complexity.Graph.toSimpleGraph_adj`, `Cslib.Complexity.Graph.adjBool_eq_true_iff`:
+  adjacency.
+* `Cslib.Complexity.Graph.isVerifier_verifySubset`,
+  `Cslib.Complexity.Graph.computableTidilyInPolyTime_verifySubset`: the subset verifier is a
+  polynomial-time verifier.
 * `Cslib.Complexity.Graph.length_vertices_le_encGraph`: a graph has no more declared vertices than
   the length of its encoding.
 * `Cslib.Complexity.countP_unaryBlocks`: counting the set bits of a block reads its number.
+
+## References
+
+* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*, Section 2.4][AroraBarak09]
 -/
 
 @[expose] public section
@@ -42,6 +65,138 @@ namespace Cslib.Complexity
 
 open Turing.MultiTapeTM ComputableTidilyInPolyTime
 
+/-- A graph on natural numbers, given by its vertices and its edges. -/
+abbrev Graph : Type := List ℕ × List (ℕ × ℕ)
+
+/-- Graphs encoded by framed lists of binary vertex labels and binary edge pairs. -/
+def encGraph : Graph ↪ List Bool :=
+  encPair (encList encNat) (encList (encPair encNat encNat))
+
+/-- The simple graph of an edge list: two distinct vertices are adjacent when an edge joins them,
+in either direction. -/
+def Graph.toSimpleGraph (G : Graph) : SimpleGraph ℕ := SimpleGraph.fromRel fun u v => (u, v) ∈ G.2
+
+
+/-- Adjacency in the simple graph of an edge list: two distinct vertices joined by an edge in
+either direction. It is not a `simp` lemma, so that the adjacency stays folded until a proof
+unfolds it. -/
+theorem Graph.toSimpleGraph_adj {G : Graph} {u v : ℕ} :
+    G.toSimpleGraph.Adj u v ↔ u ≠ v ∧ ((u, v) ∈ G.2 ∨ (v, u) ∈ G.2) :=
+  SimpleGraph.fromRel_adj _ _ _
+
+namespace Graph
+
+/-! ### Subset verification on encoded graphs -/
+
+/-- Executable adjacency test on an edge list: two distinct vertices are adjacent when an edge
+joins them in either direction. -/
+def adjBool (G : Graph) (u v : ℕ) : Bool :=
+  decide (u ≠ v) &&
+    (G.2.any (fun e => decide (e = (u, v))) || G.2.any (fun e => decide (e = (v, u))))
+
+@[simp]
+theorem adjBool_eq_true_iff (G : Graph) (u v : ℕ) :
+    G.adjBool u v = true ↔ G.toSimpleGraph.Adj u v := by
+  simp [adjBool, toSimpleGraph, SimpleGraph.fromRel_adj]
+
+@[simp]
+theorem adjBool_eq_false_iff (G : Graph) (u v : ℕ) :
+    G.adjBool u v = false ↔ ¬G.toSimpleGraph.Adj u v := by
+  rw [← Bool.not_eq_true, ← adjBool_eq_true_iff, Bool.not_eq_true]
+
+/-- Testing adjacency in an encoded graph is polynomial-time. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_adjBool :
+    ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => p.1.1.adjBool p.1.2 p.2)
+      (encPair (encPair encGraph encNat) encNat) encBool := by
+  unfold adjBool encGraph
+  fun_prop
+
+/-- Select distinct declared vertices from `V` using the certificate mask `w`: position `i` of `V`
+is kept when bit `i` of `w` is `true` and `i` is the first occurrence of that vertex in `V`. This is
+`Cslib.Complexity.selectDistinct` on vertex lists (`selectVertices_eq_selectDistinct`). -/
+def selectVertices (V : List ℕ) (w : List Bool) : List ℕ :=
+  (V.zipIdx.filter fun p => w.getD p.2 false && decide (V.idxOf p.1 = p.2)).map Prod.fst
+
+theorem selectVertices_eq_selectDistinct : selectVertices = selectDistinct := rfl
+
+theorem mem_selectVertices {V : List ℕ} {w : List Bool} {v : ℕ} :
+    v ∈ selectVertices V w ↔ v ∈ V ∧ w.getD (V.idxOf v) false = true :=
+  mem_selectDistinct
+
+theorem nodup_selectVertices (V : List ℕ) (w : List Bool) : (selectVertices V w).Nodup :=
+  nodup_selectDistinct V w
+
+/-- Selecting distinct declared vertices from a certificate mask is polynomial-time. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_selectVertices :
+    ComputableTidilyInPolyTime (fun p : List ℕ × List Bool => selectVertices p.1 p.2)
+      (encPair (encList encNat) encBits) (encList encNat) :=
+  computableTidilyInPolyTime_selectDistinct encNat
+
+/-- Verify a cardinality-`m` vertex subset problem with pairwise relation `rel`: select distinct
+declared vertices from `G.1` by the certificate mask, compare the selected count with `m` in
+binary, and test `rel` on all distinct selected pairs. -/
+def verifySubset (rel : Graph → ℕ → ℕ → Bool) : (Graph × ℕ) × List Bool → Bool :=
+  subsetVerifier (fun x => x.1.1) fun y =>
+    decide (y.2.length = y.1.2) && y.2.all fun u => y.2.all fun v => decide (u = v) || rel y.1.1 u v
+
+/-- A graph has no more declared vertices than the length of its encoded instance. -/
+theorem length_vertices_le (x : Graph × ℕ) :
+    x.1.1.length ≤ (encPair encGraph encNat x).length := by
+  calc x.1.1.length
+      ≤ (encList encNat x.1.1).length := length_le_length_encList encNat x.1.1
+    _ ≤ (encGraph x.1).length := by
+        simp only [encGraph, length_encPair]
+        omega
+    _ ≤ (encPair encGraph encNat x).length := by
+        simp only [length_encPair]
+        omega
+
+/-- `verifySubset` is a polynomial-length verifier for any graph subset problem whose pairwise
+relation agrees with `rel` on distinct vertices. -/
+theorem isVerifier_verifySubset {rel : Graph → ℕ → ℕ → Bool} {P : Graph → ℕ → ℕ → Prop}
+    (hrel : ∀ G u v, u ≠ v → (rel G u v = true ↔ P G u v)) :
+    IsVerifier (encPair encGraph encNat) Polynomial.X (verifySubset rel)
+      {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧ (S : Set ℕ).Pairwise (P x.1) ∧ S.card = x.2} := by
+  refine isVerifier_subsetVerifier (fun x => by simpa using length_vertices_le x)
+    fun x l hl _ => ?_
+  simp only [Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, Bool.or_eq_true,
+    List.toFinset_card_of_nodup hl, List.coe_toFinset]
+  refine ⟨fun ⟨hlen, h⟩ => ⟨fun u hu v hv huv => ?_, hlen⟩,
+    fun ⟨h, hlen⟩ => ⟨hlen, fun u hu v hv => ?_⟩⟩
+  · exact (hrel x.1 u v huv).1 ((h u hu v hv).resolve_left huv)
+  · by_cases huv : u = v
+    · exact Or.inl huv
+    · exact Or.inr ((hrel x.1 u v huv).2 (h hu hv huv))
+
+@[fun_prop]
+private theorem bool_or' {α : Type} {encA : α ↪ List Bool} {left right : α → Bool}
+    (hleft : ComputableTidilyInPolyTime left encA encBool)
+    (hright : ComputableTidilyInPolyTime right encA encBool) :
+    ComputableTidilyInPolyTime (fun a => left a || right a) encA encBool :=
+  bool_or.comp (hleft.prod hright)
+
+/-- `verifySubset` is computable in polynomial time whenever the pairwise test `rel` is. -/
+@[fun_prop]
+theorem computableTidilyInPolyTime_verifySubset {rel : Graph → ℕ → ℕ → Bool}
+    (hrel : ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => rel p.1.1 p.1.2 p.2)
+      (encPair (encPair encGraph encNat) encNat) encBool) :
+    ComputableTidilyInPolyTime (verifySubset rel)
+      (encPair (encPair encGraph encNat) encBits) encBool := by
+  refine computableTidilyInPolyTime_subsetVerifier (encγ := encNat)
+    (by unfold encGraph; fun_prop) (bool_and' ?_ ?_)
+  · exact (unary_to_binary.comp ((length_list encNat).comp (snd _ _))).decide_eq' (by fun_prop)
+  · apply allWithInput (snd _ _)
+    apply allWithInput ((snd _ _).comp (fst _ _))
+    have hproj : ComputableTidilyInPolyTime
+        (fun p : (((Graph × ℕ) × List ℕ) × ℕ) × ℕ => ((p.1.1.1.1, p.1.2), p.2))
+        (encPair (encPair (encPair (encPair encGraph encNat) (encList encNat)) encNat) encNat)
+        (encPair (encPair encGraph encNat) encNat) := by fun_prop
+    exact bool_or' (by fun_prop) (hrel.comp hproj)
+
+end Graph
+
 namespace Graph
 
 /-! ### Declared vertices -/

Complexity/Computability/Complexity/Problems/GraphIsomorphism.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Problems.Graph
+public import Mathlib.Combinatorics.SimpleGraph.Maps
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 

Complexity/Computability/Complexity/Problems/IndependentSet.lean

@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Computability.Complexity.Classes.NP.Witness
+public import Complexity.Computability.Complexity.Problems.Graph
 public import Complexity.Computability.Complexity.Problems.SAT
 public import Complexity.Computability.Complexity.Reduction
 public import Mathlib.Combinatorics.SimpleGraph.Clique
@@ -41,10 +41,7 @@ first-order interpretations.
 
 ## Main definitions
 
-* `Cslib.Complexity.Graph.toSimpleGraph`, `Cslib.Complexity.encGraph`,
-  `Cslib.Complexity.IndependentSet`.
-* `Cslib.Complexity.Graph.adjBool`, `Cslib.Complexity.Graph.selectVertices`,
-  `Cslib.Complexity.Graph.verifySubset`.
+* `Cslib.Complexity.IndependentSet`.
 * `Cslib.Complexity.IndependentSet.verifier`.
 * `Cslib.Complexity.SAT.toIndependentSet`.
 * `Cslib.Complexity.Graph.indepNum`: the independence number.
@@ -76,135 +73,11 @@ namespace Cslib.Complexity
 
 open Cslib.Logic.PL Turing.MultiTapeTM ComputableTidilyInPolyTime
 
-/-- A graph on natural numbers, given by its vertices and its edges. -/
-abbrev Graph : Type := List ℕ × List (ℕ × ℕ)
-
-/-- Graphs encoded by framed lists of binary vertex labels and binary edge pairs. -/
-def encGraph : Graph ↪ List Bool :=
-  encPair (encList encNat) (encList (encPair encNat encNat))
-
-/-- The simple graph of an edge list: two distinct vertices are adjacent when an edge joins them,
-in either direction. -/
-def Graph.toSimpleGraph (G : Graph) : SimpleGraph ℕ := SimpleGraph.fromRel fun u v => (u, v) ∈ G.2
-
 /-- The graphs with an independent set of `m` of their vertices
 [Arora and Barak, Section 2.4][AroraBarak09]. -/
 def IndependentSet : Set (Graph × ℕ) :=
   {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧ x.1.toSimpleGraph.IsNIndepSet x.2 S}
 
-namespace Graph
-
-/-! ### Subset verification on encoded graphs -/
-
-/-- Executable adjacency test on an edge list: two distinct vertices are adjacent when an edge
-joins them in either direction. -/
-def adjBool (G : Graph) (u v : ℕ) : Bool :=
-  decide (u ≠ v) &&
-    (G.2.any (fun e => decide (e = (u, v))) || G.2.any (fun e => decide (e = (v, u))))
-
-@[simp]
-theorem adjBool_eq_true_iff (G : Graph) (u v : ℕ) :
-    G.adjBool u v = true ↔ G.toSimpleGraph.Adj u v := by
-  simp [adjBool, toSimpleGraph, SimpleGraph.fromRel_adj]
-
-@[simp]
-theorem adjBool_eq_false_iff (G : Graph) (u v : ℕ) :
-    G.adjBool u v = false ↔ ¬G.toSimpleGraph.Adj u v := by
-  rw [← Bool.not_eq_true, ← adjBool_eq_true_iff, Bool.not_eq_true]
-
-/-- Testing adjacency in an encoded graph is polynomial-time. -/
-@[fun_prop]
-theorem computableTidilyInPolyTime_adjBool :
-    ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => p.1.1.adjBool p.1.2 p.2)
-      (encPair (encPair encGraph encNat) encNat) encBool := by
-  unfold adjBool encGraph
-  fun_prop
-
-/-- Select distinct declared vertices from `V` using the certificate mask `w`: position `i` of `V`
-is kept when bit `i` of `w` is `true` and `i` is the first occurrence of that vertex in `V`. This is
-`Cslib.Complexity.selectDistinct` on vertex lists (`selectVertices_eq_selectDistinct`). -/
-def selectVertices (V : List ℕ) (w : List Bool) : List ℕ :=
-  (V.zipIdx.filter fun p => w.getD p.2 false && decide (V.idxOf p.1 = p.2)).map Prod.fst
-
-theorem selectVertices_eq_selectDistinct : selectVertices = selectDistinct := rfl
-
-theorem mem_selectVertices {V : List ℕ} {w : List Bool} {v : ℕ} :
-    v ∈ selectVertices V w ↔ v ∈ V ∧ w.getD (V.idxOf v) false = true :=
-  mem_selectDistinct
-
-theorem nodup_selectVertices (V : List ℕ) (w : List Bool) : (selectVertices V w).Nodup :=
-  nodup_selectDistinct V w
-
-/-- Selecting distinct declared vertices from a certificate mask is polynomial-time. -/
-@[fun_prop]
-theorem computableTidilyInPolyTime_selectVertices :
-    ComputableTidilyInPolyTime (fun p : List ℕ × List Bool => selectVertices p.1 p.2)
-      (encPair (encList encNat) encBits) (encList encNat) :=
-  computableTidilyInPolyTime_selectDistinct encNat
-
-/-- Verify a cardinality-`m` vertex subset problem with pairwise relation `rel`: select distinct
-declared vertices from `G.1` by the certificate mask, compare the selected count with `m` in
-binary, and test `rel` on all distinct selected pairs. -/
-def verifySubset (rel : Graph → ℕ → ℕ → Bool) : (Graph × ℕ) × List Bool → Bool :=
-  subsetVerifier (fun x => x.1.1) fun y =>
-    decide (y.2.length = y.1.2) && y.2.all fun u => y.2.all fun v => decide (u = v) || rel y.1.1 u v
-
-/-- A graph has no more declared vertices than the length of its encoded instance. -/
-theorem length_vertices_le (x : Graph × ℕ) :
-    x.1.1.length ≤ (encPair encGraph encNat x).length := by
-  calc x.1.1.length
-      ≤ (encList encNat x.1.1).length := length_le_length_encList encNat x.1.1
-    _ ≤ (encGraph x.1).length := by
-        simp only [encGraph, length_encPair]
-        omega
-    _ ≤ (encPair encGraph encNat x).length := by
-        simp only [length_encPair]
-        omega
-
-/-- `verifySubset` is a polynomial-length verifier for any graph subset problem whose pairwise
-relation agrees with `rel` on distinct vertices. -/
-theorem isVerifier_verifySubset {rel : Graph → ℕ → ℕ → Bool} {P : Graph → ℕ → ℕ → Prop}
-    (hrel : ∀ G u v, u ≠ v → (rel G u v = true ↔ P G u v)) :
-    IsVerifier (encPair encGraph encNat) Polynomial.X (verifySubset rel)
-      {x | ∃ S : Finset ℕ, (∀ v ∈ S, v ∈ x.1.1) ∧ (S : Set ℕ).Pairwise (P x.1) ∧ S.card = x.2} := by
-  refine isVerifier_subsetVerifier (fun x => by simpa using length_vertices_le x)
-    fun x l hl _ => ?_
-  simp only [Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true, Bool.or_eq_true,
-    List.toFinset_card_of_nodup hl, List.coe_toFinset]
-  refine ⟨fun ⟨hlen, h⟩ => ⟨fun u hu v hv huv => ?_, hlen⟩,
-    fun ⟨h, hlen⟩ => ⟨hlen, fun u hu v hv => ?_⟩⟩
-  · exact (hrel x.1 u v huv).1 ((h u hu v hv).resolve_left huv)
-  · by_cases huv : u = v
-    · exact Or.inl huv
-    · exact Or.inr ((hrel x.1 u v huv).2 (h hu hv huv))
-
-@[fun_prop]
-private theorem bool_or' {α : Type} {encA : α ↪ List Bool} {left right : α → Bool}
-    (hleft : ComputableTidilyInPolyTime left encA encBool)
-    (hright : ComputableTidilyInPolyTime right encA encBool) :
-    ComputableTidilyInPolyTime (fun a => left a || right a) encA encBool :=
-  bool_or.comp (hleft.prod hright)
-
-/-- `verifySubset` is computable in polynomial time whenever the pairwise test `rel` is. -/
-@[fun_prop]
-theorem computableTidilyInPolyTime_verifySubset {rel : Graph → ℕ → ℕ → Bool}
-    (hrel : ComputableTidilyInPolyTime (fun p : (Graph × ℕ) × ℕ => rel p.1.1 p.1.2 p.2)
-      (encPair (encPair encGraph encNat) encNat) encBool) :
-    ComputableTidilyInPolyTime (verifySubset rel)
-      (encPair (encPair encGraph encNat) encBits) encBool := by
-  refine computableTidilyInPolyTime_subsetVerifier (encγ := encNat)
-    (by unfold encGraph; fun_prop) (bool_and' ?_ ?_)
-  · exact (unary_to_binary.comp ((length_list encNat).comp (snd _ _))).decide_eq' (by fun_prop)
-  · apply allWithInput (snd _ _)
-    apply allWithInput ((snd _ _).comp (fst _ _))
-    have hproj : ComputableTidilyInPolyTime
-        (fun p : (((Graph × ℕ) × List ℕ) × ℕ) × ℕ => ((p.1.1.1.1, p.1.2), p.2))
-        (encPair (encPair (encPair (encPair encGraph encNat) (encList encNat)) encNat) encNat)
-        (encPair (encPair encGraph encNat) encNat) := by fun_prop
-    exact bool_or' (by fun_prop) (hrel.comp hproj)
-
-end Graph
-
 namespace SAT
 
 /-! ### Karp's reduction -/

Complexity/Computability/Complexity/Problems/VertexCover.lean

@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Computability.Complexity.Problems.Graph
+public import Complexity.Computability.Complexity.Problems.IndependentSet
 public import Mathlib.Combinatorics.SimpleGraph.VertexCover
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List