coNP: structural theory and coNP-completeness

This file develops the elementary structural theory of coNP on top of the definition coNP = complClass NP from Complexitylib.Classes.NP:

• P_subset_coNP and P_subset_NP_inter_coNP — deterministic polynomial time sits inside NP ∩ coNP, via closure of P under complement.
• MapReducesPoly.compl — a Karp reduction L₁ ≤ₚ L₂ is simultaneously a reduction L₁ᶜ ≤ₚ L₂ᶜ (the same function witnesses both).
• coNPHard / coNPComplete — hardness and completeness for coNP, dual to NPHard / NPComplete.
• NPHard.compl, NPComplete.compl and their converses — completeness dualizes: L is NP-complete iff Lᶜ is coNP-complete.
• NP_eq_coNP_of_P_eq_NP — if P = NP then NP = coNP; contrapositively (P_ne_NP_of_NP_ne_coNP), separating NP from coNP separates P from NP.

The headline application is SAT.coNPComplete_compl_language (the complement of SAT is coNP-complete), in Complexitylib/SAT/CookLevin/Corollaries.lean.

Complements and membership

@[simp]

theorem Complexity.compl_mem_coNP_iff {L : Language} : Lᶜ ∈ coNP ↔ L ∈ NP

Complementation swaps NP and coNP: Lᶜ ∈ coNP ↔ L ∈ NP. (The companion direction L ∈ coNP ↔ Lᶜ ∈ NP is mem_complClass.)

theorem Complexity.P_subset_coNP : P ⊆ coNP

P is contained in coNP. A language decidable in deterministic polynomial time has its complement decidable in deterministic polynomial time (P_compl), hence in NP.

theorem Complexity.P_subset_NP_inter_coNP : P ⊆ NP ∩ coNP

P is contained in NP ∩ coNP (Arora–Barak, discussion after Definition 2.20). Whether the containment is strict is open.

Reductions dualize

theorem Complexity.MapReducesPoly.compl {L₁ L₂ : Language} (h : L₁ ≤ₚ L₂) : L₁ᶜ ≤ₚ L₂ᶜ

Karp reductions dualize to complements. The same polynomial-time function that reduces L₁ to L₂ also reduces L₁ᶜ to L₂ᶜ, since x ∈ L₁ ↔ f x ∈ L₂ gives x ∉ L₁ ↔ f x ∉ L₂.

coNP-hardness and coNP-completeness

def Complexity.coNPHard (L : Language) : Prop

coNP-hardness. L is coNP-hard when every language in coNP reduces to L in polynomial time.

Equations

• Complexity.coNPHard L = ∀ L' ∈ Complexity.coNP, L' ≤ₚ L

def Complexity.coNPComplete (L : Language) : Prop

coNP-completeness. L is coNP-complete when it is in coNP and coNP-hard.

Equations

• Complexity.coNPComplete L = (L ∈ Complexity.coNP ∧ Complexity.coNPHard L)

theorem Complexity.coNPHard.of_reduction {L₁ L₂ : Language} (h₁ : coNPHard L₁) (h₂ : L₁ ≤ₚ L₂) : coNPHard L₂

coNP-hardness transfers forward along a polynomial-time many-one reduction.

theorem Complexity.coNPComplete.of_mem_of_reduction {L₁ L₂ : Language} (h₁ : coNPHard L₁) (hmem : L₂ ∈ coNP) (h₂ : L₁ ≤ₚ L₂) : coNPComplete L₂

A language in coNP is coNP-complete when a coNP-hard language reduces to it.

theorem Complexity.coNPComplete.transfer {L₁ L₂ : Language} (h₁ : coNPComplete L₁) (hmem : L₂ ∈ coNP) (h₂ : L₁ ≤ₚ L₂) : coNPComplete L₂

coNP-completeness transfers forward along a polynomial-time reduction once membership of the target language in coNP is known.

Completeness dualizes

theorem Complexity.NPHard.compl {L : Language} (h : NPHard L) : coNPHard Lᶜ

The complement of an NP-hard language is coNP-hard: any L' ∈ coNP has L'ᶜ ∈ NP, so L'ᶜ ≤ₚ L, and dualizing gives L' ≤ₚ Lᶜ.

theorem Complexity.coNPHard.compl {L : Language} (h : coNPHard L) : NPHard Lᶜ

The complement of a coNP-hard language is NP-hard.

theorem Complexity.NPComplete.compl {L : Language} (h : NPComplete L) : coNPComplete Lᶜ

The complement of an NP-complete language is coNP-complete (Arora–Barak, Definition 2.20 and the surrounding discussion).

theorem Complexity.coNPComplete.compl {L : Language} (h : coNPComplete L) : NPComplete Lᶜ

The complement of a coNP-complete language is NP-complete.

P = NP collapses NP and coNP

theorem Complexity.NP_eq_coNP_of_P_eq_NP (h : P = NP) : NP = coNP

If P = NP then NP = coNP. Under P = NP the class NP inherits closure under complement from P (P_compl), and a class closed under complement equals its complement class.

theorem Complexity.P_ne_NP_of_NP_ne_coNP (h : NP ≠ coNP) : P ≠ NP

If NP ≠ coNP then P ≠ NP. The standard route to P ≠ NP through the (believed stronger) separation of NP from coNP.