scilib documentation

data.nat.bits

Additional properties of binary recursion on `nat` #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file documents additional properties of binary recursion, which allows us to more easily work with operations which do depend on the number of leading zeros in the binary representation of n. For example, we can more easily work with nat.bits and nat.size.

See also: nat.bitwise, nat.pow (for various lemmas about size and shiftl/shiftr), and nat.digits.

`bodd_div2` and `bodd` #

@[simp]

theorem nat.bodd_div2_eq (n : ℕ) :

n.bodd_div2 = (n.bodd, n.div2)

@[simp]

theorem nat.bodd_bit0 (n : ℕ) :

(bit0 n).bodd = bool.ff

@[simp]

theorem nat.bodd_bit1 (n : ℕ) :

(bit1 n).bodd = bool.tt

@[simp]

theorem nat.div2_bit0 (n : ℕ) :

(bit0 n).div2 = n

@[simp]

theorem nat.div2_bit1 (n : ℕ) :

(bit1 n).div2 = n

`bit0` and `bit1` #

@[simp]

theorem nat.bit0_eq_bit0 {m n : ℕ} :

bit0 m = bit0 n ↔ m = n

@[simp]

theorem nat.bit1_eq_bit1 {m n : ℕ} :

bit1 m = bit1 n ↔ m = n

@[simp]

theorem nat.bit1_eq_one {n : ℕ} :

bit1 n = 1 ↔ n = 0

@[simp]

theorem nat.one_eq_bit1 {n : ℕ} :

1 = bit1 n ↔ n = 0

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

nat.bit b (n + m) = nat.bit bool.ff n + nat.bit b m

theorem nat.bit_add' (b : bool) (n m : ℕ) :

nat.bit b (n + m) = nat.bit b n + nat.bit bool.ff m

theorem nat.bit_ne_zero (b : bool) {n : ℕ} (h : n ≠ 0) :

nat.bit b n ≠ 0

theorem nat.bit0_mod_two {n : ℕ} :

bit0 n % 2 = 0

theorem nat.bit1_mod_two {n : ℕ} :

bit1 n % 2 = 1

theorem nat.pos_of_bit0_pos {n : ℕ} (h : 0 < bit0 n) :

0 < n

@[simp]

theorem nat.bit_cases_on_bit {C : ℕ → Sort u} (H : Π (b : bool) (n : ℕ), C (nat.bit b n)) (b : bool) (n : ℕ) :

(nat.bit b n).bit_cases_on H = H b n

@[simp]

theorem nat.bit_cases_on_bit0 {C : ℕ → Sort u} (H : Π (b : bool) (n : ℕ), C (nat.bit b n)) (n : ℕ) :

(bit0 n).bit_cases_on H = H bool.ff n

@[simp]

theorem nat.bit_cases_on_bit1 {C : ℕ → Sort u} (H : Π (b : bool) (n : ℕ), C (nat.bit b n)) (n : ℕ) :

(bit1 n).bit_cases_on H = H bool.tt n

theorem nat.bit_cases_on_injective {C : ℕ → Sort u} :

function.injective (λ (H : Π (b : bool) (n : ℕ), C (nat.bit b n)) (n : ℕ), n.bit_cases_on H)

@[simp]

theorem nat.bit_cases_on_inj {C : ℕ → Sort u} (H₁ H₂ : Π (b : bool) (n : ℕ), C (nat.bit b n)) :

((λ (n : ℕ), n.bit_cases_on H₁) = λ (n : ℕ), n.bit_cases_on H₂) ↔ H₁ = H₂

@[protected]

theorem nat.bit0_eq_zero {n : ℕ} :

bit0 n = 0 ↔ n = 0

theorem nat.bit_eq_zero_iff {n : ℕ} {b : bool} :

nat.bit b n = 0 ↔ n = 0 ∧ b = bool.ff

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

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

The same as binary_rec_eq, but that one unfortunately requires f to be the identity when appending ff to 0. Here, we allow you to explicitly say that that case is not happening, i.e. supplying n = 0 → b = tt.

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

C n

The same as binary_rec, but the induction step can assume that if n=0, the bit being appended is tt

Equations

nat.binary_rec' z f = nat.binary_rec z (λ (b : bool) (n : ℕ) (ih : C n), dite (n = 0 → b = bool.tt) (λ (h : n = 0 → b = bool.tt), f b n h ih) (λ (h : ¬(n = 0 → b = bool.tt)), _.mpr z))

def nat.binary_rec_from_one {C : ℕ → Sort u_1} (z₀ : C 0) (z₁ : C 1) (f : Π (b : bool) (n : ℕ), n ≠ 0 → C n → C (nat.bit b n)) (n : ℕ) :

C n

The same as binary_rec, but special casing both 0 and 1 as base cases

Equations

nat.binary_rec_from_one z₀ z₁ f = nat.binary_rec' z₀ (λ (b : bool) (n : ℕ) (h : n = 0 → b = bool.tt) (ih : C n), dite (n = 0) (λ (h' : n = 0), _.mpr (_.mpr z₁)) (λ (h' : ¬n = 0), f b n h' ih))

@[simp]

theorem nat.zero_bits :

0.bits = list.nil

@[simp]

theorem nat.bits_append_bit (n : ℕ) (b : bool) (hn : n = 0 → b = bool.tt) :

(nat.bit b n).bits = b :: n.bits

@[simp]

theorem nat.bit0_bits (n : ℕ) (hn : n ≠ 0) :

(bit0 n).bits = bool.ff :: n.bits

@[simp]

theorem nat.bit1_bits (n : ℕ) :

(bit1 n).bits = bool.tt :: n.bits

@[simp]

theorem nat.one_bits :

1.bits = [bool.tt]

theorem nat.bodd_eq_bits_head (n : ℕ) :

n.bodd = n.bits.head

theorem nat.div2_bits_eq_tail (n : ℕ) :

n.div2.bits = n.bits.tail