Lemmas about bitwise operations on natural numbers.

Possibly only of archaeological significance.

ink

def Nat.boddDiv2 : ℕ → Bool × ℕ

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

• Nat.boddDiv2 0 = (false, 0)
• Nat.boddDiv2 (Nat.succ n) = match Nat.boddDiv2 n with | (false, m) => (true, m) | (true, m) => (false, Nat.succ m)

ink

def Nat.div2 (n : ℕ) : ℕ

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

Equations

• Nat.div2 n = (Nat.boddDiv2 n).snd

ink

def Nat.bodd (n : ℕ) : Bool

bodd n returns true if n is odd

Equations

• Nat.bodd n = (Nat.boddDiv2 n).fst

ink

@[simp]

theorem Nat.bodd_zero : Nat.bodd 0 = false

ink

theorem Nat.bodd_one : Nat.bodd 1 = true

ink

theorem Nat.bodd_two : Nat.bodd 2 = false

ink

@[simp]

theorem Nat.bodd_succ (n : ℕ) : Nat.bodd (Nat.succ n) = !Nat.bodd n

ink

@[simp]

theorem Nat.bodd_add (m : ℕ) (n : ℕ) : Nat.bodd (m + n) = xor (Nat.bodd m) (Nat.bodd n)

ink

@[simp]

theorem Nat.bodd_mul (m : ℕ) (n : ℕ) : Nat.bodd (m * n) = (Nat.bodd m && Nat.bodd n)

ink

theorem Nat.mod_two_of_bodd (n : ℕ) : n % 2 = bif Nat.bodd n then 1 else 0

ink

@[simp]

theorem Nat.div2_zero : Nat.div2 0 = 0

ink

theorem Nat.div2_one : Nat.div2 1 = 0

ink

theorem Nat.div2_two : Nat.div2 2 = 1

ink

@[simp]

theorem Nat.div2_succ (n : ℕ) : Nat.div2 (Nat.succ n) = bif Nat.bodd n then Nat.succ (Nat.div2 n) else Nat.div2 n

ink

theorem Nat.bodd_add_div2 (n : ℕ) : (bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n = n

ink

theorem Nat.div2_val (n : ℕ) : Nat.div2 n = n / 2

ink

def Nat.bit (b : Bool) : ℕ → ℕ

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

Equations

• Nat.bit b = bif b then bit1 else bit0

ink

theorem Nat.bit0_val (n : ℕ) : bit0 n = 2 * n

ink

theorem Nat.bit1_val (n : ℕ) : bit1 n = 2 * n + 1

ink

theorem Nat.bit_val (b : Bool) (n : ℕ) : Nat.bit b n = 2 * n + bif b then 1 else 0

ink

theorem Nat.bit_decomp (n : ℕ) : Nat.bit (Nat.bodd n) (Nat.div2 n) = n

ink

def Nat.bitCasesOn {C : ℕ → Sort u} (n : ℕ) (h : (b : Bool) → (n : ℕ) → C (Nat.bit b n)) : C n

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

Equations

• Nat.bitCasesOn n h = (_ : Nat.bit (Nat.bodd n) (Nat.div2 n) = n) ▸ h (Nat.bodd n) (Nat.div2 n)

ink

theorem Nat.bit_zero : Nat.bit false 0 = 0

ink

def Nat.shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ

shiftl' 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

• Nat.shiftl' b m 0 = m
• Nat.shiftl' b m (Nat.succ n) = Nat.bit b (Nat.shiftl' b m n)

ink

def Nat.shiftl : ℕ → ℕ → ℕ

shiftl m n produces a natural number whose binary representation is obtained by left-shifting the binary representation of m by n places

Equations

• Nat.shiftl = Nat.shiftl' false

ink

@[simp]

theorem Nat.shiftl_zero (m : ℕ) : Nat.shiftl m 0 = m

ink

@[simp]

theorem Nat.shiftl_succ (m : ℕ) (n : ℕ) : Nat.shiftl m (n + 1) = bit0 (Nat.shiftl m n)

ink

def Nat.shiftr : ℕ → ℕ → ℕ

shiftr n m performs returns the m-step right shift operation on n and returns the resultant number. This is equivalent to performing ⌊n/2ᵐ⌋

Equations

• Nat.shiftr x 0 = x
• Nat.shiftr x (Nat.succ n) = Nat.div2 (Nat.shiftr x n)

ink

theorem Nat.shiftr_zero (n : ℕ) : Nat.shiftr 0 n = 0

ink

def Nat.testBit (m : ℕ) (n : ℕ) : Bool

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

Equations

• Nat.testBit m n = Nat.bodd (Nat.shiftr m n)

ink

theorem Nat.binaryRec_decreasing {n : ℕ} (h : n ≠ 0) : Nat.div2 n < n

ink

def Nat.binaryRec {C : ℕ → Sort u} (z : C 0) (f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)) (n : ℕ) : C n

A recursion principle for bit representations of natural numbers. For a predicate C : Nat → Sort _→ 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.

ink

def Nat.size : ℕ → ℕ

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

Equations

• Nat.size = Nat.binaryRec 0 fun x x => Nat.succ

ink

def Nat.bits : ℕ → List Bool

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

Equations

• Nat.bits = Nat.binaryRec [] fun b x IH => b :: IH

ink

def Nat.bitwise' (f : Bool → Bool → Bool) : ℕ → ℕ → ℕ

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.

Equations

• Nat.bitwise' f = Nat.binaryRec (fun n => bif f false true then n else 0) fun a m Ia => Nat.binaryRec (bif f true false then Nat.bit a m else 0) fun b n x => Nat.bit (f a b) (Ia n)

ink

def Nat.lor' : ℕ → ℕ → ℕ

lor' takes two natural numbers and returns their bitwise or

Equations

• Nat.lor' = Nat.bitwise' or

ink

def Nat.land' : ℕ → ℕ → ℕ

land' takes two naturals numbers and returns their and

Equations

• Nat.land' = Nat.bitwise' and

ink

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ᵢ∧ bᵢ to obtain the iᵗʰ bit of the result.

Equations

• Nat.ldiff' = Nat.bitwise' fun a b => a && !b

ink

def Nat.lxor' : ℕ → ℕ → ℕ

lxor' computes the bitwise xor of two natural numbers

Equations

• Nat.lxor' = Nat.bitwise' xor

ink

@[simp]

theorem Nat.binaryRec_zero {C : ℕ → Sort u} (z : C 0) (f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)) : Nat.binaryRec z f 0 = z

bitwise ops

ink

theorem Nat.bodd_bit (b : Bool) (n : ℕ) : Nat.bodd (Nat.bit b n) = b

ink

theorem Nat.div2_bit (b : Bool) (n : ℕ) : Nat.div2 (Nat.bit b n) = n

ink

theorem Nat.shiftl'_add (b : Bool) (m : ℕ) (n : ℕ) (k : ℕ) : Nat.shiftl' b m (n + k) = Nat.shiftl' b (Nat.shiftl' b m n) k

ink

theorem Nat.shiftl_add (m : ℕ) (n : ℕ) (k : ℕ) : Nat.shiftl m (n + k) = Nat.shiftl (Nat.shiftl m n) k

ink

theorem Nat.shiftr_add (m : ℕ) (n : ℕ) (k : ℕ) : Nat.shiftr m (n + k) = Nat.shiftr (Nat.shiftr m n) k

ink

theorem Nat.shiftl'_sub (b : Bool) (m : ℕ) {n : ℕ} {k : ℕ} : k ≤ n → Nat.shiftl' b m (n - k) = Nat.shiftr (Nat.shiftl' b m n) k

ink

theorem Nat.shiftl_sub (m : ℕ) {n : ℕ} {k : ℕ} : k ≤ n → Nat.shiftl m (n - k) = Nat.shiftr (Nat.shiftl m n) k

ink

@[simp]

theorem Nat.testBit_zero (b : Bool) (n : ℕ) : Nat.testBit (Nat.bit b n) 0 = b

ink

theorem Nat.testBit_succ (m : ℕ) (b : Bool) (n : ℕ) : Nat.testBit (Nat.bit b n) (Nat.succ m) = Nat.testBit n m

ink

theorem Nat.binaryRec_eq {C : ℕ → Sort u} {z : C 0} {f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)} (h : f false 0 z = z) (b : Bool) (n : ℕ) : Nat.binaryRec z f (Nat.bit b n) = f b n (Nat.binaryRec z f n)

ink

theorem Nat.bitwise'_bit_aux {f : Bool → Bool → Bool} (h : f false false = false) : (Nat.binaryRec (bif f true false then Nat.bit false 0 else 0) fun b n x => Nat.bit (f false b) (bif f false true then n else 0)) = fun n => bif f false true then n else 0

ink

theorem Nat.bitwise'_zero_left (f : Bool → Bool → Bool) (n : ℕ) : Nat.bitwise' f 0 n = bif f false true then n else 0

ink

@[simp]

theorem Nat.bitwise'_zero_right (f : Bool → Bool → Bool) (h : f false false = false) (m : ℕ) : Nat.bitwise' f m 0 = bif f true false then m else 0

ink

@[simp]

theorem Nat.bitwise'_zero (f : Bool → Bool → Bool) : Nat.bitwise' f 0 0 = 0

ink

@[simp]

theorem Nat.bitwise'_bit {f : Bool → Bool → Bool} (h : f false false = false) (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)

ink

theorem Nat.bitwise'_swap {f : Bool → Bool → Bool} (h : f false false = false) : Nat.bitwise' (Function.swap f) = Function.swap (Nat.bitwise' f)

ink

@[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)

ink

@[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) (Nat.land' m n)

ink

@[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) (Nat.ldiff' m n)

ink

@[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) (Nat.lxor' m n)

ink

@[simp]

theorem Nat.testBit_bitwise' {f : Bool → Bool → Bool} (h : f false false = false) (m : ℕ) (n : ℕ) (k : ℕ) : Nat.testBit (Nat.bitwise' f m n) k = f (Nat.testBit m k) (Nat.testBit n k)

ink

@[simp]

theorem Nat.testBit_lor' (m : ℕ) (n : ℕ) (k : ℕ) : Nat.testBit (Nat.lor' m n) k = (Nat.testBit m k || Nat.testBit n k)

ink

@[simp]

theorem Nat.testBit_land' (m : ℕ) (n : ℕ) (k : ℕ) : Nat.testBit (Nat.land' m n) k = (Nat.testBit m k && Nat.testBit n k)

ink

@[simp]

theorem Nat.testBit_ldiff' (m : ℕ) (n : ℕ) (k : ℕ) : Nat.testBit (Nat.ldiff' m n) k = (Nat.testBit m k && !Nat.testBit n k)

ink

@[simp]

theorem Nat.testBit_lxor' (m : ℕ) (n : ℕ) (k : ℕ) : Nat.testBit (Nat.lxor' m n) k = xor (Nat.testBit m k) (Nat.testBit n k)