# Documentation

Mathlib.Init.Data.Nat.Bitwise

# Lemmas about bitwise operations on natural numbers. #

Possibly only of archaeological significance.

def Nat.boddDiv2 :

boddDiv2 n returns a 2-tuple of type (Bool,Nat) where the Bool value indicates whether n is odd or not and the Nat value returns ⌊n/2⌋

Equations
Instances For
def Nat.div2 (n : ) :

div2 n = ⌊n/2⌋ the greatest integer smaller than n/2

Instances For
def Nat.bodd (n : ) :

bodd n returns true if n is odd

Instances For
@[simp]
theorem Nat.bodd_zero :
@[simp]
theorem Nat.bodd_succ (n : ) :
@[simp]
theorem Nat.bodd_add (m : ) (n : ) :
Nat.bodd (m + n) = xor () ()
@[simp]
theorem Nat.bodd_mul (m : ) (n : ) :
Nat.bodd (m * n) = ()
theorem Nat.mod_two_of_bodd (n : ) :
n % 2 = bif then 1 else 0
@[simp]
theorem Nat.div2_zero :
= 0
theorem Nat.div2_one :
= 0
theorem Nat.div2_two :
= 1
@[simp]
theorem Nat.div2_succ (n : ) :
Nat.div2 () = bif then Nat.succ () else
theorem Nat.bodd_add_div2 (n : ) :
(bif then 1 else 0) + 2 * = n
theorem Nat.div2_val (n : ) :
= n / 2
def Nat.bit (b : Bool) :

bit b appends the digit b to the binary representation of its natural number input.

Instances For
theorem Nat.bit0_val (n : ) :
bit0 n = 2 * n
theorem Nat.bit1_val (n : ) :
bit1 n = 2 * n + 1
theorem Nat.bit_val (b : Bool) (n : ) :
Nat.bit b n = 2 * n + bif b then 1 else 0
theorem Nat.bit_decomp (n : ) :
Nat.bit () () = n
def Nat.bitCasesOn {C : Sort u} (n : ) (h : (b : Bool) → (n : ) → C (Nat.bit b n)) :
C n

For a predicate C : Nat → Sort*, if instances can be constructed for natural numbers of the form bit b n, they can be constructed for any given natural number.

Instances For
theorem Nat.bit_zero :
= 0
def Nat.shiftLeft' (b : Bool) (m : ) :

shiftLeft' b m n performs a left shift of m n times and adds the bit b as the least significant bit each time. Returns the corresponding natural number

Equations
Instances For
@[simp]
theorem Nat.shiftLeft'_false {m : } (n : ) :
= m <<< n
@[simp]
theorem Nat.shiftLeft_eq' (m : ) (n : ) :
= m <<< n

Std4 takes the unprimed name for Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n.

@[simp]
theorem Nat.shiftRight_eq (m : ) (n : ) :
= m >>> n
theorem Nat.shiftLeft_zero (m : ) :
m <<< 0 = m
theorem Nat.shiftLeft_succ (m : ) (n : ) :
m <<< (n + 1) = 2 * m <<< n
@[simp]
theorem Nat.shiftRight_zero {n : } :
n >>> 0 = n
@[simp]
theorem Nat.shiftRight_succ (m : ) (n : ) :
m >>> (n + 1) = m >>> n / 2
@[simp]
theorem Nat.zero_shiftRight (n : ) :
0 >>> n = 0
def Nat.testBit (m : ) (n : ) :

testBit m n returns whether the (n+1)ˢᵗ least significant bit is 1 or 0

Instances For
theorem Nat.binaryRec_decreasing {n : } (h : n 0) :
< n
def Nat.binaryRec {C : Sort u} (z : C 0) (f : (b : Bool) → (n : ) → C nC (Nat.bit b n)) (n : ) :
C n

A recursion principle for bit representations of natural numbers. For a predicate C : Nat → Sort*, if instances can be constructed for natural numbers of the form bit b n, they can be constructed for all natural numbers.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Nat.size :

size n : Returns the size of a natural number in bits i.e. the length of its binary representation

Instances For
def Nat.bits :

bits n returns a list of Bools which correspond to the binary representation of n

Instances For
def Nat.bitwise' (f : ) :

Nat.bitwise' (different from Nat.bitwise in Lean 4 core) applies the function f to pairs of bits in the same position in the binary representations of its inputs.

Instances For
def Nat.lor' :

lor' takes two natural numbers and returns their bitwise or

Instances For
def Nat.land' :

land' takes two naturals numbers and returns their and

Instances For
def Nat.ldiff' :

ldiff' a b performs bitwise set difference. For each corresponding pair of bits taken as booleans, say aᵢ and bᵢ, it applies the boolean operation aᵢ ∧ bᵢ to obtain the iᵗʰ bit of the result.

Instances For
def Nat.lxor' :

lxor' computes the bitwise xor of two natural numbers

Instances For
@[simp]
theorem Nat.binaryRec_zero {C : Sort u} (z : C 0) (f : (b : Bool) → (n : ) → C nC (Nat.bit b n)) :
= z

bitwise ops

theorem Nat.bodd_bit (b : Bool) (n : ) :
theorem Nat.div2_bit (b : Bool) (n : ) :
theorem Nat.shiftLeft'_add (b : Bool) (m : ) (n : ) (k : ) :
Nat.shiftLeft' b m (n + k) = Nat.shiftLeft' b () k
theorem Nat.shiftLeft_add (m : ) (n : ) (k : ) :
m <<< (n + k) = m <<< n <<< k
theorem Nat.shiftRight_add (m : ) (n : ) (k : ) :
m >>> (n + k) = m >>> n >>> k
theorem Nat.shiftLeft'_sub (b : Bool) (m : ) {n : } {k : } :
k nNat.shiftLeft' b m (n - k) = >>> k
theorem Nat.shiftLeft_sub (m : ) {n : } {k : } :
k nm <<< (n - k) = m <<< n >>> k
@[simp]
theorem Nat.testBit_zero (b : Bool) (n : ) :
theorem Nat.testBit_succ (m : ) (b : Bool) (n : ) :
theorem Nat.binaryRec_eq {C : Sort u} {z : C 0} {f : (b : Bool) → (n : ) → C nC (Nat.bit b n)} (h : f false 0 z = z) (b : Bool) (n : ) :
Nat.binaryRec z f (Nat.bit b n) = f b n ()
theorem Nat.bitwise'_bit_aux {f : } (h : ) :
(Nat.binaryRec (bif then else 0) fun b n x => Nat.bit (f false b) (bif then n else 0)) = fun n => bif then n else 0
theorem Nat.bitwise'_zero_left (f : ) (n : ) :
Nat.bitwise' f 0 n = bif then n else 0
@[simp]
theorem Nat.bitwise'_zero_right (f : ) (h : ) (m : ) :
Nat.bitwise' f m 0 = bif then m else 0
@[simp]
theorem Nat.bitwise'_zero (f : ) :
Nat.bitwise' f 0 0 = 0
@[simp]
theorem Nat.bitwise'_bit {f : } (h : ) (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.bitwise' f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise' f m n)
theorem Nat.bitwise'_swap {f : } (h : ) :
@[simp]
theorem Nat.lor'_bit (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.lor' (Nat.bit a m) (Nat.bit b n) = Nat.bit (a || b) (Nat.lor' m n)
@[simp]
theorem Nat.land'_bit (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.land' (Nat.bit a m) (Nat.bit b n) = Nat.bit (a && b) ()
@[simp]
theorem Nat.ldiff'_bit (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.ldiff' (Nat.bit a m) (Nat.bit b n) = Nat.bit (a && !b) ()
@[simp]
theorem Nat.lxor'_bit (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.lxor' (Nat.bit a m) (Nat.bit b n) = Nat.bit (xor a b) ()
@[simp]
theorem Nat.testBit_bitwise' {f : } (h : ) (m : ) (n : ) (k : ) :
Nat.testBit (Nat.bitwise' f m n) k = f () ()
@[simp]
theorem Nat.testBit_lor' (m : ) (n : ) (k : ) :
Nat.testBit (Nat.lor' m n) k = ( || )
@[simp]
theorem Nat.testBit_land' (m : ) (n : ) (k : ) :
Nat.testBit () k = ( && )
@[simp]
theorem Nat.testBit_ldiff' (m : ) (n : ) (k : ) :
Nat.testBit () k = ( && !)
@[simp]
theorem Nat.testBit_lxor' (m : ) (n : ) (k : ) :
Nat.testBit () k = xor () ()