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). The simp lemmas BitString.block_blocksEquiv_symm and BitString.blocksEquiv_symm_block state the two inverse laws with block.
• Cslib.BitString.blockBits: the positions of the entries of a block.
• Cslib.BitString.listBlock: a block of a list (BitString.listBlock_ofFn, BitString.listBlock_flatMap).

Main results

• Cslib.BitString.pairwiseDisjoint_blockBits: blocks occupy disjoint positions.
• Cslib.BitString.block_piecewise: gluing two tuples along one block.
• Cslib.BitString.ofFn_blocksEquiv_symm: concatenating blocks concatenates their lists.

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.

@[simp]

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

Concatenating the blocks of a tuple recovers it. Equiv.symm_apply_apply does not fire after blocksEquiv_apply has rewritten blocksEquiv x to block x.

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.

theorem Cslib.BitString.listBlock_flatMap {α : Type u_1} {k : ℕ} {β : Type u_2} (f : β → List α) (hf : ∀ (b : β), (f b).length = k) (l : List β) (i : ℕ) (hi : i < l.length) : listBlock k (List.flatMap f l) i = f l[i]

Block i of a concatenation of blocks of uniform length k is block i itself.

theorem Cslib.BitString.ofFn_blocksEquiv_symm {α : Type u_1} {m k : ℕ} (z : Fin m → Fin k → α) : List.ofFn (blocksEquiv.symm z) = (List.ofFn fun (i : Fin m) => List.ofFn (z i)).flatten

The list of the concatenation of blocks is the concatenation of the lists of the blocks.