Boolean closure of NP

Main results

• Cslib.Complexity.empty_mem_NP, Cslib.Complexity.univ_mem_NP: the trivial problems are in NP.
• Cslib.Complexity.inter_mem_NP, Cslib.Complexity.union_mem_NP, Cslib.Complexity.ite_mem_NP: NP is closed under intersection, union and P-guarded Set.ite.
• Cslib.Complexity.mem_NP_of_guard: the members of a problem in NP passing a polynomial-time test form a problem in NP.
• Cslib.Complexity.inter_mem_coNP, Cslib.Complexity.union_mem_coNP, Cslib.Complexity.ite_mem_coNP: coNP is closed under intersection, union and P-guarded Set.ite.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach

theorem Cslib.Complexity.empty_mem_NP {α : Type} {enc : α ↪ List Bool} : ∅ ∈ NP enc

The empty problem is in NP.

theorem Cslib.Complexity.univ_mem_NP {α : Type} {enc : α ↪ List Bool} : Set.univ ∈ NP enc

The universal problem is in NP.

theorem Cslib.Complexity.inter_mem_NP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ NP enc) (hB : B ∈ NP enc) : A ∩ B ∈ NP enc

NP is closed under intersection.

theorem Cslib.Complexity.union_mem_NP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ NP enc) (hB : B ∈ NP enc) : A ∪ B ∈ NP enc

NP is closed under union.

theorem Cslib.Complexity.mem_NP_of_guard {α : Type} {enc : α ↪ List Bool} {A L : Set α} {c : α → Bool} (hc : Turing.MultiTapeTM.ComputableInPolyTime c enc Turing.MultiTapeTM.encBool) (hA : A ∈ NP enc) (h : ∀ (a : α), a ∈ L ↔ c a = true ∧ a ∈ A) : L ∈ NP enc

Guarded NP membership. The members of a problem in NP that pass a polynomial-time test form a problem in NP.

theorem Cslib.Complexity.inter_mem_coNP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ coNP enc) (hB : B ∈ coNP enc) : A ∩ B ∈ coNP enc

coNP is closed under intersection.

theorem Cslib.Complexity.union_mem_coNP {α : Type} {enc : α ↪ List Bool} {A B : Set α} (hA : A ∈ coNP enc) (hB : B ∈ coNP enc) : A ∪ B ∈ coNP enc

coNP is closed under union.

theorem Cslib.Complexity.ite_mem_NP {α : Type} {enc : α ↪ List Bool} {A B G : Set α} (hG : G ∈ P enc) (hA : A ∈ NP enc) (hB : B ∈ NP enc) : G.ite A B ∈ NP enc

NP is closed under P-guarded Set.ite: G.ite A B = (A ∩ G) ∪ (B ∩ Gᶜ).

theorem Cslib.Complexity.ite_mem_coNP {α : Type} {enc : α ↪ List Bool} {A B G : Set α} (hG : G ∈ P enc) (hA : A ∈ coNP enc) (hB : B ∈ coNP enc) : G.ite A B ∈ coNP enc

coNP is closed under P-guarded Set.ite.