Mathlib.Data.Nat.BinaryRec

Nat.bit definition

(b : Bool) (n : Nat) : Nat

Full source

/-- `bit b` appends the digit `b` to the little end of the binary representation of
its natural number input. -/
def bit (b : Bool) (n : Nat) : Nat :=
  cond b (2 * n + 1) (2 * n)

Appending a bit to a natural number

Informal description

The function `Nat.bit` takes a boolean `b` and a natural number `n`, and returns `2n + 1` if `b` is true, or `2n` if `b` is false. This operation effectively appends the bit `b` to the little-endian binary representation of `n`.

Nat.shiftRight_one theorem

(n) : n >>> 1 = n / 2

Full source

theorem shiftRight_one (n) : n >>> 1 = n / 2 := rfl

Right Shift by One Equals Division by Two for Natural Numbers

Informal description

For any natural number $n$, the right shift operation by one bit is equal to division by two, i.e., $n \gg 1 = n / 2$.

Nat.bit_decide_mod_two_eq_one_shiftRight_one theorem

(n : Nat) : bit (n % 2 = 1) (n >>> 1) = n

Full source

@[simp]
theorem bit_decide_mod_two_eq_one_shiftRight_one (n : Nat) : bit (n % 2 = 1) (n >>> 1) = n := by
  simp only [bit, shiftRight_one]
  cases mod_two_eq_zero_or_one n with | _ h => simpa [h] using Nat.div_add_mod n 2

Reconstruction of Natural Number from Its Least Significant Bit and Right Shift

Informal description

For any natural number $n$, the operation of appending the bit indicating whether $n$ is odd (i.e., $n \bmod 2 = 1$) to the result of right-shifting $n$ by one bit reconstructs the original number $n$. In other words, $\text{bit}(n \bmod 2 = 1, n \gg 1) = n$.

Nat.bit_testBit_zero_shiftRight_one theorem

(n : Nat) : bit (n.testBit 0) (n >>> 1) = n

Full source

theorem bit_testBit_zero_shiftRight_one (n : Nat) : bit (n.testBit 0) (n >>> 1) = n := by
  simp

Reconstruction of Natural Number from Least Significant Bit and Right Shift: $\text{bit}(\text{testBit}\,0\,n, n \gg 1) = n$

Informal description

For any natural number $n$, the operation of appending the bit corresponding to the least significant bit of $n$ (given by `n.testBit 0`) to the result of right-shifting $n$ by one bit reconstructs the original number $n$. In other words, $\text{bit}(n.\text{testBit}\, 0, n \gg 1) = n$.

Nat.bit_eq_zero_iff theorem

{n : Nat} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false

Full source

@[simp]
theorem bit_eq_zero_iff {n : Nat} {b : Bool} : bitbit b n = 0 ↔ n = 0 ∧ b = false := by
  cases n <;> cases b <;> simp [bit, Nat.shiftLeft_succ, Nat.two_mul, ← Nat.add_assoc]

Zero Condition for Bit-Appended Natural Numbers: $\text{bit}(b, n) = 0 \leftrightarrow n = 0 \land b = \text{false}$

Informal description

For any natural number $n$ and boolean $b$, the result of appending bit $b$ to $n$ (denoted by $\text{bit}(b, n)$) equals zero if and only if both $n = 0$ and $b$ is false.

Nat.bitCasesOn definition

{motive : Nat → Sort u} (n) (h : ∀ b n, motive (bit b n)) : motive n

Full source

/-- For a predicate `motive : Nat → Sort u`, if instances can be
  constructed for natural numbers of the form `bit b n`,
  they can be constructed for any given natural number. -/
@[inline]
def bitCasesOn {motive : Nat → Sort u} (n) (h : ∀ b n, motive (bit b n)) : motive n :=
  -- `1 &&& n != 0` is faster than `n.testBit 0`. This may change when we have faster `testBit`.
  let x := h (1 &&& n != 0) (n >>> 1)
  -- `congrArg motive _ ▸ x` is defeq to `x` in non-dependent case
  congrArg motive n.bit_testBit_zero_shiftRight_one ▸ x

Case analysis on binary representation of natural numbers

Informal description

Given a predicate `motive : ℕ → Sort u` and a natural number `n`, if for every boolean `b` and natural number `k` we can construct an instance of `motive (bit b k)`, then we can construct an instance of `motive n`. Here, `bit b k` represents the natural number formed by appending the bit `b` to the binary representation of `k` (yielding `2k + 1` if `b` is true, or `2k` if `b` is false).

Nat.binaryRec definition

{motive : Nat → Sort u} (z : motive 0) (f : ∀ b n, motive n → motive (bit b n)) (n : Nat) : motive n

Full source

/-- A recursion principle for `bit` representations of natural numbers.
  For a predicate `motive : Nat → Sort u`, if instances can be
  constructed for natural numbers of the form `bit b n`,
  they can be constructed for all natural numbers. -/
@[elab_as_elim, specialize]
def binaryRec {motive : Nat → Sort u} (z : motive 0) (f : ∀ b n, motive n → motive (bit b n))
    (n : Nat) : motive n :=
  if n0 : n = 0 then congrArg motive n0 ▸ z
  else
    let x := f (1 &&& n != 0) (n >>> 1) (binaryRec z f (n >>> 1))
    congrArg motive n.bit_testBit_zero_shiftRight_one ▸ x
decreasing_by exact bitwise_rec_lemma n0

Binary recursion principle for natural numbers

Informal description

Given a predicate `motive : ℕ → Sort u`, if we can construct instances for `motive 0` and for `motive (bit b n)` assuming we already have an instance for `motive n`, then we can construct an instance for any natural number `n`. Here, `bit b n` represents the number obtained by appending the bit `b` to the binary representation of `n` (yielding `2n + 1` if `b` is true, or `2n` if `b` is false).

Nat.binaryRec' definition

 {motive : Nat → Sort u} (z : motive 0) (f : ∀ b n, (n = 0 → b = true) → motive n → motive (bit b n)) : ∀ n, motive n

Full source

/-- The same as `binaryRec`, but the induction step can assume that if `n=0`,
  the bit being appended is `true` -/
@[elab_as_elim, specialize]
def binaryRec' {motive : Nat → Sort u} (z : motive 0)
    (f : ∀ b n, (n = 0 → b = true) → motive n → motive (bit b n)) :
    ∀ n, motive n :=
  binaryRec z fun b n ih =>
    if h : n = 0 → b = true then f b n h ih
    else
      have : bit b n = 0 := by
        rw [bit_eq_zero_iff]
        cases n <;> cases b <;> simp at h ⊢
      congrArg motive this ▸ z

Binary recursion principle for natural numbers with zero case constraint

Informal description

Given a predicate `motive : ℕ → Sort u`, if we can construct an instance for `motive 0` and for `motive (bit b n)` assuming we already have an instance for `motive n` and that whenever `n = 0` the bit `b` must be `true`, then we can construct an instance for any natural number `n`. Here, `bit b n` represents the number obtained by appending the bit `b` to the binary representation of `n` (yielding `2n + 1` if `b` is true, or `2n` if `b` is false).

Nat.binaryRecFromOne definition

 {motive : Nat → Sort u} (z₀ : motive 0) (z₁ : motive 1) (f : ∀ b n, n ≠ 0 → motive n → motive (bit b n)) :
  ∀ n, motive n

Full source

/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
@[elab_as_elim, specialize]
def binaryRecFromOne {motive : Nat → Sort u} (z₀ : motive 0) (z₁ : motive 1)
    (f : ∀ b n, n ≠ 0 → motive n → motive (bit b n)) :
    ∀ n, motive n :=
  binaryRec' z₀ fun b n h ih =>
    if h' : n = 0 then
      have : bit b n = bit true 0 := by
        rw [h', h h']
      congrArg motive this ▸ z₁
    else f b n h' ih

Binary recursion principle for natural numbers with base cases 0 and 1

Informal description

Given a predicate `motive : ℕ → Sort u`, if we can construct instances for `motive 0` and `motive 1`, and for `motive (bit b n)` assuming we already have an instance for `motive n` and that `n ≠ 0`, then we can construct an instance for any natural number `n`. Here, `bit b n` represents the number obtained by appending the bit `b` to the binary representation of `n` (yielding `2n + 1` if `b` is true, or `2n` if `b` is false).

Nat.bit_val theorem

(b n) : bit b n = 2 * n + b.toNat

Full source

theorem bit_val (b n) : bit b n = 2 * n + b.toNat := by
  cases b <;> rfl

Bit Appending Formula: $\operatorname{bit}(b, n) = 2n + \operatorname{toNat}(b)$

Informal description

For any boolean $b$ and natural number $n$, the operation of appending bit $b$ to $n$ satisfies $\operatorname{bit}(b, n) = 2n + \operatorname{toNat}(b)$, where $\operatorname{toNat}(b)$ is $1$ if $b$ is true and $0$ otherwise.

Nat.bit_div_two theorem

(b n) : bit b n / 2 = n

Full source

@[simp]
theorem bit_div_two (b n) : bit b n / 2 = n := by
  rw [bit_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
  · cases b <;> decide
  · decide

Division by Two After Bit Appending: $\operatorname{bit}(b, n)/2 = n$

Informal description

For any boolean $b$ and natural number $n$, the result of appending bit $b$ to $n$ and then performing integer division by 2 equals $n$, i.e., $\operatorname{bit}(b, n) / 2 = n$.

Nat.bit_mod_two theorem

(b n) : bit b n % 2 = b.toNat

Full source

@[simp]
theorem bit_mod_two (b n) : bit b n % 2 = b.toNat := by
  cases b <;> simp [bit_val, mul_add_mod]

Modulo Two of Bit-Appended Number: $\operatorname{bit}(b, n) \mod 2 = \operatorname{toNat}(b)$

Informal description

For any boolean $b$ and natural number $n$, the remainder when $\operatorname{bit}(b, n)$ is divided by 2 equals $\operatorname{toNat}(b)$, i.e., $\operatorname{bit}(b, n) \mod 2 = \operatorname{toNat}(b)$.

Nat.bit_shiftRight_one theorem

(b n) : bit b n >>> 1 = n

Full source

@[simp]
theorem bit_shiftRight_one (b n) : bitbit b n >>> 1 = n :=
  bit_div_two b n

Right-shift by One of Bit-Appended Number Equals Original Number

Informal description

For any boolean $b$ and natural number $n$, the result of right-shifting the number $\operatorname{bit}(b, n)$ by one bit equals $n$, i.e., $\operatorname{bit}(b, n) \gg 1 = n$.

Nat.testBit_bit_zero theorem

(b n) : (bit b n).testBit 0 = b

Full source

theorem testBit_bit_zero (b n) : (bit b n).testBit 0 = b := by
  simp

Zeroth Bit of Bit-Appended Number Equals Appended Bit

Informal description

For any boolean $b$ and natural number $n$, the zeroth bit (least significant bit) of the number obtained by appending $b$ to $n$ is equal to $b$, i.e., $\operatorname{testBit}(\operatorname{bit}(b, n), 0) = b$.

Nat.bitCasesOn_bit theorem

(h : ∀ b n, motive (bit b n)) (b : Bool) (n : Nat) : bitCasesOn (bit b n) h = h b n

Full source

@[simp]
theorem bitCasesOn_bit (h : ∀ b n, motive (bit b n)) (b : Bool) (n : Nat) :
    bitCasesOn (bit b n) h = h b n := by
  change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
  generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
  rw [testBit_bit_zero, bit_shiftRight_one]
  intros; rfl

Case Analysis on Bit-Appended Number Reduces to Given Function

Informal description

For any predicate `motive : ℕ → Sort u` and function `h` such that `h b n` constructs an instance of `motive (bit b n)` for all booleans `b` and natural numbers `n`, the case analysis `bitCasesOn` applied to the number `bit b n` with `h` evaluates to `h b n`. In other words, $\text{bitCasesOn}\,(\text{bit}\,b\,n)\,h = h\,b\,n$.

Nat.binaryRec_zero theorem

(z : motive 0) (f : ∀ b n, motive n → motive (bit b n)) : binaryRec z f 0 = z

Full source

@[simp]
theorem binaryRec_zero (z : motive 0) (f : ∀ b n, motive n → motive (bit b n)) :
    binaryRec z f 0 = z := by
  rw [binaryRec]
  simp

Base Case of Binary Recursion on Natural Numbers

Informal description

For any predicate `motive : ℕ → Sort u`, the binary recursion principle `binaryRec` applied to the base case `z : motive 0` and step function `f` evaluates to `z` when the input is `0`. That is, $\text{binaryRec}\,z\,f\,0 = z$.

Nat.binaryRec_one theorem

(z : motive 0) (f : ∀ b n, motive n → motive (bit b n)) : binaryRec (motive := motive) z f 1 = f true 0 z

Full source

@[simp]
theorem binaryRec_one (z : motive 0) (f : ∀ b n, motive n → motive (bit b n)) :
    binaryRec (motive := motive) z f 1 = f true 0 z := by
  rw [binaryRec]
  simp only [add_one_ne_zero, ↓reduceDIte, Nat.reduceShiftRight, binaryRec_zero]
  rfl

Binary Recursion Evaluation at One

Informal description

For any predicate `motive : ℕ → Sort u`, the binary recursion principle `binaryRec` applied to the base case `z : motive 0` and step function `f` evaluates to `f true 0 z` when the input is `1`. That is, $\text{binaryRec}\,z\,f\,1 = f\,\text{true}\,0\,z$.

Nat.binaryRec_eq theorem

 {z : motive 0} {f : ∀ b n, motive n → motive (bit b n)} (b n) (h : f false 0 z = z ∨ (n = 0 → b = true)) :
  binaryRec z f (bit b n) = f b n (binaryRec z f n)

Full source

theorem binaryRec_eq {z : motive 0} {f : ∀ b n, motive n → motive (bit b n)}
    (b n) (h : f false 0 z = z ∨ (n = 0 → b = true)) :
    binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
  by_cases h' : bit b n = 0
  case pos =>
    obtain ⟨rfl, rfl⟩ := bit_eq_zero_iff.mp h'
    simp only [Bool.false_eq_true, imp_false, not_true_eq_false, or_false] at h
    unfold binaryRec
    exact h.symm
  case neg =>
    rw [binaryRec, dif_neg h']
    change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ f _ _ _ = _
    generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
    rw [testBit_bit_zero, bit_shiftRight_one]
    intros; rfl

Binary Recursion Step for Natural Numbers: $\text{binaryRec}\,z\,f\,(\text{bit}\,b\,n) = f\,b\,n\,(\text{binaryRec}\,z\,f\,n)$

Informal description

Let `motive : ℕ → Sort u` be a predicate, `z : motive 0` a base case, and `f : ∀ (b : Bool) (n : ℕ), motive n → motive (bit b n)` a recursive step function. For any boolean `b` and natural number `n`, if either `f false 0 z = z` holds or the implication `n = 0 → b = true` holds, then the binary recursion satisfies: \[ \text{binaryRec}\,z\,f\,(\text{bit}\,b\,n) = f\,b\,n\,(\text{binaryRec}\,z\,f\,n) \]

Main results