A binary counter

A word of fixed length is a counter, read least significant bit first (Cslib.BitString.lsbValue). Increment (Cslib.BitString.increment) flips the trailing ones of the least significant end and the first zero, discarding the final carry, so it keeps the length and wraps around from the word of ones to the word of zeros. Counting from the word of m zeros enumerates the words of length m in order of value (Cslib.BitString.iterate_increment), each reached at its value (Cslib.BitString.iterate_increment_lsbValue). Exhaustive searches in polynomial space enumerate their candidates in this way, storing only the current one.

Main definitions

• Cslib.BitString.increment: binary increment, least significant bit first.
• Cslib.BitString.lsbValue: the value of a word, least significant bit first.

Main results

• Cslib.BitString.lsbValue_increment: increment adds one below the largest value.
• Cslib.BitString.lsbValue_injective: words of the same length are determined by their values.
• Cslib.BitString.iterate_increment, Cslib.BitString.iterate_increment_lsbValue: counting from zero enumerates the words of a length.
• Cslib.BitString.lsbValue_eq_foldr_bit: lsbValue is a right fold of Nat.bit.

def Cslib.BitString.increment : List Bool → List Bool

Binary increment, least significant bit first, discarding the final carry.

def Cslib.BitString.lsbValue : List Bool → ℕ

The value of a word in binary, least significant bit first.

@[simp]

theorem Cslib.BitString.length_increment (w : List Bool) : (increment w).length = w.length

Increment keeps the length.

@[simp]

theorem Cslib.BitString.length_iterate_increment (j : ℕ) (w : List Bool) : (increment^[j] w).length = w.length

Iterated increment keeps the length.

theorem Cslib.BitString.lsbValue_lt (w : List Bool) : lsbValue w < 2 ^ w.length

A word of length m has value below 2 ^ m.

theorem Cslib.BitString.lsbValue_increment (w : List Bool) : lsbValue w + 1 < 2 ^ w.length → lsbValue (increment w) = lsbValue w + 1

Below the largest value, increment adds one.

theorem Cslib.BitString.lsbValue_injective {w w' : List Bool} : w.length = w'.length → lsbValue w = lsbValue w' → w = w'

Words of the same length are determined by their values.

@[simp]

theorem Cslib.BitString.lsbValue_replicate_false (m : ℕ) : lsbValue (List.replicate m false) = 0

The word of zeros has value 0.

theorem Cslib.BitString.lsbValue_replicate_true (m : ℕ) : lsbValue (List.replicate m true) + 1 = 2 ^ m

The word of ones has the largest value.

theorem Cslib.BitString.lsbValue_pos_of_true_mem {u : List Bool} : true ∈ u → 0 < lsbValue u

A word with a true has a positive value.

theorem Cslib.BitString.lsbValue_eq_zero_of_true_not_mem {u : List Bool} : ¬true ∈ u → lsbValue u = 0

A word without true has value 0.

theorem Cslib.BitString.iterate_increment (m j : ℕ) : j < 2 ^ m → lsbValue (increment^[j] (List.replicate m false)) = j ∧ (increment^[j] (List.replicate m false)).length = m

The counter counts: the j-th iterate from the word of m zeros has value j, for j < 2 ^ m.

theorem Cslib.BitString.iterate_increment_lsbValue (u : List Bool) : increment^[lsbValue u] (List.replicate u.length false) = u

Every word is reached by counting up to its value.

theorem Cslib.BitString.lsbValue_eq_foldr_bit (w : List Bool) : lsbValue w = List.foldr Nat.bit 0 w

lsbValue is a right fold of Nat.bit.