The canonical bits of a number

DataEncode writes a natural number as Nat.bits, its little-endian bits with no trailing zero. A fixed-width counter, which is what a polynomial-time machine can produce, carries trailing zeros; dropping them is the missing step between the two.

Dropping trailing zeros is a right fold — what to do with a bit depends on whether everything after it vanished — so recFoldClamp expresses it directly, with no reversal.

Main definitions

• Complexity.stripTrailing — drop trailing zeros

Main results

• Complexity.stripTrailing_eq_bits — the result is Nat.bits of the value
• Complexity.stripTrailing_mem_FP — it is polynomial time

def Complexity.stripTrailing : List Bool → List Bool

Drop trailing zeros from a little-endian bit string.

Equations

• Complexity.stripTrailing [] = []
• Complexity.stripTrailing (false :: t) = if Complexity.stripTrailing t = [] then [] else false :: Complexity.stripTrailing t
• Complexity.stripTrailing (true :: t) = true :: Complexity.stripTrailing t

@[simp]

theorem Complexity.stripTrailing_nil : stripTrailing [] = []

theorem Complexity.stripTrailing_false (t : List Bool) : stripTrailing (false :: t) = if stripTrailing t = [] then [] else false :: stripTrailing t

theorem Complexity.stripTrailing_true (t : List Bool) : stripTrailing (true :: t) = true :: stripTrailing t

theorem Complexity.length_stripTrailing (l : List Bool) : (stripTrailing l).length ≤ l.length

theorem Complexity.stripTrailing_eq_bits (l : List Bool) : stripTrailing l = (binValLE l).bits

Dropping trailing zeros gives the canonical bits.

Polynomial time

def Complexity.stripZero (z : List Bool) : List Bool

The fold step on a zero.

Equations

• Complexity.stripZero z = Complexity.Cobham.selectHead (Complexity.emptyFlag (Complexity.pairSnd (Complexity.pairFst z))) [] (false :: Complexity.pairSnd (Complexity.pairFst z))

def Complexity.stripOne (z : List Bool) : List Bool

The fold step on a one.

Equations

• Complexity.stripOne z = true :: Complexity.pairSnd (Complexity.pairFst z)

theorem Complexity.stripZero_mem_FP : stripZero ∈ FP

theorem Complexity.stripOne_mem_FP : stripOne ∈ FP

theorem Complexity.recFoldClamp_stripTrailing (bound : ℕ) (W l : List Bool) : l.length ≤ bound → Cobham.recFoldClamp stripZero stripOne bound [] W l = stripTrailing l

The fold computes stripTrailing, as long as the clamp allows the answer.

def Complexity.stripFn (z : List Bool) : List Bool

Dropping trailing zeros, on pair anything bits.

Equations

• Complexity.stripFn z = Complexity.Cobham.recFoldClamp Complexity.stripZero Complexity.stripOne z.length [] (Complexity.pairFst z) (Complexity.pairSnd z)

theorem Complexity.stripFn_mem_FP : stripFn ∈ FP

theorem Complexity.stripFn_eq (z : List Bool) : stripFn z = stripTrailing (pairSnd z)