Pairing binary strings

This file defines the low-level self-delimiting pairing codec used by machine inputs throughout Complexitylib. It deliberately has no dependency on the machine or complexity-class layers, so parsers and encoders can reuse it without introducing an import cycle.

def Complexity.pair (x y : List Bool) : List Bool

Encode a pair of binary strings as a single binary string. Each bit of x is doubled (false ↦ [false, false], true ↦ [true, true]), followed by the separator [false, true], followed by y verbatim. This encoding is injective and computable in linear time.

Equations

• Complexity.pair x y = Complexity.delimit x ++ y

theorem Complexity.pair_cons_eq (b : Bool) (x y : List Bool) : pair (b :: x) y = b :: b :: pair x y

One step of the doubling encoder: pair on b :: x prepends the doubled bit b, b.

@[simp]

theorem Complexity.pair_length (x y : List Bool) : (pair x y).length = 2 * x.length + 2 + y.length

|pair x y| = 2·|x| + 2 + |y|. The 2·|x| comes from doubling every bit of x; the +2 is the separator [false, true].

theorem Complexity.pair_inj {x₁ x₂ y₁ y₂ : List Bool} (h : pair x₁ y₁ = pair x₂ y₂) : x₁ = x₂ ∧ y₁ = y₂

pair is injective: if pair x₁ y₁ = pair x₂ y₂ then x₁ = x₂ and y₁ = y₂.

@[simp]

theorem Complexity.unpair?_pair (x y : List Bool) : unpair? (pair x y) = some (x, y)

unpair? is a left inverse of pair: decoding an encoded pair recovers exactly its two components.

theorem Complexity.eq_pair_of_unpair?_eq_some {z x y : List Bool} (h : unpair? z = some (x, y)) : z = pair x y

Soundness of the decoder: if unpair? succeeds on z, producing (x, y), then z was exactly the encoding pair x y.

theorem Complexity.unpair?_eq_some_iff {z x y : List Bool} : unpair? z = some (x, y) ↔ z = pair x y

unpair? z returns some (x, y) if and only if z = pair x y, characterizing exactly which strings are valid pair encodings.

theorem Complexity.pair_getElem_left_first (x y : List Bool) (i : ℕ) (hi : i < x.length) : (pair x y)[2 * i] = x[i]

In pair x y, the first duplicated copy of x[i] sits at position 2*i.

theorem Complexity.pair_getElem_left_second (x y : List Bool) (i : ℕ) (hi : i < x.length) : (pair x y)[2 * i + 1] = x[i]

In pair x y, the second duplicated copy of x[i] sits at position 2*i+1.

theorem Complexity.pair_getElem_sep_zero (x y : List Bool) : (pair x y)[2 * x.length] = false

The first separator bit in pair x y is false.

theorem Complexity.pair_getElem_sep_one (x y : List Bool) : (pair x y)[2 * x.length + 1] = true

The second separator bit in pair x y is true.

theorem Complexity.pair_getElem_right (x y : List Bool) (j : ℕ) (hj : j < y.length) : (pair x y)[2 * x.length + 2 + j] = y[j]

In pair x y, the suffix after the separator is exactly y.

The projections

Total decoders for the two components. pairFst is defined by scanning rather than through unpair? so that a single-pass machine can compute it; only the behaviour of either projection on canonical pairs is ever used.

def Complexity.pairFst : List Bool → List Bool

The first component of a canonical pair: read doubled bits until the [false, true] separator. On pair x y this returns x (see pairFst_pair); on malformed input it returns the bits decoded so far.

Equations

• Complexity.pairFst (false :: false :: z) = false :: Complexity.pairFst z
• Complexity.pairFst (true :: true :: z) = true :: Complexity.pairFst z
• Complexity.pairFst x✝ = []

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

The second component of a canonical pair: the suffix after the leading self-delimiting block, or [] if the input is not a valid pair.

Equations

• Complexity.pairSnd z = match Complexity.unpair? z with | some (fst, s) => s | none => []

@[simp]

theorem Complexity.pairFst_pair (x y : List Bool) : pairFst (pair x y) = x

@[simp]

theorem Complexity.pairSnd_pair (x y : List Bool) : pairSnd (pair x y) = y

theorem Complexity.pairSnd_eq_unpair? (z : List Bool) : pairSnd z = (Option.map Prod.snd (unpair? z)).getD []

pairSnd agrees with the partial decoder unpair?, defaulting to [].

theorem Complexity.pairSnd_length_le (z : List Bool) : (pairSnd z).length ≤ z.length

The second component of a pair is no longer than the pair.