Checking polynomially many conditions

An algorithm that has to verify a condition at every one of polynomially many places is a loop, and a loop of polynomial length is still polynomial time. This module states that as closure of P under quantification over an index bounded by a polynomial-time unary length function.

The proof reuses the bit-by-bit construction: run the condition at each index, collect the verdicts into a string, and compare it against the all-ones string of the same length. The comparison is what turns a list of verdicts into a single one, and it costs nothing beyond the string equality test already in the toolkit.

Main results

• Complexity.forall_unary_mem_P — a bounded conjunction of P conditions
• Complexity.exists_unary_mem_P — a bounded disjunction of P conditions

theorem Complexity.forall_unary_mem_P {L : Language} (hL : L ∈ P) {len : List Bool → ℕ} (hlen : (fun (x : List Bool) => List.replicate (len x) true) ∈ FP) : {x : List Bool | ∀ i < len x, pair x (List.replicate i true) ∈ L} ∈ P

A bounded conjunction of polynomial-time conditions is polynomial time. The index runs over 0, …, len x - 1 and is passed to the condition in unary.

theorem Complexity.exists_unary_mem_P {L : Language} (hL : L ∈ P) {len : List Bool → ℕ} (hlen : (fun (x : List Bool) => List.replicate (len x) true) ∈ FP) : {x : List Bool | ∃ i < len x, pair x (List.replicate i true) ∈ L} ∈ P

A bounded disjunction of polynomial-time conditions is polynomial time.