Mathlib.Data.Nat.Bits

Nat.boddDiv2 definition

: ℕ → Bool × ℕ

Full source

/-- `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⌋` -/
def boddDiv2 : ℕ → BoolBool × ℕ
  | 0 => (false, 0)
  | succ n =>
    match boddDiv2 n with
    | (false, m) => (true, m)
    | (true, m) => (false, succ m)

Oddness and Half of a Natural Number

Informal description

The function `Nat.boddDiv2` takes a natural number `n` and returns a pair `(b, m)`, where `b` is `true` if `n` is odd and `false` otherwise, and `m` is the floor of `n / 2` (i.e., `⌊n/2⌋`). More formally, for any natural number `n`, `Nat.boddDiv2 n` returns `(n % 2 ≠ 0, n / 2)`.

Nat.div2 definition

(n : ℕ) : ℕ

Full source

/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2` -/
def div2 (n : ℕ) : ℕ := (boddDiv2 n).2

Floor division of a natural number by 2

Informal description

The function `Nat.div2` takes a natural number `n` and returns the greatest integer less than or equal to `n / 2`, i.e., $\lfloor n/2 \rfloor$. This is equivalent to the second component of the pair returned by `Nat.boddDiv2 n`.

Nat.bodd definition

(n : ℕ) : Bool

Full source

/-- `bodd n` returns `true` if `n` is odd -/
def bodd (n : ℕ) : Bool := (boddDiv2 n).1

Oddness of a natural number

Informal description

The function `Nat.bodd` takes a natural number `n` and returns `true` if `n` is odd, and `false` otherwise. More formally, for any natural number `n`, `Nat.bodd n` returns whether `n` is odd (i.e., `n % 2 ≠ 0`).

Nat.bodd_zero theorem

: bodd 0 = false

Full source

@[simp] lemma bodd_zero : bodd 0 = false := rfl

Oddness of Zero: $\text{bodd}(0) = \text{false}$

Informal description

The function `bodd` evaluates to `false` when applied to the natural number $0$, i.e., $\text{bodd}(0) = \text{false}$.

Nat.bodd_one theorem

: bodd 1 = true

Full source

@[simp] lemma bodd_one : bodd 1 = true := rfl

Oddness of One: $\text{bodd}(1) = \text{true}$

Informal description

The function `bodd` evaluates to `true` when applied to the natural number $1$, i.e., $\text{bodd}(1) = \text{true}$.

Nat.bodd_two theorem

: bodd 2 = false

Full source

lemma bodd_two : bodd 2 = false := rfl

Oddness of Two: $\text{bodd}(2) = \text{false}$

Informal description

The function `bodd` evaluates to `false` when applied to the natural number $2$, i.e., $\text{bodd}(2) = \text{false}$.

Nat.bodd_succ theorem

(n : ℕ) : bodd (succ n) = not (bodd n)

Full source

@[simp]
lemma bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  simp only [bodd, boddDiv2]
  let ⟨b,m⟩ := boddDiv2 n
  cases b <;> rfl

Oddness of Successor: $\text{bodd}(n + 1) = \neg \text{bodd}(n)$

Informal description

For any natural number $n$, the function `bodd` evaluated at the successor of $n$ is equal to the negation of `bodd` evaluated at $n$, i.e., $\text{bodd}(n + 1) = \neg \text{bodd}(n)$.

Nat.bodd_add theorem

(m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n)

Full source

@[simp]
lemma bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n) := by
  induction n
  case zero => simp
  case succ n ih => simp [← Nat.add_assoc, Bool.xor_not, ih]

Oddness of Sum: $\text{bodd}(m + n) = \text{bodd}(m) \oplus \text{bodd}(n)$

Informal description

For any natural numbers $m$ and $n$, the function `bodd` evaluated at $m + n$ is equal to the exclusive or (XOR) of `bodd m` and `bodd n$, i.e., $\text{bodd}(m + n) = \text{bodd}(m) \oplus \text{bodd}(n)$.

Nat.bodd_mul theorem

(m n : ℕ) : bodd (m * n) = (bodd m && bodd n)

Full source

@[simp]
lemma bodd_mul (m n : ℕ) : bodd (m * n) = (boddbodd m && bodd n) := by
  induction n with
  | zero => simp
  | succ n IH =>
    simp only [mul_succ, bodd_add, IH, bodd_succ]
    cases bodd m <;> cases bodd n <;> rfl

Oddness of Product: $\text{bodd}(m \cdot n) = \text{bodd}(m) \land \text{bodd}(n)$

Informal description

For any natural numbers $m$ and $n$, the function `bodd` evaluated at $m \cdot n$ is equal to the logical AND of `bodd m` and `bodd n$, i.e., $\text{bodd}(m \cdot n) = \text{bodd}(m) \land \text{bodd}(n)$.

Nat.mod_two_of_bodd theorem

(n : ℕ) : n % 2 = (bodd n).toNat

Full source

lemma mod_two_of_bodd (n : ℕ) : n % 2 = (bodd n).toNat := by
  have := congr_arg bodd (mod_add_div n 2)
  simp? [not] at this says
    simp only [bodd_add, bodd_mul, bodd_succ, not, bodd_zero, Bool.false_and, Bool.bne_false]
      at this
  have _ : ∀ b, and false b = false := by
    intro b
    cases b <;> rfl
  have _ : ∀ b, bxor b false = b := by
    intro b
    cases b <;> rfl
  rw [← this]
  rcases mod_two_eq_zero_or_one n with h | h <;> rw [h] <;> rfl

Modulo Two Equals Oddness Indicator: $n \bmod 2 = \text{bodd}(n).\text{toNat}$

Informal description

For any natural number $n$, the remainder when $n$ is divided by $2$ is equal to $1$ if $n$ is odd and $0$ if $n$ is even, i.e., $n \bmod 2 = \begin{cases} 1 & \text{if } n \text{ is odd} \\ 0 & \text{if } n \text{ is even} \end{cases}$.

Nat.div2_zero theorem

: div2 0 = 0

Full source

@[simp] lemma div2_zero : div2 0 = 0 := rfl

Floor Division of Zero by Two is Zero

Informal description

The floor division of the natural number $0$ by $2$ equals $0$, i.e., $\lfloor 0/2 \rfloor = 0$.

Nat.div2_one theorem

: div2 1 = 0

Full source

@[simp] lemma div2_one : div2 1 = 0 := rfl

Floor Division of One by Two is Zero

Informal description

The floor division of the natural number $1$ by $2$ equals $0$, i.e., $\lfloor 1/2 \rfloor = 0$.

Nat.div2_two theorem

: div2 2 = 1

Full source

lemma div2_two : div2 2 = 1 := rfl

Floor Division of Two by Two is One

Informal description

The floor division of the natural number $2$ by $2$ equals $1$, i.e., $\lfloor 2/2 \rfloor = 1$.

Nat.div2_succ theorem

(n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n)

Full source

@[simp]
lemma div2_succ (n : ℕ) : div2 (n + 1) = cond (bodd n) (succ (div2 n)) (div2 n) := by
  simp only [bodd, boddDiv2, div2]
  rcases boddDiv2 n with ⟨_|_, _⟩ <;> simp

Recursive Formula for Floor Division of Successor by 2

Informal description

For any natural number $n$, the floor division of $n+1$ by 2 satisfies: \[ \lfloor (n+1)/2 \rfloor = \begin{cases} \lfloor n/2 \rfloor + 1 & \text{if } n \text{ is odd} \\ \lfloor n/2 \rfloor & \text{if } n \text{ is even} \end{cases} \]

Nat.bodd_add_div2 theorem

: ∀ n, (bodd n).toNat + 2 * div2 n = n

Full source

lemma bodd_add_div2 : ∀ n, (bodd n).toNat + 2 * div2 n = n
  | 0 => rfl
  | succ n => by
    simp only [bodd_succ, Bool.cond_not, div2_succ, Nat.mul_comm]
    refine Eq.trans ?_ (congr_arg succ (bodd_add_div2 n))
    cases bodd n
    · simp
    · simp; omega

Decomposition of Natural Number into Oddness and Twice Half

Informal description

For any natural number $n$, the sum of the integer representation of its oddness (1 if $n$ is odd, 0 otherwise) and twice its floor division by 2 equals $n$ itself. That is, \[ \text{bodd}(n) + 2 \cdot \lfloor n/2 \rfloor = n \] where $\text{bodd}(n)$ is 1 if $n$ is odd and 0 otherwise, and $\lfloor n/2 \rfloor$ is the floor division of $n$ by 2.

Nat.div2_val theorem

(n) : div2 n = n / 2

Full source

lemma div2_val (n) : div2 n = n / 2 := by
  refine Nat.eq_of_mul_eq_mul_left (by decide)
    (Nat.add_left_cancel (Eq.trans ?_ (Nat.mod_add_div n 2).symm))
  rw [mod_two_of_bodd, bodd_add_div2]

Floor Division Equals Integer Division for Natural Numbers by 2

Informal description

For any natural number $n$, the floor division of $n$ by 2 equals the integer division of $n$ by 2, i.e., $\lfloor n/2 \rfloor = n / 2$.

Nat.bit_decomp theorem

(n : Nat) : bit (bodd n) (div2 n) = n

Full source

lemma bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
  (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _

Binary Decomposition of Natural Numbers via Bit Operation

Informal description

For any natural number $n$, the binary operation `bit` applied to the oddness of $n$ (as a boolean) and the floor division of $n$ by 2 reconstructs $n$ itself. That is, \[ \text{bit}(\text{bodd}(n), \lfloor n/2 \rfloor) = n \] where $\text{bodd}(n)$ is `true` if $n$ is odd and `false` otherwise, and $\lfloor n/2 \rfloor$ is the greatest integer less than or equal to $n/2$.

Nat.bit_zero theorem

: bit false 0 = 0

Full source

lemma bit_zero : bit false 0 = 0 :=
  rfl

Bit Operation with False and Zero Yields Zero

Informal description

The binary operation `bit` applied to the boolean `false` and the natural number `0` results in `0`, i.e., $\text{bit}(\text{false}, 0) = 0$.

Nat.shiftLeft' definition

(b : Bool) (m : ℕ) : ℕ → ℕ

Full source

/-- `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 -/
def shiftLeft' (b : Bool) (m : ℕ) : ℕ → ℕ
  | 0 => m
  | n + 1 => bit b (shiftLeft' b m n)

Left shift with bit insertion

Informal description

The function `shiftLeft'` takes a boolean `b`, a natural number `m`, and a natural number `n`, and performs a left shift operation on `m` `n` times. Each time it shifts, it adds the bit `b` as the least significant bit. The result is the corresponding natural number obtained from this operation. More precisely: - When `n = 0`, the result is `m`. - For `n + 1`, the result is obtained by appending the bit `b` to the result of `shiftLeft' b m n`.

Nat.shiftLeft'_false theorem

: ∀ n, shiftLeft' false m n = m <<< n

Full source

@[simp]
lemma shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
  | 0 => rfl
  | n + 1 => by
    have : 2 * (m * 2^n) = 2^(n+1)*m := by
      rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp
    simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this]

Left Shift with False Bit Equals Bitwise Left Shift: $\text{shiftLeft'}(\text{false}, m, n) = m \lll n$

Informal description

For any natural number $n$, the left shift operation `shiftLeft'` with a false bit and a natural number $m$ is equal to the bitwise left shift operation $m \lll n$.

Nat.shiftLeft_eq' theorem

(m n : Nat) : shiftLeft m n = m <<< n

Full source

/-- Lean takes the unprimed name for `Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n`. -/
@[simp] lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl

Equivalence of Left Shift Operations: $\text{shiftLeft}(m, n) = m \lll n$

Informal description

For any natural numbers $m$ and $n$, the left shift operation `shiftLeft m n` is equal to the bitwise left shift operation `m <<< n`.

Nat.shiftRight_eq theorem

(m n : Nat) : shiftRight m n = m >>> n

Full source

@[simp] lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl

Equivalence of `shiftRight` and Bitwise Right Shift on Natural Numbers

Informal description

For any natural numbers $m$ and $n$, the right shift operation `shiftRight m n` is equal to the bitwise right shift operation `m >>> n`.

Nat.binaryRec_decreasing theorem

(h : n ≠ 0) : div2 n < n

Full source

lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
  rw [div2_val]
  apply (div_lt_iff_lt_mul <| succ_pos 1).2
  have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1)
    (lt_of_le_of_ne n.zero_le h.symm)
  rwa [Nat.mul_one] at this

Floor Division by Two Decreases Nonzero Natural Numbers

Informal description

For any natural number $n \neq 0$, the floor division of $n$ by 2 is strictly less than $n$, i.e., $\lfloor n/2 \rfloor < n$.

Nat.size definition

: ℕ → ℕ

Full source

/-- `size n` : Returns the size of a natural number in
bits i.e. the length of its binary representation -/
def size : ℕ → ℕ :=
  binaryRec 0 fun _ _ => succ

Bit length of a natural number

Informal description

The function `Nat.size` computes the bit length of a natural number `n`, which is the number of bits required to represent `n` in binary. For example, `Nat.size 5 = 3` since 5 is `101` in binary.

Nat.bits definition

: ℕ → List Bool

Full source

/-- `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 -/
def bits : ℕ → List Bool :=
  binaryRec [] fun b _ IH => b :: IH

Binary digits of a natural number (least significant bit first)

Informal description

The function `Nat.bits` takes a natural number `n` and returns a list of boolean values representing the binary digits of `n`, where the least significant bit is the first element of the list. More precisely, for a natural number `n`, `Nat.bits n` is defined recursively as follows: - If `n = 0`, it returns the empty list `[]`. - Otherwise, it prepends the least significant bit (`bodd n`) to the list obtained from `Nat.bits (div2 n)`.

Nat.ldiff definition

: ℕ → ℕ → ℕ

Full source

/-- `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. -/
def ldiff : ℕ → ℕ → ℕ :=
  bitwise fun a b => a && not b

Bitwise set difference of natural numbers

Informal description

The function `Nat.ldiff a b` computes the bitwise set difference of natural numbers `a` and `b`. For each corresponding pair of bits `aᵢ` and `bᵢ`, it applies the logical operation `aᵢ ∧ ¬bᵢ` to obtain the `i`-th bit of the result.

Nat.bodd_bit theorem

(b n) : bodd (bit b n) = b

Full source

lemma bodd_bit (b n) : bodd (bit b n) = b := by
  rw [bit_val]
  simp only [Nat.mul_comm, Nat.add_comm, bodd_add, bodd_mul, bodd_succ, bodd_zero, Bool.not_false,
    Bool.not_true, Bool.and_false, Bool.xor_false]
  cases b <;> cases bodd n <;> rfl

Oddness of Bit-Constructed Number: $\text{bodd}(\text{bit}(b, n)) = b$

Informal description

For any boolean value $b$ and natural number $n$, the function `bodd` evaluated at the number constructed by `bit b n` is equal to $b$, i.e., $\text{bodd}(\text{bit}(b, n)) = b$.

Nat.div2_bit theorem

(b n) : div2 (bit b n) = n

Full source

lemma div2_bit (b n) : div2 (bit b n) = n := by
  rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
  <;> cases b
  <;> decide

Floor Division by Two of Bit-Constructed Number: $\lfloor \text{bit}(b, n)/2 \rfloor = n$

Informal description

For any boolean value $b$ and natural number $n$, the floor division by 2 of the number constructed by `bit b n` equals $n$, i.e., $\lfloor \text{bit}(b, n)/2 \rfloor = n$.

Nat.shiftLeft'_add theorem

(b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k

Full source

lemma shiftLeft'_add (b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k
  | 0 => rfl
  | k + 1 => congr_arg (bit b) (shiftLeft'_add b m n k)

Additive Property of Left Shift with Bit Insertion

Informal description

For any boolean `b`, natural numbers `m` and `n`, and any natural number `k`, the left shift operation with bit insertion satisfies the additive property: \[ \text{shiftLeft'}\ b\ m\ (n + k) = \text{shiftLeft'}\ b\ (\text{shiftLeft'}\ b\ m\ n)\ k \]

Nat.shiftLeft'_sub theorem

(b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (shiftLeft' b m n) >>> k

Full source

lemma shiftLeft'_sub (b m) : ∀ {n k}, k ≤ n → shiftLeft' b m (n - k) = (shiftLeft' b m n) >>> k
  | _, 0, _ => rfl
  | n + 1, k + 1, h => by
    rw [succ_sub_succ_eq_sub, shiftLeft', Nat.add_comm, shiftRight_add]
    simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]
    simp [← div2_val, div2_bit]

Subtraction Property of Left Shift with Bit Insertion: $\text{shiftLeft'}\ b\ m\ (n - k) = (\text{shiftLeft'}\ b\ m\ n) \gg k$ for $k \leq n$

Informal description

For any boolean `b`, natural number `m`, and natural numbers `n` and `k` such that $k \leq n$, the left shift operation with bit insertion satisfies: \[ \text{shiftLeft'}\ b\ m\ (n - k) = (\text{shiftLeft'}\ b\ m\ n) \gg k \] where $\gg$ denotes the right shift operation.

Nat.shiftLeft_sub theorem

: ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k

Full source

lemma shiftLeft_sub : ∀ (m : Nat) {n k}, k ≤ n → m <<< (n - k) = (m <<< n) >>> k :=
  fun _ _ _ hk => by simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]

Shift Distance Subtraction Property: $m \ll (n - k) = (m \ll n) \gg k$ for $k \leq n$

Informal description

For any natural number $m$ and natural numbers $n, k$ such that $k \leq n$, the left shift of $m$ by $n - k$ positions is equal to the right shift by $k$ positions of the left shift of $m$ by $n$ positions. In symbols: \[ m \ll (n - k) = (m \ll n) \gg k \]

Nat.bodd_eq_one_and_ne_zero theorem

: ∀ n, bodd n = (1 &&& n != 0)

Full source

lemma bodd_eq_one_and_ne_zero : ∀ n, bodd n = (1 &&& n != 0)
  | 0 => rfl
  | 1 => rfl
  | n + 2 => by simpa using bodd_eq_one_and_ne_zero n

Oddness as Logical AND with Non-Zero Check

Informal description

For any natural number $n$, the function `bodd` evaluated at $n$ is equal to the logical AND of $1$ and the boolean value indicating whether $n$ is non-zero, i.e., $\text{bodd}(n) = (1 \text{ AND } (n \neq 0))$.

Nat.testBit_bit_succ theorem

(m b n) : testBit (bit b n) (succ m) = testBit n m

Full source

lemma testBit_bit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
  have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
    simp only [shiftRight_eq_div_pow]
    simp [← div2_val, div2_bit]
  rw [← shiftRight_add, Nat.add_comm] at this
  simp only [bodd_eq_one_and_ne_zero] at this
  exact this

Bit Test Property for Successor Position: $\text{testBit}(\text{bit}(b, n), m+1) = \text{testBit}(n, m)$

Informal description

For any natural numbers $m$, $n$ and boolean $b$, the $(m+1)$-th bit of the number constructed by `bit b n` is equal to the $m$-th bit of $n$, i.e., $\text{testBit}(\text{bit}(b, n), m+1) = \text{testBit}(n, m)$.

Nat.boddDiv2_eq theorem

(n : ℕ) : boddDiv2 n = (bodd n, div2 n)

Full source

@[simp]
theorem boddDiv2_eq (n : ℕ) : boddDiv2 n = (bodd n, div2 n) := rfl

Decomposition of `boddDiv2` into oddness and half

Informal description

For any natural number $n$, the function `boddDiv2` applied to $n$ returns a pair consisting of the oddness of $n$ (as determined by `bodd`) and the floor of $n$ divided by 2 (as determined by `div2`). That is, $\text{boddDiv2}(n) = (\text{bodd}(n), \lfloor n/2 \rfloor)$.

Nat.div2_bit0 theorem

(n) : div2 (2 * n) = n

Full source

@[simp]
theorem div2_bit0 (n) : div2 (2 * n) = n :=
  div2_bit false n

Floor Division by Two of Even Number: $\lfloor 2n/2 \rfloor = n$

Informal description

For any natural number $n$, the floor division by 2 of $2n$ equals $n$, i.e., $\lfloor 2n/2 \rfloor = n$.

Nat.div2_bit1 theorem

(n) : div2 (2 * n + 1) = n

Full source

theorem div2_bit1 (n) : div2 (2 * n + 1) = n :=
  div2_bit true n

Floor Division of Odd Natural Number by Two: $\lfloor (2n + 1)/2 \rfloor = n$

Informal description

For any natural number $n$, the floor division by 2 of $2n + 1$ equals $n$, i.e., $\lfloor (2n + 1)/2 \rfloor = n$.

Nat.bit_add theorem

: ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit false n + bit b m

Full source

theorem bit_add : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit false n + bit b m
  | true,  _, _ => by dsimp [bit]; omega
  | false, _, _ => by dsimp [bit]; omega

Bit Addition Property: $\text{bit}\,b\,(n + m) = \text{bit}\,\text{false}\,n + \text{bit}\,b\,m$

Informal description

For any boolean value $b$ and natural numbers $n$ and $m$, the operation `bit b (n + m)` equals `bit false n + bit b m`. Here, `bit b n` constructs a natural number by appending the bit $b$ to the binary representation of $n$.

Nat.bit_add' theorem

: ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit b n + bit false m

Full source

theorem bit_add' : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit b n + bit false m
  | true,  _, _ => by dsimp [bit]; omega
  | false, _, _ => by dsimp [bit]; omega

Bit Addition Property: $\text{bit}(b, n + m) = \text{bit}(b, n) + \text{bit}(0, m)$

Informal description

For any boolean $b$ and natural numbers $n$ and $m$, the operation $\text{bit}(b, n + m)$ equals $\text{bit}(b, n) + \text{bit}(\text{false}, m)$, where $\text{bit}(b, k)$ denotes the natural number obtained by prepending the bit $b$ to the binary representation of $k$.

Nat.bit_ne_zero theorem

(b) {n} (h : n ≠ 0) : bit b n ≠ 0

Full source

theorem bit_ne_zero (b) {n} (h : n ≠ 0) : bitbit b n ≠ 0 := by
  cases b <;> dsimp [bit] <;> omega

Nonzero Preservation under Bit Construction

Informal description

For any boolean `b` and natural number `n`, if `n` is nonzero, then the number constructed by `bit b n` is also nonzero.

Nat.bitCasesOn_bit0 theorem

{motive : ℕ → Sort u} (H : ∀ b n, motive (bit b n)) (n : ℕ) : bitCasesOn (2 * n) H = H false n

Full source

@[simp]
theorem bitCasesOn_bit0 {motive : ℕ → Sort u} (H : ∀ b n, motive (bit b n)) (n : ℕ) :
    bitCasesOn (2 * n) H = H false n :=
  bitCasesOn_bit H false n

Case Analysis on Even Numbers via Bit Representation

Informal description

For any type-valued function `motive` on natural numbers and any function `H` that maps a boolean `b` and a natural number `n` to `motive (bit b n)`, the application of `bitCasesOn` to an even number `2 * n` with `H` is equal to `H false n`.

Nat.bitCasesOn_bit1 theorem

{motive : ℕ → Sort u} (H : ∀ b n, motive (bit b n)) (n : ℕ) : bitCasesOn (2 * n + 1) H = H true n

Full source

@[simp]
theorem bitCasesOn_bit1 {motive : ℕ → Sort u} (H : ∀ b n, motive (bit b n)) (n : ℕ) :
    bitCasesOn (2 * n + 1) H = H true n :=
  bitCasesOn_bit H true n

Case Analysis on Odd Numbers via `bitCasesOn`

Informal description

For any type-valued function `motive` on natural numbers and any function `H` that maps a boolean `b` and a natural number `n` to a term of type `motive (bit b n)`, the application of `bitCasesOn` to an odd number `2 * n + 1` with `H` equals `H true n`.

Nat.bit_cases_on_injective theorem

{motive : ℕ → Sort u} : Function.Injective fun H : ∀ b n, motive (bit b n) => fun n => bitCasesOn n H

Full source

theorem bit_cases_on_injective {motive : ℕ → Sort u} :
    Function.Injective fun H : ∀ b n, motive (bit b n) => fun n => bitCasesOn n H := by
  intro H₁ H₂ h
  ext b n
  simpa only [bitCasesOn_bit] using congr_fun h (bit b n)

Injectivity of `bitCasesOn` with Respect to the Handler Function

Informal description

For any type-valued function `motive` on natural numbers, the function that maps a function `H : ∀ b n, motive (bit b n)` to the function `fun n => bitCasesOn n H` is injective. In other words, if two functions `H₁` and `H₂` satisfy `bitCasesOn n H₁ = bitCasesOn n H₂` for all natural numbers `n`, then `H₁ = H₂`.

Nat.bit_cases_on_inj theorem

 {motive : ℕ → Sort u} (H₁ H₂ : ∀ b n, motive (bit b n)) :
  ((fun n => bitCasesOn n H₁) = fun n => bitCasesOn n H₂) ↔ H₁ = H₂

Full source

@[simp]
theorem bit_cases_on_inj {motive : ℕ → Sort u} (H₁ H₂ : ∀ b n, motive (bit b n)) :
    ((fun n => bitCasesOn n H₁) = fun n => bitCasesOn n H₂) ↔ H₁ = H₂ :=
  bit_cases_on_injective.eq_iff

Injectivity of `bitCasesOn` Handler Functions

Informal description

For any type-valued function `motive` on natural numbers and any two functions `H₁, H₂ : ∀ b n, motive (bit b n)`, the equality `(fun n => bitCasesOn n H₁) = (fun n => bitCasesOn n H₂)` holds if and only if `H₁ = H₂`.

Nat.bit_le theorem

: ∀ (b : Bool) {m n : ℕ}, m ≤ n → bit b m ≤ bit b n

Full source

lemma bit_le : ∀ (b : Bool) {m n : ℕ}, m ≤ n → bit b m ≤ bit b n
  | true, _, _, h => by dsimp [bit]; omega
  | false, _, _, h => by dsimp [bit]; omega

Monotonicity of Bit Operation with Respect to Natural Numbers

Informal description

For any boolean value $b$ and natural numbers $m$ and $n$, if $m \leq n$, then $\text{bit}(b, m) \leq \text{bit}(b, n)$.

Nat.bit_lt_bit theorem

(a b) (h : m < n) : bit a m < bit b n

Full source

lemma bit_lt_bit (a b) (h : m < n) : bit a m < bit b n := calc
  bit a m < 2 * n   := by cases a <;> dsimp [bit] <;> omega
        _ ≤ bit b n := by cases b <;> dsimp [bit] <;> omega

Bit Prepending Preserves Strict Inequality: $\text{bit}(a, m) < \text{bit}(b, n)$ when $m < n$

Informal description

For any boolean values $a, b$ and natural numbers $m, n$ such that $m < n$, the natural number obtained by prepending the bit $a$ to $m$ is strictly less than the natural number obtained by prepending the bit $b$ to $n$, i.e., $\text{bit}(a, m) < \text{bit}(b, n)$.

Nat.zero_bits theorem

: bits 0 = []

Full source

@[simp]
theorem zero_bits : bits 0 = [] := by simp [Nat.bits]

Binary Digits of Zero is Empty List

Informal description

The binary digits of the natural number $0$ is the empty list, i.e., $\text{bits}(0) = []$.

Nat.bits_append_bit theorem

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

Full source

@[simp]
theorem bits_append_bit (n : ℕ) (b : Bool) (hn : n = 0 → b = true) :
    (bit b n).bits = b :: n.bits := by
  rw [Nat.bits, Nat.bits, binaryRec_eq]
  simpa

Binary Digits of Bit-Prepended Number: $\text{bit}(b, n).\text{bits} = b :: n.\text{bits}$ with Zero Condition

Informal description

For any natural number $n$ and boolean value $b$, if $n = 0$ implies $b = \text{true}$, then the binary digits of the number obtained by prepending bit $b$ to $n$ (denoted as $\text{bit}(b, n)$) is equal to the list $b$ followed by the binary digits of $n$.

Nat.bit0_bits theorem

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

Full source

@[simp]
theorem bit0_bits (n : ℕ) (hn : n ≠ 0) : (2 * n).bits = falsefalse :: n.bits :=
  bits_append_bit n false fun hn' => absurd hn' hn

Binary digits of even numbers: $(2n).\text{bits} = \text{false} :: n.\text{bits}$ for $n \neq 0$

Informal description

For any nonzero natural number $n$, the binary digits of $2n$ (with least significant bit first) are equal to the list `false` followed by the binary digits of $n$, i.e., $(2n).\text{bits} = \text{false} :: n.\text{bits}$.

Nat.bit1_bits theorem

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

Full source

@[simp]
theorem bit1_bits (n : ℕ) : (2 * n + 1).bits = truetrue :: n.bits :=
  bits_append_bit n true fun _ => rfl

Binary digits of odd numbers: $(2n + 1).\text{bits} = \text{true} :: n.\text{bits}$

Informal description

For any natural number $n$, the binary digits of $2n + 1$ (with least significant bit first) are equal to the list `true` followed by the binary digits of $n$.

Nat.one_bits theorem

: Nat.bits 1 = [true]

Full source

@[simp]
theorem one_bits : Nat.bits 1 = [true] := by
  convert bit1_bits 0
  simp

Binary Digits of One is `[true]`

Informal description

The binary digits of the natural number $1$ (with least significant bit first) is the singleton list containing `true`, i.e., $\text{bits}(1) = [\text{true}]$.

Nat.bodd_eq_bits_head theorem

(n : ℕ) : n.bodd = n.bits.headI

Full source

theorem bodd_eq_bits_head (n : ℕ) : n.bodd = n.bits.headI := by
  induction n using Nat.binaryRec' with
  | z => simp
  | f _ _ h _ => simp [bodd_bit, bits_append_bit _ _ h]

Equivalence of Least Significant Bit and Head of Binary Digits List

Informal description

For any natural number $n$, the least significant bit of $n$ (as determined by `Nat.bodd`) is equal to the first element of its binary digits list (with `headI` returning the default value `false` for an empty list). That is, $\text{bodd}(n) = \text{headI}(\text{bits}(n))$.

Nat.div2_bits_eq_tail theorem

(n : ℕ) : n.div2.bits = n.bits.tail

Full source

theorem div2_bits_eq_tail (n : ℕ) : n.div2.bits = n.bits.tail := by
  induction n using Nat.binaryRec' with
  | z => simp
  | f _ _ h _ => simp [div2_bit, bits_append_bit _ _ h]

Binary Digits of Half Equal Tail of Original Digits: $\text{bits}(\lfloor n/2 \rfloor) = \text{tail}(\text{bits}(n))$

Informal description

For any natural number $n$, the binary digits of $\lfloor n/2 \rfloor$ (obtained via `Nat.div2`) are equal to the tail of the binary digits of $n$ (i.e., the list obtained by removing the first element).