Closure of NP and coNP under polynomial-time reductions

Main results

• mem_NP_preimage — polynomial-time preprocessing preserves membership in NP.
• MapReducesPoly.mem_NP / MapReducesPoly.mem_coNP — membership in NP and coNP transports backward along Karp reductions.
• NPComplete.mem_coNP_iff_NP_eq_coNP — an NP-complete language lies in coNP iff NP = coNP (Arora–Barak, discussion after Definition 2.20).

theorem Complexity.mem_NP_preimage {f : List Bool → List Bool} {L : Language} (hf : f ∈ FP) (hL : L ∈ NP) : f ⁻¹' L ∈ NP

If f is polynomial-time computable and L is in NP, then the preimage language {x | f x ∈ L} is in NP.

theorem Complexity.MapReducesPoly.mem_NP {L₁ L₂ : Language} (hred : L₁ ≤ₚ L₂) (hL₂ : L₂ ∈ NP) : L₁ ∈ NP

NP is closed under polynomial-time many-one reductions. Membership in NP transports backward along a Karp reduction.

theorem Complexity.MapReducesPoly.mem_coNP {L₁ L₂ : Language} (hred : L₁ ≤ₚ L₂) (hL₂ : L₂ ∈ coNP) : L₁ ∈ coNP

coNP is closed under polynomial-time many-one reductions.

theorem Complexity.NPComplete.mem_coNP_iff_NP_eq_coNP {L : Language} (h : NPComplete L) : L ∈ coNP ↔ NP = coNP

An NP-complete language lies in coNP iff NP = coNP (Arora–Barak, discussion after Definition 2.20): once a single NP-complete language has a coNP certificate, every NP language does.