Checking polynomially many conditions

A construction that has to check a condition at every one of polynomially many places runs a loop, and a loop of polynomial length runs in polynomial time. This module states that for the tests of Complexitylib.Classes.P.Unary: quantifying a polynomial-time test over the indices below a polynomial-time number gives a polynomial-time test.

The index is passed to the test as in the loops of Complexitylib.Classes.P.Range: the test reads the loop's input z and the index i from pair z (1^i). A bounded universal statement holds when the test passes at every index, that is, when counting the indices where it passes gives the bound.

Main results

• FPPred.forall_lt — a bounded universal quantifier over a polynomial-time test
• FPPred.exists_lt — a bounded existential quantifier over a polynomial-time test

theorem Complexity.FPPred.forall_lt {n : List Bool → ℕ} {p : List Bool → Prop} (hn : UnaryFn n) (hp : FPPred p) : FPPred fun (z : List Bool) => ∀ i < n z, p (pair z (List.replicate i true))

A bounded universal quantifier over a polynomial-time test is polynomial-time. If n and the test p are polynomial-time, then so is the test that p holds of pair z (1^i) for every i < n z.

theorem Complexity.FPPred.exists_lt {n : List Bool → ℕ} {p : List Bool → Prop} (hn : UnaryFn n) (hp : FPPred p) : FPPred fun (z : List Bool) => ∃ i < n z, p (pair z (List.replicate i true))

A bounded existential quantifier over a polynomial-time test is polynomial-time. If n and the test p are polynomial-time, then so is the test that p holds of pair z (1^i) for some i < n z.