Init.Data.Nat.Bitwise.Basic

Nat.bitwise_rec_lemma theorem

{n : Nat} (hNe : n ≠ 0) : n / 2 < n

Full source

theorem bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n :=
  Nat.div_lt_self (Nat.zero_lt_of_ne_zero hNe) (Nat.lt_succ_self _)

Floor Division by Two Decreases Nonzero Natural Numbers

Informal description

For any nonzero natural number $n$, the floor division of $n$ by $2$ is strictly less than $n$, i.e., $n / 2 < n$.

Nat.bitwise definition

(f : Bool → Bool → Bool) (n m : Nat) : Nat

Full source

/--
A helper for implementing bitwise operators on `Nat`.

Each bit of the resulting `Nat` is the result of applying `f` to the corresponding bits of the input
`Nat`s, up to the position of the highest set bit in either input.
-/
def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
  if n = 0 then
    if f false true then m else 0
  else if m = 0 then
    if f true false then n else 0
  else
    let n' := n / 2
    let m' := m / 2
    let b₁ := n % 2 = 1
    let b₂ := m % 2 = 1
    let r  := bitwise f n' m'
    if f b₁ b₂ then
      r+r+1
    else
      r+r
decreasing_by apply bitwise_rec_lemma; assumption

Bitwise operation on natural numbers

Informal description

The function `Nat.bitwise` takes a binary Boolean function $f$ and two natural numbers $n$ and $m$, and returns a new natural number constructed by applying $f$ to each corresponding pair of bits in the binary representations of $n$ and $m$. The operation proceeds recursively, halving the numbers at each step until one of them becomes zero. The resulting number is built by combining the results of $f$ applied to the least significant bits of $n$ and $m$ at each step.

Nat.land definition

: @& Nat → @& Nat → Nat

Full source

/--
Bitwise and. Usually accessed via the `&&&` operator.

Each bit of the resulting value is set if the corresponding bit is set in both of the inputs.
-/
@[extern "lean_nat_land"]
def land : @& Nat → @& Nat → Nat := bitwise and

Bitwise logical AND of natural numbers

Informal description

The function `Nat.land` computes the bitwise logical AND of two natural numbers $n$ and $m$. For each bit position, the corresponding bit in the result is set to 1 if both of the corresponding bits in $n$ and $m$ are 1, and 0 otherwise.

Nat.lor definition

: @& Nat → @& Nat → Nat

Full source

/--
Bitwise or. Usually accessed via the `|||` operator.

Each bit of the resulting value is set if the corresponding bit is set in at least one of the inputs.
-/
@[extern "lean_nat_lor"]
def lor  : @& Nat → @& Nat → Nat := bitwise or

Bitwise logical OR of natural numbers

Informal description

The function `Nat.lor` computes the bitwise logical OR of two natural numbers $n$ and $m$. For each bit position, the corresponding bit in the result is set to 1 if at least one of the corresponding bits in $n$ or $m$ is 1, and 0 otherwise.

Nat.xor definition

: @& Nat → @& Nat → Nat

Full source

/--
Bitwise exclusive or. Usually accessed via the `^^^` operator.

Each bit of the resulting value is set if the corresponding bit is set in exactly one of the inputs.
-/
@[extern "lean_nat_lxor"]
def xor  : @& Nat → @& Nat → Nat := bitwise bne

Bitwise XOR of natural numbers

Informal description

The function `Nat.xor` computes the bitwise exclusive OR (XOR) of two natural numbers $n$ and $m$. For each bit position, the corresponding bit in the result is set to 1 if exactly one of the corresponding bits in $n$ or $m$ is 1, and 0 otherwise. This is implemented using the `Nat.bitwise` function with the boolean not-equal operation `bne` as the combining function.

Nat.shiftLeft definition

: @& Nat → @& Nat → Nat

Full source

/--
Shifts the binary representation of a value left by the specified number of bits. Usually accessed
via the `<<<` operator.

Examples:
 * `1 <<< 2 = 4`
 * `1 <<< 3 = 8`
 * `0 <<< 3 = 0`
 * `0xf1 <<< 4 = 0xf10`
-/
@[extern "lean_nat_shiftl"]
def shiftLeft : @& Nat → @& Nat → Nat
  | n, 0 => n
  | n, succ m => shiftLeft (2*n) m

Left bit shift on natural numbers

Informal description

The function `Nat.shiftLeft` takes two natural numbers `n` and `m` and returns the result of shifting the binary representation of `n` left by `m` bits. This is equivalent to multiplying `n` by `2^m`. The function is defined recursively: shifting by 0 returns `n` unchanged, and shifting by `m+1` is equivalent to shifting `2*n` by `m`. Examples: - `1 <<< 2 = 4` - `1 <<< 3 = 8` - `0 <<< 3 = 0` - `0xf1 <<< 4 = 0xf10`

Nat.shiftRight definition

: @& Nat → @& Nat → Nat

Full source

/--
Shifts the binary representation of a value right by the specified number of bits. Usually accessed
via the `>>>` operator.

Examples:
 * `4 >>> 2 = 1`
 * `8 >>> 2 = 2`
 * `8 >>> 3 = 1`
 * `0 >>> 3 = 0`
 * `0xf13a >>> 8 = 0xf1`
-/
@[extern "lean_nat_shiftr"]
def shiftRight : @& Nat → @& Nat → Nat
  | n, 0 => n
  | n, succ m => shiftRight n m / 2

Right bit shift on natural numbers

Informal description

The function `Nat.shiftRight` takes two natural numbers `n` and `m` and returns the result of shifting the binary representation of `n` right by `m` bits. This is equivalent to performing floor division of `n` by `2^m`. The function is defined recursively: shifting by 0 returns `n` unchanged, and shifting by `m+1` is equivalent to shifting `n` by `m` and then dividing by 2 (i.e., performing a right shift by one more bit). Examples: - `4 >>> 2 = 1` - `8 >>> 2 = 2` - `8 >>> 3 = 1` - `0 >>> 3 = 0` - `0xf13a >>> 8 = 0xf1`

Nat.instAndOp instance

: AndOp Nat

Full source

instance : AndOp Nat := ⟨Nat.land⟩

Bitwise AND Operation on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical homogeneous logical AND operation, which performs bitwise AND on their binary representations.

Nat.instOrOp instance

: OrOp Nat

Full source

instance : OrOp Nat := ⟨Nat.lor⟩

Bitwise OR Operation on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical homogeneous logical OR operation, which performs bitwise OR on their binary representations.

Nat.instXor instance

: Xor Nat

Full source

instance : Xor Nat := ⟨Nat.xor⟩

Bitwise XOR Operation on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical homogeneous exclusive OR (XOR) operation, which performs bitwise XOR on their binary representations.

Nat.instShiftLeft instance

: ShiftLeft Nat

Full source

instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩

Left Shift Operation on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical left shift operation, which performs a bitwise left shift on their binary representations. Specifically, for any natural numbers $n$ and $m$, the operation $n \ll m$ is equivalent to multiplying $n$ by $2^m$.

Nat.instShiftRight instance

: ShiftRight Nat

Full source

instance : ShiftRight Nat := ⟨Nat.shiftRight⟩

Right Shift Operation on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical right shift operation, which performs a bitwise right shift on their binary representations. Specifically, for any natural numbers $n$ and $m$, the operation $n \gg m$ is equivalent to floor division of $n$ by $2^m$.

Nat.shiftLeft_eq theorem

(a b : Nat) : a <<< b = a * 2 ^ b

Full source

theorem shiftLeft_eq (a b : Nat) : a <<< b = a * 2 ^ b :=
  match b with
  | 0 => (Nat.mul_one _).symm
  | b+1 => (shiftLeft_eq _ b).trans <| by
    simp [Nat.pow_succ, Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm]

Left Shift Equals Multiplication by Power of Two: $a \ll b = a \times 2^b$

Informal description

For any natural numbers $a$ and $b$, the left shift operation $a \ll b$ is equal to $a$ multiplied by $2^b$, i.e., $a \ll b = a \times 2^b$.

Nat.shiftRight_zero theorem

: n >>> 0 = n

Full source

@[simp] theorem shiftRight_zero : n >>> 0 = n := rfl

Right Shift by Zero Preserves Natural Number

Informal description

For any natural number $n$, the right shift operation by zero bits leaves $n$ unchanged, i.e., $n \gg 0 = n$.

Nat.shiftRight_succ theorem

(m n) : m >>> (n + 1) = (m >>> n) / 2

Full source

theorem shiftRight_succ (m n) : m >>> (n + 1) = (m >>> n) / 2 := rfl

Recursive Right Shift Property: $m \gg (n + 1) = (m \gg n) / 2$

Informal description

For any natural numbers $m$ and $n$, the right shift operation applied to $m$ with shift amount $n+1$ is equal to the right shift of $m$ by $n$ divided by 2, i.e., $m \gg (n + 1) = (m \gg n) / 2$.

Nat.shiftRight_add theorem

(m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k

Full source

theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
  | 0 => rfl
  | k + 1 => by simp [← Nat.add_assoc, shiftRight_add _ _ k, shiftRight_succ]

Additivity of Right Shift Operation on Natural Numbers: $m \gg (n + k) = (m \gg n) \gg k$

Informal description

For any natural numbers $m$ and $n$, and for any natural number $k$, the right shift operation satisfies $m \gg (n + k) = (m \gg n) \gg k$, where $\gg$ denotes the bitwise right shift operation.

Nat.shiftRight_eq_div_pow theorem

(m : Nat) : ∀ n, m >>> n = m / 2 ^ n

Full source

theorem shiftRight_eq_div_pow (m : Nat) : ∀ n, m >>> n = m / 2 ^ n
  | 0 => (Nat.div_one _).symm
  | k + 1 => by
    rw [shiftRight_add, shiftRight_eq_div_pow m k]
    simp [Nat.div_div_eq_div_mul, ← Nat.pow_succ, shiftRight_succ]

Right Shift Equals Division by Power of Two: $m \gg n = m / 2^n$

Informal description

For any natural numbers $m$ and $n$, the right shift operation $m \gg n$ is equal to the floor division of $m$ by $2^n$, i.e., $m \gg n = \lfloor m / 2^n \rfloor$.

Nat.shiftRight_eq_zero theorem

(m n : Nat) (hn : m < 2 ^ n) : m >>> n = 0

Full source

theorem shiftRight_eq_zero (m n : Nat) (hn : m < 2^n) : m >>> n = 0 := by
  simp [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt hn]

Right Shift Yields Zero for Small Numbers: $m < 2^n \Rightarrow m \gg n = 0$

Informal description

For any natural numbers $m$ and $n$ such that $m < 2^n$, the right shift operation $m \gg n$ equals zero.

Nat.shiftRight_le theorem

(m n : Nat) : m >>> n ≤ m

Full source

theorem shiftRight_le (m n : Nat) : m >>> n ≤ m := by
  simp only [shiftRight_eq_div_pow]
  apply Nat.div_le_self

Right Shift Preserves Upper Bound: $m \gg n \leq m$

Informal description

For any natural numbers $m$ and $n$, the result of right-shifting $m$ by $n$ bits is less than or equal to $m$, i.e., $m \gg n \leq m$.

Nat.testBit definition

(m n : Nat) : Bool

Full source

/--
Returns `true` if the `(n+1)`th least significant bit is `1`, or `false` if it is `0`.
-/
def testBit (m n : Nat) : Bool :=
  -- `1 &&& n` is faster than `n &&& 1` for big `n`.
  1 &&& (m >>> n) != 0

Test if the `(n+1)`-th least significant bit is set

Informal description

The function `testBit` takes two natural numbers `m` and `n` and returns `true` if the `(n+1)`-th least significant bit in the binary representation of `m` is `1`, and `false` otherwise. This is computed by right-shifting `m` by `n` positions and checking if the least significant bit of the result is `1`.