Set bits and binary finite-set codes

The increasing list of set bits of a natural number can be obtained by testing every index below the number. Mathlib's Finset.equivBitIndices identifies natural numbers with finite sets of natural numbers, using ∑ x ∈ D, 2 ^ x as the code of a finite set D.

The i-th bit of the code ∑ j ∈ s, 2 ^ j records whether i ∈ s. Bitwise union, intersection and difference decode to the corresponding finite-set operations, and inserting x sets bit x. Bounded filtering keeps the requested members of a binary code, and least-element search returns none precisely for the zero code.

References

• Mathlib's Finset.equivBitIndices supplies the binary finite-set equivalence.

theorem Nat.bitIndices_eq_filter_range (n : ℕ) : n.bitIndices = List.filter n.testBit (List.range n)

The set bits of n are found by filtering the finite interval below n.

@[simp]

theorem Nat.testBit_sum_two_pow (s : Finset ℕ) (i : ℕ) : (∑ j ∈ s, 2 ^ j).testBit i = decide (i ∈ s)

The i-th bit of the binary code of s records whether i ∈ s.

theorem Finset.equivBitIndices_lor (m n : ℕ) : equivBitIndices (m ||| n) = equivBitIndices m ∪ equivBitIndices n

Binary union decodes to finite-set union.

theorem Finset.equivBitIndices_land (m n : ℕ) : equivBitIndices (m &&& n) = equivBitIndices m ∩ equivBitIndices n

Binary intersection decodes to finite-set intersection.

theorem Finset.equivBitIndices_symm_insert (x : ℕ) (D : Finset ℕ) : equivBitIndices.symm (insert x D) = equivBitIndices.symm D ||| 2 ^ x

Inserting x into a finite set sets bit x of its binary code.

theorem Finset.equivBitIndices_ldiff (m n : ℕ) : equivBitIndices (m.ldiff n) = equivBitIndices m \ equivBitIndices n

Binary difference decodes to finite-set difference.

def Nat.filterBitIndices (n b : ℕ) (p : ℕ → Bool) : ℕ

Keep the members of the binary-coded finite set n that lie below b and satisfy p.

theorem Nat.equivBitIndices_filterBitIndices (n b : ℕ) (p : ℕ → Bool) : Finset.equivBitIndices (n.filterBitIndices b p) = {x ∈ Finset.equivBitIndices n | x < b ∧ p x = true}

Decoding bounded filtering gives the corresponding filtered finite set.

@[simp]

theorem Nat.testBit_filterBitIndices (n b x : ℕ) (p : ℕ → Bool) : (n.filterBitIndices b p).testBit x = (n.testBit x && decide (x < b) && p x)

The result of bounded filtering contains exactly the requested members.

def Nat.leastBitIndex (n : ℕ) : Option ℕ

The least member of a binary-coded finite set, or none for the empty set.

theorem Nat.leastBitIndex_def (n : ℕ) : n.leastBitIndex = n.bitIndices.head?

Least-element search is the head of the increasing list of set bits.

@[simp]

theorem Nat.leastBitIndex_eq_some_iff (n k : ℕ) : n.leastBitIndex = some k ↔ k ∈ Finset.equivBitIndices n ∧ ∀ x ∈ Finset.equivBitIndices n, k ≤ x

Least-element search succeeds precisely at a member below every other member.

@[simp]

theorem Nat.leastBitIndex_eq_none_iff (n : ℕ) : n.leastBitIndex = none ↔ n = 0

Least-element search returns none exactly for the zero code.