Bitwise operations using binary representation of integers

Definitions

• bitwise operations for PosNum and Num,
• SNum, a type that represents integers as a bit string with a sign bit at the end,
• arithmetic operations for SNum.

def PosNum.lor : PosNum → PosNum → PosNum

Bitwise "or" for PosNum.

@[implicit_reducible]

instance PosNum.instOrOp : OrOp PosNum

@[simp]

theorem PosNum.lor_eq_or (p q : PosNum) : p.lor q = p ||| q

def PosNum.land : PosNum → PosNum → Num

Bitwise "and" for PosNum.

@[implicit_reducible]

instance PosNum.instHAndNum : HAnd PosNum PosNum Num

@[simp]

theorem PosNum.land_eq_and (p q : PosNum) : p.land q = p &&& q

def PosNum.ldiff : PosNum → PosNum → Num

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

 101
1001
----
 100

def PosNum.lxor : PosNum → PosNum → Num

Bitwise "xor" for PosNum.

@[implicit_reducible]

instance PosNum.instHXorNum : HXor PosNum PosNum Num

@[simp]

theorem PosNum.lxor_eq_xor (p q : PosNum) : p.lxor q = p ^^^ q

def PosNum.testBit : PosNum → ℕ → Bool

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.

def PosNum.oneBits : PosNum → ℕ → List ℕ

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

def PosNum.shiftl : PosNum → ℕ → PosNum

Left-shift the binary representation of a PosNum.

@[implicit_reducible]

instance PosNum.instHShiftLeftNat : HShiftLeft PosNum ℕ PosNum

@[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

def PosNum.shiftr : PosNum → ℕ → Num

Right-shift the binary representation of a PosNum.

@[implicit_reducible]

instance PosNum.instHShiftRightNatNum : HShiftRight PosNum ℕ Num

@[simp]

theorem PosNum.shiftr_eq_shiftRight (p : PosNum) (n : ℕ) : p.shiftr n = p >>> n

def Num.lor : Num → Num → Num

Bitwise "or" for Num.

@[implicit_reducible]

instance Num.instOrOp : OrOp Num

@[simp]

theorem Num.lor_eq_or (p q : Num) : p.lor q = p ||| q

def Num.land : Num → Num → Num

Bitwise "and" for Num.

@[implicit_reducible]

instance Num.instAndOp : AndOp Num

@[simp]

theorem Num.land_eq_and (p q : Num) : p.land q = p &&& q

def Num.ldiff : Num → Num → Num

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

 101
1001
----
 100

def Num.lxor : Num → Num → Num

Bitwise "xor" for Num.

@[implicit_reducible]

instance Num.instXorOp : XorOp Num

@[simp]

theorem Num.lxor_eq_xor (p q : Num) : p.lxor q = p ^^^ q

def Num.shiftl : Num → ℕ → Num

Left-shift the binary representation of a Num.

@[implicit_reducible]

instance Num.instHShiftLeftNat : HShiftLeft Num ℕ Num

@[simp]

theorem Num.shiftl_eq_shiftLeft (p : Num) (n : ℕ) : p.shiftl n = p <<< n

def Num.shiftr : Num → ℕ → Num

Right-shift the binary representation of a Num.

@[implicit_reducible]

instance Num.instHShiftRightNat : HShiftRight Num ℕ Num

@[simp]

theorem Num.shiftr_eq_shiftRight (p : Num) (n : ℕ) : p.shiftr n = p >>> n

def Num.testBit : Num → ℕ → Bool

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.

def Num.oneBits : Num → List ℕ

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

inductive NzsNum : Type

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

• msb : Bool → NzsNum
• bit : Bool → NzsNum → NzsNum

  Add a bit at the end of a NzsNum.

@[implicit_reducible]

instance instDecidableEqNzsNum : DecidableEq NzsNum

def instDecidableEqNzsNum.decEq (x✝ x✝¹ : NzsNum) : Decidable (x✝ = x✝¹)

inductive SNum : Type

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

• zero : Bool → SNum
• nz : NzsNum → SNum

def instDecidableEqSNum.decEq (x✝ x✝¹ : SNum) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instDecidableEqSNum : DecidableEq SNum

@[implicit_reducible]

instance instCoeNzsNumSNum : Coe NzsNum SNum

@[implicit_reducible]

instance instZeroSNum : Zero SNum

@[implicit_reducible]

instance instOneNzsNum : One NzsNum

@[implicit_reducible]

instance instOneSNum : One SNum

@[implicit_reducible]

instance instInhabitedNzsNum : Inhabited NzsNum

@[implicit_reducible]

instance instInhabitedSNum : Inhabited SNum

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.

def NzsNum.«term_::_» : Lean.TrailingParserDescr

Add a bit at the end of a NzsNum.

def NzsNum.sign : NzsNum → Bool

Sign of a NzsNum.

@[match_pattern]

def NzsNum.not : NzsNum → NzsNum

Bitwise not for NzsNum.

def NzsNum.«term~_» : Lean.ParserDescr

Bitwise not for NzsNum.

def NzsNum.bit0 : NzsNum → NzsNum

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

def NzsNum.bit1 : NzsNum → NzsNum

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

def NzsNum.head : NzsNum → Bool

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

def NzsNum.tail : NzsNum → SNum

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

def SNum.sign : SNum → Bool

Sign of a SNum.

@[match_pattern]

def SNum.not : SNum → SNum

Bitwise not for SNum.

def SNum.«term~_» : Lean.ParserDescr

Bitwise not for SNum.

@[match_pattern]

def SNum.bit : Bool → SNum → SNum

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

def SNum.«term_::_» : Lean.TrailingParserDescr

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

def SNum.bit0 : SNum → SNum

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

def SNum.bit1 : SNum → SNum

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

theorem SNum.bit_zero (b : Bool) : bit b (zero b) = zero b

theorem SNum.bit_one (b : Bool) : bit b (zero (decide ¬b = true)) = nz (NzsNum.msb b)

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

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

def SNum.head : SNum → Bool

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

def SNum.tail : SNum → SNum

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.

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

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

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

An induction principle for SNum which avoids relying on NzsNum.

def SNum.testBit : ℕ → SNum → Bool

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.

def SNum.succ : SNum → SNum

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

def SNum.pred : SNum → SNum

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

def SNum.neg (n : SNum) : SNum

The opposite of a SNum.

@[implicit_reducible]

instance SNum.instNeg : Neg SNum

def SNum.czAdd : Bool → Bool → SNum → SNum

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.

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

def SNum.cAdd : SNum → SNum → Bool → SNum

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

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

Add two SNums.

@[implicit_reducible]

instance SNum.instAdd : Add SNum

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

Subtract two SNums.

@[implicit_reducible]

instance SNum.instSub : Sub SNum

def SNum.mul (a : SNum) : SNum → SNum

Multiply two SNums.

@[implicit_reducible]

instance SNum.instMul : Mul SNum