Polynomial-time numbers and tests

Rules for showing that a function to the natural numbers is polynomial-time (UnaryFn: its value can be written in unary in polynomial time) and that a test is (FPPred: a polynomial-time function outputs its verdict as one bit), stated on numbers and propositions rather than on strings.

The rules cover

• the length of a polynomial-time output, constants, and the two halves of a pair, which is how a loop's body reads the loop's input and index;
• addition, multiplication, truncated subtraction, minimum and maximum;
• comparisons, the Boolean connectives, and case distinction on a test;
• loops over the indices below a polynomial-time bound: a sum, a count, the first index at which a test passes, a maximum, and iterating an update whose values stay below a polynomial-time bound;
• division and remainder, capped powers, binary length and logarithms, which are derived from the loops.

A loop's body reads the loop's input z and the index i from the string pair z (1^i), as in Complexitylib.Classes.P.Range: UnaryFn.lift and FPPred.lift read a rule on z there, and UnaryFn.index reads i. For example, z ↦ |z| / 3 is polynomial-time by (UnaryFn.length id_mem_FP).div (UnaryFn.const 3).

Main results

• UnaryFn.mem_FP, UnaryFn.of_eq, FPPred.of_iff — moving between the rules and FP
• UnaryFn.length, UnaryFn.const, UnaryFn.lift, UnaryFn.index
• UnaryFn.add, UnaryFn.mul, UnaryFn.sub, UnaryFn.min, UnaryFn.max
• FPPred.le, FPPred.lt, FPPred.eq, FPPred.and, FPPred.or, FPPred.not
• FPPred.ite_mem_FP, UnaryFn.ite — case distinction
• UnaryFn.sum, UnaryFn.count, UnaryFn.find, UnaryFn.bmax, UnaryFn.iterate — loops
• UnaryFn.div, UnaryFn.mod, UnaryFn.powMin, UnaryFn.pow_of_le, UnaryFn.size, UnaryFn.log, UnaryFn.clog

Between numbers and strings

theorem Complexity.unaryFn_iff {f : List Bool → ℕ} : UnaryFn f ↔ (fun (z : List Bool) => List.replicate (f z) true) ∈ FP

A polynomial-time number is a polynomial-time function that writes it in unary.

theorem Complexity.UnaryFn.mem_FP {f : List Bool → ℕ} (hf : UnaryFn f) : (fun (z : List Bool) => List.replicate (f z) true) ∈ FP

Writing a polynomial-time number in unary is polynomial-time.

theorem Complexity.UnaryFn.replicate_mem_FP {f : List Bool → ℕ} (hf : UnaryFn f) (bit : Bool) : (fun (z : List Bool) => List.replicate (f z) bit) ∈ FP

A polynomial-time number can be written with any repeated bit.

theorem Complexity.UnaryFn.of_eq {f g : List Bool → ℕ} (hf : UnaryFn f) (h : ∀ (z : List Bool), f z = g z) : UnaryFn g

UnaryFn respects pointwise equality.

theorem Complexity.UnaryFn.comp {f : List Bool → ℕ} {h : List Bool → List Bool} (hf : UnaryFn f) (hh : h ∈ FP) : UnaryFn fun (z : List Bool) => f (h z)

A polynomial-time number of a polynomial-time function of the input is polynomial-time.

theorem Complexity.FPPred.of_flag {v : List Bool → Bool} (hv : (fun (z : List Bool) => [v z]) ∈ FP) : FPPred fun (z : List Bool) => v z = true

A decided test is polynomial-time when its one-bit verdict is.

theorem Complexity.FPPred.flag_mem_FP {p : List Bool → Prop} [DecidablePred p] (hp : FPPred p) : (fun (z : List Bool) => [decide (p z)]) ∈ FP

The one-bit verdict of a polynomial-time test is polynomial-time.

theorem Complexity.FPPred.of_iff {p q : List Bool → Prop} (hp : FPPred p) (h : ∀ (z : List Bool), p z ↔ q z) : FPPred q

FPPred respects pointwise equivalence.

theorem Complexity.FPPred.comp {p : List Bool → Prop} {h : List Bool → List Bool} (hp : FPPred p) (hh : h ∈ FP) : FPPred fun (z : List Bool) => p (h z)

A polynomial-time test of a polynomial-time function of the input is polynomial-time.

Lengths, constants and pairs

theorem Complexity.UnaryFn.length {h : List Bool → List Bool} (hh : h ∈ FP) : UnaryFn fun (z : List Bool) => (h z).length

The length of a polynomial-time output is a polynomial-time number.

theorem Complexity.UnaryFn.const (m : ℕ) : UnaryFn fun (x : List Bool) => m

A constant is a polynomial-time number.

theorem Complexity.FPPred.const (P : Prop) [Decidable P] : FPPred fun (x : List Bool) => P

A constant test is polynomial-time.

theorem Complexity.UnaryFn.lift {f : List Bool → ℕ} (hf : UnaryFn f) : UnaryFn fun (w : List Bool) => f (pairFst w)

A loop's body can read a polynomial-time number of the loop's input z off pair z (1^i).

theorem Complexity.FPPred.lift {p : List Bool → Prop} (hp : FPPred p) : FPPred fun (w : List Bool) => p (pairFst w)

A loop's body can run a polynomial-time test of the loop's input z on pair z (1^i).

theorem Complexity.UnaryFn.index : UnaryFn fun (w : List Bool) => (pairSnd w).length

A loop's body can read the index i off pair z (1^i).

Arithmetic

theorem Complexity.UnaryFn.add {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => f z + g z

Addition is polynomial-time.

theorem Complexity.UnaryFn.mul {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => f z * g z

Multiplication is polynomial-time.

theorem Complexity.UnaryFn.pow_const {f : List Bool → ℕ} (hf : UnaryFn f) (k : ℕ) : UnaryFn fun (z : List Bool) => f z ^ k

Raising a polynomial-time number to a fixed natural exponent is polynomial-time.

theorem Complexity.UnaryFn.sub {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => f z - g z

Truncated subtraction is polynomial-time.

theorem Complexity.UnaryFn.min {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => Min.min (f z) (g z)

The minimum is polynomial-time.

theorem Complexity.UnaryFn.max {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => Max.max (f z) (g z)

The maximum is polynomial-time.

Comparisons and connectives

theorem Complexity.FPPred.le {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : FPPred fun (z : List Bool) => f z ≤ g z

Comparison is polynomial-time.

theorem Complexity.FPPred.lt {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : FPPred fun (z : List Bool) => f z < g z

Strict comparison is polynomial-time.

theorem Complexity.FPPred.and {p q : List Bool → Prop} (hp : FPPred p) (hq : FPPred q) : FPPred fun (z : List Bool) => p z ∧ q z

Conjunction of polynomial-time tests is polynomial-time.

theorem Complexity.FPPred.or {p q : List Bool → Prop} (hp : FPPred p) (hq : FPPred q) : FPPred fun (z : List Bool) => p z ∨ q z

Disjunction of polynomial-time tests is polynomial-time.

theorem Complexity.FPPred.not {p : List Bool → Prop} (hp : FPPred p) : FPPred fun (z : List Bool) => ¬p z

Negation of a polynomial-time test is polynomial-time.

theorem Complexity.FPPred.eq {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : FPPred fun (z : List Bool) => f z = g z

Equality of polynomial-time numbers is polynomial-time.

Case distinction

theorem Complexity.FPPred.ite_mem_FP {p : List Bool → Prop} [DecidablePred p] {x y : List Bool → List Bool} (hp : FPPred p) (hx : x ∈ FP) (hy : y ∈ FP) : (fun (z : List Bool) => if p z then x z else y z) ∈ FP

Case distinction on a polynomial-time test, between polynomial-time strings, is polynomial-time.

theorem Complexity.UnaryFn.ite {f g : List Bool → ℕ} {p : List Bool → Prop} [DecidablePred p] (hp : FPPred p) (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => if p z then f z else g z

Case distinction on a polynomial-time test, between polynomial-time numbers, is polynomial-time.

Loops over a range of indices

theorem Complexity.UnaryFn.sum {f n : List Bool → ℕ} (hn : UnaryFn n) (hf : UnaryFn f) : UnaryFn fun (z : List Bool) => ∑ i ∈ Finset.range (n z), f (pair z (List.replicate i true))

A sum over a range is polynomial-time. If n and the body f are polynomial-time, then so is the sum of f (pair z (1^i)) over i < n z.

theorem Complexity.UnaryFn.count {n : List Bool → ℕ} {p : List Bool → Prop} [DecidablePred p] (hn : UnaryFn n) (hp : FPPred p) : UnaryFn fun (z : List Bool) => {i ∈ Finset.range (n z) | p (pair z (List.replicate i true))}.card

A count over a range is polynomial-time. If n and the test p are polynomial-time, then so is the number of i < n z such that p holds of pair z (1^i).

theorem Complexity.UnaryFn.find {n : List Bool → ℕ} {p : List Bool → Prop} [DecidablePred p] (hn : UnaryFn n) (hp : FPPred p) : UnaryFn fun (z : List Bool) => List.findIdx (fun (i : ℕ) => decide (p (pair z (List.replicate i true)))) (List.range (n z))

A search over a range is polynomial-time. If n and the test p are polynomial-time, then so is the least i < n z such that p holds of pair z (1^i), or n z if there is none.

theorem Complexity.UnaryFn.bmax {f n : List Bool → ℕ} (hn : UnaryFn n) (hf : UnaryFn f) : UnaryFn fun (z : List Bool) => (Finset.range (n z)).sup fun (i : ℕ) => f (pair z (List.replicate i true))

A maximum over a range is polynomial-time. If n and the body f are polynomial-time, then so is the largest value of f (pair z (1^i)) over i < n z, or 0 if n z = 0.

theorem Complexity.UnaryFn.iterate {a k : List Bool → ℕ} {s : List Bool → ℕ → ℕ} {B : List Bool → ℕ} (hs : UnaryFn fun (w : List Bool) => s (pairFst w) (pairSnd w).length) (ha : UnaryFn a) (hk : UnaryFn k) (hB : UnaryFn B) (hbound : ∀ (z : List Bool), ∀ j ≤ k z, (s z)^[j] (a z) ≤ B z) : UnaryFn fun (z : List Bool) => (s z)^[k z] (a z)

A loop on a number is polynomial-time while its values stay below a polynomial-time bound. Starting from a z, the loop applies the update x ↦ s z x k z times; the update reads pair z (1^x), and every value along the way is at most B z.

Division, powers and logarithms

theorem Complexity.UnaryFn.div {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => f z / g z

Division is polynomial-time, with f z / 0 = 0.

theorem Complexity.UnaryFn.mod {f g : List Bool → ℕ} (hf : UnaryFn f) (hg : UnaryFn g) : UnaryFn fun (z : List Bool) => f z % g z

The remainder is polynomial-time, with f z % 0 = f z.

theorem Complexity.UnaryFn.powMin {b c k : List Bool → ℕ} (hb : UnaryFn b) (hk : UnaryFn k) (hc : UnaryFn c) : UnaryFn fun (z : List Bool) => Min.min (b z ^ k z) (c z)

A capped power is polynomial-time: min (b z ^ k z) (c z), when b, k and c are polynomial-time. The cap keeps the value polynomially bounded. (Inside the UnaryFn namespace a bare min means UnaryFn.min, hence Min.min.)

theorem Complexity.UnaryFn.pow_of_le {b c k : List Bool → ℕ} (hb : UnaryFn b) (hk : UnaryFn k) (hc : UnaryFn c) (h : ∀ (z : List Bool), b z ^ k z ≤ c z) : UnaryFn fun (z : List Bool) => b z ^ k z

A power below a polynomial-time bound is polynomial-time.

theorem Complexity.UnaryFn.size {f : List Bool → ℕ} (hf : UnaryFn f) : UnaryFn fun (z : List Bool) => (f z).size

The binary length Nat.size of a polynomial-time number is polynomial-time.

theorem Complexity.UnaryFn.log {f b : List Bool → ℕ} (hb : UnaryFn b) (hf : UnaryFn f) : UnaryFn fun (z : List Bool) => Nat.log (b z) (f z)

The floor logarithm Nat.log of polynomial-time numbers is polynomial-time.

theorem Complexity.UnaryFn.clog {f b : List Bool → ℕ} (hb : UnaryFn b) (hf : UnaryFn f) : UnaryFn fun (z : List Bool) => Nat.clog (b z) (f z)

The ceiling logarithm Nat.clog of polynomial-time numbers is polynomial-time.