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 division by two.

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) : 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 : Nat) (i : Nat) : x.testBit i.succ = (x / 2).testBit i

theorem Nat.testBit_add_one (x : Nat) (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_div_two (x : Nat) (i : Nat) : (x / 2).testBit i = x.testBit (i + 1)

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

theorem Nat.toNat_testBit (x : Nat) (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 : Nat} {y : Nat} (p : x ≠ y) : ∃ (i : Nat), x.testBit i ≠ y.testBit i

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

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

theorem Nat.testBit_lt_two_pow {x : Nat} {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 : Nat) (i : Nat) : (2 ^ i + x).testBit i = !x.testBit i

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

theorem Nat.testBit_two_pow_add_gt {i : Nat} {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 : Nat) (j : Nat) (i : Nat) : (x % 2 ^ j).testBit i = (decide (i < j) && x.testBit i)

theorem Nat.testBit_one_zero : Nat.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 : Nat} {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 : Nat) (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} : Nat.testBit 1 i = true ↔ i = 0

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

theorem Nat.testBit_two_pow {n : Nat} {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 : Nat} {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 : Nat} {j : Nat} : x % 2 ^ j % 2 = 1 ↔ 0 < j ∧ x % 2 = 1

bitwise

theorem Nat.testBit_bitwise {f : Bool → Bool → Bool} (false_false_axiom : f false false = false) (x : Nat) (y : Nat) (i : Nat) : (Nat.bitwise f x y).testBit i = f (x.testBit i) (y.testBit 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) : (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 : Nat) (y : Nat) : x &&& y = y &&& x

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

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

Equations

• Nat.instAssociativeHAnd = ⋯

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

Equations

• Nat.instCommutativeHAnd = ⋯

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

Equations

• Nat.instIdempotentOpHAnd = ⋯

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_sub_one_eq_mod (x : Nat) (n : Nat) : x &&& 2 ^ n - 1 = x % 2 ^ n

@[reducible, inline, deprecated Nat.and_pow_two_sub_one_eq_mod]

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

Equations

• Nat.and_pow_two_is_mod = Nat.and_pow_two_sub_one_eq_mod

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

@[reducible, inline, deprecated Nat.and_pow_two_sub_one_of_lt_two_pow]

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

Equations

• @Nat.and_two_pow_identity = @Nat.and_pow_two_sub_one_of_lt_two_pow

@[simp]

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

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

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 : Nat) (y : Nat) (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 : Nat) (y : Nat) : x ||| y = y ||| x

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

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

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

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

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

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

Equations

• Nat.instAssociativeHOr = ⋯

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

Equations

• Nat.instCommutativeHOr = ⋯

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

Equations

• Nat.instIdempotentOpHOr = ⋯

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

Equations

• Nat.instLawfulCommIdentityHOrOfNat = ⋯

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

@[simp]

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

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

xor

@[simp]

theorem Nat.testBit_xor (x : Nat) (y : Nat) (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 : Nat) (y : Nat) : x ^^^ y = y ^^^ x

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

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

Equations

• Nat.instAssociativeHXor = ⋯

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

Equations

• Nat.instCommutativeHXor = ⋯

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

Equations

• Nat.instLawfulCommIdentityHXorOfNat = ⋯

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

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

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

@[simp]

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

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

Arithmetic

theorem Nat.testBit_mul_pow_two_add (a : Nat) {b : Nat} {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)

theorem Nat.testBit_mul_pow_two {i : Nat} {a : Nat} {j : Nat} : (2 ^ i * a).testBit j = (decide (j ≥ i) && a.testBit (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) : (x <<< i).testBit j = (decide (j ≥ i) && x.testBit (j - i))

@[simp]

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

@[simp]

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

@[simp]

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

le

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

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

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