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