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
  • One or more equations did not get rendered due to their size.
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.and_one_is_mod (x : Nat) :
    x &&& 1 = x % 2

    testBit #

    @[simp]
    @[simp]
    theorem Nat.testBit_zero (x : Nat) :
    Nat.testBit x 0 = decide (x % 2 = 1)
    @[simp]
    theorem Nat.testBit_succ (x : Nat) (i : Nat) :
    theorem Nat.testBit_to_div_mod {i : Nat} {x : Nat} :
    Nat.testBit x i = decide (x / 2 ^ i % 2 = 1)
    theorem Nat.ne_zero_implies_bit_true {x : Nat} (xnz : x 0) :
    ∃ (i : Nat), Nat.testBit x i = true
    theorem Nat.ne_implies_bit_diff {x : Nat} {y : Nat} (p : x y) :
    ∃ (i : Nat), Nat.testBit x i Nat.testBit y i
    theorem Nat.eq_of_testBit_eq {x : Nat} {y : Nat} (pred : ∀ (i : Nat), Nat.testBit x i = Nat.testBit y 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 Nat.testBit x i = true
    theorem Nat.testBit_implies_ge {i : Nat} {x : Nat} (p : Nat.testBit x i = true) :
    x 2 ^ i
    theorem Nat.testBit_lt_two_pow {x : Nat} {i : Nat} (lt : x < 2 ^ i) :
    theorem Nat.lt_pow_two_of_testBit {n : Nat} (x : Nat) (p : ∀ (i : Nat), i nNat.testBit x i = false) :
    x < 2 ^ n

    testBit #

    theorem Nat.testBit_mul_two_pow_add_eq (a : Nat) (b : Nat) (i : Nat) :
    Nat.testBit (2 ^ i * a + b) i = Bool.xor (decide (a % 2 = 1)) (Nat.testBit b i)
    theorem Nat.testBit_two_pow_add_gt {i : Nat} {j : Nat} (j_lt_i : j < i) (x : Nat) :
    Nat.testBit (2 ^ i + x) j = Nat.testBit x j
    @[simp]
    theorem Nat.testBit_mod_two_pow (x : Nat) (j : Nat) (i : Nat) :
    Nat.testBit (x % 2 ^ j) i = (decide (i < j) && Nat.testBit x i)
    theorem Nat.testBit_two_pow_sub_succ {x : Nat} {n : Nat} (h₂ : x < 2 ^ n) (i : Nat) :
    Nat.testBit (2 ^ n - (x + 1)) i = (decide (i < n) && !Nat.testBit x i)
    @[simp]
    theorem Nat.testBit_two_pow_sub_one (n : Nat) (i : Nat) :
    Nat.testBit (2 ^ n - 1) i = decide (i < n)
    theorem Nat.testBit_bool_to_nat (b : Bool) (i : Nat) :
    Nat.testBit (Bool.toNat b) i = (decide (i = 0) && b)

    bitwise #

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

    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) :
    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

    lor #

    @[simp]
    theorem Nat.or_zero (x : Nat) :
    0 ||| x = x
    @[simp]
    theorem Nat.zero_or (x : Nat) :
    x ||| 0 = x
    @[simp]
    theorem Nat.testBit_or (x : Nat) (y : Nat) (i : Nat) :
    theorem Nat.or_lt_two_pow {x : Nat} {y : Nat} {n : Nat} (left : x < 2 ^ n) (right : y < 2 ^ n) :
    x ||| y < 2 ^ n

    xor #

    @[simp]
    theorem Nat.testBit_xor (x : Nat) (y : Nat) (i : Nat) :
    theorem Nat.xor_lt_two_pow {x : Nat} {y : Nat} {n : Nat} (left : x < 2 ^ n) (right : y < 2 ^ n) :
    x ^^^ y < 2 ^ n

    Arithmetic #

    theorem Nat.testBit_mul_pow_two_add (a : Nat) {b : Nat} {i : Nat} (b_lt : b < 2 ^ i) (j : Nat) :
    Nat.testBit (2 ^ i * a + b) j = if j < i then Nat.testBit b j else Nat.testBit a (j - i)
    theorem Nat.testBit_mul_pow_two {i : Nat} {a : Nat} {j : Nat} :
    Nat.testBit (2 ^ i * a) j = (decide (j i) && Nat.testBit a (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) :
    Nat.testBit (x <<< i) j = (decide (j i) && Nat.testBit x (j - i))
    @[simp]
    theorem Nat.testBit_shiftRight {i : Nat} {j : Nat} (x : Nat) :
    Nat.testBit (x >>> i) j = Nat.testBit x (i + j)