Documentation

Mathlib.Data.Nat.BinaryRec

Binary recursion on Nat #

This file defines binary recursion on Nat.

Main results #

source
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
    Instances For
      source
      theorem Nat.shiftRight_one (n : Nat) :
      n >>> 1 = n / 2
      source
      @[simp]
      theorem Nat.bit_decide_mod_two_eq_one_shiftRight_one (n : Nat) :
      bit (decide (n % 2 = 1)) (n >>> 1) = n
      source
      theorem Nat.bit_testBit_zero_shiftRight_one (n : Nat) :
      bit (n.testBit 0) (n >>> 1) = n
      source
      @[simp]
      theorem Nat.bit_eq_zero_iff {n : Nat} {b : Bool} :
      bit b n = 0 ↔ n = 0 ∧ b = false
      source
      @[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
        Instances For
          source
          @[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
            Instances For
              source
              @[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
                Instances For
                  source
                  @[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
                    Instances For
                      source
                      theorem Nat.bit_val (b : Bool) (n : Nat) :
                      bit b n = 2 * n + b.toNat
                      source
                      @[simp]
                      theorem Nat.bit_div_two (b : Bool) (n : Nat) :
                      bit b n / 2 = n
                      source
                      @[simp]
                      theorem Nat.bit_mod_two (b : Bool) (n : Nat) :
                      bit b n % 2 = b.toNat
                      source
                      @[simp]
                      theorem Nat.bit_shiftRight_one (b : Bool) (n : Nat) :
                      bit b n >>> 1 = n
                      source
                      theorem Nat.testBit_bit_zero (b : Bool) (n : Nat) :
                      (bit b n).testBit 0 = b
                      source
                      @[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
                      source
                      @[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
                      source
                      @[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
                      source
                      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)