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 : Nat) : Nat

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

Equations

• Nat.bit b n = bif b then 2 * n + 1 else 2 * n

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

@[simp]

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

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

@[simp]

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

@[inline]

def Nat.bitCasesOn {motive : Nat → Sort u} (n : Nat) (h : (b : Bool) → (n : Nat) → 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.

Equations

• Nat.bitCasesOn n h = ⋯ ▸ h (1 &&& n != 0) (n >>> 1)

@[irreducible, specialize #[]]

def Nat.binaryRec {motive : Nat → Sort u} (z : motive 0) (f : (b : Bool) → (n : Nat) → motive n → motive (bit b n)) (n : Nat) : 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.

Equations

• Nat.binaryRec z f n = if n0 : n = 0 then ⋯ ▸ z else let x := f (1 &&& n != 0) (n >>> 1) (Nat.binaryRec z f (n >>> 1)); ⋯ ▸ x

@[specialize #[]]

def Nat.binaryRec' {motive : Nat → Sort u} (z : motive 0) (f : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (bit b n)) (n : Nat) : motive 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 n = Nat.binaryRec z (fun (b : Bool) (n : Nat) (ih : motive n) => if h : n = 0 → b = true then f b n h ih else have this := ⋯; ⋯ ▸ z) n

@[specialize #[]]

def Nat.binaryRecFromOne {motive : Nat → Sort u} (z₀ : motive 0) (z₁ : motive 1) (f : (b : Bool) → (n : Nat) → n ≠ 0 → motive n → motive (bit b n)) (n : Nat) : motive n

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

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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