Documentation

Complexitylib.Encoding.Pairing

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.

source
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. The output has length 2|x| + 2 + |y| (pair_length) and the encoding is injective (pair_inj). Machine-level cost is recorded elsewhere: pair of two FP functions is in FP (mem_FP_pair), and x ↦ pair (f x) x has an explicit bound (TM.pairWithInputTM_computesInTime); no linear-time bound for pair itself is stated.

Equations
Instances For
    source
    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.

    source
    @[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].

    source
    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₂.

    source
    @[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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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.

    source
    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
    Instances For
      source
      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
      Instances For
        source
        @[simp]
        theorem Complexity.pairFst_pair (x y : List Bool) :
        pairFst (pair x y) = x
        source
        @[simp]
        theorem Complexity.pairSnd_pair (x y : List Bool) :
        pairSnd (pair x y) = y
        source
        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 [].

        source
        theorem Complexity.pairFst_length_le (z : List Bool) :
        (pairFst z).length ≤ z.length

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

        source
        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.