Documentation

Mathlib.Data.Nat.Bitwise

Bitwise operations on natural numbers #

In the first half of this file, we provide theorems for reasoning about natural numbers from their bitwise properties. In the second half of this file, we show properties of the bitwise operations lor, land and xor, which are defined in core.

Main results #

Future work #

There is another way to express bitwise properties of natural number: digits 2. The two ways should be connected.

Keywords #

bitwise, and, or, xor

@[simp]
theorem Nat.bitwise_zero_left {f : BoolBoolBool} (m : ) :
Nat.bitwise f 0 m = if f false true = true then m else 0
@[simp]
theorem Nat.bitwise_zero_right {f : BoolBoolBool} (n : ) :
Nat.bitwise f n 0 = if f true false = true then n else 0
theorem Nat.bitwise_zero {f : BoolBoolBool} :
Nat.bitwise f 0 0 = 0
theorem Nat.bitwise_of_ne_zero {f : BoolBoolBool} {n : } {m : } (hn : n 0) (hm : m 0) :
Nat.bitwise f n m = Nat.bit (f n.bodd m.bodd) (Nat.bitwise f (n / 2) (m / 2))
theorem Nat.binaryRec_of_ne_zero {C : Sort u_1} (z : C 0) (f : (b : Bool) → (n : ) → C nC (Nat.bit b n)) {n : } (h : n 0) :
Nat.binaryRec z f n = f n.bodd n.div2 (Nat.binaryRec z f n.div2)
@[simp]
theorem Nat.bitwise_bit {f : BoolBoolBool} (h : autoParam (f false false = false) _auto✝) (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.bit_mod_two (a : Bool) (x : ) :
Nat.bit a x % 2 = if a = true then 1 else 0
@[simp]
theorem Nat.bit_mod_two_eq_zero_iff (a : Bool) (x : ) :
Nat.bit a x % 2 = 0 (!a) = true
@[simp]
theorem Nat.bit_mod_two_eq_one_iff (a : Bool) (x : ) :
Nat.bit a x % 2 = 1 a = true
@[simp]
theorem Nat.lor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.bit a m ||| Nat.bit b n = Nat.bit (a || b) (m ||| n)
@[simp]
theorem Nat.land_bit (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.bit a m &&& Nat.bit b n = Nat.bit (a && b) (m &&& n)
@[simp]
theorem Nat.ldiff_bit (a : Bool) (m : ) (b : Bool) (n : ) :
(Nat.bit a m).ldiff (Nat.bit b n) = Nat.bit (a && !b) (m.ldiff n)
@[simp]
theorem Nat.xor_bit (a : Bool) (m : ) (b : Bool) (n : ) :
Nat.bit a m ^^^ Nat.bit b n = Nat.bit (a != b) (m ^^^ n)
theorem Nat.testBit_lor (m : ) (n : ) (k : ) :
(m ||| n).testBit k = (m.testBit k || n.testBit k)
theorem Nat.testBit_land (m : ) (n : ) (k : ) :
(m &&& n).testBit k = (m.testBit k && n.testBit k)
@[simp]
theorem Nat.testBit_ldiff (m : ) (n : ) (k : ) :
(m.ldiff n).testBit k = (m.testBit k && !n.testBit k)
@[simp]
theorem Nat.bit_false :
Nat.bit false = fun (x : ) => 2 * x
@[simp]
theorem Nat.bit_true :
Nat.bit true = fun (x : ) => 2 * x + 1
@[simp]
theorem Nat.bit_eq_zero {n : } {b : Bool} :
Nat.bit b n = 0 n = 0 b = false
theorem Nat.bit_ne_zero_iff {n : } {b : Bool} :
Nat.bit b n 0 n = 0b = true
theorem Nat.bitwise_bit' {f : BoolBoolBool} (a : Bool) (m : ) (b : Bool) (n : ) (ham : m = 0a = true) (hbn : n = 0b = true) :
Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)

An alternative for bitwise_bit which replaces the f false false = false assumption with assumptions that neither bit a m nor bit b n are 0 (albeit, phrased as the implications m = 0 → a = true and n = 0 → b = true)

theorem Nat.bitwise_eq_binaryRec (f : BoolBoolBool) :
Nat.bitwise f = Nat.binaryRec (fun (n : ) => bif f false true then n else 0) fun (a : Bool) (m : ) (Ia : ) => Nat.binaryRec (bif f true false then Nat.bit a m else 0) fun (b : Bool) (n x : ) => Nat.bit (f a b) (Ia n)
theorem Nat.zero_of_testBit_eq_false {n : } (h : ∀ (i : ), n.testBit i = false) :
n = 0
theorem Nat.testBit_eq_false_of_lt {n : } {i : } (h : n < 2 ^ i) :
n.testBit i = false
theorem Nat.testBit_eq_inth (n : ) (i : ) :
n.testBit i = n.bits.getI i

The ith bit is the ith element of n.bits.

theorem Nat.exists_most_significant_bit {n : } (h : n 0) :
∃ (i : ), n.testBit i = true ∀ (j : ), i < jn.testBit j = false
theorem Nat.lt_of_testBit {n : } {m : } (i : ) (hn : n.testBit i = false) (hm : m.testBit i = true) (hnm : ∀ (j : ), i < jn.testBit j = m.testBit j) :
n < m
theorem Nat.bitwise_comm {f : BoolBoolBool} (hf : ∀ (b b' : Bool), f b b' = f b' b) (n : ) (m : ) :

If f is a commutative operation on bools such that f false false = false, then bitwise f is also commutative.

theorem Nat.lor_comm (n : ) (m : ) :
n ||| m = m ||| n
theorem Nat.land_comm (n : ) (m : ) :
n &&& m = m &&& n
theorem Nat.and_two_pow (n : ) (i : ) :
n &&& 2 ^ i = (n.testBit i).toNat * 2 ^ i
theorem Nat.two_pow_and (n : ) (i : ) :
2 ^ i &&& n = 2 ^ i * (n.testBit i).toNat

Proving associativity of bitwise operations in general essentially boils down to a huge case distinction, so it is shorter to use this tactic instead of proving it in the general case.

Equations
Instances For
    theorem Nat.land_assoc (n : ) (m : ) (k : ) :
    n &&& m &&& k = n &&& (m &&& k)
    theorem Nat.lor_assoc (n : ) (m : ) (k : ) :
    n ||| m ||| k = n ||| (m ||| k)
    theorem Nat.xor_cancel_right (n : ) (m : ) :
    m ^^^ n ^^^ n = m
    theorem Nat.xor_cancel_left (n : ) (m : ) :
    n ^^^ (n ^^^ m) = m
    @[simp]
    theorem Nat.xor_right_inj {n : } {m : } {m' : } :
    n ^^^ m = n ^^^ m' m = m'
    @[simp]
    theorem Nat.xor_left_inj {n : } {m : } {m' : } :
    m ^^^ n = m' ^^^ n m = m'
    @[simp]
    theorem Nat.xor_eq_zero {n : } {m : } :
    n ^^^ m = 0 n = m
    theorem Nat.xor_ne_zero {n : } {m : } :
    n ^^^ m 0 n m
    theorem Nat.xor_trichotomy {a : } {b : } {c : } (h : a ^^^ b ^^^ c 0) :
    b ^^^ c < a c ^^^ a < b a ^^^ b < c
    theorem Nat.lt_xor_cases {a : } {b : } {c : } (h : a < b ^^^ c) :
    a ^^^ c < b a ^^^ b < c
    @[simp]
    theorem Nat.bit_lt_two_pow_succ_iff {b : Bool} {x : } {n : } :
    Nat.bit b x < 2 ^ (n + 1) x < 2 ^ n
    theorem Nat.bitwise_lt {f : BoolBoolBool} {x : } {y : } {n : } (hx : x < 2 ^ n) (hy : y < 2 ^ n) :
    Nat.bitwise f x y < 2 ^ n

    If x and y fit within n bits, then the result of any bitwise operation on x and y also fits within n bits

    theorem Nat.shiftLeft_lt {x : } {n : } {m : } (h : x < 2 ^ n) :
    x <<< m < 2 ^ (n + m)
    theorem Nat.append_lt {x : } {y : } {n : } {m : } (hx : x < 2 ^ n) (hy : y < 2 ^ m) :
    y <<< n ||| x < 2 ^ (n + m)

    Note that the LHS is the expression used within Std.BitVec.append, hence the name.