Bridges between BitString.equivFin and binary numeral views

Cslib.BitString.equivFin n numbers n-bit strings Fin n → Bool with 0 as the least significant coordinate. This module connects equivFin n to the list-based numeral views Cslib.BitString.lsbValue (least significant bit first) and Cslib.BitString.binaryValue (most significant bit first), as well as Nat.ofBits and Nat.testBit, without adding a BitString.Basic dependency to the list-level modules BitString.Counter or BitString.List.Binary.

Main results

• Cslib.BitString.val_equivFin_eq_ofBits: equivFin agrees with Nat.ofBits.
• Cslib.BitString.equivFin_symm_apply: the i-th bit of (equivFin n).symm k is (k : ℕ).testBit i.
• Cslib.BitString.testBit_equivFin: the i-th binary digit of equivFin n x is x i.
• Cslib.BitString.lsbValue_eq_binaryValue_reverse: little-endian digits are the reversed big-endian ones.
• Cslib.BitString.lsbValue_ofFn: reading the bits of an n-bit word in order gives its number in equivFin n.
• Cslib.BitString.binaryValue_reverse_ofFn: reading the reversed list of bits of an n-bit word gives its number in equivFin n.
• Cslib.BitString.lsbValue_lowBits: reading lowBits n x with lsbValue recovers x < 2 ^ n.
• Cslib.BitString.lowBits_lsbValue: re-encoding lsbValue w with lowBits recovers w.
• Cslib.BitString.val_equivFin_add: addition in BitString n is bitwise XOR (^^^) on equivFin n coordinates.

theorem Cslib.BitString.val_equivFin_eq_ofBits {n : ℕ} (x : BitString n) : ↑((equivFin n) x) = Nat.ofBits x

equivFin agrees with Nat.ofBits on n-bit words.

@[simp]

theorem Cslib.BitString.equivFin_symm_apply {n : ℕ} (k : Fin (2 ^ n)) (i : Fin n) : (equivFin n).symm k i = (↑k).testBit ↑i

The i-th bit of (equivFin n).symm k is the i-th binary digit of k.

theorem Cslib.BitString.testBit_equivFin {n : ℕ} (x : BitString n) (i : Fin n) : (↑((equivFin n) x)).testBit ↑i = x i

The i-th binary digit of equivFin n x is x i.

theorem Cslib.BitString.lsbValue_ofFn {n : ℕ} (x : BitString n) : lsbValue (List.ofFn x) = ↑((equivFin n) x)

Reading the bits of an n-bit word in order gives its number in equivFin n.

theorem Cslib.BitString.binaryValue_reverse_ofFn {n : ℕ} (y : BitString n) : binaryValue (List.ofFn y).reverse = ↑((equivFin n) y)

Reading the bits of an input, least significant first, gives its number in the order of BitString.equivFin.

theorem Cslib.BitString.lsbValue_eq_binaryValue_reverse (w : List Bool) : lsbValue w = binaryValue w.reverse

Reading little-endian digits (lsbValue) is reading the reversed digits most significant first (binaryValue).

theorem Cslib.BitString.lowBits_eq_ofFn_equivFin_symm (n : ℕ) (k : Fin (2 ^ n)) : lowBits n ↑k = List.ofFn ((equivFin n).symm k)

The fixed-width word lowBits n k equals the bits of (equivFin n).symm k.

@[simp]

theorem Cslib.BitString.lsbValue_lowBits {n x : ℕ} (hx : x < 2 ^ n) : lsbValue (lowBits n x) = x

For any x < 2 ^ n, reading lowBits n x with lsbValue recovers x.

@[simp]

theorem Cslib.BitString.lowBits_lsbValue (w : List Bool) : lowBits w.length (lsbValue w) = w

Converting a bit word to a natural with lsbValue and re-encoding with lowBits of the same length recovers the original word.

theorem Cslib.BitString.val_equivFin_add {n : ℕ} (a b : BitString n) : ↑((equivFin n) (a + b)) = ↑((equivFin n) a) ^^^ ↑((equivFin n) b)

Addition in BitString n is bitwise XOR (^^^) on equivFin n coordinates.