Bitwise Lemmas

This module defines properties of the bitwise operations on natural numbers.

This file is complements Init.Data.Nat.Bitwise.Lemmas with properties that are not necessary for the bitvector library.

and

@[simp]

theorem Nat.and_self_left (a b : Nat) : a &&& (a &&& b) = a &&& b

@[simp]

theorem Nat.and_self_right (a b : Nat) : a &&& b &&& b = a &&& b

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

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

or

@[simp]

theorem Nat.or_self_left (a b : Nat) : a ||| (a ||| b) = a ||| b

@[simp]

theorem Nat.or_self_right (a b : Nat) : a ||| b ||| b = a ||| b

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

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

xor

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

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

@[simp]

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

@[simp]

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

theorem Nat.eq_of_xor_eq_zero {x y : Nat} : x ^^^ y = 0 → x = y

@[simp]

theorem Nat.xor_eq_zero_iff {x y : Nat} : x ^^^ y = 0 ↔ x = y

theorem Nat.xor_ne_zero_iff {x y : Nat} : x ^^^ y ≠ 0 ↔ x ≠ y

injectivity lemmas

theorem Nat.xor_right_injective {x : Nat} : Function.Injective fun (x_1 : Nat) => x ^^^ x_1

theorem Nat.xor_left_injective {x : Nat} : Function.Injective fun (x_1 : Nat) => x_1 ^^^ x

@[simp]

theorem Nat.xor_right_inj {x y z : Nat} : x ^^^ y = x ^^^ z ↔ y = z

@[simp]

theorem Nat.xor_left_inj {x y z : Nat} : x ^^^ z = y ^^^ z ↔ x = y

theorem Nat.and_or_right_injective {m x y : Nat} : x &&& m = y &&& m → x ||| m = y ||| m → x = y

theorem Nat.and_or_right_inj {m x y : Nat} : x &&& m = y &&& m ∧ x ||| m = y ||| m ↔ x = y

theorem Nat.and_or_left_injective {m x y : Nat} : m &&& x = m &&& y → m ||| x = m ||| y → x = y

theorem Nat.and_or_left_inj {m x y : Nat} : m &&& x = m &&& y ∧ m ||| x = m ||| y ↔ x = y