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.

boddDiv2_eq and bodd

@[simp]

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

@[simp]

theorem Nat.bodd_bit0 (n : ℕ) : Nat.bodd (bit0 n) = false

@[simp]

theorem Nat.bodd_bit1 (n : ℕ) : Nat.bodd (bit1 n) = true

@[simp]

theorem Nat.div2_bit0 (n : ℕ) : Nat.div2 (bit0 n) = n

@[simp]

theorem Nat.div2_bit1 (n : ℕ) : Nat.div2 (bit1 n) = 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 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

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.bitCasesOn_bit {C : ℕ → Sort u} (H : (b : Bool) → (n : ℕ) → C (Nat.bit b n)) (b : Bool) (n : ℕ) : Nat.bitCasesOn (Nat.bit b n) H = H b n

@[simp]

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

@[simp]

theorem Nat.bitCasesOn_bit1 {C : ℕ → Sort u} (H : (b : Bool) → (n : ℕ) → C (Nat.bit b n)) (n : ℕ) : Nat.bitCasesOn (bit1 n) H = H true n

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

@[simp]

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

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 = false

theorem Nat.bit0_le {m : ℕ} {n : ℕ} (h : n ≤ m) : bit0 n ≤ bit0 m

theorem Nat.bit1_le {n : ℕ} {m : ℕ} (h : n ≤ m) : bit1 n ≤ bit1 m

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

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

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

theorem Nat.bit_lt_bit0 (b : Bool) {m : ℕ} {n : ℕ} : m < n → Nat.bit b m < bit0 n

theorem Nat.bit0_lt_bit0 {m : ℕ} {n : ℕ} : bit0 m < bit0 n ↔ m < 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.bit0_le_bit1_iff {m : ℕ} {n : ℕ} : bit0 m ≤ bit1 n ↔ m ≤ n

@[simp]

theorem Nat.bit0_lt_bit1_iff {m : ℕ} {n : ℕ} : bit0 m < bit1 n ↔ m ≤ n

@[simp]

theorem Nat.bit1_le_bit0_iff {m : ℕ} {n : ℕ} : bit1 m ≤ bit0 n ↔ m < n

@[simp]

theorem Nat.bit1_lt_bit0_iff {m : ℕ} {n : ℕ} : bit1 m < bit0 n ↔ m < n

theorem Nat.binaryRec_eq' {C : ℕ → Sort u_1} {z : C 0} {f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)} (b : Bool) (n : ℕ) (h : f false 0 z = z ∨ (n = 0 → b = true)) : Nat.binaryRec z f (Nat.bit b n) = f b n (Nat.binaryRec z f n)

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

def Nat.binaryRec' {C : ℕ → Sort u_1} (z : C 0) (f : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → C n → C (Nat.bit b n)) (n : ℕ) : C n

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

Equations

• Nat.binaryRec' z f = Nat.binaryRec z fun (b : Bool) (n : ℕ) (ih : C n) => if h : n = 0 → b = true then f b n h ih else Eq.mpr ⋯ (id z)

def Nat.binaryRecFromOne {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 binaryRec, but special casing both 0 and 1 as base cases

Equations

• Nat.binaryRecFromOne z₀ z₁ f n = Nat.binaryRec' z₀ (fun (b : Bool) (n : ℕ) (h : n = 0 → b = true) (ih : C n) => if h' : n = 0 then Eq.mpr ⋯ (Eq.mpr ⋯ z₁) else f b n h' ih) n

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Nat.bit1_bits (n : ℕ) : Nat.bits (bit1 n) = true :: Nat.bits n

@[simp]

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

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

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