@[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

theorem Nat.one_shiftLeft_lt_pow {n w : Nat} (h : n < w) : 1 <<< n < 2 ^ w

@[simp]

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

theorem Nat.zero_of_or_zero {n m : Nat} (h : n ||| m = 0) : n = 0 ∧ m = 0

theorem Nat.or_ne_zero {n m : Nat} (h : m ≠ 0) : n ||| m ≠ 0

theorem Nat.or_one_shiftLeft_ne_zero {i n : Nat} : n ||| 1 <<< i ≠ 0

theorem Nat.or_one_mod_two {n : Nat} : (n ||| 1) % 2 = 1

theorem Nat.one_shiftLeft_succ_div_two {i : Nat} : 1 <<< (i + 1) / 2 = 1 <<< i

theorem Nat.or_one_shiftLeft_succ_mod_two {i n : Nat} : (n ||| 1 <<< (i + 1)) % 2 = n % 2

theorem Nat.ne_zero_of_testBit {n i : Nat} (h : n.testBit i = true) : n ≠ 0

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