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.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.

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.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.