2.3. P, Verifiers and NP
A problem is in P when a Boolean function deciding it is computable in polynomial time
(mem_P):
example : {l : List ℕ | 0 ∈ l} ∈ P (encList encNat) :=
⟨fun l => decide (0 ∈ l), ⊢ ComputableInPolyTime (fun l => decide (0 ∈ l)) (encList encNat) encBool All goals completed! 🐙, fun l => l:List ℕ⊢ l ∈ {l | 0 ∈ l} ↔ (fun l => decide (0 ∈ l)) l = true All goals completed! 🐙⟩
NP is defined by verifiers. A verifier V : α × List Bool → Bool reads an instance
together with a certificate. IsVerifier enc p V A says that a ∈ A exactly when some
certificate of length p.eval (enc a).length makes V accept, so certificates are polynomially
long in the encoded instance. A problem is in NP when it has a verifier that is
computable in polynomial time on the encoded pair (mem_NP):
example {α : Type} (enc : α ↪ List Bool) (A : Set α) :
A ∈ NP enc ↔ ∃ (p : Polynomial ℕ) (V : α × List Bool → Bool),
ComputableInPolyTime V (encPair enc encBits) encBool ∧
IsVerifier enc p V A :=
mem_NP
Certificates have exactly the prescribed length. When the natural certificate is shorter, pad it
with false and use IsVerifier.of_padding. Every problem in P is in NP,
with a verifier that ignores its certificate (P_subset_NP), and coNP consists of
the complements of problems in NP.