Small polynomial-time string functions

A few string functions that polynomial-time constructions throughout the library build on: a ruler of polynomial length, an emptiness flag, and dropping the leading bit. Each is one application of the FP closure rules of Complexitylib.Classes.Containments.Internal.FPBridge, which this module re-exports.

Main definitions

• Complexity.polyRuler — a ruler whose length is a polynomial in the input length
• Complexity.emptyFlag — whether a string is empty, as a one-bit flag
• Complexity.dropOne — a string without its leading bit

Main results

• Complexity.polyRulerFn_mem_FP, Complexity.emptyFlagFn_mem_FP, Complexity.dropOneFn_mem_FP — all three are polynomial-time

Rulers of polynomial length

def Complexity.polyRuler (q : Polynomial ℕ) (x : List Bool) : List Bool

A ruler whose length is a polynomial in the input length.

Equations

• Complexity.polyRuler q x = List.replicate (Polynomial.eval x.length q) false

@[simp]

theorem Complexity.polyRuler_length (q : Polynomial ℕ) (x : List Bool) : (polyRuler q x).length = Polynomial.eval x.length q

theorem Complexity.polyRulerFn_mem_FP (q : Polynomial ℕ) {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => polyRuler q (a z)) ∈ FP

Emptiness and the leading bit

def Complexity.emptyFlag (y : List Bool) : List Bool

Is the string empty, as a flag.

Equations

• Complexity.emptyFlag y = Complexity.Cobham.lenLeFlag [] y

@[simp]

theorem Complexity.emptyFlag_nil : emptyFlag [] = [true]

theorem Complexity.emptyFlag_cons (b : Bool) (y : List Bool) : emptyFlag (b :: y) = [false]

theorem Complexity.emptyFlag_pair (a b : List Bool) : emptyFlag (pair a b) = [false]

theorem Complexity.emptyFlagFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => emptyFlag (a z)) ∈ FP

def Complexity.dropOne (y : List Bool) : List Bool

Drop the leading bit.

Equations

• Complexity.dropOne y = List.drop 1 y

theorem Complexity.dropOneFn_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => dropOne (a z)) ∈ FP