Binary recursion on Nat

This file defines binary recursion on Nat.

Main results

• Nat.binaryRec: A recursion principle for bit representations of natural numbers.
• Nat.binaryRec': The same as binaryRec, but the induction step can assume that if n=0, the bit being appended is true.
• Nat.binaryRecFromOne: The same as binaryRec, but special casing both 0 and 1 as base cases.

def Nat.bit (b : Bool) (n : ℕ) : ℕ

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

theorem Nat.shiftRight_one (n : ℕ) : n >>> 1 = n / 2

@[simp]

theorem Nat.bit_decide_mod_two_eq_one_shiftRight_one (n : ℕ) : bit (decide (n % 2 = 1)) (n >>> 1) = n

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

@[simp]

theorem Nat.bit_false : bit false = fun (x : ℕ) => 2 * x

@[simp]

theorem Nat.bit_true : bit true = fun (x : ℕ) => 2 * x + 1

@[simp]

theorem Nat.bit_false_apply (n : ℕ) : bit false n = 2 * n

@[simp]

theorem Nat.bit_true_apply (n : ℕ) : bit true n = 2 * n + 1

@[simp]

theorem Nat.bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false

theorem Nat.bit_ne_zero_iff {n : ℕ} {b : Bool} : bit b n ≠ 0 ↔ n = 0 → b = true

@[inline]

def Nat.bitCasesOn {motive : ℕ → Sort u} (n : ℕ) (bit : (b : Bool) → (n : ℕ) → motive (bit b n)) : motive n

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.

@[simp]

theorem Nat.bit_lt_two_pow_succ_iff {b : Bool} {x n : ℕ} : bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n

theorem Nat.log2_eq_succ_log2_shiftRight {n : ℕ} (hn : n >>> 1 ≠ 0) : n.log2 = (n >>> 1).log2.succ

@[specialize #[]]

def Nat.binaryRec {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (bit b n)) (n : ℕ) : motive n

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.

@[specialize #[]]

def Nat.binaryRec' {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (bit b n)) (n : ℕ) : motive n

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

@[specialize #[]]

def Nat.binaryRecFromOne {motive : ℕ → Sort u} (zero : motive 0) (one : motive 1) (bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (bit b n)) (n : ℕ) : motive n

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

theorem Nat.bit_val (b : Bool) (n : ℕ) : bit b n = 2 * n + b.toNat

@[simp]

theorem Nat.bit_div_two (b : Bool) (n : ℕ) : bit b n / 2 = n

@[simp]

theorem Nat.bit_mod_two (b : Bool) (n : ℕ) : bit b n % 2 = b.toNat

@[simp]

theorem Nat.bit_shiftRight_one (b : Bool) (n : ℕ) : bit b n >>> 1 = n

theorem Nat.testBit_bit_zero (b : Bool) (n : ℕ) : (bit b n).testBit 0 = b

@[simp]

theorem Nat.bitCasesOn_bit {motive : ℕ → Sort u} (h : (b : Bool) → (n : ℕ) → motive (bit b n)) (b : Bool) (n : ℕ) : bitCasesOn (bit b n) h = h b n

@[simp]

theorem Nat.binaryRec_zero {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (bit b n)) : binaryRec zero bit 0 = zero

@[simp]

theorem Nat.binaryRec_one {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → motive n → motive (bit b n)) : binaryRec zero bit 1 = bit true 0 zero

theorem Nat.binaryRec_eq {motive : ℕ → Sort u} {zero : motive 0} {bit : (b : Bool) → (n : ℕ) → motive n → motive (bit b n)} (b : Bool) (n : ℕ) (h : bit false 0 zero = zero ∨ (n = 0 → b = true)) : binaryRec zero bit (Nat.bit b n) = bit b n (binaryRec zero bit n)

@[simp]

theorem Nat.binaryRec'_zero {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (bit b n)) : binaryRec' zero bit 0 = zero

@[simp]

theorem Nat.binaryRec'_one {motive : ℕ → Sort u} (zero : motive 0) (bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (bit b n)) : binaryRec' zero bit 1 = bit true 0 binaryRec'_one._proof_1 zero

theorem Nat.binaryRec'_eq {motive : ℕ → Sort u} {zero : motive 0} {bit : (b : Bool) → (n : ℕ) → (n = 0 → b = true) → motive n → motive (bit b n)} (b : Bool) (n : ℕ) (h : n = 0 → b = true) : binaryRec' zero bit (Nat.bit b n) = bit b n h (binaryRec' zero bit n)

@[simp]

theorem Nat.binaryRecFromOne_zero {motive : ℕ → Sort u} (zero : motive 0) (one : motive 1) (bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (bit b n)) : binaryRecFromOne zero one bit 0 = zero

@[simp]

theorem Nat.binaryRecFromOne_one {motive : ℕ → Sort u} {zero : motive 0} {one : motive 1} (bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (bit b n)) : binaryRecFromOne zero one bit 1 = one

theorem Nat.binaryRecFromOne_eq {motive : ℕ → Sort u} {zero : motive 0} {one : motive 1} {bit : (b : Bool) → (n : ℕ) → n ≠ 0 → motive n → motive (bit b n)} (b : Bool) (n : ℕ) (h : n ≠ 0) : binaryRecFromOne zero one bit (Nat.bit b n) = bit b n h (binaryRecFromOne zero one bit n)