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 principle for the natural numbers with two cases:

• n = 0, and the motive is satisfied for 0
• n > 0, and the motive should be satisfied for n on the assumption that it is satisfied for n / 2.

Equations

• Nat.div2Induction n ind = Nat.strongRecOn n fun (n : Nat) (hyp : (m : Nat) → m < n → motive m) => ind n fun (n_pos : n > 0) => if n_eq : n = 0 then ⋯.elim else hyp (n / 2) ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.one_and_eq_mod_two (n : Nat) : 1 &&& n = n % 2

@[simp]

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

testBit

@[simp]

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

@[simp]

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

theorem Nat.mod_two_eq_one_iff_testBit_zero {x : Nat} : x % 2 = 1 ↔ x.testBit 0 = true

theorem Nat.mod_two_eq_zero_iff_testBit_zero {x : Nat} : x % 2 = 0 ↔ x.testBit 0 = false

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

theorem Nat.testBit_add_one (x i : Nat) : x.testBit (i + 1) = (x / 2).testBit i

Depending on use cases either testBit_add_one or testBit_div_two may be more useful as a simp lemma, so neither is a global simp lemma.

theorem Nat.testBit_add (x i n : Nat) : x.testBit (i + n) = (x / 2 ^ n).testBit i

theorem Nat.testBit_div_two (x i : Nat) : (x / 2).testBit i = x.testBit (i + 1)

theorem Nat.testBit_div_two_pow {n : Nat} (x i : Nat) : (x / 2 ^ n).testBit i = x.testBit (i + n)

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

theorem Nat.toNat_testBit (x i : Nat) : (x.testBit i).toNat = x / 2 ^ i % 2

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

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

theorem Nat.eq_of_testBit_eq {x y : Nat} (pred : ∀ (i : Nat), x.testBit i = y.testBit 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 x : Nat} (p : x ≥ 2 ^ n) : ∃ (i : Nat), i ≥ n ∧ x.testBit i = true

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

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

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

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

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

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

@[simp]

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

theorem Nat.testBit_one_zero : testBit 1 0 = true

theorem Nat.not_decide_mod_two_eq_one (x : Nat) : (!decide (x % 2 = 1)) = decide (x % 2 = 0)

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

@[simp]

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

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

theorem Nat.testBit_one_eq_true_iff_self_eq_zero {i : Nat} : testBit 1 i = true ↔ i = 0

testBit 1 i is true iff the index i equals 0.

theorem Nat.testBit_two_pow {n m : Nat} : (2 ^ n).testBit m = decide (n = m)

@[simp]

theorem Nat.testBit_two_pow_self {n : Nat} : (2 ^ n).testBit n = true

@[simp]

theorem Nat.testBit_two_pow_of_ne {n m : Nat} (hm : n ≠ m) : (2 ^ n).testBit m = false

@[simp]

theorem Nat.two_pow_sub_one_mod_two {n : Nat} : (2 ^ n - 1) % 2 = 1 % 2 ^ n

@[simp]

theorem Nat.mod_two_pos_mod_two_eq_one {x j : Nat} : x % 2 ^ j % 2 = 1 ↔ 0 < j ∧ x % 2 = 1

bitwise

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

bitwise

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

This provides a bound on bitwise operations.

theorem Nat.bitwise_div_two_pow {f : Bool → Bool → Bool} {x y n : Nat} (of_false_false : f false false = false := by rfl) : bitwise f x y / 2 ^ n = bitwise f (x / 2 ^ n) (y / 2 ^ n)

theorem Nat.bitwise_mod_two_pow {f : Bool → Bool → Bool} {x y n : Nat} (of_false_false : f false false = false := by rfl) : bitwise f x y % 2 ^ n = bitwise f (x % 2 ^ n) (y % 2 ^ n)

and

@[simp]

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

@[simp]

theorem Nat.and_self (x : Nat) : x &&& x = x

theorem Nat.and_comm (x y : Nat) : x &&& y = y &&& x

theorem Nat.and_assoc (x y z : Nat) : x &&& y &&& z = x &&& (y &&& z)

instance Nat.instAssociativeHAnd : Std.Associative fun (x1 x2 : Nat) => x1 &&& x2

instance Nat.instCommutativeHAnd : Std.Commutative fun (x1 x2 : Nat) => x1 &&& x2

instance Nat.instIdempotentOpHAnd : Std.IdempotentOp fun (x1 x2 : Nat) => x1 &&& x2

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

@[simp]

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

@[reducible, inline, deprecated Nat.and_two_pow_sub_one_eq_mod (since := "2025-03-18")]

abbrev Nat.and_pow_two_sub_one_eq_mod (x n : Nat) : x &&& 2 ^ n - 1 = x % 2 ^ n

Equations

• Nat.and_pow_two_sub_one_eq_mod = Nat.and_two_pow_sub_one_eq_mod

@[reducible, inline, deprecated Nat.and_two_pow_sub_one_eq_mod (since := "2024-09-11")]

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

Equations

• Nat.and_pow_two_is_mod = Nat.and_two_pow_sub_one_eq_mod

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

@[reducible, inline, deprecated Nat.and_two_pow_sub_one_of_lt_two_pow (since := "2025-03-18")]

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

Equations

• @Nat.and_pow_two_sub_one_of_lt_two_pow = @Nat.and_two_pow_sub_one_of_lt_two_pow

@[reducible, inline, deprecated Nat.and_two_pow_sub_one_of_lt_two_pow (since := "2024-09-11")]

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

Equations

• @Nat.and_two_pow_identity = @Nat.and_two_pow_sub_one_of_lt_two_pow

@[simp]

theorem Nat.and_mod_two_eq_one {a b : Nat} : (a &&& b) % 2 = 1 ↔ a % 2 = 1 ∧ b % 2 = 1

theorem Nat.and_div_two_pow {a b n : Nat} : (a &&& b) / 2 ^ n = a / 2 ^ n &&& b / 2 ^ n

theorem Nat.and_div_two {a b : Nat} : (a &&& b) / 2 = a / 2 &&& b / 2

theorem Nat.and_mod_two_pow {a b n : Nat} : (a &&& b) % 2 ^ n = a % 2 ^ n &&& b % 2 ^ n

lor

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.or_self (x : Nat) : x ||| x = x

theorem Nat.or_comm (x y : Nat) : x ||| y = y ||| x

theorem Nat.or_assoc (x y z : Nat) : x ||| y ||| z = x ||| (y ||| z)

theorem Nat.and_or_distrib_left (x y z : Nat) : x &&& (y ||| z) = x &&& y ||| x &&& z

theorem Nat.and_distrib_right (x y z : Nat) : (x ||| y) &&& z = x &&& z ||| y &&& z

theorem Nat.or_and_distrib_left (x y z : Nat) : x ||| y &&& z = (x ||| y) &&& (x ||| z)

theorem Nat.or_and_distrib_right (x y z : Nat) : x &&& y ||| z = (x ||| z) &&& (y ||| z)

instance Nat.instAssociativeHOr : Std.Associative fun (x1 x2 : Nat) => x1 ||| x2

instance Nat.instCommutativeHOr : Std.Commutative fun (x1 x2 : Nat) => x1 ||| x2

instance Nat.instIdempotentOpHOr : Std.IdempotentOp fun (x1 x2 : Nat) => x1 ||| x2

instance Nat.instLawfulCommIdentityHOrOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Nat) => x1 ||| x2) 0

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

@[simp]

theorem Nat.or_mod_two_eq_one {a b : Nat} : (a ||| b) % 2 = 1 ↔ a % 2 = 1 ∨ b % 2 = 1

theorem Nat.or_div_two_pow {a b n : Nat} : (a ||| b) / 2 ^ n = a / 2 ^ n ||| b / 2 ^ n

theorem Nat.or_div_two {a b : Nat} : (a ||| b) / 2 = a / 2 ||| b / 2

theorem Nat.or_mod_two_pow {a b n : Nat} : (a ||| b) % 2 ^ n = a % 2 ^ n ||| b % 2 ^ n

xor

@[simp]

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

@[simp]

theorem Nat.zero_xor (x : Nat) : 0 ^^^ x = x

@[simp]

theorem Nat.xor_zero (x : Nat) : x ^^^ 0 = x

@[simp]

theorem Nat.xor_self (x : Nat) : x ^^^ x = 0

theorem Nat.xor_comm (x y : Nat) : x ^^^ y = y ^^^ x

theorem Nat.xor_assoc (x y z : Nat) : x ^^^ y ^^^ z = x ^^^ (y ^^^ z)

instance Nat.instAssociativeHXor : Std.Associative fun (x1 x2 : Nat) => x1 ^^^ x2

instance Nat.instCommutativeHXor : Std.Commutative fun (x1 x2 : Nat) => x1 ^^^ x2

instance Nat.instLawfulCommIdentityHXorOfNat : Std.LawfulCommIdentity (fun (x1 x2 : Nat) => x1 ^^^ x2) 0

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

theorem Nat.and_xor_distrib_right {a b c : Nat} : (a ^^^ b) &&& c = a &&& c ^^^ b &&& c

theorem Nat.and_xor_distrib_left {a b c : Nat} : a &&& (b ^^^ c) = a &&& b ^^^ a &&& c

@[simp]

theorem Nat.xor_mod_two_eq_one {a b : Nat} : (a ^^^ b) % 2 = 1 ↔ ¬(a % 2 = 1 ↔ b % 2 = 1)

theorem Nat.xor_div_two_pow {a b n : Nat} : (a ^^^ b) / 2 ^ n = a / 2 ^ n ^^^ b / 2 ^ n

theorem Nat.xor_div_two {a b : Nat} : (a ^^^ b) / 2 = a / 2 ^^^ b / 2

theorem Nat.xor_mod_two_pow {a b n : Nat} : (a ^^^ b) % 2 ^ n = a % 2 ^ n ^^^ b % 2 ^ n

Arithmetic

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

@[reducible, inline, deprecated Nat.testBit_two_pow_mul_add (since := "2025-03-18")]

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

Equations

• Nat.testBit_mul_pow_two_add = Nat.testBit_two_pow_mul_add

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

@[reducible, inline, deprecated Nat.testBit_two_pow_mul (since := "2025-03-18")]

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

Equations

• @Nat.testBit_mul_pow_two = @Nat.testBit_two_pow_mul

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

@[reducible, inline, deprecated Nat.two_pow_add_eq_or_of_lt (since := "2025-03-18")]

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

Equations

• @Nat.mul_add_lt_is_or = @Nat.two_pow_add_eq_or_of_lt

shiftLeft and shiftRight

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.shiftLeft_mod_two_eq_one {x i : Nat} : x <<< i % 2 = 1 ↔ i = 0 ∧ x % 2 = 1

theorem Nat.testBit_mul_two_pow (x i n : Nat) : (x * 2 ^ n).testBit i = (decide (n ≤ i) && x.testBit (i - n))

theorem Nat.bitwise_mul_two_pow {f : Bool → Bool → Bool} {x y n : Nat} (of_false_false : f false false = false := by rfl) : bitwise f x y * 2 ^ n = bitwise f (x * 2 ^ n) (y * 2 ^ n)

theorem Nat.shiftLeft_bitwise_distrib {f : Bool → Bool → Bool} {i a b : Nat} (of_false_false : f false false = false := by rfl) : bitwise f a b <<< i = bitwise f (a <<< i) (b <<< i)

theorem Nat.shiftLeft_and_distrib {i a b : Nat} : (a &&& b) <<< i = a <<< i &&& b <<< i

theorem Nat.shiftLeft_or_distrib {i a b : Nat} : (a ||| b) <<< i = a <<< i ||| b <<< i

theorem Nat.shiftLeft_xor_distrib {i a b : Nat} : (a ^^^ b) <<< i = a <<< i ^^^ b <<< i

@[simp]

theorem Nat.decide_shiftRight_mod_two_eq_one {x i : Nat} : decide (x >>> i % 2 = 1) = x.testBit i

theorem Nat.shiftRight_bitwise_distrib {f : Bool → Bool → Bool} {i a b : Nat} (of_false_false : f false false = false := by rfl) : bitwise f a b >>> i = bitwise f (a >>> i) (b >>> i)

theorem Nat.shiftRight_and_distrib {i a b : Nat} : (a &&& b) >>> i = a >>> i &&& b >>> i

theorem Nat.shiftRight_or_distrib {i a b : Nat} : (a ||| b) >>> i = a >>> i ||| b >>> i

theorem Nat.shiftRight_xor_distrib {i a b : Nat} : (a ^^^ b) >>> i = a >>> i ^^^ b >>> i

theorem Nat.mod_two_pow_shiftLeft_mod_two_pow {a b c : Nat} : (a % 2 ^ c) <<< b % 2 ^ c = a <<< b % 2 ^ c

theorem Nat.le_shiftLeft {a b : Nat} : a ≤ a <<< b

theorem Nat.lt_of_shiftLeft_lt {a b c : Nat} (h : a <<< b < c) : a < c

le

theorem Nat.le_of_testBit {n m : Nat} (h : ∀ (i : Nat), n.testBit i = true → m.testBit i = true) : n ≤ m

theorem Nat.and_le_left {n m : Nat} : n &&& m ≤ n

theorem Nat.and_le_right {n m : Nat} : n &&& m ≤ m

theorem Nat.left_le_or {n m : Nat} : n ≤ n ||| m

theorem Nat.right_le_or {n m : Nat} : m ≤ n ||| m