Counting, numbering and adding bit strings

There are 2 ^ n strings of n bits (BitString.card), numbered 0, …, 2 ^ n - 1 by reading their bits as binary digits, least significant first (BitString.equivFin).

Bits form the two-element Boolean ring (Mathlib's BooleanRing Bool), in which a + b = (a ^^ b) and a * b = (a && b), so bit strings ι → Bool form an additive group under coordinatewise exclusive or, the vector space 𝔽₂ⁿ of O'Donnell, Chapter 1: (x + y) i = (x i ^^ y i) holds by definition. Every bit string is its own negative (BitString.add_self). Translating by a fixed string is the permutation Equiv.addLeft x.

Throughout the library, bit strings are added with +, while single bits, such as the values of Boolean functions, are combined with ^^.

Main definitions

• Cslib.BitString.equivFin: the numbering of the strings of n bits by Fin (2 ^ n).
• Cslib.BitString.fstBits, Cslib.BitString.sndBits: the two parts of an appended word.
• Cslib.BitString.indexBits: a finite index represented in ⌈log₂ n⌉ bits.

Main results

• Cslib.BitString.card: the number of strings of n bits.
• Cslib.BitString.val_equivFin_eq_sum: the unsigned value as a sum of binary digits.
• Cslib.BitString.val_equivFin_cons: a new first bit is the least significant binary digit.
• Cslib.BitString.val_equivFin_succ, Cslib.BitString.decide_equivFin_le_succ: numbering and comparing words by their highest bit.
• Cslib.BitString.indexBits_injective: distinct finite indices have distinct encodings.
• Cslib.BitString.add_self, Cslib.BitString.add_cancel_left, Cslib.BitString.add_cancel_right: every bit string is its own negative.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.card {n : ℕ} : Fintype.card (BitString n) = 2 ^ n

There are 2 ^ n strings of n bits.

def Cslib.BitString.equivFin (n : ℕ) : BitString n ≃ Fin (2 ^ n)

The strings of n bits numbered 0, …, 2 ^ n - 1, reading the bits as binary digits with the least significant bit first.

theorem Cslib.BitString.val_equivFin_cons {n : ℕ} (b : Bool) (z : BitString n) : ↑((equivFin (n + 1)) (Fin.cons b z)) = b.toNat + 2 * ↑((equivFin n) z)

A new first bit is the least significant digit of the number of a bit string.

theorem Cslib.BitString.val_equivFin_succ {n : ℕ} (x : BitString (n + 1)) : ↑((equivFin (n + 1)) x) = ↑((equivFin n) (Fin.init x)) + (x (Fin.last n)).toNat * 2 ^ n

The number of a word of n + 1 bits is the number of its first n bits plus its last bit times 2 ^ n.

theorem Cslib.BitString.val_equivFin_eq_sum {n : ℕ} (x : BitString n) : ↑((equivFin n) x) = ∑ i : Fin n, (x i).toNat * 2 ^ ↑i

The unsigned value of an n-bit word (least significant bit first) as an explicit sum.

@[simp]

theorem Cslib.BitString.val_equivFin_false (n : ℕ) : ↑((equivFin n) fun (x : Fin n) => false) = 0

The zero word of n bits has unsigned value zero.

def Cslib.BitString.fstBits {a b : ℕ} (x : BitString (a + b)) : BitString a

The first a bits of an (a + b)-bit word.

def Cslib.BitString.sndBits {a b : ℕ} (x : BitString (a + b)) : BitString b

The last b bits of an (a + b)-bit word.

@[simp]

theorem Cslib.BitString.fstBits_append {a b : ℕ} (u : BitString a) (v : BitString b) : fstBits (Fin.append u v) = u

The first a bits of Fin.append u v are u.

@[simp]

theorem Cslib.BitString.sndBits_append {a b : ℕ} (u : BitString a) (v : BitString b) : sndBits (Fin.append u v) = v

The last b bits of Fin.append u v are v.

theorem Cslib.BitString.decide_equivFin_le_succ {n : ℕ} (x y : BitString (n + 1)) : decide ((equivFin (n + 1)) x ≤ (equivFin (n + 1)) y) = (!x (Fin.last n) && y (Fin.last n) || (!x (Fin.last n) || y (Fin.last n)) && decide ((equivFin n) (Fin.init x) ≤ (equivFin n) (Fin.init y)))

Comparing words of n + 1 bits: x ≤ y when the last bit of x is below that of y, or when they are equal and x ≤ y on the first n bits.

def Cslib.BitString.indexBits {n : ℕ} (i : Fin n) : BitString (Nat.clog 2 n)

The binary numeral of i : Fin n in ⌈log₂ n⌉ bits.

theorem Cslib.BitString.indexBits_injective {n : ℕ} : Function.Injective indexBits

Distinct finite indices have distinct binary numerals.

@[simp]

theorem Cslib.BitString.add_self {ι : Type u_1} (x : ι → Bool) : x + x = 0

A bit string added to itself gives zero.

@[simp]

theorem Cslib.BitString.add_cancel_left {ι : Type u_1} (x y : ι → Bool) : x + (x + y) = y

Adding x twice cancels: x + (x + y) = y.

@[simp]

theorem Cslib.BitString.add_cancel_right {ι : Type u_1} (x y : ι → Bool) : x + y + y = x

Adding y twice cancels: x + y + y = x.