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

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

Equations

Left-shift the binary representation of a PosNum.

Equations
def Num.lor :
NumNumNum

Bitwise "or" for Num.

Equations
def Num.land :
NumNumNum

Bitwise "and" for Num.

Equations
def Num.ldiff :
NumNumNum

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

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

Bitwise "xor" for Num.

Equations
def Num.shiftl :
NumNum

Left-shift the binary representation of a Num.

Equations
def Num.shiftr :
NumNum

Right-shift the binary representation of a Num.

Equations
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

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

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

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

      Equations

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

      Equations

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

      Equations

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

      Equations

      Sign of a SNum.

      Equations
      @[match_pattern]
      def SNum.not :

      Bitwise not for SNum.

      Equations
      @[match_pattern]
      def SNum.bit :
      BoolSNumSNum

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

      Equations

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

      Equations

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

      Equations
      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

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

      Equations

      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
      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
      def SNum.rec' {α : Sort u_1} (z : Boolα) (s : BoolSNumαα) :
      SNumα

      An induction principle for SNum which avoids relying on NzsNum.

      Equations
      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

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

      Equations

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

      Equations
      def SNum.neg (n : SNum) :

      The opposite of a SNum.

      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
      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
      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.
      def SNum.add (a : SNum) (b : SNum) :

      Add two SNums.

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

      Subtract two SNums.

      Equations
      def SNum.mul (a : SNum) :

      Multiply two SNums.

      Equations