Documentation

Mathlib.Data.Num.Bitwise

Bitwise operations using binary representation of integers #

Definitions #

a.testBit n is true iff the n-th bit (starting from the LSB) in the binary representation of a is active. If the size of a is less than n, this evaluates to false.

Equations
Instances For

    n.oneBits 0 is the list of indices of active bits in the binary representation of n.

    Equations
    Instances For

      Left-shift the binary representation of a PosNum.

      Equations
      Instances For

        Right-shift the binary representation of a PosNum.

        Equations
        Instances For
          def Num.lor :
          NumNumNum

          Bitwise "or" for Num.

          Instances For
            def Num.land :
            NumNumNum

            Bitwise "and" for Num.

            Instances For
              def Num.ldiff :
              NumNumNum

              Bitwise fun a b ↦ a && !b for Num. For example, ldiff 5 9 = 4:

               101
              1001
              ----
               100
              
              Instances For
                def Num.lxor :
                NumNumNum

                Bitwise "xor" for Num.

                Instances For
                  def Num.shiftl :
                  NumNum

                  Left-shift the binary representation of a Num.

                  Instances For
                    def Num.shiftr :
                    NumNum

                    Right-shift the binary representation of a Num.

                    Instances For
                      def Num.testBit :
                      NumBool

                      a.testBit n is true iff the n-th bit (starting from the LSB) in the binary representation of a is active. If the size of a is less than n, this evaluates to false.

                      Instances For

                        n.oneBits is the list of indices of active bits in the binary representation of n.

                        Instances For
                          inductive NzsNum :

                          This is a nonzero (and "non minus one") version of SNum. See the documentation of SNum for more details.

                          Instances For
                            inductive SNum :

                            Alternative representation of integers using a sign bit at the end. The convention on sign here is to have the argument to msb denote the sign of the MSB itself, with all higher bits set to the negation of this sign. The result is interpreted in two's complement.

                            13 = ..0001101(base 2) = nz (bit1 (bit0 (bit1 (msb true)))) -13 = ..1110011(base 2) = nz (bit1 (bit1 (bit0 (msb false))))

                            As with Num, a special case must be added for zero, which has no msb, but by two's complement symmetry there is a second special case for -1. Here the Bool field indicates the sign of the number.

                            0 = ..0000000(base 2) = zero false -1 = ..1111111(base 2) = zero true

                            Instances For

                              The SNum representation uses a bit string, essentially a list of 0 (false) and 1 (true) bits, and the negation of the MSB is sign-extended to all higher bits.

                              Add a bit at the end of a NzsNum.

                              Instances For

                                Sign of a NzsNum.

                                Equations
                                Instances For
                                  @[match_pattern]

                                  Bitwise not for NzsNum.

                                  Equations
                                  Instances For

                                    Bitwise not for NzsNum.

                                    Instances For

                                      Add an inactive bit at the end of a NzsNum. This mimics PosNum.bit0.

                                      Instances For

                                        Add an active bit at the end of a NzsNum. This mimics PosNum.bit1.

                                        Instances For

                                          The head of a NzsNum is the boolean value of its LSB.

                                          Instances For

                                            The tail of a NzsNum is the SNum obtained by removing the LSB. Edge cases: tail 1 = 0 and tail (-2) = -1.

                                            Instances For

                                              Sign of a SNum.

                                              Instances For
                                                @[match_pattern]
                                                def SNum.not :

                                                Bitwise not for SNum.

                                                Instances For

                                                  Bitwise not for SNum.

                                                  Instances For
                                                    @[match_pattern]
                                                    def SNum.bit :
                                                    BoolSNumSNum

                                                    Add a bit at the end of a SNum. This mimics NzsNum.bit.

                                                    Instances For

                                                      Add a bit at the end of a SNum. This mimics NzsNum.bit.

                                                      Instances For

                                                        Add an inactive bit at the end of a SNum. This mimics ZNum.bit0.

                                                        Instances For

                                                          Add an active bit at the end of a SNum. This mimics ZNum.bit1.

                                                          Instances For
                                                            def NzsNum.drec' {C : SNumSort u_1} (z : (b : Bool) → C (SNum.zero b)) (s : (b : Bool) → (p : SNum) → C pC (SNum.bit b p)) (p : NzsNum) :
                                                            C (SNum.nz p)

                                                            A dependent induction principle for NzsNum, with base cases 0 : SNum and (-1) : SNum.

                                                            Equations
                                                            Instances For

                                                              The head of a SNum is the boolean value of its LSB.

                                                              Instances For

                                                                The tail of a SNum is obtained by removing the LSB. Edge cases: tail 1 = 0, tail (-2) = -1, tail 0 = 0 and tail (-1) = -1.

                                                                Instances For
                                                                  def SNum.drec' {C : SNumSort u_1} (z : (b : Bool) → C (SNum.zero b)) (s : (b : Bool) → (p : SNum) → C pC (SNum.bit b p)) (p : SNum) :
                                                                  C p

                                                                  A dependent induction principle for SNum which avoids relying on NzsNum.

                                                                  Instances For
                                                                    def SNum.rec' {α : Sort u_1} (z : Boolα) (s : BoolSNumαα) :
                                                                    SNumα

                                                                    An induction principle for SNum which avoids relying on NzsNum.

                                                                    Instances For
                                                                      def SNum.testBit :
                                                                      SNumBool

                                                                      SNum.testBit n a is true iff the n-th bit (starting from the LSB) of a is active. If the size of a is less than n, this evaluates to false.

                                                                      Equations
                                                                      Instances For

                                                                        The successor of a SNum (i.e. the operation adding one).

                                                                        Instances For

                                                                          The predecessor of a SNum (i.e. the operation of removing one).

                                                                          Instances For
                                                                            def SNum.neg (n : SNum) :

                                                                            The opposite of a SNum.

                                                                            Instances For
                                                                              def SNum.czAdd :
                                                                              BoolBoolSNumSNum

                                                                              SNum.czAdd a b n is n + a - b (where a and b should be read as either 0 or 1). This is useful to implement the carry system in cAdd.

                                                                              Instances For
                                                                                def SNum.bits :
                                                                                SNum(n : ) → Vector Bool n

                                                                                a.bits n is the vector of the n first bits of a (starting from the LSB).

                                                                                Equations
                                                                                Instances For
                                                                                  def SNum.cAdd :
                                                                                  SNumSNumBoolSNum

                                                                                  SNum.cAdd n m a is n + m + a (where a should be read as either 0 or 1). a represents a carry bit.

                                                                                  Instances For
                                                                                    def SNum.add (a : SNum) (b : SNum) :

                                                                                    Add two SNums.

                                                                                    Instances For
                                                                                      def SNum.sub (a : SNum) (b : SNum) :

                                                                                      Subtract two SNums.

                                                                                      Instances For
                                                                                        def SNum.mul (a : SNum) :

                                                                                        Multiply two SNums.

                                                                                        Instances For