Documentation

Init.Data.Nat.Bitwise.Lemmas

Preliminaries #

noncomputable def Nat.div2Induction {motive : NatSort u} (n : Nat) (ind : (n : Nat) → (n > 0motive (n / 2))motive n) :
motive n

An induction principal that works on divison by two.

Equations
Instances For
    @[simp]
    theorem Nat.zero_and (x : Nat) :
    0 &&& x = 0
    @[simp]
    theorem Nat.and_zero (x : Nat) :
    x &&& 0 = 0
    @[simp]
    theorem Nat.one_and_eq_mod_two (n : Nat) :
    1 &&& n = n % 2
    @[simp]
    theorem Nat.and_one_is_mod (x : Nat) :
    x &&& 1 = x % 2

    testBit #

    @[simp]
    @[simp]
    theorem Nat.testBit_zero (x : Nat) :
    x.testBit 0 = decide (x % 2 = 1)
    theorem Nat.mod_two_eq_one_iff_testBit_zero {x : Nat} :
    x % 2 = 1 x.testBit 0 = true
    theorem Nat.mod_two_eq_zero_iff_testBit_zero {x : Nat} :
    x % 2 = 0 x.testBit 0 = false
    theorem Nat.testBit_succ (x : Nat) (i : Nat) :
    x.testBit i.succ = (x / 2).testBit i
    @[simp]
    theorem Nat.testBit_add_one (x : Nat) (i : Nat) :
    x.testBit (i + 1) = (x / 2).testBit i
    theorem Nat.testBit_div_two (x : Nat) (i : Nat) :
    (x / 2).testBit i = x.testBit (i + 1)
    theorem Nat.testBit_to_div_mod {i : Nat} {x : Nat} :
    x.testBit i = decide (x / 2 ^ i % 2 = 1)
    theorem Nat.toNat_testBit (x : Nat) (i : Nat) :
    (x.testBit i).toNat = x / 2 ^ i % 2
    theorem Nat.ne_zero_implies_bit_true {x : Nat} (xnz : x 0) :
    ∃ (i : Nat), x.testBit i = true
    theorem Nat.ne_implies_bit_diff {x : Nat} {y : Nat} (p : x y) :
    ∃ (i : Nat), x.testBit i y.testBit i
    theorem Nat.eq_of_testBit_eq {x : Nat} {y : Nat} (pred : ∀ (i : Nat), x.testBit i = y.testBit i) :
    x = y

    eq_of_testBit_eq allows proving two natural numbers are equal if their bits are all equal.

    theorem Nat.ge_two_pow_implies_high_bit_true {n : Nat} {x : Nat} (p : x 2 ^ n) :
    ∃ (i : Nat), i n x.testBit i = true
    theorem Nat.testBit_implies_ge {i : Nat} {x : Nat} (p : x.testBit i = true) :
    x 2 ^ i
    theorem Nat.testBit_lt_two_pow {x : Nat} {i : Nat} (lt : x < 2 ^ i) :
    x.testBit i = false
    theorem Nat.lt_pow_two_of_testBit {n : Nat} (x : Nat) (p : ∀ (i : Nat), i nx.testBit i = false) :
    x < 2 ^ n
    theorem Nat.testBit_two_pow_add_eq (x : Nat) (i : Nat) :
    (2 ^ i + x).testBit i = !x.testBit i
    theorem Nat.testBit_mul_two_pow_add_eq (a : Nat) (b : Nat) (i : Nat) :
    (2 ^ i * a + b).testBit i = (decide (a % 2 = 1)).xor (b.testBit i)
    theorem Nat.testBit_two_pow_add_gt {i : Nat} {j : Nat} (j_lt_i : j < i) (x : Nat) :
    (2 ^ i + x).testBit j = x.testBit j
    @[simp]
    theorem Nat.testBit_mod_two_pow (x : Nat) (j : Nat) (i : Nat) :
    (x % 2 ^ j).testBit i = (decide (i < j) && x.testBit i)
    theorem Nat.not_decide_mod_two_eq_one (x : Nat) :
    (!decide (x % 2 = 1)) = decide (x % 2 = 0)
    theorem Nat.testBit_two_pow_sub_succ {x : Nat} {n : Nat} (h₂ : x < 2 ^ n) (i : Nat) :
    (2 ^ n - (x + 1)).testBit i = (decide (i < n) && !x.testBit i)
    @[simp]
    theorem Nat.testBit_two_pow_sub_one (n : Nat) (i : Nat) :
    (2 ^ n - 1).testBit i = decide (i < n)
    theorem Nat.testBit_bool_to_nat (b : Bool) (i : Nat) :
    b.toNat.testBit i = (decide (i = 0) && b)

    testBit 1 i is true iff the index i equals 0.

    theorem Nat.testBit_two_pow {n : Nat} {m : Nat} :
    (2 ^ n).testBit m = decide (n = m)
    @[simp]
    theorem Nat.testBit_two_pow_self {n : Nat} :
    (2 ^ n).testBit n = true
    @[simp]
    theorem Nat.testBit_two_pow_of_ne {n : Nat} {m : Nat} (hm : n m) :
    (2 ^ n).testBit m = false
    @[simp]
    theorem Nat.two_pow_sub_one_mod_two {n : Nat} :
    (2 ^ n - 1) % 2 = 1 % 2 ^ n
    @[simp]
    theorem Nat.mod_two_pos_mod_two_eq_one {x : Nat} {j : Nat} :
    x % 2 ^ j % 2 = 1 0 < j x % 2 = 1

    bitwise #

    theorem Nat.testBit_bitwise {f : BoolBoolBool} (false_false_axiom : f false false = false) (x : Nat) (y : Nat) (i : Nat) :
    (Nat.bitwise f x y).testBit i = f (x.testBit i) (y.testBit i)

    bitwise #

    theorem Nat.bitwise_lt_two_pow {x : Nat} {n : Nat} {y : Nat} {f : BoolBoolBool} (left : x < 2 ^ n) (right : y < 2 ^ n) :
    Nat.bitwise f x y < 2 ^ n

    This provides a bound on bitwise operations.

    and #

    @[simp]
    theorem Nat.testBit_and (x : Nat) (y : Nat) (i : Nat) :
    (x &&& y).testBit i = (x.testBit i && y.testBit i)
    theorem Nat.and_lt_two_pow (x : Nat) {y : Nat} {n : Nat} (right : y < 2 ^ n) :
    x &&& y < 2 ^ n
    @[simp]
    theorem Nat.and_pow_two_is_mod (x : Nat) (n : Nat) :
    x &&& 2 ^ n - 1 = x % 2 ^ n
    theorem Nat.and_pow_two_identity {n : Nat} {x : Nat} (lt : x < 2 ^ n) :
    x &&& 2 ^ n - 1 = x
    @[simp]
    theorem Nat.and_mod_two_eq_one {a : Nat} {b : Nat} :
    (a &&& b) % 2 = 1 a % 2 = 1 b % 2 = 1
    theorem Nat.and_div_two {a : Nat} {b : Nat} :
    (a &&& b) / 2 = a / 2 &&& b / 2

    lor #

    @[simp]
    theorem Nat.zero_or (x : Nat) :
    0 ||| x = x
    @[simp]
    theorem Nat.or_zero (x : Nat) :
    x ||| 0 = x
    @[simp]
    theorem Nat.testBit_or (x : Nat) (y : Nat) (i : Nat) :
    (x ||| y).testBit i = (x.testBit i || y.testBit i)
    theorem Nat.or_lt_two_pow {x : Nat} {y : Nat} {n : Nat} (left : x < 2 ^ n) (right : y < 2 ^ n) :
    x ||| y < 2 ^ n
    @[simp]
    theorem Nat.or_mod_two_eq_one {a : Nat} {b : Nat} :
    (a ||| b) % 2 = 1 a % 2 = 1 b % 2 = 1
    theorem Nat.or_div_two {a : Nat} {b : Nat} :
    (a ||| b) / 2 = a / 2 ||| b / 2

    xor #

    @[simp]
    theorem Nat.testBit_xor (x : Nat) (y : Nat) (i : Nat) :
    (x ^^^ y).testBit i = (x.testBit i).xor (y.testBit i)
    theorem Nat.xor_lt_two_pow {x : Nat} {y : Nat} {n : Nat} (left : x < 2 ^ n) (right : y < 2 ^ n) :
    x ^^^ y < 2 ^ n
    theorem Nat.and_xor_distrib_right {a : Nat} {b : Nat} {c : Nat} :
    (a ^^^ b) &&& c = a &&& c ^^^ b &&& c
    theorem Nat.and_xor_distrib_left {a : Nat} {b : Nat} {c : Nat} :
    a &&& (b ^^^ c) = a &&& b ^^^ a &&& c
    @[simp]
    theorem Nat.xor_mod_two_eq_one {a : Nat} {b : Nat} :
    (a ^^^ b) % 2 = 1 ¬(a % 2 = 1 b % 2 = 1)
    theorem Nat.xor_div_two {a : Nat} {b : Nat} :
    (a ^^^ b) / 2 = a / 2 ^^^ b / 2

    Arithmetic #

    theorem Nat.testBit_mul_pow_two_add (a : Nat) {b : Nat} {i : Nat} (b_lt : b < 2 ^ i) (j : Nat) :
    (2 ^ i * a + b).testBit j = if j < i then b.testBit j else a.testBit (j - i)
    theorem Nat.testBit_mul_pow_two {i : Nat} {a : Nat} {j : Nat} :
    (2 ^ i * a).testBit j = (decide (j i) && a.testBit (j - i))
    theorem Nat.mul_add_lt_is_or {i : Nat} {b : Nat} (b_lt : b < 2 ^ i) (a : Nat) :
    2 ^ i * a + b = 2 ^ i * a ||| b

    shiftLeft and shiftRight #

    @[simp]
    theorem Nat.testBit_shiftLeft {i : Nat} {j : Nat} (x : Nat) :
    (x <<< i).testBit j = (decide (j i) && x.testBit (j - i))
    @[simp]
    theorem Nat.testBit_shiftRight {i : Nat} {j : Nat} (x : Nat) :
    (x >>> i).testBit j = x.testBit (i + j)
    @[simp]
    theorem Nat.shiftLeft_mod_two_eq_one {x : Nat} {i : Nat} :
    x <<< i % 2 = 1 i = 0 x % 2 = 1
    @[simp]
    theorem Nat.decide_shiftRight_mod_two_eq_one {x : Nat} {i : Nat} :
    decide (x >>> i % 2 = 1) = x.testBit i

    le #

    theorem Nat.le_of_testBit {n : Nat} {m : Nat} (h : ∀ (i : Nat), n.testBit i = truem.testBit i = true) :
    n m
    theorem Nat.and_le_left {n : Nat} {m : Nat} :
    n &&& m n
    theorem Nat.and_le_right {n : Nat} {m : Nat} :
    n &&& m m