Preliminaries

noncomputable def Nat.div2Induction {motive : Nat → Sort u} (n : Nat) (ind : (n : Nat) → (n > 0 → motive (n / 2)) → motive n) : motive n

An induction principal that works on divison by two.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Nat.zero_and (x : Nat) : 0 &&& x = 0

@[simp]

theorem Nat.and_zero (x : Nat) : x &&& 0 = 0

@[simp]

theorem Nat.and_one_is_mod (x : Nat) : x &&& 1 = x % 2

testBit

@[simp]

theorem Nat.zero_testBit (i : Nat) : Nat.testBit 0 i = false

@[simp]

theorem Nat.testBit_zero (x : Nat) : Nat.testBit x 0 = decide (x % 2 = 1)

@[simp]

theorem Nat.testBit_succ (x : Nat) (i : Nat) : Nat.testBit x (Nat.succ i) = Nat.testBit (x / 2) i

theorem Nat.testBit_to_div_mod {i : Nat} {x : Nat} : Nat.testBit x i = decide (x / 2 ^ i % 2 = 1)

theorem Nat.ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ (i : Nat), Nat.testBit x i = true

theorem Nat.ne_implies_bit_diff {x : Nat} {y : Nat} (p : x ≠ y) : ∃ (i : Nat), Nat.testBit x i ≠ Nat.testBit y i

theorem Nat.eq_of_testBit_eq {x : Nat} {y : Nat} (pred : ∀ (i : Nat), Nat.testBit x i = Nat.testBit y i) : x = y

eq_of_testBit_eq allows proving two natural numbers are equal if their bits are all equal.

theorem Nat.ge_two_pow_implies_high_bit_true {n : Nat} {x : Nat} (p : x ≥ 2 ^ n) : ∃ (i : Nat), i ≥ n ∧ Nat.testBit x i = true

theorem Nat.testBit_implies_ge {i : Nat} {x : Nat} (p : Nat.testBit x i = true) : x ≥ 2 ^ i

theorem Nat.testBit_lt_two_pow {x : Nat} {i : Nat} (lt : x < 2 ^ i) : Nat.testBit x i = false

theorem Nat.lt_pow_two_of_testBit {n : Nat} (x : Nat) (p : ∀ (i : Nat), i ≥ n → Nat.testBit x i = false) : x < 2 ^ n

testBit

theorem Nat.testBit_two_pow_add_eq (x : Nat) (i : Nat) : Nat.testBit (2 ^ i + x) i = !Nat.testBit x i

theorem Nat.testBit_mul_two_pow_add_eq (a : Nat) (b : Nat) (i : Nat) : Nat.testBit (2 ^ i * a + b) i = Bool.xor (decide (a % 2 = 1)) (Nat.testBit b i)

theorem Nat.testBit_two_pow_add_gt {i : Nat} {j : Nat} (j_lt_i : j < i) (x : Nat) : Nat.testBit (2 ^ i + x) j = Nat.testBit x j

@[simp]

theorem Nat.testBit_mod_two_pow (x : Nat) (j : Nat) (i : Nat) : Nat.testBit (x % 2 ^ j) i = (decide (i < j) && Nat.testBit x i)

theorem Nat.testBit_one_zero : Nat.testBit 1 0 = true

theorem Nat.testBit_two_pow_sub_succ {x : Nat} {n : Nat} (h₂ : x < 2 ^ n) (i : Nat) : Nat.testBit (2 ^ n - (x + 1)) i = (decide (i < n) && !Nat.testBit x i)

@[simp]

theorem Nat.testBit_two_pow_sub_one (n : Nat) (i : Nat) : Nat.testBit (2 ^ n - 1) i = decide (i < n)

theorem Nat.testBit_bool_to_nat (b : Bool) (i : Nat) : Nat.testBit (Bool.toNat b) i = (decide (i = 0) && b)

bitwise

theorem Nat.testBit_bitwise {f : Bool → Bool → Bool} (false_false_axiom : f false false = false) (x : Nat) (y : Nat) (i : Nat) : Nat.testBit (Nat.bitwise f x y) i = f (Nat.testBit x i) (Nat.testBit y i)

bitwise

theorem Nat.bitwise_lt_two_pow {x : Nat} {n : Nat} {y : Nat} {f : Bool → Bool → Bool} (left : x < 2 ^ n) (right : y < 2 ^ n) : Nat.bitwise f x y < 2 ^ n

This provides a bound on bitwise operations.

and

@[simp]

theorem Nat.testBit_and (x : Nat) (y : Nat) (i : Nat) : Nat.testBit (x &&& y) i = (Nat.testBit x i && Nat.testBit y i)

theorem Nat.and_lt_two_pow (x : Nat) {y : Nat} {n : Nat} (right : y < 2 ^ n) : x &&& y < 2 ^ n

@[simp]

theorem Nat.and_pow_two_is_mod (x : Nat) (n : Nat) : x &&& 2 ^ n - 1 = x % 2 ^ n

theorem Nat.and_pow_two_identity {n : Nat} {x : Nat} (lt : x < 2 ^ n) : x &&& 2 ^ n - 1 = x

lor

@[simp]

theorem Nat.or_zero (x : Nat) : 0 ||| x = x

@[simp]

theorem Nat.zero_or (x : Nat) : x ||| 0 = x

@[simp]

theorem Nat.testBit_or (x : Nat) (y : Nat) (i : Nat) : Nat.testBit (x ||| y) i = (Nat.testBit x i || Nat.testBit y i)

theorem Nat.or_lt_two_pow {x : Nat} {y : Nat} {n : Nat} (left : x < 2 ^ n) (right : y < 2 ^ n) : x ||| y < 2 ^ n

xor

@[simp]

theorem Nat.testBit_xor (x : Nat) (y : Nat) (i : Nat) : Nat.testBit (x ^^^ y) i = Bool.xor (Nat.testBit x i) (Nat.testBit y i)

theorem Nat.xor_lt_two_pow {x : Nat} {y : Nat} {n : Nat} (left : x < 2 ^ n) (right : y < 2 ^ n) : x ^^^ y < 2 ^ n

Arithmetic

theorem Nat.testBit_mul_pow_two_add (a : Nat) {b : Nat} {i : Nat} (b_lt : b < 2 ^ i) (j : Nat) : Nat.testBit (2 ^ i * a + b) j = if j < i then Nat.testBit b j else Nat.testBit a (j - i)

theorem Nat.testBit_mul_pow_two {i : Nat} {a : Nat} {j : Nat} : Nat.testBit (2 ^ i * a) j = (decide (j ≥ i) && Nat.testBit a (j - i))

theorem Nat.mul_add_lt_is_or {i : Nat} {b : Nat} (b_lt : b < 2 ^ i) (a : Nat) : 2 ^ i * a + b = 2 ^ i * a ||| b

shiftLeft and shiftRight

@[simp]

theorem Nat.testBit_shiftLeft {i : Nat} {j : Nat} (x : Nat) : Nat.testBit (x <<< i) j = (decide (j ≥ i) && Nat.testBit x (j - i))

@[simp]

theorem Nat.testBit_shiftRight {i : Nat} {j : Nat} (x : Nat) : Nat.testBit (x >>> i) j = Nat.testBit x (i + j)