mathlib docs: core.init.data.nat.bitwise

source

def nat.bodd_div2 :

ℕ → bool × ℕ

Equations

n.succ.bodd_div2 = nat.bodd_div2._match_1 n.bodd_div2
0.bodd_div2 = (bool.ff, 0)
nat.bodd_div2._match_1 (bool.tt, m) = (bool.ff, m.succ)
nat.bodd_div2._match_1 (bool.ff, m) = (bool.tt, m)

source

def nat.div2 :

ℕ → ℕ

Equations

n.div2 = n.bodd_div2.snd

source

def nat.bodd :

ℕ → bool

Equations

n.bodd = n.bodd_div2.fst

source

@[simp]

theorem nat.bodd_zero :

0.bodd = bool.ff

source

@[simp]

theorem nat.bodd_one :

1.bodd = bool.tt

source

@[simp]

theorem nat.bodd_two :

2.bodd = bool.ff

source

@[simp]

theorem nat.bodd_succ (n : ℕ) :

n.succ.bodd = !n.bodd

source

@[simp]

theorem nat.bodd_add (m n : ℕ) :

(m + n).bodd = bxor m.bodd n.bodd

source

@[simp]

theorem nat.bodd_mul (m n : ℕ) :

(m * n).bodd = m.bodd && n.bodd

source

theorem nat.mod_two_of_bodd (n : ℕ) :

n % 2 = cond n.bodd 1 0

source

@[simp]

theorem nat.div2_zero :

0.div2 = 0

source

@[simp]

theorem nat.div2_one :

1.div2 = 0

source

@[simp]

theorem nat.div2_two :

2.div2 = 1

source

@[simp]

theorem nat.div2_succ (n : ℕ) :

n.succ.div2 = cond n.bodd n.div2.succ n.div2

source

theorem nat.bodd_add_div2 (n : ℕ) :

cond n.bodd 1 0 + 2 * n.div2 = n

source

theorem nat.div2_val (n : ℕ) :

n.div2 = n / 2

source

def nat.bit :

bool → ℕ → ℕ

Equations

nat.bit b = cond b bit1 bit0

source

theorem nat.bit0_val (n : ℕ) :

bit0 n = 2 * n

source

theorem nat.bit1_val (n : ℕ) :

bit1 n = 2 * n + 1

source

theorem nat.bit_val (b : bool) (n : ℕ) :

nat.bit b n = 2 * n + cond b 1 0

source

theorem nat.bit_decomp (n : ℕ) :

nat.bit n.bodd n.div2 = n

source

def nat.bit_cases_on {C : ℕ → Sort u} (n : ℕ) :

(Π (b : bool) (n : ℕ), C (nat.bit b n)) → C n

Equations

n.bit_cases_on h = _.mpr (h n.bodd n.div2)

source

@[simp]

theorem nat.bit_zero :

nat.bit bool.ff 0 = 0

source

def nat.shiftl' :

bool → ℕ → ℕ → ℕ

Equations

nat.shiftl' b m (n + 1) = nat.bit b (nat.shiftl' b m n)
nat.shiftl' b m 0 = m

source

def nat.shiftl :

ℕ → ℕ → ℕ

Equations

nat.shiftl = nat.shiftl' bool.ff

source

@[simp]

theorem nat.shiftl_zero (m : ℕ) :

m.shiftl 0 = m

source

@[simp]

theorem nat.shiftl_succ (m n : ℕ) :

m.shiftl (n + 1) = bit0 (m.shiftl n)

source

def nat.shiftr :

ℕ → ℕ → ℕ

Equations

m.shiftr (n + 1) = (m.shiftr n).div2
m.shiftr 0 = m

source

def nat.test_bit :

ℕ → ℕ → bool

Equations

m.test_bit n = (m.shiftr n).bodd

source

def nat.binary_rec {C : ℕ → Sort u} (z : C 0) (f : Π (b : bool) (n : ℕ), C n → C (nat.bit b n)) (n : ℕ) :

C n

Equations

nat.binary_rec z f n = dite (n = 0) (λ (n0 : n = 0), _.mpr z) (λ (n0 : ¬n = 0), let n' : ℕ := n.div2 in _.mpr (f n.bodd n' (nat.binary_rec z f n')))

source

def nat.size :

ℕ → ℕ

Equations

nat.size = nat.binary_rec 0 (λ (_x : bool) (_x : ℕ), nat.succ)

source

def nat.bits :

ℕ → list bool

Equations

nat.bits = nat.binary_rec list.nil (λ (b : bool) (_x : ℕ) (IH : list bool), b :: IH)

source

def nat.bitwise :

(bool → bool → bool) → ℕ → ℕ → ℕ

Equations

nat.bitwise f = nat.binary_rec (λ (n : ℕ), cond (f bool.ff bool.tt) n 0) (λ (a : bool) (m : ℕ) (Ia : ℕ → ℕ), nat.binary_rec (cond (f bool.tt bool.ff) (nat.bit a m) 0) (λ (b : bool) (n _x : ℕ), nat.bit (f a b) (Ia n)))

source

def nat.lor :

ℕ → ℕ → ℕ

Equations

nat.lor = nat.bitwise bor

source

def nat.land :

ℕ → ℕ → ℕ

Equations

nat.land = nat.bitwise band

source

def nat.ldiff :

ℕ → ℕ → ℕ

Equations

nat.ldiff = nat.bitwise (λ (a b : bool), a && !b)

source

def nat.lxor :

ℕ → ℕ → ℕ

Equations

nat.lxor = nat.bitwise bxor

source

@[simp]

theorem nat.binary_rec_zero {C : ℕ → Sort u} (z : C 0) (f : Π (b : bool) (n : ℕ), C n → C (nat.bit b n)) :

nat.binary_rec z f 0 = z

source

theorem nat.bodd_bit (b : bool) (n : ℕ) :

(nat.bit b n).bodd = b

source

theorem nat.div2_bit (b : bool) (n : ℕ) :

(nat.bit b n).div2 = n

source

theorem nat.shiftl'_add (b : bool) (m n k : ℕ) :

nat.shiftl' b m (n + k) = nat.shiftl' b (nat.shiftl' b m n) k

source

theorem nat.shiftl_add (m n k : ℕ) :

m.shiftl (n + k) = (m.shiftl n).shiftl k

source

theorem nat.shiftr_add (m n k : ℕ) :

m.shiftr (n + k) = (m.shiftr n).shiftr k

source

theorem nat.shiftl'_sub (b : bool) (m : ℕ) {n k : ℕ} :

k ≤ n → nat.shiftl' b m (n - k) = (nat.shiftl' b m n).shiftr k

source

theorem nat.shiftl_sub (m : ℕ) {n k : ℕ} :

k ≤ n → m.shiftl (n - k) = (m.shiftl n).shiftr k

source

theorem nat.shiftl_eq_mul_pow (m n : ℕ) :

m.shiftl n = m * 2 ^ n

source

theorem nat.shiftl'_tt_eq_mul_pow (m n : ℕ) :

nat.shiftl' bool.tt m n + 1 = (m + 1) * 2 ^ n

source

theorem nat.one_shiftl (n : ℕ) :

1.shiftl n = 2 ^ n

source

@[simp]

theorem nat.zero_shiftl (n : ℕ) :

0.shiftl n = 0

source

theorem nat.shiftr_eq_div_pow (m n : ℕ) :

m.shiftr n = m / 2 ^ n

source

@[simp]

theorem nat.zero_shiftr (n : ℕ) :

0.shiftr n = 0

source

@[simp]

theorem nat.test_bit_zero (b : bool) (n : ℕ) :

(nat.bit b n).test_bit 0 = b

source

theorem nat.test_bit_succ (m : ℕ) (b : bool) (n : ℕ) :

(nat.bit b n).test_bit m.succ = n.test_bit m

source

theorem nat.binary_rec_eq {C : ℕ → Sort u} {z : C 0} {f : Π (b : bool) (n : ℕ), C n → C (nat.bit b n)} (h : f bool.ff 0 z = z) (b : bool) (n : ℕ) :

nat.binary_rec z f (nat.bit b n) = f b n (nat.binary_rec z f n)

source

theorem nat.bitwise_bit_aux {f : bool → bool → bool} :

f bool.ff bool.ff = bool.ff → (nat.binary_rec (cond (f bool.tt bool.ff) (nat.bit bool.ff 0) 0) (λ (b : bool) (n : ℕ) (_x : (λ (_x : ℕ), ℕ) n), nat.bit (f bool.ff b) (cond (f bool.ff bool.tt) n 0)) = λ (n : ℕ), cond (f bool.ff bool.tt) n 0)

source

@[simp]

theorem nat.bitwise_zero_left (f : bool → bool → bool) (n : ℕ) :

nat.bitwise f 0 n = cond (f bool.ff bool.tt) n 0

source

@[simp]

theorem nat.bitwise_zero_right (f : bool → bool → bool) (h : f bool.ff bool.ff = bool.ff) (m : ℕ) :

nat.bitwise f m 0 = cond (f bool.tt bool.ff) m 0

source

@[simp]

theorem nat.bitwise_zero (f : bool → bool → bool) :

nat.bitwise f 0 0 = 0

source

@[simp]

theorem nat.bitwise_bit {f : bool → bool → bool} (h : f bool.ff bool.ff = bool.ff) (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)

source

theorem nat.bitwise_swap {f : bool → bool → bool} :

f bool.ff bool.ff = bool.ff → nat.bitwise (function.swap f) = function.swap (nat.bitwise f)

source

@[simp]

theorem nat.lor_bit (a : bool) (m : ℕ) (b : bool) (n : ℕ) :

(nat.bit a m).lor (nat.bit b n) = nat.bit (a || b) (m.lor n)

source

@[simp]

theorem nat.land_bit (a : bool) (m : ℕ) (b : bool) (n : ℕ) :

(nat.bit a m).land (nat.bit b n) = nat.bit (a && b) (m.land n)

source

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

source

@[simp]

theorem nat.lxor_bit (a : bool) (m : ℕ) (b : bool) (n : ℕ) :

(nat.bit a m).lxor (nat.bit b n) = nat.bit (bxor a b) (m.lxor n)

source

@[simp]

theorem nat.test_bit_bitwise {f : bool → bool → bool} (h : f bool.ff bool.ff = bool.ff) (m n k : ℕ) :

(nat.bitwise f m n).test_bit k = f (m.test_bit k) (n.test_bit k)

source

@[simp]

theorem nat.test_bit_lor (m n k : ℕ) :

(m.lor n).test_bit k = m.test_bit k || n.test_bit k

source

@[simp]

theorem nat.test_bit_land (m n k : ℕ) :

(m.land n).test_bit k = m.test_bit k && n.test_bit k

source

@[simp]

theorem nat.test_bit_ldiff (m n k : ℕ) :

(m.ldiff n).test_bit k = m.test_bit k && !n.test_bit k

source

@[simp]

theorem nat.test_bit_lxor (m n k : ℕ) :

(m.lxor n).test_bit k = bxor (m.test_bit k) (n.test_bit k)

mathlib documentation

core.init.data.nat.bitwise

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​data.​nat.​bitwise

General documentation

Additional documentation

Library

core.init.data.nat.bitwise