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

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
Instances For
def Nat.div2 (n : ) :

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

Equations
• = ().2
Instances For
def Nat.bodd (n : ) :

bodd n returns true if n is odd

Equations
• = ().1
Instances For
@[simp]
theorem Nat.bodd_zero :
@[simp]
theorem Nat.bodd_succ (n : ) :
@[simp]
theorem Nat.bodd_add (m : ) (n : ) :
Nat.bodd (m + n) = xor () ()
@[simp]
theorem Nat.bodd_mul (m : ) (n : ) :
Nat.bodd (m * n) = ()
theorem Nat.mod_two_of_bodd (n : ) :
n % 2 = bif then 1 else 0
@[simp]
theorem Nat.div2_zero :
= 0
theorem Nat.div2_one :
= 0
theorem Nat.div2_two :
= 1
@[simp]
theorem Nat.div2_succ (n : ) :
Nat.div2 () = bif then Nat.succ () else
theorem Nat.bodd_add_div2 (n : ) :
(bif then 1 else 0) + 2 * = n
theorem Nat.div2_val (n : ) :
= n / 2
def Nat.bit (b : Bool) :

bit b appends the digit b to the binary representation of its natural number input.

Equations
• = bif b then bit1 else bit0
Instances For
theorem Nat.bit0_val (n : ) :
bit0 n = 2 * n
theorem Nat.bit1_val (n : ) :
bit1 n = 2 * n + 1
theorem Nat.bit_val (b : Bool) (n : ) :
Nat.bit b n = 2 * n + bif b then 1 else 0
theorem Nat.bit_decomp (n : ) :
Nat.bit () () = n
def Nat.bitCasesOn {C : Sort u} (n : ) (h : (b : Bool) → (n : ) → C (Nat.bit b n)) :
C n

For a predicate C : Nat → Sort*, if instances can be constructed for natural numbers of the form bit b n, they can be constructed for any given natural number.

Equations
• = h () ()
Instances For
theorem Nat.bit_zero :
= 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
Instances For
@[simp]
theorem Nat.shiftLeft'_false {m : } (n : ) :
= m <<< n
@[simp]
theorem Nat.shiftLeft_eq' (m : ) (n : ) :
= m <<< n

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

@[simp]
theorem Nat.shiftRight_eq (m : ) (n : ) :
= m >>> n
theorem Nat.binaryRec_decreasing {n : } (h : n 0) :
< n
def Nat.binaryRec {C : Sort u} (z : C 0) (f : (b : Bool) → (n : ) → C nC (Nat.bit b n)) (n : ) :
C n

A recursion principle for bit representations of natural numbers. For a predicate C : Nat → Sort*, if instances can be constructed for natural numbers of the form bit b n, they can be constructed for all natural numbers.

Equations
Instances For
def Nat.size :

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

Equations
Instances For
def Nat.bits :

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
Instances For
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
Instances For
@[simp]
theorem Nat.binaryRec_zero {C : Sort u} (z : C 0) (f : (b : Bool) → (n : ) → C nC (Nat.bit b n)) :
= z

bitwise ops

theorem Nat.bodd_bit (b : Bool) (n : ) :
theorem Nat.div2_bit (b : Bool) (n : ) :
theorem Nat.shiftLeft'_add (b : Bool) (m : ) (n : ) (k : ) :
Nat.shiftLeft' b m (n + k) = Nat.shiftLeft' b () k
theorem Nat.shiftLeft_add (m : ) (n : ) (k : ) :
m <<< (n + k) = m <<< n <<< k
theorem Nat.shiftLeft'_sub (b : Bool) (m : ) {n : } {k : } :
k nNat.shiftLeft' b m (n - k) = >>> k
theorem Nat.shiftLeft_sub (m : ) {n : } {k : } :
k nm <<< (n - k) = m <<< n >>> k
theorem Nat.testBit_bit_zero (b : Bool) (n : ) :
theorem Nat.bodd_eq_and_one_ne_zero (n : ) :
= (n &&& 1 != 0)
theorem Nat.testBit_bit_succ (m : ) (b : Bool) (n : ) :
theorem Nat.binaryRec_eq {C : Sort u} {z : C 0} {f : (b : Bool) → (n : ) → C nC (Nat.bit b n)} (h : f false 0 z = z) (b : Bool) (n : ) :
Nat.binaryRec z f (Nat.bit b n) = f b n ()

### boddDiv2_eq and bodd#

@[simp]
theorem Nat.boddDiv2_eq (n : ) :
= (, )
@[simp]
theorem Nat.bodd_bit0 (n : ) :
@[simp]
theorem Nat.bodd_bit1 (n : ) :
@[simp]
theorem Nat.div2_bit0 (n : ) :
@[simp]
theorem Nat.div2_bit1 (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 b m
theorem Nat.bit_add' (b : Bool) (n : ) (m : ) :
Nat.bit b (n + m) = Nat.bit b n +
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 : ) :
@[simp]
theorem Nat.bitCasesOn_bit1 {C : Sort u} (H : (b : Bool) → (n : ) → C (Nat.bit b n)) (n : ) :
theorem Nat.bit_cases_on_injective {C : Sort u} :
Function.Injective fun (H : (b : Bool) → (n : ) → C (Nat.bit b n)) (n : ) =>
@[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 : ) => ) = fun (n : ) => ) 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
theorem Nat.bit0_le {m : } {n : } (h : n m) :
theorem Nat.bit1_le {n : } {m : } (h : n m) :
theorem Nat.bit_le (b : Bool) {m : } {n : } :
m nNat.bit b m Nat.bit b n
theorem Nat.bit0_le_bit (b : Bool) {m : } {n : } :
m nbit0 m Nat.bit b n
theorem Nat.bit_le_bit1 (b : Bool) {m : } {n : } :
m nNat.bit b m bit1 n
theorem Nat.bit_lt_bit0 (b : Bool) {m : } {n : } :
m < nNat.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 nC (Nat.bit b n)} (b : Bool) (n : ) (h : f false 0 z = z (n = 0)) :
Nat.binaryRec z f (Nat.bit b n) = f b 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)C nC (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
Instances For
def Nat.binaryRecFromOne {C : Sort u_1} (z₀ : C 0) (z₁ : C 1) (f : (b : Bool) → (n : ) → n 0C nC (Nat.bit b n)) (n : ) :
C n

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

Equations
Instances For
@[simp]
theorem Nat.zero_bits :
= []
@[simp]
theorem Nat.bits_append_bit (n : ) (b : Bool) (hn : n = 0) :
Nat.bits (Nat.bit b n) = b ::
@[simp]
theorem Nat.bit0_bits (n : ) (hn : n 0) :
@[simp]
theorem Nat.bit1_bits (n : ) :
@[simp]
theorem Nat.one_bits :
= [true]