Blocks of bit strings

A string of m * k bits is read as m consecutive blocks of k bits through finProdFinEquiv: bit j of block i is bit finProdFinEquiv (i, j) of the string (BitString.block). Cutting a string into its blocks is an equivalence BitString (m * k) ≃ (Fin m → BitString k) (BitString.blocksEquiv). The positions of the blocks (BitString.blockBits) are pairwise disjoint, and gluing two strings along the positions of one block takes that block from the first string and every other block from the second (BitString.block_piecewise).

Main definitions

• Cslib.BitString.block: the i-th block of k bits of a string of m * k bits.
• Cslib.BitString.blocksEquiv: cutting a string into its blocks; its inverse reads bit p of the string in its block (BitString.blocksEquiv_symm_apply).
• Cslib.BitString.blockBits: the positions of the bits of a block.
• Cslib.BitString.listBlock: a block of a bit list (BitString.listBlock_ofFn).

Main results

• Cslib.BitString.pairwiseDisjoint_blockBits: blocks occupy disjoint positions.
• Cslib.BitString.block_piecewise: gluing two strings along one block.

def Cslib.BitString.block {m k : ℕ} (x : BitString (m * k)) (i : Fin m) : BitString k

The i-th block of k consecutive bits of a string of m blocks.

@[simp]

theorem Cslib.BitString.block_apply {m k : ℕ} (x : BitString (m * k)) (i : Fin m) (j : Fin k) : x.block i j = x (finProdFinEquiv (i, j))

Bit j of block i is bit finProdFinEquiv (i, j) of the string.

def Cslib.BitString.blocksEquiv {m k : ℕ} : BitString (m * k) ≃ (Fin m → BitString k)

Cutting a string of m * k bits into its m blocks of k bits.

@[simp]

theorem Cslib.BitString.blocksEquiv_symm_apply {m k : ℕ} (y : Fin m → BitString k) (p : Fin (m * k)) : blocksEquiv.symm y p = y (finProdFinEquiv.symm p).1 (finProdFinEquiv.symm p).2

@[simp]

theorem Cslib.BitString.blocksEquiv_apply {m k : ℕ} (x : BitString (m * k)) : blocksEquiv x = x.block

blocksEquiv cuts a string into its blocks with block.

@[simp]

theorem Cslib.BitString.block_blocksEquiv_symm {m k : ℕ} (z : Fin m → BitString k) : (blocksEquiv.symm z).block = z

Cutting the concatenation of blocks into its blocks recovers them.

def Cslib.BitString.blockBits {m : ℕ} (k : ℕ) (i : Fin m) : Finset (Fin (m * k))

The positions of the bits of the i-th block of k bits.

theorem Cslib.BitString.mem_blockBits {m k : ℕ} {i : Fin m} {p : Fin (m * k)} : p ∈ blockBits k i ↔ (finProdFinEquiv.symm p).1 = i

A position lies in block i exactly when its block index under finProdFinEquiv is i.

theorem Cslib.BitString.pairwiseDisjoint_blockBits {m : ℕ} (k : ℕ) : (↑Finset.univ).PairwiseDisjoint (blockBits k)

Distinct blocks occupy disjoint positions.

theorem Cslib.BitString.block_piecewise {m k : ℕ} (i : Fin m) (x z : BitString (m * k)) (j : Fin m) : block ((blockBits k i).piecewise x z) j = if j = i then x.block j else z.block j

Gluing x and z along the positions of block i takes block i from x and the other blocks from z.

def Cslib.BitString.listBlock (k : ℕ) (z : List Bool) (i : ℕ) : List Bool

Block i of k bits of a bit list: the k bits from position i * k on.

theorem Cslib.BitString.listBlock_ofFn {m k : ℕ} (z : BitString (m * k)) (i : Fin m) : listBlock k (List.ofFn z) ↑i = List.ofFn (z.block i)

Block i of the list of a bit string is the list of its block i.