Selecting and packing bit-string records

A record has a prefix key of k bits followed by a payload of p bits. Keys are unsigned numbers with the least significant bit first. Pairwise minimum selection retains the first record on equal keys, including empty keys. Packing places records in consecutive blocks.

Main definitions

• Cslib.BitString.recordKey: the prefix key.
• Cslib.BitString.keyedMinFn: a least-key record, the first on ties.
• Cslib.BitString.packRecords: concatenate a finite family of records.

Main results

• Cslib.BitString.keyedMinFn_eq_or_eq: selection returns one of its inputs.
• Cslib.BitString.equivFin_recordKey_keyedMinFn_le_left, Cslib.BitString.equivFin_recordKey_keyedMinFn_le_right: the selected key is least.
• Cslib.BitString.packRecords_comp: recover a record from its packed block.

References

Adapted from Samuel Schlesinger's earlier Complexitylib modules Circuits/{KeyedMinimum,KeyedMinimumTournament}.

def Cslib.BitString.recordKey {k p : ℕ} (r : BitString (k + p)) : BitString k

The key of a record: its first k bits.

def Cslib.BitString.keyedMinFn {k p : ℕ} (r s : BitString (k + p)) : BitString (k + p)

Of two records, the one with the smaller key, the first on ties.

theorem Cslib.BitString.keyedMinFn_eq_or_eq {k p : ℕ} (r s : BitString (k + p)) : r.keyedMinFn s = r ∨ r.keyedMinFn s = s

The selected record is one of the two inputs.

theorem Cslib.BitString.equivFin_recordKey_keyedMinFn_le_left {k p : ℕ} (r s : BitString (k + p)) : (equivFin k) (r.keyedMinFn s).recordKey ≤ (equivFin k) r.recordKey

The key of the selected record is at most the key of the first record.

theorem Cslib.BitString.equivFin_recordKey_keyedMinFn_le_right {k p : ℕ} (r s : BitString (k + p)) : (equivFin k) (r.keyedMinFn s).recordKey ≤ (equivFin k) s.recordKey

The key of the selected record is at most the key of the second record.

def Cslib.BitString.packRecords {m r : ℕ} (records : Fin m → BitString r) : BitString (m * r)

m records of r bits packed one after the other: bit j of record i is input finProdFinEquiv (i, j), that is i r + j.

theorem Cslib.BitString.packRecords_comp {m r : ℕ} (records : Fin m → BitString r) (i : Fin m) : (packRecords records ∘ fun (j : Fin r) => finProdFinEquiv (i, j)) = records i

Reading block i of the packed records recovers record i.