Additional properties of binary recursion on Nat

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 shiftLeft/shiftRight), and Nat.digits.

def Nat.boddDiv2 : ℕ → Bool × ℕ

boddDiv2 n returns a 2-tuple of type (Bool, Nat) where the Bool value indicates whether n is odd or not and the Nat value returns ⌊n/2⌋

Equations

• Nat.boddDiv2 0 = (false, 0)
• n.succ.boddDiv2 = match n.boddDiv2 with | (false, m) => (true, m) | (true, m) => (false, m.succ)

def Nat.div2 (n : ℕ) : ℕ

div2 n = ⌊n/2⌋ the greatest integer smaller than n/2

Equations

• n.div2 = n.boddDiv2.2

def Nat.bodd (n : ℕ) : Bool

bodd n returns true if n is odd

Equations

• n.bodd = n.boddDiv2.1

@[simp]

theorem Nat.bodd_zero : Nat.bodd 0 = false

@[simp]

theorem Nat.bodd_one : Nat.bodd 1 = true

theorem Nat.bodd_two : Nat.bodd 2 = false

@[simp]

theorem Nat.bodd_succ (n : ℕ) : n.succ.bodd = !n.bodd

@[simp]

theorem Nat.bodd_add (m : ℕ) (n : ℕ) : (m + n).bodd = (m.bodd ^^ n.bodd)

@[simp]

theorem Nat.bodd_mul (m : ℕ) (n : ℕ) : (m * n).bodd = (m.bodd && n.bodd)

theorem Nat.mod_two_of_bodd (n : ℕ) : n % 2 = n.bodd.toNat

@[simp]

theorem Nat.div2_zero : Nat.div2 0 = 0

@[simp]

theorem Nat.div2_one : Nat.div2 1 = 0

theorem Nat.div2_two : Nat.div2 2 = 1

@[simp]

theorem Nat.div2_succ (n : ℕ) : (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2

theorem Nat.bodd_add_div2 (n : ℕ) : n.bodd.toNat + 2 * n.div2 = n

theorem Nat.div2_val (n : ℕ) : n.div2 = n / 2

theorem Nat.bit_decomp (n : ℕ) : Nat.bit n.bodd n.div2 = n

theorem Nat.bit_zero : Nat.bit false 0 = 0

def Nat.shiftLeft' (b : Bool) (m : ℕ) : ℕ → ℕ

shiftLeft' b m n performs a left shift of m n times and adds the bit b as the least significant bit each time. Returns the corresponding natural number

Equations

• Nat.shiftLeft' b m 0 = m
• Nat.shiftLeft' b m n.succ = Nat.bit b (Nat.shiftLeft' b m n)

@[simp]

theorem Nat.shiftLeft'_false {m : ℕ} (n : ℕ) : Nat.shiftLeft' false m n = m <<< n

@[simp]

theorem Nat.shiftLeft_eq' (m : ℕ) (n : ℕ) : m.shiftLeft n = m <<< n

Lean takes the unprimed name for Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n.

@[simp]

theorem Nat.shiftRight_eq (m : ℕ) (n : ℕ) : m.shiftRight n = m >>> n

theorem Nat.binaryRec_decreasing {n : ℕ} (h : n ≠ 0) : n.div2 < n

def Nat.size : ℕ → ℕ

size n : Returns the size of a natural number in bits i.e. the length of its binary representation

Equations

• n.size = Nat.binaryRec 0 (fun (x : Bool) (x : ℕ) => Nat.succ) n

def Nat.bits : ℕ → List Bool

bits n returns a list of Bools which correspond to the binary representation of n, where the head of the list represents the least significant bit

Equations

• n.bits = Nat.binaryRec [] (fun (b : Bool) (x : ℕ) (IH : List Bool) => b :: IH) n

def Nat.ldiff : ℕ → ℕ → ℕ

ldiff a b performs bitwise set difference. For each corresponding pair of bits taken as booleans, say aᵢ and bᵢ, it applies the boolean operation aᵢ ∧ ¬bᵢ to obtain the iᵗʰ bit of the result.

Equations

• Nat.ldiff = Nat.bitwise fun (a b : Bool) => a && !b

bitwise ops

theorem Nat.bodd_bit (b : Bool) (n : ℕ) : (Nat.bit b n).bodd = b

theorem Nat.div2_bit (b : Bool) (n : ℕ) : (Nat.bit b n).div2 = n

theorem Nat.shiftLeft'_add (b : Bool) (m : ℕ) (n : ℕ) (k : ℕ) : Nat.shiftLeft' b m (n + k) = Nat.shiftLeft' b (Nat.shiftLeft' b m n) k

theorem Nat.shiftLeft'_sub (b : Bool) (m : ℕ) {n : ℕ} {k : ℕ} : k ≤ n → Nat.shiftLeft' b m (n - k) = Nat.shiftLeft' b m n >>> k

theorem Nat.shiftLeft_sub (m : ℕ) {n : ℕ} {k : ℕ} : k ≤ n → m <<< (n - k) = m <<< n >>> k

theorem Nat.bodd_eq_one_and_ne_zero (n : ℕ) : n.bodd = (1 &&& n != 0)

theorem Nat.testBit_bit_succ (m : ℕ) (b : Bool) (n : ℕ) : (Nat.bit b n).testBit m.succ = n.testBit m

boddDiv2_eq and bodd

@[simp]

theorem Nat.boddDiv2_eq (n : ℕ) : n.boddDiv2 = (n.bodd, n.div2)

@[simp]

theorem Nat.div2_bit0 (n : ℕ) : (2 * n).div2 = n

theorem Nat.div2_bit1 (n : ℕ) : (2 * n + 1).div2 = n

bit0 and bit1

theorem Nat.bit_add (b : Bool) (n : ℕ) (m : ℕ) : Nat.bit b (n + m) = Nat.bit false n + Nat.bit b m

theorem Nat.bit_add' (b : Bool) (n : ℕ) (m : ℕ) : Nat.bit b (n + m) = Nat.bit b n + Nat.bit false m

theorem Nat.bit_ne_zero (b : Bool) {n : ℕ} (h : n ≠ 0) : Nat.bit b n ≠ 0

@[simp]

theorem Nat.bitCasesOn_bit0 {motive : ℕ → Sort u} (H : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) (n : ℕ) : Nat.bitCasesOn (2 * n) H = H false n

@[simp]

theorem Nat.bitCasesOn_bit1 {motive : ℕ → Sort u} (H : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) (n : ℕ) : Nat.bitCasesOn (2 * n + 1) H = H true n

theorem Nat.bit_cases_on_injective {motive : ℕ → Sort u} : Function.Injective fun (H : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) (n : ℕ) => Nat.bitCasesOn n H

@[simp]

theorem Nat.bit_cases_on_inj {motive : ℕ → Sort u} (H₁ : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) (H₂ : (b : Bool) → (n : ℕ) → motive (Nat.bit b n)) : ((fun (n : ℕ) => Nat.bitCasesOn n H₁) = fun (n : ℕ) => Nat.bitCasesOn n H₂) ↔ H₁ = H₂

theorem Nat.bit_le (b : Bool) {m : ℕ} {n : ℕ} : m ≤ n → Nat.bit b m ≤ Nat.bit b n

theorem Nat.bit_lt_bit {m : ℕ} {n : ℕ} (a : Bool) (b : Bool) (h : m < n) : Nat.bit a m < Nat.bit b n

@[simp]

theorem Nat.zero_bits : Nat.bits 0 = []

@[simp]

theorem Nat.bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) : (Nat.bit b n).bits = b :: n.bits

@[simp]

theorem Nat.bit0_bits (n : ℕ) (hn : n ≠ 0) : (2 * n).bits = false :: n.bits

@[simp]

theorem Nat.bit1_bits (n : ℕ) : (2 * n + 1).bits = true :: n.bits

@[simp]

theorem Nat.one_bits : Nat.bits 1 = [true]

theorem Nat.bodd_eq_bits_head (n : ℕ) : n.bodd = n.bits.headI

theorem Nat.div2_bits_eq_tail (n : ℕ) : n.div2.bits = n.bits.tail