@[irreducible]

def Nat.popcount (n : Nat) : Nat

Equations

• n.popcount = if n = 0 then 0 else (n / 2).popcount + n % 2

@[simp]

theorem Nat.popcount_zero : popcount 0 = 0

theorem Nat.popcount_ne {n : Nat} (h : n ≠ 0) : n.popcount = (n / 2).popcount + n % 2

theorem Nat.popcount_odd {n : Nat} (h : n.testBit 0 = true) : n.popcount = (n / 2).popcount + 1

theorem Nat.popcount_even {n : Nat} (h : ¬n.testBit 0 = true) : n.popcount = (n / 2).popcount

theorem Nat.popcount_le_of_lt_pow {n w : Nat} (h : n < 2 ^ w) : n.popcount ≤ w

@[simp]

theorem Nat.one_shiftLeft_mod_two_pow {n w : Nat} (h : n < w) : 1 <<< n % 2 ^ w = 1 <<< n

theorem Nat.popcount_or_one_shiftLeft (n i : Nat) : (n ||| 1 <<< i).popcount = if n.testBit i = true then n.popcount else n.popcount + 1