Promise problems -- proof internals

Elementary set, solver, complement, and reduction laws supporting the public promise-problem interface.

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

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

theorem Complexity.PromiseProblem.mem_promise_iff_internal (problem : PromiseProblem) (x : List Bool) : x ∈ problem.promise ↔ x ∈ problem.yesInstances ∨ x ∈ problem.noInstances

theorem Complexity.PromiseProblem.complement_complement_internal (problem : PromiseProblem) : problem.complement.complement = problem

theorem Complexity.PromiseProblem.promise_complement_internal (problem : PromiseProblem) : problem.complement.promise = problem.promise

theorem Complexity.PromiseProblem.solvedBy_complement_iff_internal (problem : PromiseProblem) (decide : List Bool → Bool) : problem.complement.SolvedBy decide ↔ problem.SolvedBy fun (x : List Bool) => !decide x

theorem Complexity.PromiseProblem.promise_ofLanguage_internal (L : Language) : (ofLanguage L).promise = Set.univ

theorem Complexity.PromiseProblem.solvedBy_ofLanguage_iff_internal (L : Language) (decide : List Bool → Bool) : (ofLanguage L).SolvedBy decide ↔ ∀ (x : List Bool), decide x = true ↔ x ∈ L

theorem Complexity.PromiseProblem.mapReducesVia_refl_internal (problem : PromiseProblem) : problem.MapReducesVia problem id

theorem Complexity.PromiseProblem.MapReducesVia.trans_internal {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)

theorem Complexity.PromiseProblem.mapReducesPoly_refl_internal (problem : PromiseProblem) : problem.MapReducesPoly problem

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

theorem Complexity.PromiseProblem.mapReducesVia_ofLanguage_iff_internal (first second : Language) (f : List Bool → List Bool) : (ofLanguage first).MapReducesVia (ofLanguage second) f ↔ ∀ (x : List Bool), x ∈ first ↔ f x ∈ second

theorem Complexity.PromiseProblem.MapReducesPoly.mem_promiseClass_internal {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

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

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

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

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

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

theorem Complexity.ofLanguage_mem_promiseClass_iff_internal (C : Set Language) (L : Language) : PromiseProblem.ofLanguage L ∈ PromiseClass C ↔ L ∈ C

theorem Complexity.PromiseP_subset_PromiseNP_internal : PromiseP ⊆ PromiseNP

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

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

theorem Complexity.promiseHardFor_iff_forall_promiseClass_internal (C : Set Language) (target : PromiseProblem) : PromiseHardFor C target ↔ ∀ source ∈ PromiseClass C, source.MapReducesPoly target

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

theorem Complexity.ofLanguage_promiseNPComplete_iff_internal (L : Language) : PromiseNPComplete (PromiseProblem.ofLanguage L) ↔ NPComplete L

theorem Complexity.PromiseNPHard.P_eq_NP_of_mem_PromiseP_internal {target : PromiseProblem} (hhard : PromiseNPHard target) (hmembership : target ∈ PromiseP) : P = NP

theorem Complexity.promiseP_eq_promiseNP_iff_internal : PromiseP = PromiseNP ↔ P = NP

theorem Complexity.PromiseNPComplete.mem_PromiseP_iff_P_eq_NP_internal {target : PromiseProblem} (hcomplete : PromiseNPComplete target) : target ∈ PromiseP ↔ P = NP