Writing encodings in polynomial time — proof internals

The fold behind Complexitylib.Classes.P.DataEncode. DataEncode writes a list of bits as its entries' encodings between a leading false and a trailing true, and a bit's encoding is 01 for false and 0011 for true. The part between the brackets, encodeBody, is built by a fold that puts one bit's encoding in front of the encoding of the rest, so its state is at most four times as long as the list.

Contents

• bitstringEncode_false, bitstringEncode_true — the encodings of a bit
• encodeBody — the entries' encodings, run together
• bitstringEncode_eq_encodeBody — a list's encoding is its body in brackets
• encodeBody_mem_FP — writing the body is polynomial-time

theorem Complexity.bitstringEncode_false : DataEncode.bitstringEncode false = [false, true]

The encoding of false is 01.

theorem Complexity.bitstringEncode_true : DataEncode.bitstringEncode true = [false, false, true, true]

The encoding of true is 0011.

def Complexity.encodeBody (l : List Bool) : List Bool

The encodings of a list's bits, run together: the encoding of the list without its two brackets.

Equations

• Complexity.encodeBody l = (List.map Complexity.DataEncode.bitstringEncode l).flatten

theorem Complexity.bitstringEncode_eq_encodeBody (l : List Bool) : DataEncode.bitstringEncode l = false :: (encodeBody l ++ [true])

A list's encoding is its body between a leading false and a trailing true.

theorem Complexity.length_encodeBody_le (l : List Bool) : (encodeBody l).length ≤ 4 * l.length

The body is at most four bits per entry.

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

Writing the body is polynomial-time. It is a fold over the list that puts 01 or 0011 in front of the body of the rest.