Fixed-length bit strings and lists

Circuits consume fixed-length functions BitString n = Fin n → Bool, while machine languages consume List Bool. This module makes List.ofFn the canonical serialization and provides round-trip lemmas in both directions.

The variable-length equivalence is already available from Mathlib as List.equivSigmaTuple : List Bool ≃ Σ n, BitString n.

def Complexity.BitString.toTotal {n : ℕ} (x : BitString n) : ℕ → Bool

Extend a fixed-length bit string to a total assignment by setting every out-of-range variable to false. This is the canonical semantic bridge from typed Boolean functions to formula and branching-program syntax.

Equations

• x.toTotal i = if h : i < n then x ⟨i, h⟩ else false

@[simp]

theorem Complexity.BitString.toTotal_apply {n : ℕ} (x : BitString n) (i : Fin n) : x.toTotal ↑i = x i

The total extension agrees with the original bit string on every in-range index.

theorem Complexity.BitString.toTotal_of_lt {n : ℕ} (x : BitString n) (i : ℕ) (h : i < n) : x.toTotal i = x ⟨i, h⟩

An explicit natural index below the arity is read from the original bit string by the total extension.

theorem Complexity.BitString.toTotal_of_le {n : ℕ} (x : BitString n) (i : ℕ) (h : n ≤ i) : x.toTotal i = false

Every out-of-range index is false in the canonical total extension.

def Complexity.BitString.toList {n : ℕ} (x : BitString n) : List Bool

Serialize a fixed-length bit string in increasing index order.

Equations

• x.toList = List.ofFn x

def Complexity.BitString.ofList (xs : List Bool) {n : ℕ} (h : xs.length = n) : BitString n

Read a list of the specified length as a fixed-length bit string.

Equations

• Complexity.BitString.ofList xs h i = xs.get (Fin.cast ⋯ i)

@[simp]

theorem Complexity.BitString.length_toList {n : ℕ} (x : BitString n) : x.toList.length = n

Serialization preserves length: toList of an n-bit string has length n.

@[simp]

theorem Complexity.BitString.getElem_toList {n : ℕ} (x : BitString n) (i : Fin n) : x.toList[↑i] = x i

Indexing into the serialized list agrees with the original bit string: x.toList[i] = x i.

@[simp]

theorem Complexity.BitString.toList_ofList (xs : List Bool) {n : ℕ} (h : xs.length = n) : (ofList xs h).toList = xs

Round trip, list side: serializing ofList xs h recovers the original list xs.

@[simp]

theorem Complexity.BitString.ofList_toList {n : ℕ} (x : BitString n) : ofList x.toList ⋯ = x

Round trip, bit-string side: deserializing toList x recovers the original bit string x.

@[simp]

theorem Complexity.BitString.toList_inj {n : ℕ} {x y : BitString n} : x.toList = y.toList ↔ x = y

Serialization is injective: two bit strings have equal toList iff they are equal.

@[simp]

theorem Complexity.BitString.toList_map {n : ℕ} (f : Bool → Bool) (x : BitString n) : (toList fun (i : Fin n) => f (x i)) = List.map f x.toList

Serialization commutes with pointwise maps: toList (f ∘ x) = x.toList.map f.

@[simp]

theorem Complexity.BitString.toList_append {m n : ℕ} (x : BitString m) (y : BitString n) : toList (Fin.append x y) = x.toList ++ y.toList

Serialization sends Fin.append to list append: toList (x ++ y) = x.toList ++ y.toList.