Blocks of bit strings and finite tuples

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

Main definitions

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

Main results

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

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

The i-th block of k consecutive entries of a tuple of m blocks.

@[simp]

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

Entry j of block i is entry finProdFinEquiv (i, j) of the tuple.

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

Cutting a tuple of m * k entries into its m blocks of k entries. This is definitionally (finProdFinEquiv.symm.arrowCongr (Equiv.refl α)).trans (Equiv.curry _ _ _).

@[simp]

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

@[simp]

theorem Cslib.BitString.blocksEquiv_apply {α : Type u_1} {m k : ℕ} (x : Fin (m * k) → α) : blocksEquiv x = block x

blocksEquiv cuts a tuple into its blocks with block.

@[simp]

theorem Cslib.BitString.block_blocksEquiv_symm {α : Type u_1} {m k : ℕ} (z : Fin m → Fin k → α) : block (blocksEquiv.symm z) = 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 {α : Type u_1} {m k : ℕ} (i : Fin m) (x z : Fin (m * k) → α) (j : Fin m) : block ((blockBits k i).piecewise x z) j = if j = i then block x j else block z 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 {α : Type u_1} (k : ℕ) (z : List α) (i : ℕ) : List α

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

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

Block i of the list of a tuple is the list of its block i.