Documentation

Mathlib.Init.Data.Nat.Bitwise

Lemmas about bitwise operations on natural numbers. #

Possibly only of archaeological significance.

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⌋

Equations
Instances For
    def Nat.div2 (n : ) :

    div2 n = ⌊n/2⌋ the greatest integer smaller than n/2

    Equations
    Instances For
      def Nat.bodd (n : ) :

      bodd n returns true if n is odd

      Equations
      Instances For
        @[simp]
        @[simp]
        @[simp]
        theorem Nat.bodd_add (m : ) (n : ) :
        @[simp]
        theorem Nat.bodd_mul (m : ) (n : ) :
        theorem Nat.mod_two_of_bodd (n : ) :
        n % 2 = bif Nat.bodd n then 1 else 0
        @[simp]
        theorem Nat.div2_zero :
        @[simp]
        theorem Nat.div2_succ (n : ) :
        theorem Nat.bodd_add_div2 (n : ) :
        (bif Nat.bodd n then 1 else 0) + 2 * Nat.div2 n = n
        theorem Nat.div2_val (n : ) :
        Nat.div2 n = n / 2
        def Nat.bit (b : Bool) :

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

        Equations
        Instances For
          theorem Nat.bit0_val (n : ) :
          bit0 n = 2 * n
          theorem Nat.bit1_val (n : ) :
          bit1 n = 2 * n + 1
          theorem Nat.bit_val (b : Bool) (n : ) :
          Nat.bit b n = 2 * n + bif b then 1 else 0
          def Nat.bitCasesOn {C : Sort u} (n : ) (h : (b : Bool) → (n : ) → C (Nat.bit b n)) :
          C n

          For a predicate C : Nat → Sort*, 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
            def Nat.shiftLeft' (b : Bool) (m : ) :

            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

            Equations
            Instances For
              @[simp]
              theorem Nat.shiftLeft'_false {m : } (n : ) :
              @[simp]
              theorem Nat.shiftLeft_eq' (m : ) (n : ) :

              Std4 takes the unprimed name for Nat.shiftLeft_eq m n : m <<< n = m * 2 ^ n.

              @[simp]
              theorem Nat.shiftRight_eq (m : ) (n : ) :
              theorem Nat.binaryRec_decreasing {n : } (h : n 0) :
              def Nat.binaryRec {C : Sort u} (z : C 0) (f : (b : Bool) → (n : ) → C nC (Nat.bit b n)) (n : ) :
              C n

              A recursion principle for bit representations of natural numbers. For a predicate C : Nat → Sort*, 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
                def Nat.size :

                size n : Returns the size of a natural number in bits i.e. the length of its binary representation

                Equations
                Instances For

                  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

                  Equations
                  Instances For
                    def Nat.ldiff :

                    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.

                    Equations
                    Instances For
                      @[simp]
                      theorem Nat.binaryRec_zero {C : Sort u} (z : C 0) (f : (b : Bool) → (n : ) → C nC (Nat.bit b n)) :

                      bitwise ops

                      theorem Nat.bodd_bit (b : Bool) (n : ) :
                      theorem Nat.div2_bit (b : Bool) (n : ) :
                      theorem Nat.shiftLeft'_add (b : Bool) (m : ) (n : ) (k : ) :
                      theorem Nat.shiftLeft_add (m : ) (n : ) (k : ) :
                      m <<< (n + k) = m <<< n <<< k
                      theorem Nat.shiftLeft'_sub (b : Bool) (m : ) {n : } {k : } :
                      k nNat.shiftLeft' b m (n - k) = Nat.shiftLeft' b m n >>> k
                      theorem Nat.shiftLeft_sub (m : ) {n : } {k : } :
                      k nm <<< (n - k) = m <<< n >>> k
                      theorem Nat.testBit_bit_zero (b : Bool) (n : ) :
                      theorem Nat.binaryRec_eq {C : Sort u} {z : C 0} {f : (b : Bool) → (n : ) → C nC (Nat.bit b n)} (h : f false 0 z = z) (b : Bool) (n : ) :
                      Nat.binaryRec z f (Nat.bit b n) = f b n (Nat.binaryRec z f n)