Documentation

Mathlib.Data.Num.Bitwise

Bitwise operations using binary representation of integers #

Definitions #

Bitwise "or" for PosNum.

Equations
Instances For
    @[simp]
    theorem PosNum.lor_eq_or (p q : PosNum) :
    p.lor q = p ||| q

    Bitwise "and" for PosNum.

    Equations
    Instances For
      @[simp]
      theorem PosNum.land_eq_and (p q : PosNum) :
      p.land q = p &&& q

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

       101
      1001
      ----
       100
      
      Equations
      Instances For
        @[simp]
        theorem PosNum.lxor_eq_xor (p q : PosNum) :
        p.lxor q = p ^^^ q

        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
              @[simp]
              theorem PosNum.shiftl_eq_shiftLeft (p : PosNum) (n : ) :
              p.shiftl n = p <<< n

              Right-shift the binary representation of a PosNum.

              Equations
              Instances For
                @[simp]
                theorem PosNum.shiftr_eq_shiftRight (p : PosNum) (n : ) :
                p.shiftr n = p >>> n
                def Num.lor :
                NumNumNum

                Bitwise "or" for Num.

                Equations
                Instances For
                  @[simp]
                  theorem Num.lor_eq_or (p q : Num) :
                  p.lor q = p ||| q
                  def Num.land :
                  NumNumNum

                  Bitwise "and" for Num.

                  Equations
                  Instances For
                    @[simp]
                    theorem Num.land_eq_and (p q : Num) :
                    p.land q = p &&& q
                    def Num.ldiff :
                    NumNumNum

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

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

                      Bitwise "xor" for Num.

                      Equations
                      Instances For
                        @[simp]
                        theorem Num.lxor_eq_xor (p q : Num) :
                        p.lxor q = p ^^^ q
                        def Num.shiftl :
                        NumNum

                        Left-shift the binary representation of a Num.

                        Equations
                        Instances For
                          @[simp]
                          theorem Num.shiftl_eq_shiftLeft (p : Num) (n : ) :
                          p.shiftl n = p <<< n
                          def Num.shiftr :
                          NumNum

                          Right-shift the binary representation of a Num.

                          Equations
                          Instances For
                            @[simp]
                            theorem Num.shiftr_eq_shiftRight (p : Num) (n : ) :
                            p.shiftr n = p >>> n
                            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.

                            Equations
                            Instances For

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

                              Equations
                              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
                                  def instDecidableEqNzsNum.decEq (x✝ x✝¹ : NzsNum) :
                                  Decidable (x✝ = x✝¹)
                                  Equations
                                  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
                                      def instDecidableEqSNum.decEq (x✝ x✝¹ : SNum) :
                                      Decidable (x✝ = x✝¹)
                                      Equations
                                      Instances For
                                        instance instOneSNum :
                                        Equations

                                        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.

                                        Equations
                                        Instances For

                                          Sign of a NzsNum.

                                          Equations
                                          Instances For
                                            @[match_pattern]

                                            Bitwise not for NzsNum.

                                            Equations
                                            Instances For

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

                                              Equations
                                              Instances For

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

                                                Equations
                                                Instances For

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

                                                  Equations
                                                  Instances For

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

                                                    Equations
                                                    Instances For

                                                      Sign of a SNum.

                                                      Equations
                                                      Instances For
                                                        @[match_pattern]
                                                        def SNum.not :

                                                        Bitwise not for SNum.

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

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

                                                          Equations
                                                          Instances For

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

                                                            Equations
                                                            Instances For

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

                                                              Equations
                                                              Instances For

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

                                                                Equations
                                                                Instances For
                                                                  theorem SNum.bit_zero (b : Bool) :
                                                                  bit b (zero b) = zero b
                                                                  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.

                                                                    Equations
                                                                    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.

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

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

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

                                                                          An induction principle for SNum which avoids relying on NzsNum.

                                                                          Equations
                                                                          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).

                                                                              Equations
                                                                              Instances For

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

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

                                                                                  The opposite of a SNum.

                                                                                  Equations
                                                                                  Instances For
                                                                                    Equations
                                                                                    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.

                                                                                    Equations
                                                                                    Instances For
                                                                                      def SNum.bits :
                                                                                      SNum(n : ) → List.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.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          def SNum.add (a b : SNum) :

                                                                                          Add two SNums.

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

                                                                                            Subtract two SNums.

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

                                                                                              Multiply two SNums.

                                                                                              Equations
                                                                                              Instances For
                                                                                                Equations