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 : PosNum) (q : PosNum) :
    p.lor q = p ||| q

    Bitwise "and" for PosNum.

    Equations
    Instances For
      @[simp]
      theorem PosNum.land_eq_and (p : PosNum) (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

        Bitwise "xor" for PosNum.

        Equations
        Instances For
          @[simp]
          theorem PosNum.lxor_eq_xor (p : PosNum) (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
            • PosNum.one.oneBits x = [x]
            • p.bit0.oneBits x = p.oneBits (x + 1)
            • p.bit1.oneBits x = x :: p.oneBits (x + 1)
            Instances For

              Left-shift the binary representation of a PosNum.

              Equations
              • x.shiftl 0 = x
              • x.shiftl n.succ = x.bit0.shiftl n
              Instances For
                @[simp]
                theorem PosNum.shiftl_eq_shiftLeft (p : PosNum) (n : ) :
                p.shiftl n = p <<< n
                theorem PosNum.shiftl_succ_eq_bit0_shiftl (p : PosNum) (n : ) :
                p <<< n.succ = (p <<< n).bit0

                Right-shift the binary representation of a PosNum.

                Equations
                • x.shiftr 0 = Num.pos x
                • PosNum.one.shiftr x = 0
                • p.bit0.shiftr n.succ = p.shiftr n
                • p.bit1.shiftr n.succ = p.shiftr n
                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
                    Equations
                    @[simp]
                    theorem Num.lor_eq_or (p : Num) (q : Num) :
                    p.lor q = p ||| q
                    def Num.land :
                    NumNumNum

                    Bitwise "and" for Num.

                    Equations
                    Instances For
                      Equations
                      @[simp]
                      theorem Num.land_eq_and (p : Num) (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
                          instance Num.instXor :
                          Equations
                          @[simp]
                          theorem Num.lxor_eq_xor (p : Num) (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
                                    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
                                      Equations
                                      instance instOneSNum :
                                      Equations
                                      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.

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

                                                                    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
                                                                              • n.neg = n.not.succ
                                                                              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 : ) → Mathlib.Vector Bool n

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

                                                                                  Equations
                                                                                  • x.bits 0 = Mathlib.Vector.nil
                                                                                  • x.bits n.succ = x.head ::ᵥ x.tail.bits n
                                                                                  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 : SNum) (b : SNum) :

                                                                                      Add two SNums.

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

                                                                                        Subtract two SNums.

                                                                                        Equations
                                                                                        • a.sub b = a + -b
                                                                                        Instances For
                                                                                          Equations
                                                                                          def SNum.mul (a : SNum) :

                                                                                          Multiply two SNums.

                                                                                          Equations
                                                                                          • a.mul = SNum.rec' (fun (b : Bool) => bif b then -a else 0) fun (b : Bool) (x IH : SNum) => bif b then IH.bit0 + a else IH.bit0
                                                                                          Instances For
                                                                                            Equations