Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.2. Polynomial-Time Verification
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_1_Polynomial_Time import CLRSLean.Chapter_34.Section_34_2_Polynomial_Time_Verification.PairProjection

34.2 Polynomial-Time Verification

CLRS §34.2: the complexity class NP — languages whose membership can be verified in polynomial time given a polynomial-size certificate.

Main results:

  • Definition PolyTimeVerifiable: a language verifiable by a polynomial-time verifier with polynomial-size certificates.

  • Definition ClassNP: the class of polynomially verifiable languages.

  • Theorem PolyTimeVerifiable.of_decidable: every P language is verifiable (the decider is a verifier that ignores the certificate).

  • Theorem ClassP_subset_ClassNP: P ⊆ NP (CLRS Theorem 34.2).

The verifier takes a certificate and an input (encoded as a single string with a separator); the certificate is required to have length bounded by a polynomial in the input length.

namespace CLRSnamespace Chapter34

A language L is polynomially verifiable (L ∈ NP) when there is a polynomial-time computable verifier V : List Γ → List Γ → Bool and a polynomial p such that x ∈ L iff some certificate c of length at most p(|x|) satisfies V c x = true (CLRS §34.2).

def PolyTimeVerifiable {Γ : Type} (L : Language Γ) : Prop := ∃ V : List Γ → List Γ → Bool, ∃ p : Polynomial ℕ, PolyTimeComputable (fun pr : List Γ × List Γ => pairEncoding pr.1 pr.2) boolEncoding (fun pr : List Γ × List Γ => V pr.1 pr.2) ∧ (∀ x : List Γ, x ∈ L ↔ ∃ c : List Γ, c.length ≤ p.eval x.length ∧ V c x = true)

The complexity class NP: polynomially verifiable languages.

def ClassNP (Γ : Type) : Set (Language Γ) := { L | PolyTimeVerifiable (Γ := Γ) L }

A language is in NP iff it is polynomially verifiable.

theorem mem_ClassNP {Γ : Type} (L : Language Γ) : L ∈ ClassNP Γ ↔ PolyTimeVerifiable L := by rfl

Theorem 34.2 (P ⊆ NP). A polynomial-time decidable language is polynomially verifiable: the decider f is a verifier V c x := f x that ignores the certificate, run on the pair-encoded input via the projection machine Turing.Prj.prjComputableInPolyTime.

theorem PolyTimeVerifiable.of_decidable {Γ : Type} [Inhabited Γ] (L : Language Γ) (hL : PolyTimeDecidable L) : PolyTimeVerifiable L := by rcases hL with ⟨f, hf, hf_iff⟩ have hf' := hf rcases hf with ⟨M⟩ letI : Fintype (M.tm.Γ M.tm.k₀) := M.tm.Γk₀Fin letI : Fintype Γ := Fintype.ofEquiv (M.tm.Γ M.tm.k₀) M.inputAlphabet refine ⟨fun c x => f x, 0, ?comp, ?iff⟩ · -- the verifier machine is the projection machine composed with the decider exact PolyTimeComputable.comp ⟨Turing.Prj.prjComputableInPolyTime (Γ := Γ)⟩ hf' · intro x rw [← hf_iff x] constructor · intro hfx exact ⟨[], by simpa using hfx⟩ · rintro ⟨c, hc, hfx⟩ exact hfx

Theorem 34.2: P ⊆ NP (CLRS §34.2).

theorem ClassP_subset_ClassNP {Γ : Type} [Inhabited Γ] : ClassP Γ ⊆ ClassNP Γ := by intro L hL exact (mem_ClassNP L).mpr (PolyTimeVerifiable.of_decidable (L := L) hL)
end Chapter34end CLRS