Documentation

Complexitylib.Classes.Promise

Promise problems and promise complexity classes #

This module exposes disjoint yes/no promise problems, semantic Boolean solvers, side-preserving maps, polynomial-time many-one reductions, complements, and the total embedding of ordinary languages. PromiseClass lifts an ordinary language class by completions, yielding PromiseP, PromiseNP, and PromiseCoNP without assigning semantics outside the promise.

theorem Complexity.PromiseProblem.not_mem_no_of_mem_yes (problem : PromiseProblem) {x : List Bool} (hyes : x ∈ problem.yesInstances) :

x ∉ problem.noInstances

A promised yes-instance cannot also be a promised no-instance.

theorem Complexity.PromiseProblem.not_mem_yes_of_mem_no (problem : PromiseProblem) {x : List Bool} (hno : x ∈ problem.noInstances) :

x ∉ problem.yesInstances

A promised no-instance cannot also be a promised yes-instance.

theorem Complexity.PromiseProblem.mem_promise_iff (problem : PromiseProblem) (x : List Bool) :

x ∈ problem.promise ↔ x ∈ problem.yesInstances ∨ x ∈ problem.noInstances

The promise is exactly the union of the two constrained sides.

@[simp]

theorem Complexity.PromiseProblem.complement_complement (problem : PromiseProblem) :

problem.complement.complement = problem

Complementing a promise problem twice recovers it.

@[simp]

theorem Complexity.PromiseProblem.promise_complement (problem : PromiseProblem) :

problem.complement.promise = problem.promise

Complementing a problem does not change its promised input set.

theorem Complexity.PromiseProblem.solvedBy_complement_iff (problem : PromiseProblem) (decide : List Bool → Bool) :

problem.complement.SolvedBy decide ↔ problem.SolvedBy fun (x : List Bool) => !decide x

Solving the complemented promise is equivalent to complementing the Boolean output of a solver for the original problem.

@[simp]

theorem Complexity.PromiseProblem.promise_ofLanguage (L : Language) :

(ofLanguage L).promise = Set.univ

The ordinary-language embedding promises every input.

theorem Complexity.PromiseProblem.solvedBy_ofLanguage_iff (L : Language) (decide : List Bool → Bool) :

(ofLanguage L).SolvedBy decide ↔ ∀ (x : List Bool), decide x = true ↔ x ∈ L

Solving an embedded ordinary language is exactly deciding it everywhere.

theorem Complexity.PromiseProblem.mapReducesVia_refl (problem : PromiseProblem) :

problem.MapReducesVia problem id

Identity preserves both sides of every promise problem.

theorem Complexity.PromiseProblem.MapReducesVia.trans {first second third : PromiseProblem} {f g : List Bool → List Bool} (hfirst : first.MapReducesVia second f) (hsecond : second.MapReducesVia third g) :

first.MapReducesVia third (g ∘ f)

Side-preserving maps compose.

theorem Complexity.PromiseProblem.mapReducesPoly_refl (problem : PromiseProblem) :

problem.MapReducesPoly problem

Polynomial-time promise reducibility is reflexive.

theorem Complexity.PromiseProblem.MapReducesPoly.trans {first second third : PromiseProblem} (hfirst : first.MapReducesPoly second) (hsecond : second.MapReducesPoly third) :

first.MapReducesPoly third

Polynomial-time promise reductions compose.

theorem Complexity.PromiseProblem.mapReducesVia_ofLanguage_iff (first second : Language) (f : List Bool → List Bool) :

(ofLanguage first).MapReducesVia (ofLanguage second) f ↔ ∀ (x : List Bool), x ∈ first ↔ f x ∈ second

On total embedded languages, preserving both promised sides is equivalent to the usual membership equivalence.

theorem Complexity.PromiseProblem.MapReducesPoly.mem_promiseClass {C : Set Language} {source target : PromiseProblem} (hpreimage : ∀ {f : List Bool → List Bool} {L : Language}, f ∈ FP → L ∈ C → f ⁻¹' L ∈ C) (hred : source.MapReducesPoly target) (htarget : target ∈ PromiseClass C) :

source ∈ PromiseClass C

Promise-class membership transports backward along a polynomial-time side-preserving reduction whenever the underlying language class is closed under polynomial-time preimages.

theorem Complexity.PromiseProblem.MapReducesPoly.mem_PromiseP {source target : PromiseProblem} (hred : source.MapReducesPoly target) (htarget : target ∈ PromiseP) :

source ∈ PromiseP

PromiseP is closed backward under polynomial-time promise reductions.

theorem Complexity.PromiseProblem.MapReducesPoly.mem_PromiseNP {source target : PromiseProblem} (hred : source.MapReducesPoly target) (htarget : target ∈ PromiseNP) :

source ∈ PromiseNP

PromiseNP is closed backward under polynomial-time promise reductions.

theorem Complexity.PromiseProblem.mem_PromiseNP_of_yesInstances_mem_NP (problem : PromiseProblem) (hyes : problem.yesInstances ∈ NP) :

problem ∈ PromiseNP

A promise problem belongs to PromiseNP whenever its yes-instance language itself belongs to NP.

theorem Complexity.PromiseProblem.mem_PromiseNP_of_FNP_witness (problem : PromiseProblem) (hwitness : NP.WitnessNTMConstruction) {R : List Bool → List Bool → Prop} (hR : R ∈ FNP) (hchar : ∀ (x : List Bool), x ∈ problem.yesInstances ↔ ∃ (y : List Bool), R x y) :

problem ∈ PromiseNP

An FNP relation characterizing the promised yes-instances yields PromiseNP membership, conditional only on the generic guess-and-verify NTM construction.

@[simp]

theorem Complexity.PromiseProblem.ofLanguage_mem_promiseClass_iff (C : Set Language) (L : Language) :

ofLanguage L ∈ PromiseClass C ↔ L ∈ C

A total embedded language lies in a lifted promise class exactly when the language lies in the underlying class.

@[simp]

theorem Complexity.PromiseProblem.ofLanguage_mem_PromiseP_iff (L : Language) :

ofLanguage L ∈ PromiseP ↔ L ∈ P

Total-language embedding preserves and reflects P.

@[simp]

theorem Complexity.PromiseProblem.ofLanguage_mem_PromiseNP_iff (L : Language) :

ofLanguage L ∈ PromiseNP ↔ L ∈ NP

Total-language embedding preserves and reflects NP.

@[simp]

theorem Complexity.PromiseProblem.ofLanguage_mem_PromiseCoNP_iff (L : Language) :

ofLanguage L ∈ PromiseCoNP ↔ L ∈ coNP

Total-language embedding preserves and reflects coNP.

theorem Complexity.PromiseProblem.mapReducesPoly_to_ofLanguage {problem : PromiseProblem} {completion : Language} (hyes : problem.yesInstances ⊆ completion) (hno : Disjoint completion problem.noInstances) :

problem.MapReducesPoly (ofLanguage completion)

Every completion induces an identity reduction from the promise problem to the corresponding total embedded language.

@[simp]

theorem Complexity.PromiseProblem.ofLanguage_promiseNPComplete_iff (L : Language) :

PromiseNPComplete (ofLanguage L) ↔ NPComplete L

Embedding a total language is promise-NP-complete exactly when the original language is NP-complete.

theorem Complexity.promiseClass_mono {C D : Set Language} (hsubset : C ⊆ D) :

PromiseClass C ⊆ PromiseClass D

Inclusion of ordinary language classes lifts to their completion-based promise classes.

theorem Complexity.PromiseP_subset_PromiseNP :

PromiseP ⊆ PromiseNP

Deterministic polynomial-time promise problems lie in PromiseNP.

theorem Complexity.promiseHardFor_iff_forall_promiseClass (C : Set Language) (target : PromiseProblem) :

PromiseHardFor C target ↔ ∀ source ∈ PromiseClass C, source.MapReducesPoly target

Hardness against all total languages in C is equivalent to hardness against every problem in the completion-based promise lift of C.

theorem Complexity.promiseNPHard_iff_forall_promiseNP (target : PromiseProblem) :

PromiseNPHard target ↔ ∀ source ∈ PromiseNP, source.MapReducesPoly target

In particular, NP-hardness of a promise target may equivalently quantify over every source problem in PromiseNP.

theorem Complexity.PromiseHardFor.of_reduction {C : Set Language} {first second : PromiseProblem} (hfirst : PromiseHardFor C first) (hred : first.MapReducesPoly second) :

PromiseHardFor C second

Promise hardness transfers forward along a side-preserving polynomial reduction.

theorem Complexity.PromiseP.complement {problem : PromiseProblem} (hproblem : problem ∈ PromiseP) :

problem.complement ∈ PromiseP

PromiseP is closed under swapping its promised yes and no sides.

@[simp]

theorem Complexity.complement_mem_PromiseP_iff (problem : PromiseProblem) :

problem.complement ∈ PromiseP ↔ problem ∈ PromiseP

Complementing a promise problem preserves PromiseP in both directions.

theorem Complexity.promiseP_eq_promiseNP_iff :

PromiseP = PromiseNP ↔ P = NP

The completion-based promise classes collapse exactly when P = NP.

theorem Complexity.PromiseNPHard.P_eq_NP_of_mem_PromiseP {target : PromiseProblem} (hhard : PromiseNPHard target) (hmembership : target ∈ PromiseP) :

If an NP-hard promise target has a deterministic polynomial-time completion, then P = NP.

theorem Complexity.PromiseNPHard.not_mem_PromiseP_of_P_ne_NP {target : PromiseProblem} (hhard : PromiseNPHard target) (hne : P ≠ NP) :

target ∉ PromiseP

Assuming P ≠ NP, no NP-hard promise target can have a deterministic polynomial-time completion.

theorem Complexity.PromiseNPComplete.mem_PromiseP_iff_P_eq_NP {target : PromiseProblem} (hcomplete : PromiseNPComplete target) :

target ∈ PromiseP ↔ P = NP

A promise-NP-complete problem lies in PromiseP exactly if P = NP.